Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
This commit is contained in:
commit
13db9a9e77
46
Isa_DOF.thy
46
Isa_DOF.thy
|
@ -1434,26 +1434,25 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
||||||
else {unchecked = true, define= false}))
|
else {unchecked = true, define= false}))
|
||||||
{unchecked = false, define= false} (* default *);
|
{unchecked = false, define= false} (* default *);
|
||||||
|
|
||||||
|
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.cartouche_input))
|
||||||
|
|
||||||
fun docitem_antiquotation_generic enclose name cid_decl =
|
fun docitem_antiquotation_generic cid_decl
|
||||||
Thy_Output.antiquotation name (Scan.lift (docitem_modes -- Args.cartouche_input))
|
{context = ctxt, source = src:Token.src, state}
|
||||||
(fn {context = ctxt, source = src:Token.src, state} =>
|
({unchecked = x, define= y}, source:Input.source) =
|
||||||
fn ({unchecked = x, define= y}, source:Input.source) =>
|
let fun label_latex flag = enclose (if flag then "\\label{" else "\\autoref{") "}"
|
||||||
|
in
|
||||||
(Thy_Output.output_text state {markdown=false} #>
|
(Thy_Output.output_text state {markdown=false} #>
|
||||||
check_and_mark ctxt
|
check_and_mark ctxt
|
||||||
cid_decl
|
cid_decl
|
||||||
({strict_checking = not x})
|
({strict_checking = not x})
|
||||||
(Input.pos_of source) #>
|
(Input.pos_of source) #>
|
||||||
enclose y)
|
label_latex y)
|
||||||
source)
|
source
|
||||||
|
end
|
||||||
|
|
||||||
|
|
||||||
fun docitem_antiquotation name cid_decl =
|
fun docitem_antiquotation name cid_decl =
|
||||||
let fun open_par x = if x then "\\label{"
|
Thy_Output.antiquotation name docitem_antiquotation_parser (docitem_antiquotation_generic cid_decl)
|
||||||
else "\\autoref{"
|
|
||||||
val close = "}"
|
|
||||||
in docitem_antiquotation_generic (fn y => enclose (open_par y) close) name cid_decl end
|
|
||||||
|
|
||||||
|
|
||||||
fun check_and_mark_term ctxt oid =
|
fun check_and_mark_term ctxt oid =
|
||||||
let val thy = Context.theory_of ctxt;
|
let val thy = Context.theory_of ctxt;
|
||||||
|
@ -1470,22 +1469,24 @@ fun check_and_mark_term ctxt oid =
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
||||||
fun ML_antiquotation_docitem_value binding =
|
|
||||||
ML_Antiquotation.inline binding
|
|
||||||
(fn (ctxt, toks) => (Scan.lift (Args.cartouche_input)
|
|
||||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
|
||||||
(check_and_mark_term ctxt (Input.source_content inp))))
|
|
||||||
(ctxt, toks))
|
|
||||||
|
|
||||||
|
fun ML_antiquotation_docitem_value (ctxt, toks) =
|
||||||
|
(Scan.lift (Args.cartouche_input)
|
||||||
|
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||||
|
((check_and_mark_term ctxt o Input.source_content) inp)))
|
||||||
|
(ctxt, toks)
|
||||||
|
|
||||||
|
|
||||||
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
||||||
val _ = Theory.setup((docitem_antiquotation @{binding docref} DOF_core.default_cid) #>
|
val _ = Theory.setup((docitem_antiquotation @{binding docref} DOF_core.default_cid) #>
|
||||||
(* deprecated syntax ^^^^^^*)
|
(* deprecated syntax ^^^^^^*)
|
||||||
(docitem_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
|
(docitem_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
|
||||||
(* deprecated syntax ^^^^^^^^^^*)
|
(* deprecated syntax ^^^^^^^^^^*)
|
||||||
(docitem_antiquotation @{binding docitem} DOF_core.default_cid) #>
|
docitem_antiquotation @{binding docitem} DOF_core.default_cid #>
|
||||||
|
(* Thy_Output.antiquotation @{binding docitem} docitem_antiquotation_parser
|
||||||
ML_antiquotation_docitem_value @{binding docitem_value})
|
(docitem_antiquotation_generic DOF_core.default_cid) #>
|
||||||
|
*)
|
||||||
|
ML_Antiquotation.inline @{binding docitem_value} ML_antiquotation_docitem_value)
|
||||||
|
|
||||||
end (* struct *)
|
end (* struct *)
|
||||||
\<close>
|
\<close>
|
||||||
|
@ -1666,7 +1667,6 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||||
" in doc class:" ^ def_occurrence);
|
" in doc class:" ^ def_occurrence);
|
||||||
SOME(bind,ty,mf))
|
SOME(bind,ty,mf))
|
||||||
else error("no overloading allowed.")
|
else error("no overloading allowed.")
|
||||||
val gen_antiquotation = OntoLinkParser.docitem_antiquotation
|
|
||||||
val _ = map_filter (check_n_filter thy) fields
|
val _ = map_filter (check_n_filter thy) fields
|
||||||
|
|
||||||
|
|
||||||
|
@ -1674,7 +1674,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||||
|> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)])
|
|> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)])
|
||||||
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps reject_Atoms
|
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps reject_Atoms
|
||||||
(* adding const symbol representing doc-class for Monitor-RegExps.*)
|
(* adding const symbol representing doc-class for Monitor-RegExps.*)
|
||||||
|> (fn thy => gen_antiquotation binding (cid thy) thy)
|
|> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy)
|
||||||
(* defines the ontology-checked text antiquotation to this document class *)
|
(* defines the ontology-checked text antiquotation to this document class *)
|
||||||
|
|
||||||
end;
|
end;
|
||||||
|
|
|
@ -648,7 +648,9 @@ subsection\<open> Theories \<close>
|
||||||
|
|
||||||
text \<open> This structure yields the datatype \verb*thy* which becomes the content of
|
text \<open> This structure yields the datatype \verb*thy* which becomes the content of
|
||||||
\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
|
\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
|
||||||
which inspired me (bu) to this naming. \<close>
|
which inspired me (bu) to this naming.
|
||||||
|
|
||||||
|
\<close>
|
||||||
ML\<open>
|
ML\<open>
|
||||||
|
|
||||||
(* intern Theory.Thy;
|
(* intern Theory.Thy;
|
||||||
|
@ -1157,6 +1159,12 @@ ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
|
||||||
(* MORE TO COME *)
|
(* MORE TO COME *)
|
||||||
|
|
||||||
|
|
||||||
|
section\<open>Low-level Markup Reporting\<close>
|
||||||
|
|
||||||
|
section\<open>Environment Structured Reporting\<close>
|
||||||
|
|
||||||
|
text\<open> @{ML_type "'a Name_Space.table"} \<close>
|
||||||
|
|
||||||
section\<open> Parsing issues \<close>
|
section\<open> Parsing issues \<close>
|
||||||
|
|
||||||
text\<open> Parsing combinators represent the ground building blocks of both generic input engines
|
text\<open> Parsing combinators represent the ground building blocks of both generic input engines
|
||||||
|
|
|
@ -47,7 +47,23 @@ datatype kind = expert_opinion | argument | "proof"
|
||||||
|
|
||||||
doc_class result = technical +
|
doc_class result = technical +
|
||||||
evidence :: kind
|
evidence :: kind
|
||||||
property :: "thm list" <= "[]"
|
c :: "thm list" <= "[]"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
ML\<open>fun check_invariant_invariant oid {is_monitor:bool} ctxt =
|
||||||
|
let val kind_term = AttributeAccess.compute_attr_access ctxt "kind" oid @{here} @{here}
|
||||||
|
val property_termS = AttributeAccess.compute_attr_access ctxt "property" oid @{here} @{here}
|
||||||
|
val tS = HOLogic.dest_list property_termS
|
||||||
|
in case kind_term of
|
||||||
|
@{term "proof"} => if not(null tS) then true
|
||||||
|
else error("class class invariant violation")
|
||||||
|
| _ => false
|
||||||
|
end
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
setup\<open>DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\<close>
|
||||||
|
|
||||||
|
|
||||||
doc_class example = technical +
|
doc_class example = technical +
|
||||||
referring_to :: "(notion + definition) set" <= "{}"
|
referring_to :: "(notion + definition) set" <= "{}"
|
||||||
|
|
Loading…
Reference in New Issue