diff --git a/src/DOF/DOF_Core.thy b/src/DOF/DOF_Core.thy index 632a5350..753721de 100644 --- a/src/DOF/DOF_Core.thy +++ b/src/DOF/DOF_Core.thy @@ -662,6 +662,8 @@ fun update_value_global oid upd_input_term upd_value thy = in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end | NONE => error("undefined doc object: "^oid) +fun err msg pos = error (msg ^ Position.here pos); +fun warn msg pos = warning (msg ^ Position.here pos); val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) @@ -785,6 +787,41 @@ val (invariants_strict_checking, invariants_strict_checking_setup) val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) = Attrib.config_bool \<^binding>\invariants_checking_with_tactics\ (K false); +fun symbex_attr_access0 ctxt proj_term term = +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_option pos' = (* template *) + case get_value_global oid (Context.theory_of ctxt) of + SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt)) + val SOME{cid,pos=pos_decl,id,...} = get_object_local oid ctxt + val docitem_markup = docref_markup false oid id pos_decl; + val _ = Context_Position.report ctxt pos' docitem_markup; + val (* (long_cid, attr_b,ty) = *) + {long_name, typ=ty, def_pos, ...} = + case get_attribute_info_local cid attr ctxt of + SOME f => f + | NONE => error("attribute undefined for reference: " + ^ oid + ^ Position.here + (the pos_option handle Option.Option => + error("Attribute " + ^ attr + ^ " undefined for reference: " + ^ oid ^ Position.here pos'))) + val proj_term = Const(long_name,dummyT --> ty) + val _ = case pos_option of + NONE => () + | SOME pos => + let + val class_name = Long_Name.qualifier long_name + val SOME{id,...} = get_doc_class_local class_name ctxt + val class_markup = docclass_markup false class_name id def_pos + in Context_Position.report ctxt pos class_markup end + 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') end (* struct *) @@ -797,4 +834,8 @@ setup\DOF_core.strict_monitor_checking_setup #> DOF_core.invariants_strict_checking_setup #> DOF_core.invariants_checking_with_tactics_setup\ +subsection\ Syntax \ + +datatype "doc_class" = mk string + end \ No newline at end of file diff --git a/src/DOF/DOF_Deep.thy b/src/DOF/DOF_Deep.thy new file mode 100644 index 00000000..1e3f88d1 --- /dev/null +++ b/src/DOF/DOF_Deep.thy @@ -0,0 +1,21 @@ +theory DOF_Deep + imports "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF.Deep_Interpretation" + +begin + +(* tests *) +term "@{typ ''int => int''}" +term "@{term ''Bound 0''}" +term "@{thm ''refl''}" +term "@{docitem ''''}" +ML\ @{term "@{docitem ''''}"}\ + +term "@{typ \int \ int\}" +term "@{term \\x. P x \ Q\}" +term "@{thm \refl\}" +term "@{docitem \doc_ref\}" +ML\ @{term "@{docitem \doc_ref\}"}\ +(**) + +end \ No newline at end of file diff --git a/src/DOF/DOF_Shallow.thy b/src/DOF/DOF_Shallow.thy new file mode 100644 index 00000000..148f3951 --- /dev/null +++ b/src/DOF/DOF_Shallow.thy @@ -0,0 +1,21 @@ +theory DOF_Shallow + imports "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF.Shallow_Interpretation" + +begin + +(* tests *) +term "@{typ ''int => int''}" +term "@{term ''Bound 0''}" +term "@{thm ''refl''}" +term "@{docitem ''''}" +ML\ @{term "@{docitem ''''}"}\ + +term "@{typ \int \ int\}" +term "@{term \\x. P x \ Q\}" +term "@{thm \refl\}" +term "@{docitem \doc_ref\}" +ML\ @{term "@{docitem \doc_ref\}"}\ +(**) + +end \ No newline at end of file diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index e649ec36..039f2e70 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -22,7 +22,7 @@ text\ Building a fundamental infrastructure for common document elements s \ theory Isa_COL - imports Isa_DOF + imports DOF_Shallow keywords "title*" "subtitle*" "chapter*" "section*" "subsection*" "subsubsection*" diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index f320906f..8ca0392b 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -29,8 +29,9 @@ text\ In this section, we develop on the basis of a management of referenc that provide direct support in the PIDE framework. \ theory Isa_DOF (* Isabelle Document Ontology Framework *) - imports Main - "meta_interpretation/Deep_Interpretation" + imports Main + "Isabelle_DOF.DOF_Core" + "Isabelle_DOF.ISA_Class" keywords "+=" ":=" "accepts" "rejects" "invariant" @@ -134,19 +135,6 @@ parse_translation \ , parse_translation_cartouche \<^binding>\cartouche_type\ Cartouche_Grammar.default (K I) ())] \ -(* tests *) -term "@{typ ''int => int''}" -term "@{term ''Bound 0''}" -term "@{thm ''refl''}" -term "@{docitem ''''}" -ML\ @{term "@{docitem ''''}"}\ - -term "@{typ \int \ int\}" -term "@{term \\x. P x \ Q\}" -term "@{thm \refl\}" -term "@{docitem \doc_ref\}" -ML\ @{term "@{docitem \doc_ref\}"}\ -(**) declare [[cartouche_type = "String.literal"]] term "\Université\ :: String.literal" declare [[cartouche_type = "char list"]] @@ -403,7 +391,7 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long else case inherits_from of NONE => - ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos + DOF_core.err ("Attribute not defined for class: " ^ cid_long) pos | SOME (_, parent_name) => get_class_name parent_name attribute_name pos end @@ -445,8 +433,8 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long in Sign.certify_term thy (fold read_assn S term) end fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking - then ISA_core.err txt pos - else ISA_core.warn txt pos + then DOF_core.err txt pos + else DOF_core.warn txt pos fun register_oid_cid_in_open_monitors oid pos cid_pos thy = let val {monitor_tab,...} = DOF_core.get_data_global thy @@ -493,9 +481,9 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = ^ " not enabled for doc_class: " ^ cid_long) in if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking - then ISA_core.err msg_intro pos' + then DOF_core.err msg_intro pos' else if Config.get_global thy DOF_core.free_class_in_monitor_checking - then (ISA_core.warn msg_intro pos';A) + then (DOF_core.warn msg_intro pos';A) else A end | SOME _ => (msg thy ("accepts clause " ^ Int.toString n @@ -589,8 +577,8 @@ fun check_invariants thy oid = ^ " with error:\n" in if Config.get_global thy DOF_core.invariants_strict_checking - then ISA_core.err (msg_intro ^ e) pos - else (ISA_core.warn (msg_intro ^ e) pos; trivial_true) end + then DOF_core.err (msg_intro ^ e) pos + else (DOF_core.warn (msg_intro ^ e) pos; trivial_true) end (* If Goal.prove does not fail, then the evaluation is considered True, else an error is triggered by Goal.prove *) in @{term True} end) @@ -605,12 +593,12 @@ fun check_invariants thy oid = ^ "if your invariant is checked against doc_class algebraic " ^ "types like 'doc_class list' or 'doc_class set'" in if Config.get_global thy DOF_core.invariants_strict_checking - then ISA_core.err (msg_intro) pos - else (ISA_core.warn (msg_intro) pos; ((inv_name, pos), term)) end + then DOF_core.err (msg_intro) pos + else (DOF_core.warn (msg_intro) pos; ((inv_name, pos), term)) end | _ => let val msg_intro = "Invariant " ^ inv_name ^ " violated" in if Config.get_global thy DOF_core.invariants_strict_checking - then ISA_core.err msg_intro pos - else (ISA_core.warn msg_intro pos; ((inv_name, pos), term)) end + then DOF_core.err msg_intro pos + else (DOF_core.warn msg_intro pos; ((inv_name, pos), term)) end end val _ = map check_invariants' inv_and_apply_list in thy end @@ -896,7 +884,7 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars end fun create_monitor_entry thy = let val cid = case cid_pos of - NONE => ISA_core.err ("You must specified a monitor class.") pos + NONE => DOF_core.err ("You must specified a monitor class.") pos | SOME (cid, _) => cid val (accS, rejectS, aS) = compute_enabled_set cid thy val info = {accepted_cids = accS, rejected_cids = rejectS, automatas = aS } @@ -1392,7 +1380,7 @@ val basic_entity = Document_Output.antiquotation_pretty_source fun compute_trace_ML ctxt oid pos_opt pos' = (* grabs attribute, and converts its HOL-term into (textual) ML representation *) - let val term = ISA_core.compute_attr_access ctxt "trace" oid pos_opt pos' + let val term = DOF_core.compute_attr_access ctxt "trace" oid pos_opt pos' fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.read_cid (Context.proof_of ctxt) (HOLogic.dest_string s) @@ -1417,7 +1405,7 @@ val parse_attribute_access' = Term_Style.parse -- parse_attribute_access ((string * Position.T) * (string * Position.T))) context_parser fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o ML_Syntax.print_term) - (ISA_core.compute_attr_access ctxt attr oid (SOME pos) pos') + (DOF_core.compute_attr_access ctxt attr oid (SOME pos) pos') val TERM_STORE = let val dummy_term = Bound 0 @@ -1438,15 +1426,15 @@ fun trace_attr_2_ML ctxt (oid:string,pos) = fun compute_cid_repr ctxt cid pos = if DOF_core.is_defined_cid_local cid ctxt then Const(cid,dummyT) - else ISA_core.err ("Undefined Class Identifier:"^cid) pos + else DOF_core.err ("Undefined Class Identifier:"^cid) pos local fun pretty_attr_access_style ctxt (style, ((attr,pos),(oid,pos'))) = - Document_Output.pretty_term ctxt (style (ISA_core.compute_attr_access (Context.Proof ctxt) + Document_Output.pretty_term ctxt (style (DOF_core.compute_attr_access (Context.Proof ctxt) attr oid (SOME pos) pos')); fun pretty_trace_style ctxt (style, (oid,pos)) = - Document_Output.pretty_term ctxt (style (ISA_core.compute_attr_access (Context.Proof ctxt) + Document_Output.pretty_term ctxt (style (DOF_core.compute_attr_access (Context.Proof ctxt) "trace" oid NONE pos)); fun pretty_cid_style ctxt (style, (cid,pos)) = Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos)); @@ -1461,7 +1449,7 @@ fun context_position_parser parse_con (ctxt, toks) = val parse_cid = (context_position_parser Args.typ_abbrev) >> (fn (Type(ss,_),pos) => (pos,ss) - |( _,pos) => ISA_core.err "Undefined Class Id" pos); + |( _,pos) => DOF_core.err "Undefined Class Id" pos); val parse_cid' = Term_Style.parse -- parse_cid @@ -1657,8 +1645,8 @@ fun add_doc_class_cmd overloaded (raw_params, binding) (* The function declare_ISA_class_accessor_and_check_instance uses a prefix because the class name is already bound to "doc_class Regular_Exp.rexp" constant by add_doc_class_cmd function *) - |> ISA_core.declare_ISA_class_accessor_and_check_instance binding - |> (fn thy => (ISA_core.declare_class_instances_annotation thy binding) thy) + |> ISA_class.declare_ISA_class_accessor_and_check_instance binding + |> (fn thy => (ISA_class.declare_class_instances_annotation thy binding) thy) end; diff --git a/src/DOF/meta_interpretation/Deep_Interpretation.thy b/src/DOF/meta_interpretation/Deep_Interpretation.thy index 170076de..77ebbba5 100644 --- a/src/DOF/meta_interpretation/Deep_Interpretation.thy +++ b/src/DOF/meta_interpretation/Deep_Interpretation.thy @@ -4,9 +4,7 @@ theory Deep_Interpretation begin -subsection\ Syntax \ - -datatype "doc_class" = mk string +subsection\ Syntax \ \ \and others in the future : file, http, thy, ...\ @@ -27,22 +25,19 @@ ML\ structure ISA_core = struct -fun err msg pos = error (msg ^ Position.here pos); -fun warn msg pos = warning (msg ^ Position.here pos); - fun check_path check_file ctxt dir (name, pos) = let val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be "lifted" to type source *) - val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos; - val _ = Path.expand path handle ERROR msg => err msg pos; + val path = Path.append dir (Path.explode name) handle ERROR msg => DOF_core.err msg pos; + val _ = Path.expand path handle ERROR msg => DOF_core.err msg pos; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ = (case check_file of NONE => path - | SOME check => (check path handle ERROR msg => err msg pos)); + | SOME check => (check path handle ERROR msg => DOF_core.err msg pos)); in path end; @@ -75,7 +70,7 @@ fun ML_isa_check_term thy (term, _, pos) _ = fun ML_isa_check_thm thy (term, _, pos) _ = (* this works for long-names only *) let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of - NONE => err ("No Theorem:" ^name) pos + NONE => DOF_core.err ("No Theorem:" ^name) pos | SOME X => X in ML_isa_check_generic check thy (term, pos) end @@ -87,25 +82,6 @@ fun ML_isa_check_file thy (term, _, pos) _ = (name, pos); in ML_isa_check_generic check thy (term, pos) end; -fun check_instance thy (term, _, pos) s = - let - val bname = Long_Name.base_name s; - val qual = Long_Name.qualifier s; - val class_name = - Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE)); - fun check thy (name, _) = - let - val object_cid = case DOF_core.get_object_global name thy of - NONE => err ("No class instance: " ^ name) pos - | SOME(object) => #cid object - fun check' (class_name, object_cid) = - if class_name = object_cid then - DOF_core.get_value_global name thy - else err (name ^ " is not an instance of " ^ class_name) pos - in check' (class_name, object_cid) end; - in ML_isa_check_generic check thy (term, pos) end - - fun ML_isa_id thy (term,pos) = SOME term @@ -126,14 +102,14 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) _ = ^cid^" vs. "^req_class^ Position.here pos_decl) else () end - else err ("faulty reference to docitem: "^name) pos + else DOF_core.err ("faulty reference to docitem: "^name) pos in ML_isa_check_generic check thy (term, pos) end fun ML_isa_check_trace_attribute thy (term, _, pos) s = let fun check thy (name, _) = case DOF_core.get_object_global name thy of - NONE => err ("No class instance: " ^ name) pos + NONE => DOF_core.err ("No class instance: " ^ name) pos | SOME(_) => () in ML_isa_check_generic check thy (term, pos) end @@ -224,11 +200,13 @@ fun reify_proofterm (PBound i) =\<^Const>\PBound\ $ (HOLogic.mk_nat fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos = case term_option of - NONE => err ("Malformed term annotation") pos + NONE => DOF_core.err ("Malformed term annotation") pos | SOME term => let val thm_name = HOLogic.dest_string term + val _ = writeln ("In ML_isa_elaborate_thm thm_name: " ^ \<^make_string> thm_name) val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name + val _ = writeln ("In ML_isa_elaborate_thm thm: " ^ \<^make_string> thm) val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); val prf = Proofterm.proof_of body; (* Proof_Syntax.standard_proof_of reconstructs the proof and seems to rewrite @@ -239,6 +217,7 @@ fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos = all the option types of the proof datatype constructors *) val proof = Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm + val _ = writeln ("In ML_isa_elaborate_thm proof: " ^ \<^make_string> proof) (* After a small discussion with Simon Roßkopf, It seems preferable to use Thm.reconstruct_proof_of instead of Proof_Syntax.standard_proof_of whose operation is not well known. @@ -252,7 +231,7 @@ fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos = fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos = case term_option of - NONE => err ("Malformed term annotation") pos + NONE => DOF_core.err ("Malformed term annotation") pos | SOME term => let val thm_name = HOLogic.dest_string term @@ -265,139 +244,13 @@ fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos = (*in HOLogic.mk_list \<^Type>\thm\ (map (fn proof => \<^Const>\Thm_content\ $ reify_proofterm proof) all_proofs) end*) in HOLogic.mk_list \<^typ>\string\ (map HOLogic.mk_string all_thms_name) end -fun elaborate_instance thy _ _ term_option pos = - case term_option of - NONE => error ("Malformed term annotation") - | SOME term => let val instance_name = HOLogic.dest_string term - in case DOF_core.get_value_global instance_name thy of - NONE => error ("No class instance: " ^ instance_name) - | SOME(value) => - DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy - end - -(* - The function declare_ISA_class_accessor_and_check_instance uses a prefix - because the class name is already bound to "doc_class Regular_Exp.rexp" constant - by add_doc_class_cmd function -*) -fun declare_ISA_class_accessor_and_check_instance doc_class_name = - let - val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name - val typestring = "string => " ^ (Binding.name_of doc_class_name) - (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols - we can not use "_" for classes names in term antiquotation. - We chose to convert "_" to "-".*) - val conv_class_name = String.translate (fn #"_" => "-" - | x => String.implode [x] ) - (Binding.name_of doc_class_name) - val mixfix_string = "@{" ^ conv_class_name ^ " _}" - in - Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))] - #> (fn thy => let - val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - val qual = Long_Name.qualifier long_name - val class_name = Long_Name.qualify qual - (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind)) - in - DOF_core.update_isa_global - (class_name, {check=check_instance, elaborate=elaborate_instance}) thy - end) - end - -fun elaborate_instances_list thy isa_name _ _ _ = - let - val base_name = Long_Name.base_name isa_name - fun get_isa_name_without_intances_suffix s = - String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN))) - val base_name_without_suffix = get_isa_name_without_intances_suffix base_name - val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix) - val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy) - (base_name') - val tab = #tab(#docobj_tab(DOF_core.get_data_global thy)) - val table_list = Symtab.dest tab - fun get_instances_name_list _ [] = [] - | get_instances_name_list class_name (x::xs) = - let - val (_, docobj_option) = x - in - case docobj_option of - NONE => get_instances_name_list class_name xs - | SOME {cid=cid, value=value, ...} => - if cid = class_name - then value::get_instances_name_list class_name xs - else get_instances_name_list class_name xs - end - val long_class_name = DOF_core.read_cid_global thy base_name' - val values_list = get_instances_name_list long_class_name table_list - in HOLogic.mk_list class_typ values_list end - -fun declare_class_instances_annotation thy doc_class_name = - let - val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name - val bind' = Binding.suffix_name instances_of_suffixN bind - val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy) - ((Binding.name_of doc_class_name) ^ " List.list") - (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols - we can not use "_" for classes names in term antiquotation. - We chose to convert "_" to "-".*) - val conv_class_name' = String.translate (fn #"_" => "-" | x=> String.implode [x]) - ((Binding.name_of doc_class_name) ^ instances_of_suffixN) - val mixfix_string = "@{" ^ conv_class_name' ^ "}" - in - Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] - #> (fn thy => let - val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - val qual = Long_Name.qualifier long_name - val transformer_name = Long_Name.qualify qual - (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind')) - in - DOF_core.update_isa_global (transformer_name, - {check=check_identity, elaborate= elaborate_instances_list}) thy end) - end - -fun symbex_attr_access0 ctxt proj_term term = -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_option pos' = (* template *) - case DOF_core.get_value_global oid (Context.theory_of ctxt) of - SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt)) - val SOME{cid,pos=pos_decl,id,...} = DOF_core.get_object_local oid ctxt - val docitem_markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report ctxt pos' docitem_markup; - val (* (long_cid, attr_b,ty) = *) - {long_name, typ=ty, def_pos, ...} = - case DOF_core.get_attribute_info_local cid attr ctxt of - SOME f => f - | NONE => error("attribute undefined for reference: " - ^ oid - ^ Position.here - (the pos_option handle Option.Option => - error("Attribute " - ^ attr - ^ " undefined for reference: " - ^ oid ^ Position.here pos'))) - val proj_term = Const(long_name,dummyT --> ty) - val _ = case pos_option of - NONE => () - | SOME pos => - let - val class_name = Long_Name.qualifier long_name - val SOME{id,...} = DOF_core.get_doc_class_local class_name ctxt - val class_markup = docclass_markup false class_name id def_pos - in Context_Position.report ctxt pos class_markup end - 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') - fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos = case term_option of - NONE => err ("Malformed term annotation") pos + NONE => DOF_core.err ("Malformed term annotation") pos | SOME term => let val oid = HOLogic.dest_string term - val traces = compute_attr_access (Context.Theory thy) "trace" oid NONE pos + val traces = DOF_core.compute_attr_access (Context.Theory thy) "trace" oid NONE pos fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s) diff --git a/src/DOF/meta_interpretation/ISA_Class.thy b/src/DOF/meta_interpretation/ISA_Class.thy new file mode 100644 index 00000000..77866207 --- /dev/null +++ b/src/DOF/meta_interpretation/ISA_Class.thy @@ -0,0 +1,129 @@ +theory ISA_Class + imports Isabelle_DOF.DOF_Core + +begin + +ML\ +structure ISA_class = +struct + +fun ML_isa_check_generic check thy (term, pos) = + let val name = (HOLogic.dest_string term + handle TERM(_,[t]) => error ("wrong term format: must be string constant: " + ^ Syntax.string_of_term_global thy t )) + val _ = check thy (name,pos) + in SOME term end; + +fun check_identity _ (term, _, _) _ = SOME term +fun check_instance thy (term, _, pos) s = + let + val bname = Long_Name.base_name s; + val qual = Long_Name.qualifier s; + val class_name = + Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE)); + fun check thy (name, _) = + let + val object_cid = case DOF_core.get_object_global name thy of + NONE => DOF_core.err ("No class instance: " ^ name) pos + | SOME(object) => #cid object + fun check' (class_name, object_cid) = + if class_name = object_cid then + DOF_core.get_value_global name thy + else DOF_core.err (name ^ " is not an instance of " ^ class_name) pos + in check' (class_name, object_cid) end; + in ML_isa_check_generic check thy (term, pos) end + +fun elaborate_instance thy _ _ term_option pos = + case term_option of + NONE => error ("Malformed term annotation") + | SOME term => let val instance_name = HOLogic.dest_string term + in case DOF_core.get_value_global instance_name thy of + NONE => error ("No class instance: " ^ instance_name) + | SOME(value) => + DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy + end + +(* + The function declare_ISA_class_accessor_and_check_instance uses a prefix + because the class name is already bound to "doc_class Regular_Exp.rexp" constant + by add_doc_class_cmd function +*) +fun declare_ISA_class_accessor_and_check_instance doc_class_name = + let + val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name + val typestring = "string => " ^ (Binding.name_of doc_class_name) + (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols + we can not use "_" for classes names in term antiquotation. + We chose to convert "_" to "-".*) + val conv_class_name = String.translate (fn #"_" => "-" + | x => String.implode [x] ) + (Binding.name_of doc_class_name) + val mixfix_string = "@{" ^ conv_class_name ^ " _}" + in + Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))] + #> (fn thy => let + val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) + val qual = Long_Name.qualifier long_name + val class_name = Long_Name.qualify qual + (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind)) + in + DOF_core.update_isa_global + (class_name, {check=check_instance, elaborate=elaborate_instance}) thy + end) + end + +fun elaborate_instances_list thy isa_name _ _ _ = + let + val base_name = Long_Name.base_name isa_name + fun get_isa_name_without_intances_suffix s = + String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN))) + val base_name_without_suffix = get_isa_name_without_intances_suffix base_name + val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix) + val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy) + (base_name') + val tab = #tab(#docobj_tab(DOF_core.get_data_global thy)) + val table_list = Symtab.dest tab + fun get_instances_name_list _ [] = [] + | get_instances_name_list class_name (x::xs) = + let + val (_, docobj_option) = x + in + case docobj_option of + NONE => get_instances_name_list class_name xs + | SOME {cid=cid, value=value, ...} => + if cid = class_name + then value::get_instances_name_list class_name xs + else get_instances_name_list class_name xs + end + val long_class_name = DOF_core.read_cid_global thy base_name' + val values_list = get_instances_name_list long_class_name table_list + in HOLogic.mk_list class_typ values_list end + +fun declare_class_instances_annotation thy doc_class_name = + let + val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name + val bind' = Binding.suffix_name instances_of_suffixN bind + val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy) + ((Binding.name_of doc_class_name) ^ " List.list") + (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols + we can not use "_" for classes names in term antiquotation. + We chose to convert "_" to "-".*) + val conv_class_name' = String.translate (fn #"_" => "-" | x=> String.implode [x]) + ((Binding.name_of doc_class_name) ^ instances_of_suffixN) + val mixfix_string = "@{" ^ conv_class_name' ^ "}" + in + Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] + #> (fn thy => let + val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) + val qual = Long_Name.qualifier long_name + val transformer_name = Long_Name.qualify qual + (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind')) + in + DOF_core.update_isa_global (transformer_name, + {check=check_identity, elaborate= elaborate_instances_list}) thy end) + end + +end (* ISA_class *) +\ + +end \ No newline at end of file diff --git a/src/DOF/meta_interpretation/Shallow_Interpretation.thy b/src/DOF/meta_interpretation/Shallow_Interpretation.thy index df88ffba..01ff5226 100644 --- a/src/DOF/meta_interpretation/Shallow_Interpretation.thy +++ b/src/DOF/meta_interpretation/Shallow_Interpretation.thy @@ -4,8 +4,6 @@ begin subsection\ Syntax \ -datatype "doc_class" = mk string - \ \and others in the future : file, http, thy, ...\ datatype "typ" = ISA_typ string ("@{typ _}") @@ -24,22 +22,19 @@ ML\ structure ISA_core = struct -fun err msg pos = error (msg ^ Position.here pos); -fun warn msg pos = warning (msg ^ Position.here pos); - fun check_path check_file ctxt dir (name, pos) = let val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be "lifted" to type source *) - val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos; - val _ = Path.expand path handle ERROR msg => err msg pos; + val path = Path.append dir (Path.explode name) handle ERROR msg => DOF_core.err msg pos; + val _ = Path.expand path handle ERROR msg => DOF_core.err msg pos; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ = (case check_file of NONE => path - | SOME check => (check path handle ERROR msg => err msg pos)); + | SOME check => (check path handle ERROR msg => DOF_core.err msg pos)); in path end; @@ -72,7 +67,7 @@ fun ML_isa_check_term thy (term, _, pos) _ = fun ML_isa_check_thm thy (term, _, pos) _ = (* this works for long-names only *) let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of - NONE => err ("No Theorem:" ^name) pos + NONE => DOF_core.err ("No Theorem:" ^name) pos | SOME X => X in ML_isa_check_generic check thy (term, pos) end @@ -84,28 +79,8 @@ fun ML_isa_check_file thy (term, _, pos) _ = (name, pos); in ML_isa_check_generic check thy (term, pos) end; -fun check_instance thy (term, _, pos) s = - let - val bname = Long_Name.base_name s; - val qual = Long_Name.qualifier s; - val class_name = - Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE)); - fun check thy (name, _) = - let - val object_cid = case DOF_core.get_object_global name thy of - NONE => err ("No class instance: " ^ name) pos - | SOME(object) => #cid object - fun check' (class_name, object_cid) = - if class_name = object_cid then - DOF_core.get_value_global name thy - else err (name ^ " is not an instance of " ^ class_name) pos - in check' (class_name, object_cid) end; - in ML_isa_check_generic check thy (term, pos) end - - fun ML_isa_id thy (term,pos) = SOME term - fun ML_isa_check_docitem thy (term, req_ty, pos) _ = let fun check thy (name, _) s = if DOF_core.is_declared_oid_global name thy @@ -123,14 +98,14 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) _ = ^cid^" vs. "^req_class^ Position.here pos_decl) else () end - else err ("faulty reference to docitem: "^name) pos + else DOF_core.err ("faulty reference to docitem: "^name) pos in ML_isa_check_generic check thy (term, pos) end fun ML_isa_check_trace_attribute thy (term, _, pos) s = let fun check thy (name, _) = case DOF_core.get_object_global name thy of - NONE => err ("No class instance: " ^ name) pos + NONE => DOF_core.err ("No class instance: " ^ name) pos | SOME(_) => () in ML_isa_check_generic check thy (term, pos) end @@ -139,139 +114,13 @@ fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = NONE => error("Wrong term option. You must use a defined term") | SOME term => Const (isa_name, ty) $ term -fun elaborate_instance thy _ _ term_option pos = - case term_option of - NONE => error ("Malformed term annotation") - | SOME term => let val instance_name = HOLogic.dest_string term - in case DOF_core.get_value_global instance_name thy of - NONE => error ("No class instance: " ^ instance_name) - | SOME(value) => - DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy - end - -(* - The function declare_ISA_class_accessor_and_check_instance uses a prefix - because the class name is already bound to "doc_class Regular_Exp.rexp" constant - by add_doc_class_cmd function -*) -fun declare_ISA_class_accessor_and_check_instance doc_class_name = - let - val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name - val typestring = "string => " ^ (Binding.name_of doc_class_name) - (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols - we can not use "_" for classes names in term antiquotation. - We chose to convert "_" to "-".*) - val conv_class_name = String.translate (fn #"_" => "-" - | x => String.implode [x] ) - (Binding.name_of doc_class_name) - val mixfix_string = "@{" ^ conv_class_name ^ " _}" - in - Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))] - #> (fn thy => let - val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - val qual = Long_Name.qualifier long_name - val class_name = Long_Name.qualify qual - (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind)) - in - DOF_core.update_isa_global - (class_name, {check=check_instance, elaborate=elaborate_instance}) thy - end) - end - -fun elaborate_instances_list thy isa_name _ _ _ = - let - val base_name = Long_Name.base_name isa_name - fun get_isa_name_without_intances_suffix s = - String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN))) - val base_name_without_suffix = get_isa_name_without_intances_suffix base_name - val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix) - val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy) - (base_name') - val tab = #tab(#docobj_tab(DOF_core.get_data_global thy)) - val table_list = Symtab.dest tab - fun get_instances_name_list _ [] = [] - | get_instances_name_list class_name (x::xs) = - let - val (_, docobj_option) = x - in - case docobj_option of - NONE => get_instances_name_list class_name xs - | SOME {cid=cid, value=value, ...} => - if cid = class_name - then value::get_instances_name_list class_name xs - else get_instances_name_list class_name xs - end - val long_class_name = DOF_core.read_cid_global thy base_name' - val values_list = get_instances_name_list long_class_name table_list - in HOLogic.mk_list class_typ values_list end - -fun declare_class_instances_annotation thy doc_class_name = - let - val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name - val bind' = Binding.suffix_name instances_of_suffixN bind - val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy) - ((Binding.name_of doc_class_name) ^ " List.list") - (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols - we can not use "_" for classes names in term antiquotation. - We chose to convert "_" to "-".*) - val conv_class_name' = String.translate (fn #"_" => "-" | x=> String.implode [x]) - ((Binding.name_of doc_class_name) ^ instances_of_suffixN) - val mixfix_string = "@{" ^ conv_class_name' ^ "}" - in - Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] - #> (fn thy => let - val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - val qual = Long_Name.qualifier long_name - val transformer_name = Long_Name.qualify qual - (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind')) - in - DOF_core.update_isa_global (transformer_name, - {check=check_identity, elaborate= elaborate_instances_list}) thy end) - end - -fun symbex_attr_access0 ctxt proj_term term = -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_option pos' = (* template *) - case DOF_core.get_value_global oid (Context.theory_of ctxt) of - SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt)) - val SOME{cid,pos=pos_decl,id,...} = DOF_core.get_object_local oid ctxt - val docitem_markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report ctxt pos' docitem_markup; - val (* (long_cid, attr_b,ty) = *) - {long_name, typ=ty, def_pos, ...} = - case DOF_core.get_attribute_info_local cid attr ctxt of - SOME f => f - | NONE => error("attribute undefined for reference: " - ^ oid - ^ Position.here - (the pos_option handle Option.Option => - error("Attribute " - ^ attr - ^ " undefined for reference: " - ^ oid ^ Position.here pos'))) - val proj_term = Const(long_name,dummyT --> ty) - val _ = case pos_option of - NONE => () - | SOME pos => - let - val class_name = Long_Name.qualifier long_name - val SOME{id,...} = DOF_core.get_doc_class_local class_name ctxt - val class_markup = docclass_markup false class_name id def_pos - in Context_Position.report ctxt pos class_markup end - 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') - fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos = case term_option of - NONE => err ("Malformed term annotation") pos + NONE => DOF_core.err ("Malformed term annotation") pos | SOME term => let val oid = HOLogic.dest_string term - val traces = compute_attr_access (Context.Theory thy) "trace" oid NONE pos + val traces = DOF_core.compute_attr_access (Context.Theory thy) "trace" oid NONE pos fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s) diff --git a/src/ROOT b/src/ROOT index ca90a5b6..1c94f424 100644 --- a/src/ROOT +++ b/src/ROOT @@ -14,7 +14,8 @@ session "Isabelle_DOF" = "Functional-Automata" + "ontologies/technical_report" "ontologies/CC_v3_1_R5" theories - "DOF/Isa_DOF" + "DOF/DOF_Shallow" + "DOF/DOF_Deep" "ontologies/ontologies" export_classpath diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index fb9c6e54..a263e38f 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -16,7 +16,7 @@ section\A conceptual introduction into DOF and its features:\ theory Conceptual imports - "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF.DOF_Shallow" "Isabelle_DOF.Isa_COL" begin diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 05a034a6..6002e088 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -465,7 +465,7 @@ in fun check ctxt cidS mon_id pos_opt = let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos_opt @{here} val groups = partition (Context.proof_of ctxt) cidS trace - fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here}; + fun get_level_raw oid = DOF_core.compute_attr_access ctxt "level" oid NONE @{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 ^ diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index d132926e..d82f730e 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -65,8 +65,8 @@ doc_class result = technical + ML\fun check_invariant_invariant oid {is_monitor:bool} ctxt = - let val kind_term = ISA_core.compute_attr_access ctxt "kind" oid NONE @{here} - val property_termS = ISA_core.compute_attr_access ctxt "property" oid NONE @{here} + let val kind_term = DOF_core.compute_attr_access ctxt "kind" oid NONE @{here} + val property_termS = DOF_core.compute_attr_access ctxt "property" oid NONE @{here} val tS = HOLogic.dest_list property_termS in case kind_term of @{term "proof"} => if not(null tS) then true @@ -140,7 +140,7 @@ in fun check ctxt cidS mon_id pos_opt = let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos_opt @{here} val groups = partition (Context.proof_of ctxt) cidS trace - fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here}; + fun get_level_raw oid = DOF_core.compute_attr_access ctxt "level" oid NONE @{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 ^ diff --git a/src/tests/Concept_Example_Low_Level_Invariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy index de11e0a9..29c6ed9e 100644 --- a/src/tests/Concept_Example_Low_Level_Invariant.thy +++ b/src/tests/Concept_Example_Low_Level_Invariant.thy @@ -44,7 +44,7 @@ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ ML\fun check_A_invariant oid {is_monitor:bool} ctxt = - let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here} + let val term = DOF_core.compute_attr_access ctxt "x" oid NONE @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term in if x_value > 5 then error("class A invariant violation") else true end \ @@ -80,7 +80,7 @@ to take sub-classing into account: \ ML\fun check_M_invariant oid {is_monitor} ctxt = - let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} + let val term = DOF_core.compute_attr_access ctxt "trace" oid NONE @{here} fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.read_cid (Context.proof_of ctxt) (HOLogic.dest_string s) @@ -117,7 +117,7 @@ section*[f2::E] \ Lectus accumsan velit ultrices, ... }\< *) ML\val ctxt = @{context} - val term = ISA_core.compute_attr_access + val term = DOF_core.compute_attr_access (Context.Proof ctxt) "trace" "struct" NONE @{here} ; fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) fun conv' (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ diff --git a/src/tests/High_Level_Syntax_Invariants.thy b/src/tests/High_Level_Syntax_Invariants.thy index 1c6626f0..42b3070e 100644 --- a/src/tests/High_Level_Syntax_Invariants.thy +++ b/src/tests/High_Level_Syntax_Invariants.thy @@ -1,7 +1,7 @@ chapter\High level syntax Invariants\ theory High_Level_Syntax_Invariants - imports "Isabelle_DOF.Isa_DOF" + imports "Isabelle_DOF.DOF_Shallow" begin text\ diff --git a/src/tests/ROOT b/src/tests/ROOT index 39f6ee73..00aa768a 100644 --- a/src/tests/ROOT +++ b/src/tests/ROOT @@ -9,5 +9,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" + "Evaluation" "High_Level_Syntax_Invariants" "Ontology_Matching_Example" + "Reification_Test" theories [condition = ISABELLE_DOF_HOME] "Isabelle2022" diff --git a/src/tests/Reification.thy b/src/tests/Reification_Test.thy similarity index 92% rename from src/tests/Reification.thy rename to src/tests/Reification_Test.thy index 83461042..5eadc7b7 100644 --- a/src/tests/Reification.thy +++ b/src/tests/Reification_Test.thy @@ -1,5 +1,5 @@ -theory Reification - imports "Isabelle_DOF.Conceptual" +theory Reification_Test + imports "Isabelle_DOF.DOF_Deep" begin @@ -103,10 +103,10 @@ ML\ prf test full_prf test -term*\@{thm \Reification.test\}\ -value*\@{thm \Reification.test\}\ -term*\@{thms-of \Reification.test\}\ -value*\@{thms-of \Reification.test\}\ +term*\@{thm \Reification_Test.test\}\ +value*\@{thm \Reification_Test.test\}\ +term*\@{thms-of \Reification_Test.test\}\ +value*\@{thms-of \Reification_Test.test\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\ @@ -150,8 +150,8 @@ ML\ prf test2 full_prf test2 -term*\@{thm \Reification.test2\}\ -value*\proof @{thm \Reification.test2\}\ +term*\@{thm \Reification_Test.test2\}\ +value*\proof @{thm \Reification_Test.test2\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\ @@ -175,8 +175,8 @@ ML\ prf test2 full_prf test2 -term*\@{thm \Reification.test3\}\ -value*\@{thm \Reification.test3\}\ +term*\@{thm \Reification_Test.test3\}\ +value*\@{thm \Reification_Test.test3\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\