From 466552a3d778ab0afedc82d7d862252b2de09ace Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 24 Aug 2018 21:57:16 +0200 Subject: [PATCH] - debugging calculations for mutated text items - cleanup - a wee bit serious testing in Attributes.thy of this feature. --- Isa_DOF.thy | 58 ++++++++++------------------- examples/simple/Concept_Example.thy | 4 +- test/conceptual/Attributes.thy | 49 +++++++++++++----------- 3 files changed, 49 insertions(+), 62 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 0c179a4..d50e8f0 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -392,7 +392,7 @@ fun print_doc_items b ctxt = (writeln ("docitem: "^n); writeln (" type: "^cid); writeln (" origine: "^thy_name); - writeln (" value: " ^ (Syntax.string_of_term ctxt value)) + writeln (" value: "^(Syntax.string_of_term ctxt value)) ) | print_item (n, NONE) = (writeln ("forward reference for docitem: "^n)); @@ -565,6 +565,9 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) "=" => Const(lnu,lnut) $ Abs ("uu_", lnt, instantiate_term tyenv' (generalize_term rhs)) $ term + | ":=" => Const(lnu,lnut) + $ Abs ("uu_", lnt, instantiate_term tyenv' (generalize_term rhs)) + $ term | "+=" => Const(lnu,lnut) $ Abs ("uu_", lnt, join lnt $ (Bound 0) @@ -585,21 +588,6 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta this label is used as jump-target for point-and-click feature. *) fun enrich_trans thy = let val cid_long = check_classref cid_pos thy -(* OLD - fun convert((Const(s,ty),_), t) X = Const(s^"_update", dummyT) - $ Abs("uuu_", type_of t, t) $ X - |convert _ _ = error("Left-hand side not a doc_class attribute.") - - val count = Unsynchronized.ref (~1); - fun incr () = Unsynchronized.inc count - val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end - fun read_assn ((lhs, pos), rhs) = - ((Syntax.read_term_global thy lhs |> generalize_term,pos), - Syntax.read_term_global thy rhs |> generalize_term) - val assns = map read_assn doc_attrs - (* val _ = (SPY:=assns) - val _ = (SPY2 := Input.source_explode toks) *) -*) val defaults_init = base_default_term cid_long thy fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term); val S = map conv (DOF_core.get_attribute_defaults cid_long thy); @@ -628,10 +616,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta fun update_instance_command (((oid:string,pos),cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) : Toplevel.transition -> Toplevel.transition = - let fun convert((Const(s,ty),_), t) X = Const(s^"_update", dummyT) - $ Abs("uuu_", type_of t, t) $ X - |convert _ _ = error("Left-hand side not a doc_class attribute.") - fun upd thy = + let fun upd thy = let val cid = case DOF_core.get_object_global oid thy of SOME{cid,...} => cid | NONE => error("undefined doc_class.") @@ -639,21 +624,13 @@ fun update_instance_command (((oid:string,pos),cid_pos), val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then () else error("incompatible classes:"^cid^":"^cid_long) + fun markup2string x = XML.content_of (YXML.parse_body x) - val count = Unsynchronized.ref (0 - 1); - fun incr () = Unsynchronized.inc count - val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end - fun read_assn (((lhs, pos), opn), rhs) = - let val _ = writeln opn in - ((Syntax.read_term_global thy lhs |> generalize_term ,pos), - (* this is problematic, - lhs need to be qualified *) - Syntax.read_term_global thy rhs |> generalize_term) - end - (* Missing: Check that attributes are legal here *) - val assns = map read_assn doc_attrs - val _ = (SPY:=assns) - in thy |> DOF_core.update_value_global oid ((fold convert assns) #> (infer_type thy)) + fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs) + val assns' = map conv_attrs doc_attrs + val def_trans = #1 o (calc_update_term thy cid_long assns') + in + thy |> DOF_core.update_value_global oid (def_trans) end in Toplevel.theory(upd) end @@ -802,10 +779,8 @@ in end\ assert "True" -lemma X : "True" by simp (* experiments >>> *) -text{* fghfgh *} text*[sdf] {* f @{thm refl}*} text*[sdfg] {* fg @{thm refl}*} @@ -914,12 +889,19 @@ fun calculate_attr_access ctxt proj_term term = (* term assumed to be ground type, (f term) not necessarily *) let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term] val ty = type_of (subterm') + val _ = writeln ("calculate_attr_access raw term: " ^ Syntax.string_of_term ctxt subterm') val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT) $ subterm' $ Free("_XXXXXXX", ty)) val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term'))); - val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm) - in lhs end + in case HOLogic.dest_Trueprop (Thm.concl_of thm) of + Free("_XXXXXXX", @{typ "bool"}) => @{const "True"} + | @{const "HOL.Not"} $ Free("_XXXXXXX", @{typ "bool"}) => @{const "False"} + | Const(@{const_name "HOL.eq"},_) $ lhs $ Free("_XXXXXXX", _ )=> lhs + | Const(@{const_name "HOL.eq"},_) $ Free("_XXXXXXX", _ ) $ rhs => rhs + | _ => error ("could not reduce attribute term: " ^ + Syntax.string_of_term ctxt subterm') + end fun calculate_attr_access_check ctxt attr oid = (* template *) case DOF_core.get_value_local oid (Context.the_proof ctxt) of diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index c0357df..512346a 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -26,11 +26,11 @@ section*[f::F] \ Lectus accumsan velit ultrices, ... }\ theorem some_proof : "P" sorry -update_instance*[f,r:="[@{thm ''some_proof''}]"] +update_instance*[f::F,r:="[@{thm ''some_proof''}]"] text{* ..., mauris amet, id elit aliquam aptent id, ... *} -update_instance*[f,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C), +update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C), (@{docitem ''a''}, @{docitem ''c1''})}"] close_monitor*[struct] diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index a03249a..db8e71d 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -2,6 +2,9 @@ theory Attributes imports "../../ontologies/Conceptual" begin +section\Elementary Creation of DocItems and Access of their Attibutes\ + +text\Current status:\ print_doc_classes print_doc_items @@ -24,12 +27,11 @@ ML\val Type("Conceptual.B.B_ext",[Type("Conceptual.C.C_ext",t)]) = @{typ " text*[dfgdfg2::C, z = "None"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ -text*[omega::E, x = "''g''"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ +text*[omega::E, x = "''def''"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ text\ @{docitem_ref \dfgdfg\} \ - term "A.x (undefined\A.x := 3\)" term "B.x ((undefined::C)\B.y := [''sdf'']\)" term "C.z ((undefined::C)\B.y := [''sdf''], z:= Some undefined\)" @@ -62,30 +64,33 @@ text\A not too trivial test: default y -> []. Then @{term "t"}: creation of a multi inheritance object omega, triple updates, the last one wins.\ ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}); - val t = HOLogic.dest_string (@{docitem_attr x::omega}); - \ - -(* separate checking and term construction ?*) + val t = HOLogic.dest_string (@{docitem_attr x::omega}); \ -ML\val t = @{term "Conceptual.B.y_update"}\ -declare [[ML_print_depth=30]] -ML\ +section\Mutation of Attibutes in DocItems\ + +ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \ + +update_instance*[omega::E, a2+="1"] + +ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \ + +update_instance*[omega::E, a2+="6"] + +ML\ @{docitem_attr a2::omega} \ +ML\ HOLogic.dest_number @{docitem_attr a2::omega} \ + +update_instance*[omega::E, x+="''inition''"] + +ML\ val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \ + +update_instance*[omega::E, y+="[''defini'',''tion'']"] + +update_instance*[omega::E, y+="[''en'']"] + +ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \ -ML\ -val cid_long = "Conceptual.B" -val attr_name = "dfgdfg" -val thy = @{theory}; - -val S = DOF_core.get_attribute_defaults cid_long thy; -fun conv (na, _ (* ty *), term) = (Binding.name_of na, Binding.pos_of na, "=", term); -val (tt, ty, n) = ODL_Command_Parser.calc_update_term thy cid_long (map conv S) - (the(DOF_core.get_value_global attr_name thy)); -\ - - - end \ No newline at end of file