forked from Isabelle_DOF/Isabelle_DOF
intermediate stage for onto after discussion this morning.
This commit is contained in:
parent
33fd8a0f7b
commit
6a2a479699
|
@ -29,46 +29,54 @@ where the author of the exam is not expected to be physically present.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
datatype ContentClass =
|
datatype ContentClass = setter | checker | externalExaminer | student
|
||||||
setter (* \<open>the 'author' of the exam\<close> *)
|
|
||||||
| checker (* \<open>the 'proof-reader' of the exam\<close> *)
|
|
||||||
| externalExaminer (* \<open>an external 'proof-reader' of the exam\<close> *)
|
|
||||||
| student (* \<open>the victim ;-) ... \<close> *)
|
|
||||||
|
|
||||||
|
|
||||||
doc_class Author =
|
doc_class Author =
|
||||||
affiliation :: "string"
|
affiliation :: "string"
|
||||||
email :: "string"
|
roles :: "ContentClass set"
|
||||||
|
email :: "string"
|
||||||
|
|
||||||
|
|
||||||
datatype Subject =
|
|
||||||
algebra | geometry | statistical | analysis
|
|
||||||
|
|
||||||
datatype Level =
|
|
||||||
oneStar | twoStars | threeStars
|
|
||||||
|
|
||||||
|
|
||||||
datatype Grade =
|
|
||||||
A1 | A2 | A3
|
|
||||||
|
|
||||||
|
|
||||||
doc_class Exam_item =
|
doc_class Exam_item =
|
||||||
level :: "int option"
|
level :: "int option"
|
||||||
concerns :: "ContentClass set"
|
concerns :: "ContentClass set"
|
||||||
|
visible_for :: "ContentClass set"
|
||||||
|
|
||||||
doc_class Header = Exam_item +
|
doc_class Header = Exam_item +
|
||||||
examSubject :: "(Subject) list"
|
date :: string
|
||||||
date :: string
|
authors :: "Author list"
|
||||||
timeAllowed :: int (* minutes *)
|
timeAllowed :: int (* minutes *)
|
||||||
|
|
||||||
|
doc_class marking = Exam_item +
|
||||||
|
marks :: int
|
||||||
|
|
||||||
type_synonym SubQuestion = string
|
doc_class Answer_Element = Exam_item +
|
||||||
|
|
||||||
doc_class Answer_Formal_Step = Exam_item +
|
|
||||||
justification :: string
|
justification :: string
|
||||||
"term" :: "string"
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class text_answer = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class program_text = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class formula_text = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class checkbox = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class radiobuttons = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class equational_derivation = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class proof_derivation = Answer_Element +
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
|
||||||
doc_class Answer_YesNo = Exam_item +
|
doc_class Answer_YesNo = Exam_item +
|
||||||
step_label :: string
|
step_label :: string
|
||||||
yes_no :: bool (* \<open>for checkboxes\<close> *)
|
yes_no :: bool (* \<open>for checkboxes\<close> *)
|
||||||
|
@ -77,13 +85,16 @@ datatype Question_Type =
|
||||||
formal | informal | mixed
|
formal | informal | mixed
|
||||||
|
|
||||||
doc_class Task = Exam_item +
|
doc_class Task = Exam_item +
|
||||||
local_grade :: Level
|
local_grade :: marking
|
||||||
type :: Question_Type
|
type :: Question_Type
|
||||||
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
||||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
||||||
mark :: int
|
mark :: int
|
||||||
|
|
||||||
|
|
||||||
|
doc_class SubTask = Task +
|
||||||
|
local_grade :: Level
|
||||||
|
|
||||||
doc_class Exercise = Exam_item +
|
doc_class Exercise = Exam_item +
|
||||||
content :: "(Task) list"
|
content :: "(Task) list"
|
||||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
||||||
|
@ -101,13 +112,11 @@ doc_class Validation =
|
||||||
proofs :: "thm list" <="[]"
|
proofs :: "thm list" <="[]"
|
||||||
|
|
||||||
doc_class Solution = Exam_item +
|
doc_class Solution = Exam_item +
|
||||||
content :: "Exercise list"
|
|
||||||
valids :: "Validation list"
|
valids :: "Validation list"
|
||||||
concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
|
concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
|
||||||
|
|
||||||
doc_class MathExam =
|
doc_class MathExam =
|
||||||
content :: "(Header + Author + Exercise) list"
|
global_grade :: Mark
|
||||||
global_grade :: Grade
|
|
||||||
accepts "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
accepts "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
||||||
|
|
||||||
|
|
||||||
|
@ -120,6 +129,7 @@ tasks > subtask
|
||||||
|
|
||||||
answer > subanswer
|
answer > subanswer
|
||||||
|
|
||||||
|
|
||||||
answer_element
|
answer_element
|
||||||
- text
|
- text
|
||||||
- program-text ? ? ?
|
- program-text ? ? ?
|
||||||
|
|
Reference in New Issue