From ec33e70bbf75465119716a8dc4c2161e65275ed3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 24 Mar 2022 08:22:41 +0100 Subject: [PATCH 1/4] Loosen dependency on Toplevel.transition Loosen the dependency of the implementation of value* and term* on Toplevel.transition. Toplevel.transition should be avoided as it has specific behaviors like only allowing atomic transactions. --- src/DOF/Isa_DOF.thy | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 87e1d46..a225fef 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1850,7 +1850,7 @@ sig val value: Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string - -> Toplevel.state -> Toplevel.transition -> unit + -> Toplevel.state -> Position.T -> unit val add_evaluator: binding * (Proof.context -> term -> term) -> theory -> string * theory end; @@ -1898,13 +1898,13 @@ fun meta_args_exec NONE thy = thy {is_monitor = false} {is_inline = false} oid pos (I cid_pos) (I doc_attrs)) -fun value_cmd meta_args_opt raw_name modes raw_t state trans = +fun value_cmd meta_args_opt raw_name modes raw_t state pos = let val _ = meta_args_exec meta_args_opt val ctxt = Toplevel.context_of state; val name = intern_evaluator ctxt raw_name; val t = Syntax.read_term ctxt raw_t; - val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , Toplevel.pos_of trans) + val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos) (Proof_Context.theory_of ctxt); val t' = value_select name ctxt term'; val ty' = Term.type_of t'; @@ -1928,8 +1928,10 @@ val opt_evaluator = val opt_attributes = Scan.option ODL_Command_Parser.attributes fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = - Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state trans) trans - +let val pos = Toplevel.pos_of trans +in + Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state pos) trans +end \ \c.f. \<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ (* @@ -1937,13 +1939,13 @@ fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = and adds the possibility to check Term Annotation Antiquotations (TA) with the help of DOF_core.transduce_term_global function *) -fun string_of_term meta_args_opt ctxt s trans = +fun string_of_term meta_args_opt ctxt s pos = let val _ = meta_args_exec meta_args_opt val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; - val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , Toplevel.pos_of trans) + val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , pos) (Proof_Context.theory_of ctxt'); in Pretty.string_of @@ -1958,11 +1960,14 @@ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); We want to have the current position to pass it to transduce_term_global in string_of_term, so we pass the Toplevel.transition *) -fun print_term meta_args_opt (string_list, string) trans = print_item - (fn state => - fn string => - string_of_term meta_args_opt (Toplevel.context_of state) string trans) - (string_list, string) trans; +fun print_term meta_args_opt (string_list, string) trans = +let + val pos = Toplevel.pos_of trans +in + print_item (fn state => + fn string => string_of_term meta_args_opt (Toplevel.context_of state) string pos) + (string_list, string) trans +end val _ = Outer_Syntax.command \<^command_keyword>\term*\ "read and print term" -- 2.39.2 From 444d6d077cab2ee9916439c516e895d651023fa2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 28 Mar 2022 18:19:41 +0200 Subject: [PATCH 2/4] Add eager and lazy elaboration - Isabelle uses eager evaluation, so should the elaboration of terms which are evaluated. The value of instances are now registered in the data tables of Isabelle/DOF when fully elaborated, ie, term annotation antiquotations proposed by Isabelle/DOF in an instance value are replaced by its value before registration in Isabelle/DOF data A new field, input_term, stores the lazy elaboration and is used when elaboration is not wished (to print the original input term declared by the user, for example) - Clean up the simplication mechanism of the internal trace attribute (used by monitor classes) --- src/DOF/Isa_DOF.thy | 261 +++++++++++++++++++++++--------------------- 1 file changed, 137 insertions(+), 124 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index a225fef..aae411f 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -185,6 +185,7 @@ struct type docobj = {pos : Position.T, thy_name : string, + input_term : term, value : term, inline : bool, id : serial, @@ -613,11 +614,12 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of | NONE => NONE (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun update_value_global oid upd thy = +fun update_value_global oid upd_input_term upd_value thy = case get_object_global oid thy of - SOME{pos,thy_name,value,inline,id,cid,vcid} => + SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} => let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - value=upd value,id=id, + input_term=upd_input_term input_term, + value=upd_value value,id=id, inline=inline,cid=cid, vcid=vcid}) in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end | NONE => error("undefined doc object: "^oid) @@ -701,60 +703,10 @@ fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt) fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) in writeln (String.concatWith "," (Symtab.keys tab)) end -fun print_doc_items b ctxt = - let val {docobj_tab={tab = x, ...},...}= get_data ctxt; - val _ = writeln "====================================="; - fun dfg true = "true" - |dfg false= "false" - fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline,value})) = - (writeln ("docitem: "^n); - writeln (" type: "^cid); - case vcid of NONE => () | SOME (s) => - writeln (" virtual type: "^ s); - writeln (" origine: "^thy_name); - writeln (" inline: "^dfg inline); - writeln (" value: "^(Syntax.string_of_term ctxt value)) - ) - | print_item (n, NONE) = - (writeln ("forward reference for docitem: "^n)); - in map print_item (Symtab.dest x); - writeln "=====================================\n\n\n" end; -fun print_docclass_template cid ctxt = - let val cid_long = read_cid ctxt cid (* assure that given cid is really a long_cid *) - val brute_hierarchy = (get_attributes_local cid_long ctxt) - val flatten_hrchy = flat o (map(fn(lname, attrS) => - map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS)) - fun filter_overrides [] = [] - |filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S) - val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy)) - val args = String.concatWith "=%\n , " (" label=,type":: hierarchy); - val template = "\\newisadof{"^cid_long^"}%\n["^args^"=%\n][1]\n{%\n#1%\n}\n\n"; - in writeln template end; -fun print_doc_classes b ctxt = - let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt; - val _ = writeln "====================================="; - fun print_attr (n, ty, NONE) = (Binding.print n) - | print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")") - fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) - fun print_virtual {virtual} = Bool.toString virtual - fun print_class (n, {attribute_decl, id, inherits_from, name, virtual, params, thy_name, rejectS, rex,invs}) = - (case inherits_from of - NONE => writeln ("docclass: "^n) - | SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + "); - writeln (" name: "^(Binding.print name)); - writeln (" virtual: "^(print_virtual virtual)); - writeln (" origin: "^thy_name); - writeln (" attrs: "^commas (map print_attr attribute_decl)); - writeln (" invs: "^commas (map print_inv invs)) - ); - in map print_class (Symtab.dest docclass_tab); - writeln "=====================================\n\n\n" - end; - fun print_doc_class_tree ctxt P T = let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt; val class_tab:(string * docclass_struct)list = (Symtab.dest docclass_tab) @@ -769,38 +721,7 @@ fun print_doc_class_tree ctxt P T = in ".0 .\n" ^ tree 1 roots end - -fun check_doc_global (strict_checking : bool) ctxt = - let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = get_data ctxt; - val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x) - val T = map fst (Symtab.dest monitor_tab) - in if null S - then if null T then () - else error("Global consistency error - there are open monitors: " - ^ String.concatWith "," T) - else error("Global consistency error - Unresolved forward references: " - ^ String.concatWith "," S) - end - -val _ = - Outer_Syntax.command \<^command_keyword>\print_doc_classes\ "print document classes" - (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of))); - -val _ = - Outer_Syntax.command \<^command_keyword>\print_doc_class_template\ - "print document class latex template" - (Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of))); - - -val _ = - Outer_Syntax.command \<^command_keyword>\print_doc_items\ "print document items" - (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of))); - -val _ = - Outer_Syntax.command \<^command_keyword>\check_doc_global\ "check global document consistency" - (Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of))); - -val (strict_monitor_checking, strict_monitor_checking_setup) +val (strict_monitor_checking, strict_monitor_checking_setup) = Attrib.config_bool \<^binding>\strict_monitor_checking\ (K false); val (invariants_checking, invariants_checking_setup) @@ -1051,7 +972,6 @@ fun elaborate_instance thy _ _ term_option pos = | SOME(value) => DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy end -(*DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy*) (* The function declare_ISA_class_accessor_and_check_instance uses a prefix @@ -1323,7 +1243,8 @@ fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),so fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term]) -fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) term = +fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long + (S:(string * Position.T * string * term)list) term = let val cid_ty = cid_2_cidType cid_long thy val generalize_term = Term.map_types (generalize_typ 0) fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t @@ -1357,7 +1278,8 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) |join _ = error("implicit fusion operation not defined for attribute: "^ lhs) (* could be extended to bool, map, multisets, ... *) val rhs' = instantiate_term tyenv' (generalize_term rhs) - val rhs'' = DOF_core.transduce_term_global {mk_elaboration=false} (rhs',pos) thy + val rhs'' = DOF_core.transduce_term_global {mk_elaboration=mk_elaboration} + (rhs',pos) thy in case opr of "=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term | ":=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term @@ -1402,7 +1324,11 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] val assns' = map conv_attrs trace_attr fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy)) - fun def_trans oid = #1 o (calc_update_term thy (cid_of oid) assns') + fun def_trans_input_term oid = + #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') + fun def_trans_value oid = + #1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns') + val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; (* check that any transition is possible : *) @@ -1414,7 +1340,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = in Symtab.update(n, {accepted_cids=accepted_cids, rejected_cids=rejected_cids, automatas=aS}) tab end - fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid) + fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid) val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) in thy |> (* update traces of all enabled monitors *) fold (update_trace) (enabled_monitors) @@ -1492,8 +1418,10 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do | SOME (cid,_) => if (DOF_core.is_virtual cid thy) then SOME (DOF_core.parse_cid_global thy cid) else NONE - val value_term = if (cid_long = DOF_core.default_cid) - then (Free ("Undefined_Value", @{typ "unit"})) + val value_terms = if (cid_long = DOF_core.default_cid) + then let + val undefined_value = Free ("Undefined_Value", @{typ "unit"}) + in (undefined_value, undefined_value) end (* Handle initialization of docitem without a class associated, for example when you just want a document element to be referenceable @@ -1504,21 +1432,26 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do val defaults_init = create_default_object thy cid_long 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); - val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init; + val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false} + thy cid_long S defaults_init; fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs - val (value_term', _(*ty*), _) = calc_update_term thy cid_long assns' defaults - in value_term' end + val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false} + thy cid_long assns' defaults + val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true} + thy cid_long assns' defaults + in (input_term, value_term') end val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) o Context.Theory - in thy |> DOF_core.define_object_global (oid, {pos = pos, - thy_name = Context.theory_name thy, - value = value_term, - inline = is_inline, - id = id, - cid = cid_long, - vcid = vcid}) + in thy |> DOF_core.define_object_global (oid, {pos = pos, + thy_name = Context.theory_name thy, + input_term = fst value_terms, + value = snd value_terms, + inline = is_inline, + id = id, + cid = cid_long, + vcid = vcid}) |> register_oid_cid_in_open_monitors oid pos cid_long |> (fn thy => (check_inv thy; thy)) |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true @@ -1546,12 +1479,15 @@ fun update_instance_command (((oid:string,pos),cid_pos), 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')) + val def_trans_input_term = + #1 o (calc_update_term {mk_elaboration=false} thy cid_long assns') + val def_trans_value = + #1 o (calc_update_term {mk_elaboration=true} thy cid_long assns') fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} o Context.Theory ) thy ; thy) in - thy |> DOF_core.update_value_global oid (def_trans) + thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value |> check_inv end @@ -1848,6 +1784,7 @@ Generic value command for arbitrary evaluators, with default using nbe or SML. signature VALUE_COMMAND = sig val value: Proof.context -> term -> term + val value_without_elaboration: Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string -> Toplevel.state -> Position.T -> unit @@ -1892,6 +1829,8 @@ fun value_select name ctxt = fun value ctxt term = value_select "" ctxt (DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>) (Proof_Context.theory_of ctxt)) +val value_without_elaboration = value_select "" + fun meta_args_exec NONE thy = thy |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = thy |> (ODL_Command_Parser.create_and_check_docitem @@ -1991,6 +1930,94 @@ val _ = Theory.setup end; \ +ML\ +fun print_doc_classes b ctxt = + let val {docobj_tab={tab = x, ...},docclass_tab, ...} = DOF_core.get_data ctxt; + val _ = writeln "====================================="; + fun print_attr (n, ty, NONE) = (Binding.print n) + | print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")") + fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) + fun print_virtual {virtual} = Bool.toString virtual + fun print_class (n, {attribute_decl, id, inherits_from, name, virtual, params, thy_name, rejectS, rex,invs}) = + (case inherits_from of + NONE => writeln ("docclass: "^n) + | SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + "); + writeln (" name: "^(Binding.print name)); + writeln (" virtual: "^(print_virtual virtual)); + writeln (" origin: "^thy_name); + writeln (" attrs: "^commas (map print_attr attribute_decl)); + writeln (" invs: "^commas (map print_inv invs)) + ); + in map print_class (Symtab.dest docclass_tab); + writeln "=====================================\n\n\n" + end; + +val _ = + Outer_Syntax.command \<^command_keyword>\print_doc_classes\ "print document classes" + (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of))); + +fun print_docclass_template cid ctxt = + let val cid_long = DOF_core.read_cid ctxt cid (* assure that given cid is really a long_cid *) + val brute_hierarchy = (DOF_core.get_attributes_local cid_long ctxt) + val flatten_hrchy = flat o (map(fn(lname, attrS) => + map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS)) + fun filter_overrides [] = [] + |filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S) + val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy)) + val args = String.concatWith "=%\n , " (" label=,type":: hierarchy); + val template = "\\newisadof{"^cid_long^"}%\n["^args^"=%\n][1]\n{%\n#1%\n}\n\n"; + in writeln template end; + +val _ = + Outer_Syntax.command \<^command_keyword>\print_doc_class_template\ + "print document class latex template" + (Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of))); + +fun print_doc_items b ctxt = + let val {docobj_tab={tab = x, ...},...}= DOF_core.get_data ctxt; + val _ = writeln "====================================="; + fun dfg true = "true" + |dfg false= "false" + fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline, input_term, value})) = + (writeln ("docitem: "^n); + writeln (" type: "^cid); + case vcid of NONE => () | SOME (s) => + writeln (" virtual type: "^ s); + writeln (" origine: "^thy_name); + writeln (" inline: "^dfg inline); + writeln (" input_term: " + ^ (Syntax.string_of_term + ctxt (Value_Command.value_without_elaboration ctxt input_term))); + writeln (" value: " + ^ (Syntax.string_of_term + ctxt (Value_Command.value_without_elaboration ctxt value))) + ) + | print_item (n, NONE) = + (writeln ("forward reference for docitem: "^n)); + in map print_item (Symtab.dest x); + writeln "=====================================\n\n\n" end; + +val _ = + Outer_Syntax.command \<^command_keyword>\print_doc_items\ "print document items" + (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of))); + +fun check_doc_global (strict_checking : bool) ctxt = + let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = DOF_core.get_data ctxt; + val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x) + val T = map fst (Symtab.dest monitor_tab) + in if null S + then if null T then () + else error("Global consistency error - there are open monitors: " + ^ String.concatWith "," T) + else error("Global consistency error - Unresolved forward references: " + ^ String.concatWith "," S) + end + +val _ = + Outer_Syntax.command \<^command_keyword>\check_doc_global\ "check global document consistency" + (Parse.opt_bang >> (fn b => Toplevel.keep (check_doc_global b o Toplevel.context_of))); + +\ \ \c.f. \<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ (* @@ -2213,25 +2240,9 @@ val basic_entity = Document_Output.antiquotation_pretty_source : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; fun symbex_attr_access0 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') - (* Debug : - 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'))); - 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 + let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term] + in Value_Command.value ctxt (subterm') end + fun compute_attr_access ctxt attr oid pos pos' = (* template *) case DOF_core.get_value_global oid (Context.theory_of ctxt) of @@ -2247,6 +2258,7 @@ fun compute_attr_access ctxt attr oid pos pos' = (* template *) ^ oid ^ Position.here pos) val proj_term = Const(long_name,dummyT --> ty) in symbex_attr_access0 ctxt proj_term term end + (*in Value_Command.value ctxt term end*) | NONE => error("identifier not a docitem reference" ^ Position.here pos) @@ -2404,7 +2416,8 @@ fun define_inv cid_long ((lbl, pos), inv) thy = then Free (s, class_scheme_ty) else Free (s, ty) | update_attribute_type _ _ t = t - val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) ("'a " ^ cid_long ^ schemeN) + val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) + (Name.aT ^ " " ^ cid_long ^ schemeN) (* Update the type of each attribute update function to match the type of the current class. *) val inv_term' = update_attribute_type thy inv_ty inv_term -- 2.39.2 From 9cd53230638e5df920b45c135885691e642f5dbd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 28 Mar 2022 18:49:03 +0200 Subject: [PATCH 3/4] Update DOF manual meta-types as types section Types of the implementation language inside the HOL type system are now represented as datatypes and not just abstract types --- examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 19fb679..27c73ce 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -993,8 +993,8 @@ text\ entities, \<^eg>, \<^ML_type>\term\ (\\\-term), \<^ML_type>\typ\, or \<^ML_type>\thm\, we represent the types of the implementation language \<^emph>\inside\ the HOL type system. We do, however, not reflect the data of - these types. They are just declared abstract types, - ``inhabited'' by special constant symbols carrying strings, for + these types. They are just types declared in HOL, + which are ``inhabited'' by special constant symbols carrying strings, for example of the format \<^boxed_theory_text>\@{thm }\. % TODO: % Update meta-types implementation explanation to the new implementation -- 2.39.2 From e4e4a708a57f032ced42c1d549dd2b95cbd9a0b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 30 Mar 2022 07:54:38 +0200 Subject: [PATCH 4/4] Update assert* to use isabelle/DOF evaluation --- .../Isabelle_DOF-Manual/04_RefMan.thy | 72 ++++++++------- src/DOF/.Isa_DOF.thy.marks | Bin 0 -> 15 bytes src/DOF/Assert.thy | 82 ------------------ src/DOF/AssertLong.thy | 70 --------------- src/DOF/Isa_DOF.thy | 33 +++++-- .../scholarly_paper/scholarly_paper.thy | 34 -------- src/tests/Evaluation.thy | 32 ++++++- 7 files changed, 97 insertions(+), 226 deletions(-) create mode 100644 src/DOF/.Isa_DOF.thy.marks delete mode 100755 src/DOF/Assert.thy delete mode 100755 src/DOF/AssertLong.thy diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 27c73ce..31fc481 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -324,21 +324,28 @@ is currently only available in the SML API's of the kernel. as specified in @{technical \odl-manual0\}. \<^item> \meta_args\ : \<^rail>\obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \ +\<^item> \<^emph>\evaluator\: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML, + falling back to normalization by evaluation if this fails. Alternatively a specific + evaluator can be selected using square brackets; typical evaluators use the + current set of code equations to normalize and include \simp\ for fully + symbolic evaluation using the simplifier, \nbe\ for \<^emph>\normalization by + evaluation\ and \<^emph>\code\ for code generation in SML. \<^item> \upd_meta_args\ : \<^rail>\ (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\ \<^item> \annotated_text_element\ : \<^rail>\ - ( ( @@{command "text*"} '[' meta_args ']' '\' formal_text '\' + ( @@{command "text*"} '[' meta_args ']' '\' formal_text '\' | @@{command "ML*"} ('[' meta_args ']')? '\' SML_code '\' | @@{command "term*"} ('[' meta_args ']')? '\' HOL_term '\' - | @@{command "value*"} ('[' meta_args ']')? '\' HOL_term '\' - ) - | - ( @@{command "open_monitor*"} + | @@{command "value*"} \ ('[' meta_args ']' ('[' evaluator ']')?)? '\' HOL_term '\' + | @@{command "assert*"} \ ('[' meta_args ']' ('[' evaluator ']')?)? '\' HOL_term '\' + ) + \ +\<^rail>\ + ( @@{command "open_monitor*"} | @@{command "close_monitor*"} | @@{command "declare_reference*"} - ) '[' meta_args ']' - ) + ) '[' meta_args ']' | change_status_command | inspection_command | macro_command @@ -399,23 +406,35 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin \<^theory_text>\ML\ \ SML-code \ \\-command. \ +(*<*) +declare_reference*["text-elements-expls"::technical] +(*>*) + subsection\Ontological Term-Contexts and their Management\ text\The major commands providing term-contexts are -\<^theory_text>\term*[oid::cid, ...] \ \ HOL-term \ \\ and -\<^theory_text>\value*[oid::cid, ...] \ \ HOL-term \ \\\<^footnote>\The meta-argument list is optional.\. +\<^theory_text>\term*[oid::cid, ...] \ \ HOL-term \ \\, +\<^theory_text>\value*[oid::cid, ...] \ \ HOL-term \ \\ and +\<^theory_text>\assert*[oid::cid, ...] \ \ HOL-term \ \\\<^footnote>\The meta-argument list is optional.\. Wrt. creation, track-ability and checking they are analogous to the ontological text and code-commands. However the argument terms may contain term-antiquotations stemming from an ontology definition. Both term-contexts were type-checked and \<^emph>\validated\ against the global context (so: in the term \@{A \oid\}\, \oid\ is indeed a string which refers to a meta-object belonging to the document class \A\, for example). -The term-context in the \value*\-command is additionally expanded (\<^eg> replaced) by a term -denoting the meta-object. This expansion happens \<^emph>\before\ evaluation of the term, thus permitting +The term-context in the \value*\-command and \<^emph>\assert*\-command is additionally expanded +(\<^eg> replaced) by a term denoting the meta-object. +This expansion happens \<^emph>\before\ evaluation of the term, thus permitting executable HOL-functions to interact with meta-objects. +The \<^emph>\assert*\-command allows for logical statements to be checked in the global context +(see @{technical (unchecked) \text-elements-expls\}). +% TODO: +% Section reference @{docitem (unchecked) \text-elements-expls\} has not the right number +This is particularly useful to explore formal definitions wrt. their border cases. Note unspecified attribute values were represented by free fresh variables which constrains \<^dof> to choose either the normalization-by-evaluation strategy \<^theory_text>\nbe\ or a proof attempt via the \<^theory_text>\auto\ method. A failure of these strategies will be reported and regarded as non-validation of this meta-object. The latter leads to a failure of the entire command. + \ (*<*) @@ -619,9 +638,6 @@ during the editing process but is only visible in the integrated source but usua a \<^typ>\text_element\ to a specific \<^typ>\author\. Note that this is possible since \<^isadof> assigns to each document class also a class-type which is declared in the HOL environment.\ -(*<*) -declare_reference*["text-elements-expls"::example] -(*>*) text*[s23::example, main_author = "Some(@{author \bu\})"]\ Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example, this may be for a text fragment like @@ -649,7 +665,7 @@ of the \<^isadof> language: \ '[' meta_args ']' '\' text '\' ) - | @@{command "assert*"} '[' meta_args ']' '\' term '\' + \ \ @@ -680,14 +696,13 @@ text\ \<^boxed_theory_text>\title*\ ... \\ or \<^boxed_theory_text>\section*\ ... \\, \<^eg>: @{boxed_theory_text [display]\ - title*[title::title]\Isabelle/DOF\ - subtitle*[subtitle::subtitle]\User and Implementation Manual\ - author*[adb::author, email="\a.brucker@exeter.ac.uk\", - orcid="\0000-0002-6355-1200\", http_site="\https://brucker.ch/\", - affiliation="\University of Exeter, Exeter, UK\"] \Achim D. Brucker\ - author*[bu::author, email = "\wolff@lri.fr\", - affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ -\} +title*[title::title]\Isabelle/DOF\ +subtitle*[subtitle::subtitle]\User and Implementation Manual\ +author*[adb::author, email="\a.brucker@exeter.ac.uk\", + orcid="\0000-0002-6355-1200\", http_site="\https://brucker.ch/\", + affiliation="\University of Exeter, Exeter, UK\"] \Achim D. Brucker\ +author*[bu::author, email = "\wolff@lri.fr\", + affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\\} \ @@ -701,8 +716,7 @@ text\We want to check the consequences of this definition and can add the text*[claim::assertion]\For non-empty lists, our definition yields indeed the last element of a list.\ assert*[claim1::assertion] \last[4::int] = 4\ -assert*[claim2::assertion] \last[1,2,3,4::int] = 4\ -\} +assert*[claim2::assertion] \last[1,2,3,4::int] = 4\\} \ text\ @@ -714,14 +728,12 @@ However, in order to avoid the somewhat tedious consequence: the choice of the default class can be influenced by setting globally an attribute such as @{boxed_theory_text [display] -\declare[[ Definition_default_class = "definition"]] - declare[[ Theorem_default_class = "theorem"]] -\} +\declare[[Definition_default_class = "definition"]] +declare[[Theorem_default_class = "theorem"]]\} which allows the above example be shortened to: @{boxed_theory_text [display] -\Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] \ \ \ -\} +\Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] \ \ \\} \ subsection\The Ontology \<^verbatim>\technical_report\\ diff --git a/src/DOF/.Isa_DOF.thy.marks b/src/DOF/.Isa_DOF.thy.marks new file mode 100644 index 0000000000000000000000000000000000000000..36df4bd41d7a133f8a4d88f58d9114b07017649a GIT binary patch literal 15 RcmY#nu(mWXw=jW_TmThN0=fVI literal 0 HcmV?d00001 diff --git a/src/DOF/Assert.thy b/src/DOF/Assert.thy deleted file mode 100755 index 84b7e9e..0000000 --- a/src/DOF/Assert.thy +++ /dev/null @@ -1,82 +0,0 @@ -(************************************************************************* - * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay - * 2018 The University of Sheffield - * - * License: - * This program can be redistributed and/or modified under the terms - * of the 2-clause BSD-style license. - * - * SPDX-License-Identifier: BSD-2-Clause - *************************************************************************) - -section \ Little theory implementing the an assertion command in Isabelle/HOL. \ -text\This command is useful for certification documents allowing to validate - corner-cases of (executable) definitions. \ - -theory Assert - imports Main - keywords "assert" ::thy_decl - -begin - -subsection\Core\ - -ML\ -local -(* Reimplementation needed because not exported from ML structure Value_Command *) -fun value_maybe_select some_name = - case some_name - of NONE => Value_Command.value - | SOME name => Value_Command.value_select name; -in -(* Reimplementation needed because not exported from ML structure Value_Command *) -val opt_modes = - Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; - -(* Reimplementation needed because not exported from ML structure Value_Command *) -val opt_evaluator = - Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"}) - -(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *) -fun assert_cmd some_name modes raw_t ctxt (* state*) = - let - (* val ctxt = Toplevel.context_of state; *) - val t = Syntax.read_term ctxt raw_t; - val t' = value_maybe_select some_name ctxt t; - val ty' = Term.type_of t'; - val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean."; - val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed."; - val ctxt' = Proof_Context.augment t' ctxt; - val p = Print_Mode.with_modes modes (fn () => - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); - in Pretty.writeln p end; - -val _ = - Outer_Syntax.command @{command_keyword assert} "evaluate and print term" - (opt_evaluator -- opt_modes -- Parse.term - >> (fn ((some_name, modes), t) => - Toplevel.keep ( (assert_cmd some_name modes t) o Toplevel.context_of) )); -end -\ - - - -subsection\ Test: \ -(* - assert "" - assert "3 = 4" - assert "False" - assert "5 * 5 = 25" -*) - -subsection\Example\ - -assert "True \ True " - -assert "(5::int) * 5 = 25 " - -end - diff --git a/src/DOF/AssertLong.thy b/src/DOF/AssertLong.thy deleted file mode 100755 index 29fb26a..0000000 --- a/src/DOF/AssertLong.thy +++ /dev/null @@ -1,70 +0,0 @@ -(************************************************************************* - * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay - * 2018 The University of Sheffield - * - * License: - * This program can be redistributed and/or modified under the terms - * of the 2-clause BSD-style license. - * - * SPDX-License-Identifier: BSD-2-Clause - *************************************************************************) - -theory AssertLong - imports Main - keywords "assert" ::thy_decl - -begin - - - - -ML\ - -fun value_maybe_select some_name = - case some_name - of NONE => Value_Command.value - | SOME name => Value_Command.value_select name; - -val TT = Unsynchronized.ref (HOLogic.boolT); - -fun value_cmd2 some_name modes raw_t state = - let - val ctxt = Toplevel.context_of state; - val t = Syntax.read_term ctxt raw_t; - val t' = value_maybe_select some_name ctxt t; - val ty' = Term.type_of t'; - val t' = case ty' of @{typ "bool"} => t' | _ => error "Assertion expressions must be boolean."; - val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed."; - val ctxt' = Variable.auto_fixes t' ctxt; - val p = Print_Mode.with_modes modes (fn () => - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); - in Pretty.writeln p end; - -\ -ML\value_cmd2\ -definition ASSERT :: "bool \ bool" where "ASSERT p == (p=True)" -ML\val x = @{code "ASSERT"}\ -ML\ -val opt_modes = - Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; - -val opt_evaluator = - Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"}) - -val _ = - Outer_Syntax.command @{command_keyword assert} "evaluate and print term" - (opt_evaluator -- opt_modes -- Parse.term - >> (fn ((some_name, modes), t) => - let val _ = writeln t in - (* Toplevel.keep (Value_Command.value_cmd some_name modes (enclose "ASSERT(" ")" t)) *) - Toplevel.keep (value_cmd2 some_name modes t) - end)); -\ - -assert "True" -assert "True \ True " -ML\!TT ; - @{term "True"}\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index aae411f..dad635f 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -31,7 +31,6 @@ that provide direct support in the PIDE framework. \ theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main RegExpInterface (* Interface to functional regular automata for monitoring *) - Assert keywords "+=" ":=" "accepts" "rejects" "invariant" @@ -42,7 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) "define_shortcut*" "define_macro*" :: thy_decl and "text*" "text-macro*" :: document_body - and "term*" "value*" :: diag + and "term*" "value*" "assert*" :: diag and "print_doc_classes" "print_doc_items" "print_doc_class_template" "check_doc_global" :: diag @@ -1767,7 +1766,6 @@ end \ - ML \ \c.f. \<^file>\~~/src/HOL/Tools/value_command.ML\\ (* The value* command uses the same code as the value command @@ -1786,7 +1784,7 @@ sig val value: Proof.context -> term -> term val value_without_elaboration: Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term - val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string + val value_cmd: {assert: bool} -> (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string -> Toplevel.state -> Position.T -> unit val add_evaluator: binding * (Proof.context -> term -> term) -> theory -> string * theory @@ -1800,7 +1798,6 @@ structure Evaluators = Theory_Data ( type T = (Proof.context -> term -> term) Name_Space.table; val empty = Name_Space.empty_table "evaluator"; - val extend = I; val merge = Name_Space.merge_tables; ) @@ -1837,7 +1834,7 @@ fun meta_args_exec NONE thy = thy {is_monitor = false} {is_inline = false} oid pos (I cid_pos) (I doc_attrs)) -fun value_cmd meta_args_opt raw_name modes raw_t state pos = +fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t state pos = let val _ = meta_args_exec meta_args_opt val ctxt = Toplevel.context_of state; @@ -1847,6 +1844,16 @@ fun value_cmd meta_args_opt raw_name modes raw_t state pos = (Proof_Context.theory_of ctxt); val t' = value_select name ctxt term'; val ty' = Term.type_of t'; + val ty' = if assert + then case ty' of + \<^typ>\bool\ => ty' + | _ => error "Assertion expressions must be boolean." + else ty' + val t' = if assert + then case t' of + \<^term>\True\ => t' + | _ => error "Assertion failed." + else t' val ctxt' = Proof_Context.augment t' ctxt; val p = Print_Mode.with_modes modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, @@ -1869,7 +1876,13 @@ val opt_attributes = Scan.option ODL_Command_Parser.attributes fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = let val pos = Toplevel.pos_of trans in - Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state pos) trans + Toplevel.keep (fn state => value_cmd {assert=false} meta_args_opt name modes t state pos) trans +end + +fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = +let val pos = Toplevel.pos_of trans +in + Toplevel.keep (fn state => value_cmd {assert=true} meta_args_opt name modes t state pos) trans end \ \c.f. \<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ @@ -1927,6 +1940,11 @@ val _ = Theory.setup #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd #> add_evaluator (\<^binding>\code\, Code_Evaluation.dynamic_value_strict) #> snd); +val _ = + Outer_Syntax.command \<^command_keyword>\assert*\ "evaluate and assert term" + (opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) + >> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args)); + end; \ @@ -2050,7 +2068,6 @@ val _ = end \ - ML\ structure ODL_LTX_Converter = struct diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index b56fec6..90692b2 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -17,8 +17,6 @@ theory scholarly_paper imports "../../DOF/Isa_COL" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body - and "assert*" :: thy_decl - begin @@ -347,39 +345,7 @@ doc_class assertion = math_formal + properties :: "term list" -ML\ -(* TODO : Rework this code and make it closer to Definition*. There is still - a rest of "abstract classes in it: any class possessing a properties attribute - is admissible to this command, not just ... *) -local open ODL_Command_Parser in -fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), - prop) = - let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) - fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") - ::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_opt oid thy of - SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) - | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (create_and_check_docitem - {is_monitor = false} {is_inline = false} - oid pos cid_pos (conv_attrs thy) thy) - val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global - in - (* Toplevel.keep (check o Toplevel.context_of) *) - Toplevel.theory (fn thy => (check thy; mks thy)) - end - -val attributes = attributes (* re-export *) - -end -val _ = - Outer_Syntax.command @{command_keyword "assert*"} - "evaluate and print term" - (attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd'); - -\ subsubsection*[ex_ass::example]\Example\ text\Assertions allow for logical statements to be checked in the global context). \ diff --git a/src/tests/Evaluation.thy b/src/tests/Evaluation.thy index d33df1c..799ad50 100644 --- a/src/tests/Evaluation.thy +++ b/src/tests/Evaluation.thy @@ -6,6 +6,7 @@ theory Evaluation imports "Isabelle_DOF-tests.TermAntiquotations" + "Isabelle_DOF-tests.High_Level_Syntax_Invariants" begin section\\<^theory_text>\ML*\-Annotated SML-commands\ @@ -84,8 +85,8 @@ value*\A.x @{A \xcv1\}\ text\If the attribute of the instance is not initialized, we get an undefined value, whose type is the type of the attribute:\ -term*\level @{C \xcv2\}\ -value*\level @{C \xcv2\}\ +term*\B.level @{C \xcv2\}\ +value*\B.level @{C \xcv2\}\ text\The value of a TA is the term itself:\ term*\C.g @{C \xcv2\}\ @@ -170,4 +171,31 @@ to update the instance @{docitem \xcv4\}: update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*) +section\\<^theory_text>\assert*\-Annotated assertion-commands\ + +text\The \<^emph>\assert*\-command allows for logical statements to be checked in the global context. +It uses the same implementation as the \<^emph>\value*\-command and has the same limitations. +\ + +text\Using the ontology defined in \<^theory>\Isabelle_DOF-tests.High_Level_Syntax_Invariants\ +we can check logical statements:\ + +term*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +assert*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +assert*\\(authored_by @{introduction \introduction2\} + = authored_by @{introduction \introduction4\})\ + +text\Assertions must be boolean expressions, so the following assertion triggers an error:\ +(* Error: +assert*\@{introduction \introduction2\}\*) + +text\Assertions must be true, hence the error:\ +(* Error: +assert*\{@{author \curry\}} = {@{author \church\}}\*) + +term*\property @{result \resultProof\} = property @{result \resultProof2\}\ +assert*\\ property @{result \resultProof\} = property @{result \resultProof2\}\ + +assert*\evidence @{result \resultProof\} = evidence @{result \resultProof2\}\ + end -- 2.39.2