forked from Isabelle_DOF/Isabelle_DOF
- Added monitor class-invariant for level consistency.
- debugging here and there - integration test - remark : MathExam is in a pretty inconsistent state (requires discussion) - integration test
This commit is contained in:
parent
98565b837c
commit
eae495ac90
13
Isa_DOF.thy
13
Isa_DOF.thy
|
@ -1087,7 +1087,7 @@ fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs)
|
|||
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
|
||||
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
|
||||
in
|
||||
(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text)
|
||||
(create_and_check_docitem false oid pos cid_pos doc_attrs' #> check_text)
|
||||
(* Thanks Frederic Tuong! ! ! *)
|
||||
end;
|
||||
|
||||
|
@ -1192,7 +1192,7 @@ val _ =
|
|||
val _ =
|
||||
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = true} (SOME NONE))));
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = true} (NONE))));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "declare_reference*"}
|
||||
|
@ -1431,9 +1431,7 @@ fun compute_trace_ML ctxt oid pos pos' =
|
|||
(* grabs attribute, and converts its HOL-term into (textual) ML representation *)
|
||||
let val term = compute_attr_access ctxt "trace" oid pos pos'
|
||||
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
|
||||
val string_pair_list = map conv (HOLogic.dest_list term)
|
||||
val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
|
||||
in ML_Syntax.print_list print_string_pair string_pair_list end
|
||||
in map conv (HOLogic.dest_list term) end
|
||||
|
||||
val parse_oid = Scan.lift(Parse.position Args.name)
|
||||
val parse_oid' = Term_Style.parse -- parse_oid
|
||||
|
@ -1449,7 +1447,10 @@ val parse_attribute_access' = Term_Style.parse -- parse_attribute_access
|
|||
fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||
(compute_attr_access ctxt attr oid pos pos')
|
||||
|
||||
fun trace_attr_2_ML ctxt (oid:string,pos) = ML_Syntax.atomic (compute_trace_ML ctxt oid @{here} pos)
|
||||
fun trace_attr_2_ML ctxt (oid:string,pos) =
|
||||
let val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
|
||||
val toML = (ML_Syntax.atomic o (ML_Syntax.print_list print_string_pair))
|
||||
in toML (compute_trace_ML ctxt oid @{here} pos) end
|
||||
|
||||
local
|
||||
(* copied from "$ISABELLE_HOME/src/Pure/Thy/thy_output.ML" *)
|
||||
|
|
|
@ -2,6 +2,7 @@ chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<cl
|
|||
|
||||
theory Example
|
||||
imports "../../ontologies/CENELEC_50126"
|
||||
"../../ontologies/scholarly_paper"
|
||||
begin
|
||||
|
||||
section\<open> Some examples of Isabelle's standard antiquotations. \<close>
|
||||
|
@ -63,16 +64,17 @@ section\<open> Some Tests for Ontology Framework and its CENELEC Instance \<clos
|
|||
|
||||
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||
|
||||
paragraph* [sdfk::introduction] \<open> just a paragraph - lexical variant \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
|
||||
section*[h::example]\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
|
||||
|
||||
|
||||
|
||||
section\<open> Text Antiquotation Infrastructure ... \<close>
|
||||
section*[i::example]\<open> Text Antiquotation Infrastructure ... \<close>
|
||||
|
||||
text\<open> @{docitem \<open>lalala\<close>} -- produces warning. \<close>
|
||||
text\<open> @{docitem (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>
|
||||
|
|
|
@ -17,7 +17,7 @@ text{*
|
|||
\end{itemize}
|
||||
*}
|
||||
|
||||
subsection*[idir::Author, affiliation="''CentraleSupelec''",
|
||||
text*[idir::Author, affiliation="''CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
|
@ -93,16 +93,16 @@ text*[a2::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
|||
text*[a3::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||
text*[a4::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||
|
||||
text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
||||
text*[q1::Task, local_grade="oneStar", mark="1::int", type="formal"]
|
||||
{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *}
|
||||
|
||||
subsubsection*[exo3 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 3\<close>
|
||||
|
||||
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
||||
text*[q2::Task, local_grade="threeStars", mark="3::int", type="formal"]
|
||||
{* Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
|
||||
with a difference of 5.
|
||||
*}
|
||||
(* this does not work on the level of the LaTeX output for known restrictions of the Toplevel. *)
|
||||
close_monitor*[exam::MathExam]
|
||||
close_monitor*[exam :: MathExam]
|
||||
|
||||
end
|
||||
|
|
|
@ -45,6 +45,9 @@ for enforcing a certain document structure, and discuss ontology-specific IDE su
|
|||
\<close>
|
||||
|
||||
section*[intro::introduction]\<open> Introduction \<close>
|
||||
text\<open> drfgdfg\<close>
|
||||
ML\<open>@{trace_attribute this}\<close>
|
||||
print_doc_items
|
||||
text*[introtext::introduction]\<open>
|
||||
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
|
||||
most pervasive challenge in the digitization of knowledge and its
|
||||
|
@ -739,6 +742,7 @@ section*[bib::bibliography]\<open>References\<close>
|
|||
|
||||
close_monitor*[this]
|
||||
|
||||
|
||||
end
|
||||
(*>*)
|
||||
|
||||
|
|
|
@ -23,7 +23,7 @@ text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<c
|
|||
|
||||
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
|
||||
|
||||
section*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
text*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
|
||||
theorem some_proof : "P" sorry
|
||||
|
||||
|
|
|
@ -12,7 +12,7 @@ Common Criteria identifies:
|
|||
|
||||
(*<<*)
|
||||
theory CENELEC_50126
|
||||
imports "../Isa_DOF" "../Isa_COL"
|
||||
imports "../Isa_COL"
|
||||
begin
|
||||
(*>>*)
|
||||
|
||||
|
|
|
@ -3,9 +3,11 @@ theory Conceptual
|
|||
begin
|
||||
|
||||
doc_class A =
|
||||
level :: "int option"
|
||||
x :: int
|
||||
|
||||
doc_class B =
|
||||
level :: "int option"
|
||||
x :: "string" (* attributes live in their own name-space *)
|
||||
y :: "string list" <= "[]" (* and can have arbitrary type constructors *)
|
||||
(* LaTeX may have problems with this, though *)
|
||||
|
|
|
@ -39,14 +39,16 @@ datatype Level =
|
|||
datatype Grade =
|
||||
A1 | A2 | A3
|
||||
|
||||
doc_class Header =
|
||||
|
||||
doc_class Exam_item =
|
||||
level :: "int option"
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
doc_class Header = Exam_item +
|
||||
examSubject :: "(Subject) list"
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
||||
doc_class Exam_item =
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
|
||||
type_synonym SubQuestion = string
|
||||
|
||||
|
@ -62,7 +64,7 @@ datatype Question_Type =
|
|||
formal | informal | mixed
|
||||
|
||||
doc_class Task = Exam_item +
|
||||
level :: Level
|
||||
local_grade :: Level
|
||||
type :: Question_Type
|
||||
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
||||
|
@ -90,7 +92,7 @@ doc_class Solution = Exam_item +
|
|||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
|
||||
|
||||
doc_class MathExam=
|
||||
doc_class MathExam =
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
accepts "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
||||
|
|
|
@ -61,7 +61,7 @@ datatype formal_content_kind = "definition" | "axiom" | aux_lemma | "lemma" | "c
|
|||
doc_class "thm_elements" = "thms" +
|
||||
kind :: "formal_content_kind option"
|
||||
|
||||
doc_class bibliography =
|
||||
doc_class bibliography = text_section +
|
||||
style :: "string option" <= "Some ''LNCS''"
|
||||
|
||||
text\<open> Besides subtyping, there is another relation between
|
||||
|
@ -102,6 +102,90 @@ doc_class article =
|
|||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
bibliography)"
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure Scholarly_paper_trace_invariant =
|
||||
struct
|
||||
local
|
||||
|
||||
fun group f g cidS [] = []
|
||||
|group f g cidS (a::S) = case find_first (f a) cidS of
|
||||
NONE => [a] :: group f g cidS S
|
||||
| SOME cid => let val (pref,suff) = take_prefix (g cid) S
|
||||
in (a::pref)::(group f g cidS suff) end;
|
||||
|
||||
fun partition ctxt cidS trace =
|
||||
let fun find_lead (x,_) = DOF_core.is_subclass ctxt x;
|
||||
fun find_cont cid (cid',_) = DOF_core.is_subclass ctxt cid' cid
|
||||
in group find_lead find_cont cidS trace end;
|
||||
|
||||
fun dest_option _ (Const (@{const_name "None"}, _)) = NONE
|
||||
| dest_option f (Const (@{const_name "Some"}, _) $ t) = SOME (f t)
|
||||
|
||||
in
|
||||
|
||||
fun check ctxt cidS mon_id pos =
|
||||
let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos @{here}
|
||||
val groups = partition (Context.proof_of ctxt) cidS trace
|
||||
fun get_level_raw oid = AttributeAccess.compute_attr_access ctxt "level" oid @{here} @{here};
|
||||
fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
|
||||
fun check_level_hd a = case (get_level (snd a)) of
|
||||
NONE => error("Invariant violation: leading section" ^ snd a ^
|
||||
" must have lowest level")
|
||||
| SOME X => X
|
||||
fun check_group_elem level_hd a = case (get_level (snd a)) of
|
||||
NONE => true
|
||||
| SOME y => if level_hd <= y then true
|
||||
(* or < ? But this is too strong ... *)
|
||||
else error("Invariant violation: "^
|
||||
"subsequent section " ^ snd a ^
|
||||
" must have higher level.");
|
||||
fun check_group [] = true
|
||||
|check_group [_] = true
|
||||
|check_group (a::S) = forall (check_group_elem (check_level_hd a)) (S)
|
||||
in if forall check_group groups then ()
|
||||
else error"Invariant violation: leading section must have lowest level"
|
||||
end
|
||||
end
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
||||
setup\<open> let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical",
|
||||
"scholarly_paper.example", "scholarly_paper.conclusion"];
|
||||
val upd = DOF_core.update_class_invariant "scholarly_paper.article"
|
||||
fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check
|
||||
ctxt cidS moni_oid @{here};
|
||||
true)
|
||||
in upd body end\<close>
|
||||
|
||||
|
||||
(* some test code *)
|
||||
ML\<open>
|
||||
(*
|
||||
|
||||
val trace = AttributeAccess.compute_trace_ML (Context.Proof @{context}) "this" @{here} @{here}
|
||||
val groups = partition ( @{context}) cidS trace
|
||||
val _::_::_::_:: _ ::_ ::_ ::a::_ = groups;
|
||||
check;
|
||||
|
||||
fun get_level_raw oid = AttributeAccess.compute_attr_access (Context.Proof @{context}) "level" oid @{here} @{here};
|
||||
fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
|
||||
fun check_level_hd a = case (get_level (snd a)) of
|
||||
NONE => error("Invariant violation: leading section" ^ snd a ^
|
||||
" must have lowest level")
|
||||
| SOME X => X
|
||||
fun check_group_elem level_hd a = case (get_level (snd a)) of
|
||||
NONE => true
|
||||
| SOME y => if y > level_hd then true
|
||||
else error("Invariant violation: subsequent section " ^ snd a ^
|
||||
" must have higher level.");
|
||||
fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
|
||||
*)
|
||||
\<close>
|
||||
|
||||
|
||||
gen_sty_template
|
||||
|
||||
|
||||
|
|
|
@ -32,8 +32,5 @@ doc_class report =
|
|||
\<lbrace>index\<rbrace>\<^sup>* ~~
|
||||
bibliography)"
|
||||
|
||||
ML\<open>
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
||||
|
|
Loading…
Reference in New Issue