From 964429368b99560b632e2b65fe30e53ba5a3b3ae Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 17 Jan 2019 23:06:10 +0100 Subject: [PATCH] Repaired bug in the storage of assert* update chains. Code could still be simplified. unicode - inside - string problem hard since deeply intertwined in the inner-syntax parser. better type-checking of isa terms and types. --- Isa_DOF.thy | 33 ++++++++++++------- examples/conceptual/AssnsLemmaThmEtc.thy | 15 ++++----- .../conceptual/InnerSyntaxAntiquotations.thy | 2 +- 3 files changed, 28 insertions(+), 22 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 416fefb..837efd2 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -742,12 +742,14 @@ fun ML_isa_check_generic check thy (term, pos) = fun ML_isa_check_typ thy (term, _, pos) = - let fun check thy (name, _) = Syntax.parse_typ (Proof_Context.init_global thy) name + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end in ML_isa_check_generic check thy (term, pos) end fun ML_isa_check_term thy (term, _, pos) = - let fun check thy (name, _) = Syntax.parse_term (Proof_Context.init_global thy) name + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end in ML_isa_check_generic check thy (term, pos) end @@ -1226,20 +1228,27 @@ val _ = fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list), prop) = let fun markup2string x = XML.content_of (YXML.parse_body x) - val _ = String.explode (markup2string prop) - fun parse_convert thy = (let val h = Syntax.parse_term (Proof_Context.init_global thy) prop - in Syntax.string_of_term_global thy h end) + fun parse_convert thy = (let val ctxt = (Proof_Context.init_global thy) + val term = Syntax.parse_term ctxt prop + val str = Sledgehammer_Util.hackish_string_of_term ctxt term + fun hpp x = if x = #"\\" then "\\\\" else String.implode [x] + val str' = map hpp (String.explode str) + val str'' = String.concatWith " " str' + in str'' + end) val _ = writeln ("XXX" ^ markup2string prop) - val doc_attrs = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs - val doc_attrs' = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) doc_attrs - (* missing : registrating t as property *) + fun conv_attrs thy = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs + (* fun conv_attrs thy = (("property",pos),"[@{term ''"^parse_convert thy ^"''}]")::doc_attrs *) + fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) fun mks thy = case DOF_core.get_object_global oid thy of - SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),doc_attrs') thy) - | NONE => (writeln "NONE";create_and_check_docitem false oid pos cid_pos doc_attrs thy) + SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) + | NONE => (writeln "NONE"; create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) val check = (assert_cmd some_name modes prop) o Proof_Context.init_global in (* Toplevel.keep (check o Toplevel.context_of) *) - Toplevel.theory (fn thy => (check thy; writeln ("YYY" ^ parse_convert thy); mks thy)) + Toplevel.theory (fn thy => (check thy; + (* writeln ("YYY" ^ parse_convert thy); *) + mks thy)) end val _ = @@ -1608,5 +1617,5 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); (DOF_core.write_ontology_latex_sty_template @{theory}) \ *) - +ML\op oo\ end diff --git a/examples/conceptual/AssnsLemmaThmEtc.thy b/examples/conceptual/AssnsLemmaThmEtc.thy index 9bdab98..0d351da 100644 --- a/examples/conceptual/AssnsLemmaThmEtc.thy +++ b/examples/conceptual/AssnsLemmaThmEtc.thy @@ -11,19 +11,16 @@ print_doc_items section\Definitions, Lemmas, Theorems, Assertions\ -(* auxilliary *) -ML\fun assert_list_dest X = map HOLogic.dest_string - (map (fn Const ("Isa_DOF.ISA_term", _) $ s => s ) - (HOLogic.dest_list X))\ -text*[aa::F]\Our definition of the HOL-Logic has the following properties:\ +text*[aa::F, property = "[@{term ''True''}]"]\Our definition of the HOL-Logic has the following properties:\ assert*[aa::F] "True" -ML\assert_list_dest @{docitem_attribute property :: aa}\ -assert*[aa::F] "True & True" (* small pb: unicodes crashes here ... *) -ML\ assert_list_dest @{docitem_attribute property :: aa}\ -(* bigger pb: overrides last solution ... *) +ML\ ISA_core.property_list_dest @{docitem_attribute property :: aa}\ + +assert*[aa::F] "True --> True" (* small pb: unicodes crashes here ... *) + +ML\ ISA_core.property_list_dest @{docitem_attribute property :: aa}\ text\An example for the ontology specification character of the short-cuts such as @{command "assert*"}: in the following, we use the same notation referring to a completely diff --git a/examples/conceptual/InnerSyntaxAntiquotations.thy b/examples/conceptual/InnerSyntaxAntiquotations.thy index 5951ac3..4967e3a 100644 --- a/examples/conceptual/InnerSyntaxAntiquotations.thy +++ b/examples/conceptual/InnerSyntaxAntiquotations.thy @@ -45,7 +45,7 @@ text*[xcv4::F, r="[@{thm ''HOL.refl''}, @{thm ''InnerSyntaxAntiquotations.murks''}]", b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}", s="[@{typ ''int list''}]", - property = "[@{term ''a --> b''}]" + property = "[@{term ''H --> H''}]" ]\Lorem ipsum ...\ text*[xcv5::G, g="@{thm ''HOL.sym''}"]\Lorem ipsum ...\