From 1ec6dacd6ea96c785a090ecda0faec6368d4aa2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 21 Dec 2022 18:26:11 +0100 Subject: [PATCH] Update file hierarchy for meta-interpretation Restructure theory files to allow multiple meta-interpretation of term antiquotations --- .../IsaDofApplications.thy | 4 +- .../scholarly_paper/2020-iFM-CSP/paper.thy | 2 +- .../TR_MyCommentedIsabelle.thy | 2 +- src/DOF/DOF_Core.thy | 800 +++++++++++ src/DOF/Isa_DOF.thy | 1239 +---------------- .../Deep_Interpretation.thy | 451 ++++++ .../Shallow_Interpretation.thy | 311 +++++ src/ROOT | 2 + src/ontologies/small_math/small_math.thy | 2 +- src/tests/High_Level_Syntax_Invariants.thy | 4 +- .../{Test_Reification.thy => Reification.thy} | 153 +- src/tests/TermAntiquotations.thy | 236 ---- 12 files changed, 1628 insertions(+), 1578 deletions(-) create mode 100644 src/DOF/DOF_Core.thy create mode 100644 src/DOF/meta_interpretation/Deep_Interpretation.thy create mode 100644 src/DOF/meta_interpretation/Shallow_Interpretation.thy rename src/tests/{Test_Reification.thy => Reification.thy} (62%) diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index 56f9a192..cda1b295 100644 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -121,7 +121,7 @@ declare_reference*[bgrnd::text_section] declare_reference*[isadof::text_section] declare_reference*[ontomod::text_section] declare_reference*[ontopide::text_section] -declare_reference*[conclusion::text_section] +declare_reference*["conclusion"::text_section] (*>*) text*[plan::introduction, level="Some 1"]\ The plan of the paper is follows: we start by introducing the underlying Isabelle system (@{text_section (unchecked) \bgrnd\}) followed by presenting the @@ -700,7 +700,7 @@ directly nor indirectly (via inheritance) mentioned in the monitor are \<^emph>\ monitor; instances of independent test elements may occur freely. \ -section*[conclusion::conclusion]\ Conclusion and Related Work\ +section*["conclusion"::"conclusion"]\ Conclusion and Related Work\ text\ We have demonstrated the use of \<^isadof>, a novel ontology modeling and enforcement IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are \<^item> \<^isadof> and its ontology language are a strongly typed language that allows diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 229c48ab..c29b003f 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -995,7 +995,7 @@ restrictions on the structure of components. None of our paradigmatic examples c be automatically proven with any of the discussed SMT techniques without restrictions. \ -section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\Conclusion\ +section*["conclusion"::"conclusion",main_author="Some(@{docitem ''bu''}::author)"]\Conclusion\ text\We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical' language for the specification and analysis of concurrent systems studied in a rich body of literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 1f90b617..ffb7b115 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -2310,7 +2310,7 @@ term "\A \ B\ = ''''" -chapter*[c::conclusion]\Conclusion\ +chapter*[c::"conclusion"]\Conclusion\ text\ This interactive Isabelle Programming Cook-Book represents my current way to view and explain Isabelle programming API's to students and collaborators. It differs from the reference manual in some places on purpose, since I believe diff --git a/src/DOF/DOF_Core.thy b/src/DOF/DOF_Core.thy new file mode 100644 index 00000000..632a5350 --- /dev/null +++ b/src/DOF/DOF_Core.thy @@ -0,0 +1,800 @@ +theory DOF_Core + imports Main + RegExpInterface (* Interface to functional regular automata for monitoring *) + +begin + +section\Primitive Markup Generators\ +ML\ + +val docrefN = "docref"; +val docclassN = "doc_class"; + +(** name components **) + +val defN = "def" +val def_suffixN = "_" ^ defN +val defsN = defN ^ "s" +val instances_of_suffixN = "_instances" +val invariant_suffixN = "_inv" +val invariantN = "\" +val makeN = "make" +val schemeN = "_scheme" + +(* derived from: theory_markup *) +fun docref_markup_gen refN def name id pos = + if id = 0 then Markup.empty + else Position.make_entity_markup {def = def} id refN (name, pos); (* or better store the thy-name as property ? ? ? *) + +val docref_markup = docref_markup_gen docrefN + +val docclass_markup = docref_markup_gen docclassN + +\ + +section\ Utilities\ + +ML\ +fun spy x y = (writeln (x ^ y); y) + +fun markup2string x = XML.content_of (YXML.parse_body x) + +(* a hacky, but save encoding of unicode comming from the interface to the string format + that can be parsed by the inner-syntax string parser ''dfdf''. *) +fun bstring_to_holstring ctxt x (* (x:bstring) *) : string = + let val term = Syntax.parse_term ctxt (markup2string x) + fun hpp x = if x = #"\\" then "@" else + if x = #"@" then "@@" else String.implode [x] + in term |> Sledgehammer_Util.hackish_string_of_term ctxt + |> map hpp o String.explode |> String.concat + end; + + +fun chopper p (x:string) = + let fun hss buff [] = rev buff + |hss buff (S as a::R) = if p a then let val (front,rest) = chop_prefix p S + in hss (String.implode front :: buff) rest end + else let val (front,rest) = chop_prefix (not o p) S + in hss (String.implode front ::buff) rest end + in hss [] (String.explode x) end; + + +fun holstring_to_bstring ctxt (x:string) : bstring = + let fun collapse "" = "" + |collapse S = if String.sub(S,0) = #"@" + then let val n = String.size S + val front = replicate (n div 2) #"@" + val back = if (n mod 2)=1 then [#"\\"] else [] + in String.implode (front @ back) end + else S; + val t = String.concat (map collapse (chopper (fn x => x = #"@") x)); + in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end; + +fun map_option _ NONE = NONE + |map_option f (SOME x) = SOME (f x); + +fun map_optional _ s NONE = s + |map_optional f _ (SOME x) = f x; + +fun map_fst f (x,y) = (f x,y) +fun map_snd f (x,y) = (x,f y) + +fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y) + +\ + +section\ A HomeGrown Document Type Management (the ''Model'') \ + +ML\ +structure DOF_core = + +struct + type virtual = {virtual : bool} + type docclass_struct = {params : (string * sort) list, (*currently not used *) + name : binding, + virtual : virtual, + thy_name : string, id : serial, (* for pide *) + inherits_from : (typ list * string) option, (* imports *) + attribute_decl : (binding*typ*term option)list, (* class local *) + rejectS : term list, + rex : term list, + invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) + + + type docclass_tab = docclass_struct Symtab.table + + val initial_docclass_tab = Symtab.empty:docclass_tab + + fun merge_docclass_tab (otab,otab') = Symtab.merge (op =) (otab,otab') + + val tag_attr = (\<^binding>\tag_attribute\, \<^Type>\int\, Mixfix.NoSyn) + (* Attribute hidden to the user and used internally by isabelle_DOF. + For example, this allows to add a specific id to a class + to be able to reference the class internally. + *) + + val default_cid = "text" (* the top (default) document class: everything is a text.*) + + fun is_subclass0 (tab:docclass_tab) s t = + let val _ = case Symtab.lookup tab t of + NONE => if t <> default_cid + then error ("document superclass not defined: "^t) + else default_cid + | SOME _ => "" + fun father_is_sub s = case Symtab.lookup tab s of + NONE => error ("document subclass not defined: "^s) + | SOME ({inherits_from=NONE, ...}) => s = t + | SOME ({inherits_from=SOME (_,s'), ...}) => + s' = t orelse father_is_sub s' + in s = t orelse + (t = default_cid andalso Symtab.defined tab s ) orelse + (s <> default_cid andalso father_is_sub s) + end + + type docobj = {pos : Position.T, + thy_name : string, + input_term : term, + value : term, + inline : bool, + id : serial, + cid : string, + vcid : string option} + + type docobj_tab ={tab : (docobj option) Symtab.table, + maxano : int + } + + val initial_docobj_tab:docobj_tab = {tab = Symtab.empty, maxano = 0} + + fun merge_docobj_tab ({tab=otab,maxano=m}, {tab=otab',maxano=m'}) = + (let fun X(NONE,NONE) = false + |X(SOME _, NONE) = false + |X(NONE, SOME _) = false + |X(SOME b, SOME b') = true (* b = b' *) + in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')} + end) + type ISA_transformers = {check : + (theory -> term * typ * Position.T -> string -> term option), + elaborate : (theory -> string -> typ -> term option -> Position.T -> term) + } + + type ISA_transformer_tab = ISA_transformers Symtab.table + val initial_ISA_tab:ISA_transformer_tab = Symtab.empty + + type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table + val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty + + type docclass_eager_inv_tab = + (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table + val initial_docclass_eager_inv_tab : docclass_eager_inv_tab = Symtab.empty + + type docclass_lazy_inv_tab = + (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table + val initial_docclass_lazy_inv_tab : docclass_lazy_inv_tab = Symtab.empty + + type open_monitor_info = {accepted_cids : string list, + rejected_cids : string list, + automatas : RegExpInterface.automaton list + } + + type monitor_tab = open_monitor_info Symtab.table + val initial_monitor_tab:monitor_tab = Symtab.empty + + fun override(t1,t2) = fold(Symtab.update)(Symtab.dest t2)(t1) + +(* registrating data of the Isa_DOF component *) +structure Data = Generic_Data +( + type T = {docobj_tab : docobj_tab, + docclass_tab : docclass_tab, + ISA_transformer_tab : ISA_transformer_tab, + monitor_tab : monitor_tab, + docclass_inv_tab : docclass_inv_tab, + docclass_eager_inv_tab : docclass_eager_inv_tab, + docclass_lazy_inv_tab : docclass_lazy_inv_tab} + val empty = {docobj_tab = initial_docobj_tab, + docclass_tab = initial_docclass_tab, + ISA_transformer_tab = initial_ISA_tab, + monitor_tab = initial_monitor_tab, + docclass_inv_tab = initial_docclass_inv_tab, + docclass_eager_inv_tab = initial_docclass_eager_inv_tab, + docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab + } + fun merge( {docobj_tab=d1,docclass_tab = c1, + ISA_transformer_tab = e1, monitor_tab=m1, + docclass_inv_tab = n1, + docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, + {docobj_tab=d2,docclass_tab = c2, + ISA_transformer_tab = e2, monitor_tab=m2, + docclass_inv_tab = n2, + docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = + {docobj_tab=merge_docobj_tab (d1,d2), + docclass_tab = merge_docclass_tab (c1,c2), + (* + The following merge is ultra-critical: the transformer tabs were + just extended by letting *the first* entry with the same long-name win. + Since the range is a (call-back) function, a comparison on its content + is impossible and some choice has to be made... Alternative: Symtab.join ? + *) + ISA_transformer_tab = Symtab.merge (fn (_ , _) => true)(e1,e2), + monitor_tab = override(m1,m2), + (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) + docclass_inv_tab = override(n1,n2), + (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) + docclass_eager_inv_tab = override(en1,en2), + (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) + docclass_lazy_inv_tab = override(ln1,ln2) + (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) + } +); + + +val get_data = Data.get o Context.Proof; +val map_data = Data.map; +val get_data_global = Data.get o Context.Theory; +val map_data_global = Context.theory_map o map_data; + + +fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, + monitor_tab,docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab = f docobj_tab, docclass_tab=docclass_tab, + ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; +fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; +fun upd_ISA_transformers f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; +fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab = docobj_tab,docclass_tab = docclass_tab, + ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; +fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab = docobj_tab,docclass_tab = docclass_tab, + ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + docclass_inv_tab = f docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; + +fun upd_docclass_eager_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab = docobj_tab,docclass_tab = docclass_tab, + ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=f docclass_eager_inv_tab, + docclass_lazy_inv_tab=docclass_lazy_inv_tab}; + +fun upd_docclass_lazy_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, + monitor_tab, docclass_inv_tab, + docclass_eager_inv_tab, docclass_lazy_inv_tab} = + {docobj_tab = docobj_tab,docclass_tab = docclass_tab, + ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + docclass_inv_tab=docclass_inv_tab, + docclass_eager_inv_tab=docclass_eager_inv_tab, + docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; + +fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids +fun get_rejected_cids ({rejected_cids, ... } : open_monitor_info) = rejected_cids +fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info) +fun get_automatas ({automatas, ... } : open_monitor_info) = automatas + + +(* doc-class-name management: We still use the record-package for internally + representing doc-classes. The main motivation is that "links" to entities are + types over doc-classes, *types* in the Isabelle sense, enriched by additional data. + This has the advantage that the type-inference can be abused to infer long-names + for doc-class-names. Note, however, that doc-classes are currently implemented + by non-polymorphic records only; this means that the extensible "_ext" versions + of type names must be reduced to qualifier names only. The used Syntax.parse_typ + handling the identification does that already. + However, we use Syntax.read_typ in order to allow type-synonyms which requires + an appropriate adaption in read_cid.*) + +fun is_subclass (ctxt) s t = is_subclass0(#docclass_tab(get_data ctxt)) s t +fun is_subclass_global thy s t = is_subclass0(#docclass_tab(get_data_global thy)) s t + + +fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s + |typ_to_cid (Type(_,[T])) = typ_to_cid T + |typ_to_cid _ = error("type is not an ontological type.") + + +fun parse_cid ctxt cid = +(* parses a type lexically/syntactically, checks absence of type vars *) + (case Syntax.parse_typ ctxt cid of + Type(tyname, []) => tyname + | _ => error "illegal type-format for doc-class-name.") + handle ERROR _ => "" (* ignore error *) + + +fun read_cid ctxt "text" = default_cid (* text = default_cid *) + | read_cid ctxt cid = +(* parses a type syntactically, type-identification, checking as class id *) + (case Syntax.read_typ ctxt cid of + ty as Type(tyname, _) => let val res = typ_to_cid ty + val t = #docclass_tab(get_data ctxt) + in if Symtab.defined t res + then res + else error("type identifier not a class id:"^res) + end + | _ => error "illegal type-format for doc-class-name.") + handle ERROR _ => error("type identifier not a class id:"^cid) + +fun parse_cid_global thy cid = parse_cid (Proof_Context.init_global thy) cid +fun read_cid_global thy cid = read_cid (Proof_Context.init_global thy) cid + + +fun is_defined_cid_global cid thy = +(* works with short and long names *) + let val t = #docclass_tab(get_data_global thy) + in cid=default_cid orelse + Symtab.defined t (parse_cid_global thy cid) + end + +fun is_defined_cid_global' cid_long thy = +(* works with long names only *) + let val t = #docclass_tab(get_data_global thy) + in cid_long=default_cid orelse Symtab.defined t cid_long end + + +fun is_defined_cid_local cid ctxt = +(* works with short and long names *) + let val t = #docclass_tab(get_data ctxt) + in cid=default_cid orelse + Symtab.defined t (parse_cid ctxt cid) + end + +fun is_defined_cid_local' cid_long ctxt = +(* works with long names only *) + let val t = #docclass_tab(get_data ctxt) + in cid_long=default_cid orelse Symtab.defined t cid_long end + + +fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) + in Symtab.defined tab oid end + +fun is_declared_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) + in Symtab.defined tab oid end + +fun is_defined_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) + in case Symtab.lookup tab oid of + NONE => false + |SOME(NONE) => false + |SOME _ => true + end + +fun is_defined_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) + in case Symtab.lookup tab oid of + NONE => false + |SOME(NONE) => false + |SOME _ => true + end + +fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) + (* takes class synonyms into account *) + val long_name = read_cid_global thy cid + in case Symtab.lookup tab long_name of + NONE => error("Undefined class id: " ^ cid) + | SOME ({virtual=virtual, ...}) => #virtual virtual + end + +fun declare_object_global oid thy = + let fun decl {tab=t,maxano=x} = {tab=Symtab.update_new(oid,NONE)t, maxano=x} + in (map_data_global (upd_docobj_tab(decl)) (thy) + handle Symtab.DUP _ => error("multiple declaration of document reference")) + end + +fun declare_object_local oid ctxt = + let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, maxano=maxano} + in (map_data(upd_docobj_tab decl)(ctxt) + handle Symtab.DUP _ => error("multiple declaration of document reference")) + end + + +fun update_class_invariant cid_long f thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, + (fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt )))))) + thy + end + +fun update_class_eager_invariant cid_long f thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + in map_data_global (upd_docclass_eager_inv_tab (Symtab.update (cid_long, + (fn ctxt => ((writeln("Eager Invariant check of: " ^cid_long); f ctxt )))))) + thy + end + +fun update_class_lazy_invariant cid_long f thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + in map_data_global (upd_docclass_lazy_inv_tab (Symtab.update (cid_long, + (fn ctxt => ((writeln("Lazy Invariant check of: " ^cid_long); f ctxt )))))) + thy + end + +fun get_class_invariant cid_long thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + val {docclass_inv_tab, ...} = get_data_global thy + in case Symtab.lookup docclass_inv_tab cid_long of + NONE => K(K(K true)) + | SOME f => f + end + +fun get_class_eager_invariant cid_long thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + val {docclass_eager_inv_tab, ...} = get_data_global thy + in case Symtab.lookup docclass_eager_inv_tab cid_long of + NONE => K(K(K true)) + | SOME f => f + end + +fun get_class_lazy_invariant cid_long thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + val {docclass_lazy_inv_tab, ...} = get_data_global thy + in case Symtab.lookup docclass_lazy_inv_tab cid_long of + NONE => K(K(K true)) + | SOME f => f + end + +val SPY = Unsynchronized.ref(Bound 0) + +fun check_regexps term = + let val _ = case fold_aterms Term.add_free_names term [] of + n::_ => error("No free variables allowed in monitor regexp:" ^ n) + | _ => () + val _ = case fold_aterms Term.add_var_names term [] of + (n,_)::_ => error("No schematic variables allowed in monitor regexp:" ^ n) + | _ => () + (* Missing: Checks on constants such as undefined, ... *) + in term end + +fun check_reject_atom cid_long term = + let val _ = case fold_aterms Term.add_free_names term [] of + n::_ => error("No free variables allowed in monitor regexp:" ^ n) + | _ => () + val _ = case fold_aterms Term.add_var_names term [] of + (n,_)::_ => error("No schematic variables allowed in monitor regexp:" ^ n) + | _ => () + (* Missing: Checks on constants such as undefined, ... *) + in term end + + +fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms invs virtual thy = +(* This operation is executed in a context where the record has already been defined, but + its conversion into a class is not yet done. *) + let val nn = Context.theory_name thy (* in case that we need the thy-name to identify + the space where it is ... *) + val cid = (Binding.name_of binding) + val pos = (Binding.pos_of binding) + + val _ = if is_defined_cid_global cid thy + then error("redefinition of document class:"^cid ) + else () + val parent' = map_option (map_snd (read_cid_global thy)) parent + (* weird construction. Necessary since parse produces at rare cases + string representations that do no longer have the lexis of a type name. *) + val cid_long = parse_cid_global thy cid + val cid_long' = parse_cid_global thy cid_long + val _ = if cid_long' <> "" then () + else error("Could not construct type from doc_class (lexical problem?)") + + val id = serial (); + val _ = Position.report pos (docclass_markup true cid id pos); + + val rejectS = map (Syntax.read_term_global thy) reject_Atoms; + val _ = map (check_reject_atom cid_long) rejectS; + val reg_exps = map (Syntax.read_term_global thy) rexp; + val _ = map check_regexps reg_exps + val _ = if not(null rejectS) andalso (null reg_exps) + then error ("reject clause requires accept clause ! " ) else (); + val _ = if has_duplicates (op =) (map (fst o fst) invs) + then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) + else () + val invs' = map (map_snd(Syntax.read_term_global thy)) invs + val info = {params=params', + name = binding, + virtual = virtual, + thy_name = nn, + id = id, (* for pide --- really fresh or better reconstruct + from prior record definition ? For the moment: own + generation of serials ... *) + inherits_from = parent', + attribute_decl = fields , + rejectS = rejectS, + rex = reg_exps, + invs = invs'} + + in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy) + end + + +fun define_object_global (oid, bbb) thy = + let val nn = Context.theory_name thy (* in case that we need the thy-name to identify + the space where it is ... *) + in if is_defined_oid_global oid thy + then error("multiple definition of document reference") + else map_data_global (upd_docobj_tab(fn {tab=t,maxano=x} => + {tab=Symtab.update(oid,SOME bbb) t, + maxano=x})) + (thy) + end + +fun define_object_local (oid, bbb) ctxt = + map_data (upd_docobj_tab(fn{tab,maxano}=>{tab=Symtab.update(oid,SOME bbb)tab,maxano=maxano})) ctxt + + +(* declares an anonyme label of a given type and generates a unique reference ... *) +fun declare_anoobject_global thy cid = + let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) + val _ = writeln("Anonymous reference declared: " ^ str) + in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end + in map_data_global (upd_docobj_tab declare) (thy) + end + +fun declare_anoobject_local ctxt cid = + let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) + val _ = writeln("Anonymous reference declared: " ^str) + in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end + in map_data (upd_docobj_tab declare) (ctxt) + end + + +fun get_object_global_opt oid thy = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid + +fun get_object_global oid thy = case get_object_global_opt oid thy of + NONE => error("undefined reference: "^oid) + |SOME(bbb) => bbb + +fun get_object_local_opt oid ctxt = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid + +fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of + NONE => error("undefined reference: "^oid) + |SOME(bbb) => bbb + +fun get_doc_class_global cid thy = + if cid = default_cid then error("default class access") (* TODO *) + else let val t = #docclass_tab(get_data_global thy) + in (Symtab.lookup t cid) end + + +fun get_doc_class_local cid ctxt = + if cid = default_cid then error("default class access") (* TODO *) + else let val t = #docclass_tab(get_data ctxt) + in (Symtab.lookup t cid) end + + +fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) + in cid=default_cid orelse + Symtab.defined t (parse_cid ctxt cid) + end + +fun get_attributes_local cid ctxt = + if cid = default_cid then [] + else let val t = #docclass_tab(get_data ctxt) + val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) + in case Symtab.lookup t cid_long of + NONE => error("undefined class id for attributes: "^cid) + | (SOME ({inherits_from=NONE, + attribute_decl = X, ...})) => [(cid_long,X)] + | (SOME ({inherits_from=SOME(_,father), + attribute_decl = X, ...})) => + get_attributes_local father ctxt @ [(cid_long,X)] + end + +fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy) + + +fun get_all_attributes_local cid ctxt = + (tag_attr, get_attributes_local cid ctxt) + +fun get_all_attributes cid thy = get_all_attributes_local cid (Proof_Context.init_global thy) + + +type attributes_info = { def_occurrence : string, + def_pos : Position.T, + long_name : string, + typ : typ + } + +fun get_attribute_info_local (*long*)cid attr ctxt : attributes_info option= + let val hierarchy = get_attributes_local cid ctxt (* search in order *) + fun found (s,L) = case find_first (fn (bind,_,_) => Binding.name_of bind = attr) L of + NONE => NONE + | SOME X => SOME(s,X) + in case get_first found hierarchy of + NONE => NONE + | SOME (cid',(bind, ty,_)) => SOME({def_occurrence = cid, + def_pos = Binding.pos_of bind, + long_name = cid'^"."^(Binding.name_of bind), + typ = ty}) + end + +fun get_attribute_info (*long*)cid attr thy = + get_attribute_info_local cid attr (Proof_Context.init_global thy) + +fun get_attribute_defaults (* long*)cid thy = + let val attrS = flat(map snd (get_attributes cid thy)) + fun trans (_,_,NONE) = NONE + |trans (na,ty,SOME def) =SOME(na,ty, def) + in map_filter trans attrS end + +fun get_value_global oid thy = case get_object_global oid thy of + SOME{value=term,...} => SOME term + | NONE => NONE + +fun get_value_local oid ctxt = case get_object_local oid ctxt of + SOME{value=term,...} => SOME term + | NONE => NONE + +(* missing : setting terms to ground (no type-schema vars, no schema vars. )*) +fun update_value_global oid upd_input_term upd_value thy = + case get_object_global oid thy of + SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} => + let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, + 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) + + +val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) + +val doc_class_prefix = ISA_prefix ^ "doc_class_" + +fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s) + +fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE) + +fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE) + +fun is_class_ISA thy s = let val bname = Long_Name.base_name s + val qual = Long_Name.qualifier s + in + if String.isPrefix doc_class_prefix bname then + let + val class_name = + Long_Name.qualify qual (get_class_name_without_prefix bname) + in + is_defined_cid_global (class_name) thy end + else false end + +fun get_isa_global isa thy = + case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of + NONE => error("undefined inner syntax antiquotation: "^isa) + | SOME(bbb) => bbb + + +fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of + NONE => error("undefined inner syntax antiquotation: "^isa) + |SOME(bbb) => bbb + +fun update_isa map_data_fun (isa, trans) ctxt = + let + val bname = Long_Name.base_name isa; + val qual = Long_Name.qualifier isa; + val long_name = Long_Name.qualify qual (ISA_prefix ^ bname); + in map_data_fun (upd_ISA_transformers(Symtab.update(long_name, trans))) ctxt end + + fun update_isa_local (isa, trans) ctxt = update_isa map_data (isa, trans) ctxt + +fun update_isa_global (isa, trans) thy = update_isa map_data_global (isa, trans) thy + +fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy = + (* pre: term should be fully typed in order to allow type-related term-transformations *) + let val tab = #ISA_transformer_tab(get_data_global thy) + fun T(Const(s,ty) $ t) = if is_ISA s + then case Symtab.lookup tab s of + NONE => error("undefined inner syntax antiquotation: "^s) + | SOME({check=check, elaborate=elaborate}) => + case check thy (t,ty,pos) s of + NONE => Const(s,ty) $ t + (* checking isa, may raise error though. *) + | SOME t => if mk_elaboration + then elaborate thy s ty (SOME t) pos + else Const(s,ty) $ t + (* transforming isa *) + else (Const(s,ty) $ (T t)) + |T(t1 $ t2) = T(t1) $ T(t2) + |T(Const(s,ty)) = if is_ISA s + then case Symtab.lookup tab s of + NONE => error("undefined inner syntax antiquotation: "^s) + | SOME({elaborate=elaborate, ...}) => + if mk_elaboration + then elaborate thy s ty NONE pos + else Const(s, ty) + (* transforming isa *) + else Const(s, ty) + |T(Abs(s,ty,t)) = Abs(s,ty,T t) + |T t = t + in T term end + +fun elaborate_term ctxt term = transduce_term_global {mk_elaboration=true} + (term , Position.none) + (Proof_Context.theory_of ctxt) + +fun check_term ctxt term = transduce_term_global {mk_elaboration=false} + (term , Position.none) + (Proof_Context.theory_of ctxt) + +fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt) + in writeln (String.concatWith "," (Symtab.keys tab)) end + + +fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) + in writeln (String.concatWith "," (Symtab.keys tab)) 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) + fun is_class_son X (n, dc:docclass_struct) = (X = #inherits_from dc) + fun tree lev ([]:(string * docclass_struct)list) = "" + |tree lev ((n,R)::S) = (if P(lev,n) + then "."^Int.toString lev^" "^(T n)^"{...}.\n" + ^ (tree(lev + 1)(filter(is_class_son(SOME([],n)))class_tab)) + else "."^Int.toString lev^" ... \n") + ^ (tree lev S) + val roots = filter(is_class_son NONE) class_tab + in ".0 .\n" ^ tree 1 roots end + + +val (strict_monitor_checking, strict_monitor_checking_setup) + = Attrib.config_bool \<^binding>\strict_monitor_checking\ (K false); + +val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_checking\ (K false); + +val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_strict_checking\ (K false); + +val (invariants_checking, invariants_checking_setup) + = Attrib.config_bool \<^binding>\invariants_checking\ (K true); + +val (invariants_strict_checking, invariants_strict_checking_setup) + = Attrib.config_bool \<^binding>\invariants_strict_checking\ (K false); + +val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) + = Attrib.config_bool \<^binding>\invariants_checking_with_tactics\ (K false); + + +end (* struct *) + +\ + +setup\DOF_core.strict_monitor_checking_setup + #> DOF_core.free_class_in_monitor_checking_setup + #> DOF_core.free_class_in_monitor_strict_checking_setup + #> DOF_core.invariants_checking_setup + #> DOF_core.invariants_strict_checking_setup + #> DOF_core.invariants_checking_with_tactics_setup\ + +end \ No newline at end of file diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 755d4478..f320906f 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -30,8 +30,7 @@ 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 *) - "Metalogic_ProofChecker.ProofTerm" + "meta_interpretation/Deep_Interpretation" keywords "+=" ":=" "accepts" "rejects" "invariant" @@ -57,799 +56,6 @@ begin text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ -section\Primitive Markup Generators\ -ML\ - -val docrefN = "docref"; -val docclassN = "doc_class"; - -(** name components **) - -val defN = "def" -val def_suffixN = "_" ^ defN -val defsN = defN ^ "s" -val instances_of_suffixN = "_instances" -val invariant_suffixN = "_inv" -val invariantN = "\" -val makeN = "make" -val schemeN = "_scheme" - -(* derived from: theory_markup *) -fun docref_markup_gen refN def name id pos = - if id = 0 then Markup.empty - else Position.make_entity_markup {def = def} id refN (name, pos); (* or better store the thy-name as property ? ? ? *) - -val docref_markup = docref_markup_gen docrefN - -val docclass_markup = docref_markup_gen docclassN - -\ - -section\ Utilities\ - -ML\ -fun spy x y = (writeln (x ^ y); y) - -fun markup2string x = XML.content_of (YXML.parse_body x) - -(* a hacky, but save encoding of unicode comming from the interface to the string format - that can be parsed by the inner-syntax string parser ''dfdf''. *) -fun bstring_to_holstring ctxt x (* (x:bstring) *) : string = - let val term = Syntax.parse_term ctxt (markup2string x) - fun hpp x = if x = #"\\" then "@" else - if x = #"@" then "@@" else String.implode [x] - in term |> Sledgehammer_Util.hackish_string_of_term ctxt - |> map hpp o String.explode |> String.concat - end; - - -fun chopper p (x:string) = - let fun hss buff [] = rev buff - |hss buff (S as a::R) = if p a then let val (front,rest) = chop_prefix p S - in hss (String.implode front :: buff) rest end - else let val (front,rest) = chop_prefix (not o p) S - in hss (String.implode front ::buff) rest end - in hss [] (String.explode x) end; - - -fun holstring_to_bstring ctxt (x:string) : bstring = - let fun collapse "" = "" - |collapse S = if String.sub(S,0) = #"@" - then let val n = String.size S - val front = replicate (n div 2) #"@" - val back = if (n mod 2)=1 then [#"\\"] else [] - in String.implode (front @ back) end - else S; - val t = String.concat (map collapse (chopper (fn x => x = #"@") x)); - in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end; - -fun map_option _ NONE = NONE - |map_option f (SOME x) = SOME (f x); - -fun map_optional _ s NONE = s - |map_optional f _ (SOME x) = f x; - -fun map_fst f (x,y) = (f x,y) -fun map_snd f (x,y) = (x,f y) - -fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y) - -\ - -section\ A HomeGrown Document Type Management (the ''Model'') \ - -ML\ -structure DOF_core = - -struct - type virtual = {virtual : bool} - type docclass_struct = {params : (string * sort) list, (*currently not used *) - name : binding, - virtual : virtual, - thy_name : string, id : serial, (* for pide *) - inherits_from : (typ list * string) option, (* imports *) - attribute_decl : (binding*typ*term option)list, (* class local *) - rejectS : term list, - rex : term list, - invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) - - - type docclass_tab = docclass_struct Symtab.table - - val initial_docclass_tab = Symtab.empty:docclass_tab - - fun merge_docclass_tab (otab,otab') = Symtab.merge (op =) (otab,otab') - - val tag_attr = (\<^binding>\tag_attribute\, \<^Type>\int\, Mixfix.NoSyn) - (* Attribute hidden to the user and used internally by isabelle_DOF. - For example, this allows to add a specific id to a class - to be able to reference the class internally. - *) - - val default_cid = "text" (* the top (default) document class: everything is a text.*) - - fun is_subclass0 (tab:docclass_tab) s t = - let val _ = case Symtab.lookup tab t of - NONE => if t <> default_cid - then error ("document superclass not defined: "^t) - else default_cid - | SOME _ => "" - fun father_is_sub s = case Symtab.lookup tab s of - NONE => error ("document subclass not defined: "^s) - | SOME ({inherits_from=NONE, ...}) => s = t - | SOME ({inherits_from=SOME (_,s'), ...}) => - s' = t orelse father_is_sub s' - in s = t orelse - (t = default_cid andalso Symtab.defined tab s ) orelse - (s <> default_cid andalso father_is_sub s) - end - - type docobj = {pos : Position.T, - thy_name : string, - input_term : term, - value : term, - inline : bool, - id : serial, - cid : string, - vcid : string option} - - type docobj_tab ={tab : (docobj option) Symtab.table, - maxano : int - } - - val initial_docobj_tab:docobj_tab = {tab = Symtab.empty, maxano = 0} - - fun merge_docobj_tab ({tab=otab,maxano=m}, {tab=otab',maxano=m'}) = - (let fun X(NONE,NONE) = false - |X(SOME _, NONE) = false - |X(NONE, SOME _) = false - |X(SOME b, SOME b') = true (* b = b' *) - in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')} - end) - type ISA_transformers = {check : - (theory -> term * typ * Position.T -> string -> term option), - elaborate : (theory -> string -> typ -> term option -> Position.T -> term) - } - - type ISA_transformer_tab = ISA_transformers Symtab.table - val initial_ISA_tab:ISA_transformer_tab = Symtab.empty - - type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty - - type docclass_eager_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_eager_inv_tab : docclass_eager_inv_tab = Symtab.empty - - type docclass_lazy_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_lazy_inv_tab : docclass_lazy_inv_tab = Symtab.empty - - type open_monitor_info = {accepted_cids : string list, - rejected_cids : string list, - automatas : RegExpInterface.automaton list - } - - type monitor_tab = open_monitor_info Symtab.table - val initial_monitor_tab:monitor_tab = Symtab.empty - - fun override(t1,t2) = fold(Symtab.update)(Symtab.dest t2)(t1) - -(* registrating data of the Isa_DOF component *) -structure Data = Generic_Data -( - type T = {docobj_tab : docobj_tab, - docclass_tab : docclass_tab, - ISA_transformer_tab : ISA_transformer_tab, - monitor_tab : monitor_tab, - docclass_inv_tab : docclass_inv_tab, - docclass_eager_inv_tab : docclass_eager_inv_tab, - docclass_lazy_inv_tab : docclass_lazy_inv_tab} - val empty = {docobj_tab = initial_docobj_tab, - docclass_tab = initial_docclass_tab, - ISA_transformer_tab = initial_ISA_tab, - monitor_tab = initial_monitor_tab, - docclass_inv_tab = initial_docclass_inv_tab, - docclass_eager_inv_tab = initial_docclass_eager_inv_tab, - docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab - } - fun merge( {docobj_tab=d1,docclass_tab = c1, - ISA_transformer_tab = e1, monitor_tab=m1, - docclass_inv_tab = n1, - docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, - {docobj_tab=d2,docclass_tab = c2, - ISA_transformer_tab = e2, monitor_tab=m2, - docclass_inv_tab = n2, - docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = - {docobj_tab=merge_docobj_tab (d1,d2), - docclass_tab = merge_docclass_tab (c1,c2), - (* - The following merge is ultra-critical: the transformer tabs were - just extended by letting *the first* entry with the same long-name win. - Since the range is a (call-back) function, a comparison on its content - is impossible and some choice has to be made... Alternative: Symtab.join ? - *) - ISA_transformer_tab = Symtab.merge (fn (_ , _) => true)(e1,e2), - monitor_tab = override(m1,m2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_inv_tab = override(n1,n2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_eager_inv_tab = override(en1,en2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_lazy_inv_tab = override(ln1,ln2) - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - } -); - - -val get_data = Data.get o Context.Proof; -val map_data = Data.map; -val get_data_global = Data.get o Context.Theory; -val map_data_global = Context.theory_map o map_data; - - -fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, - monitor_tab,docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab = f docobj_tab, docclass_tab=docclass_tab, - ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; -fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; -fun upd_ISA_transformers f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; -fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab = docobj_tab,docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; -fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab = docobj_tab,docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, - docclass_inv_tab = f docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; - -fun upd_docclass_eager_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab = docobj_tab,docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=f docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; - -fun upd_docclass_lazy_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docobj_tab = docobj_tab,docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; - -fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids -fun get_rejected_cids ({rejected_cids, ... } : open_monitor_info) = rejected_cids -fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info) -fun get_automatas ({automatas, ... } : open_monitor_info) = automatas - - -(* doc-class-name management: We still use the record-package for internally - representing doc-classes. The main motivation is that "links" to entities are - types over doc-classes, *types* in the Isabelle sense, enriched by additional data. - This has the advantage that the type-inference can be abused to infer long-names - for doc-class-names. Note, however, that doc-classes are currently implemented - by non-polymorphic records only; this means that the extensible "_ext" versions - of type names must be reduced to qualifier names only. The used Syntax.parse_typ - handling the identification does that already. - However, we use Syntax.read_typ in order to allow type-synonyms which requires - an appropriate adaption in read_cid.*) - -fun is_subclass (ctxt) s t = is_subclass0(#docclass_tab(get_data ctxt)) s t -fun is_subclass_global thy s t = is_subclass0(#docclass_tab(get_data_global thy)) s t - - -fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s - |typ_to_cid (Type(_,[T])) = typ_to_cid T - |typ_to_cid _ = error("type is not an ontological type.") - - -fun parse_cid ctxt cid = -(* parses a type lexically/syntactically, checks absence of type vars *) - (case Syntax.parse_typ ctxt cid of - Type(tyname, []) => tyname - | _ => error "illegal type-format for doc-class-name.") - handle ERROR _ => "" (* ignore error *) - - -fun read_cid ctxt "text" = default_cid (* text = default_cid *) - | read_cid ctxt cid = -(* parses a type syntactically, type-identification, checking as class id *) - (case Syntax.read_typ ctxt cid of - ty as Type(tyname, _) => let val res = typ_to_cid ty - val t = #docclass_tab(get_data ctxt) - in if Symtab.defined t res - then res - else error("type identifier not a class id:"^res) - end - | _ => error "illegal type-format for doc-class-name.") - handle ERROR _ => error("type identifier not a class id:"^cid) - -fun parse_cid_global thy cid = parse_cid (Proof_Context.init_global thy) cid -fun read_cid_global thy cid = read_cid (Proof_Context.init_global thy) cid - - -fun is_defined_cid_global cid thy = -(* works with short and long names *) - let val t = #docclass_tab(get_data_global thy) - in cid=default_cid orelse - Symtab.defined t (parse_cid_global thy cid) - end - -fun is_defined_cid_global' cid_long thy = -(* works with long names only *) - let val t = #docclass_tab(get_data_global thy) - in cid_long=default_cid orelse Symtab.defined t cid_long end - - -fun is_defined_cid_local cid ctxt = -(* works with short and long names *) - let val t = #docclass_tab(get_data ctxt) - in cid=default_cid orelse - Symtab.defined t (parse_cid ctxt cid) - end - -fun is_defined_cid_local' cid_long ctxt = -(* works with long names only *) - let val t = #docclass_tab(get_data ctxt) - in cid_long=default_cid orelse Symtab.defined t cid_long end - - -fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) - in Symtab.defined tab oid end - -fun is_declared_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) - in Symtab.defined tab oid end - -fun is_defined_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) - in case Symtab.lookup tab oid of - NONE => false - |SOME(NONE) => false - |SOME _ => true - end - -fun is_defined_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) - in case Symtab.lookup tab oid of - NONE => false - |SOME(NONE) => false - |SOME _ => true - end - -fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) - (* takes class synonyms into account *) - val long_name = read_cid_global thy cid - in case Symtab.lookup tab long_name of - NONE => error("Undefined class id: " ^ cid) - | SOME ({virtual=virtual, ...}) => #virtual virtual - end - -fun declare_object_global oid thy = - let fun decl {tab=t,maxano=x} = {tab=Symtab.update_new(oid,NONE)t, maxano=x} - in (map_data_global (upd_docobj_tab(decl)) (thy) - handle Symtab.DUP _ => error("multiple declaration of document reference")) - end - -fun declare_object_local oid ctxt = - let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, maxano=maxano} - in (map_data(upd_docobj_tab decl)(ctxt) - handle Symtab.DUP _ => error("multiple declaration of document reference")) - end - - -fun update_class_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_eager_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_eager_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Eager Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_lazy_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_lazy_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Lazy Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun get_class_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_eager_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_eager_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_eager_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_lazy_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_lazy_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_lazy_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -val SPY = Unsynchronized.ref(Bound 0) - -fun check_regexps term = - let val _ = case fold_aterms Term.add_free_names term [] of - n::_ => error("No free variables allowed in monitor regexp:" ^ n) - | _ => () - val _ = case fold_aterms Term.add_var_names term [] of - (n,_)::_ => error("No schematic variables allowed in monitor regexp:" ^ n) - | _ => () - (* Missing: Checks on constants such as undefined, ... *) - in term end - -fun check_reject_atom cid_long term = - let val _ = case fold_aterms Term.add_free_names term [] of - n::_ => error("No free variables allowed in monitor regexp:" ^ n) - | _ => () - val _ = case fold_aterms Term.add_var_names term [] of - (n,_)::_ => error("No schematic variables allowed in monitor regexp:" ^ n) - | _ => () - (* Missing: Checks on constants such as undefined, ... *) - in term end - - -fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms invs virtual thy = -(* This operation is executed in a context where the record has already been defined, but - its conversion into a class is not yet done. *) - let val nn = Context.theory_name thy (* in case that we need the thy-name to identify - the space where it is ... *) - val cid = (Binding.name_of binding) - val pos = (Binding.pos_of binding) - - val _ = if is_defined_cid_global cid thy - then error("redefinition of document class:"^cid ) - else () - val parent' = map_option (map_snd (read_cid_global thy)) parent - (* weird construction. Necessary since parse produces at rare cases - string representations that do no longer have the lexis of a type name. *) - val cid_long = parse_cid_global thy cid - val cid_long' = parse_cid_global thy cid_long - val _ = if cid_long' <> "" then () - else error("Could not construct type from doc_class (lexical problem?)") - - val id = serial (); - val _ = Position.report pos (docclass_markup true cid id pos); - - val rejectS = map (Syntax.read_term_global thy) reject_Atoms; - val _ = map (check_reject_atom cid_long) rejectS; - val reg_exps = map (Syntax.read_term_global thy) rexp; - val _ = map check_regexps reg_exps - val _ = if not(null rejectS) andalso (null reg_exps) - then error ("reject clause requires accept clause ! " ) else (); - val _ = if has_duplicates (op =) (map (fst o fst) invs) - then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) - else () - val invs' = map (map_snd(Syntax.read_term_global thy)) invs - val info = {params=params', - name = binding, - virtual = virtual, - thy_name = nn, - id = id, (* for pide --- really fresh or better reconstruct - from prior record definition ? For the moment: own - generation of serials ... *) - inherits_from = parent', - attribute_decl = fields , - rejectS = rejectS, - rex = reg_exps, - invs = invs'} - - in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy) - end - - -fun define_object_global (oid, bbb) thy = - let val nn = Context.theory_name thy (* in case that we need the thy-name to identify - the space where it is ... *) - in if is_defined_oid_global oid thy - then error("multiple definition of document reference") - else map_data_global (upd_docobj_tab(fn {tab=t,maxano=x} => - {tab=Symtab.update(oid,SOME bbb) t, - maxano=x})) - (thy) - end - -fun define_object_local (oid, bbb) ctxt = - map_data (upd_docobj_tab(fn{tab,maxano}=>{tab=Symtab.update(oid,SOME bbb)tab,maxano=maxano})) ctxt - - -(* declares an anonyme label of a given type and generates a unique reference ... *) -fun declare_anoobject_global thy cid = - let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous reference declared: " ^ str) - in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end - in map_data_global (upd_docobj_tab declare) (thy) - end - -fun declare_anoobject_local ctxt cid = - let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous reference declared: " ^str) - in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end - in map_data (upd_docobj_tab declare) (ctxt) - end - - -fun get_object_global_opt oid thy = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid - -fun get_object_global oid thy = case get_object_global_opt oid thy of - NONE => error("undefined reference: "^oid) - |SOME(bbb) => bbb - -fun get_object_local_opt oid ctxt = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid - -fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of - NONE => error("undefined reference: "^oid) - |SOME(bbb) => bbb - -fun get_doc_class_global cid thy = - if cid = default_cid then error("default class access") (* TODO *) - else let val t = #docclass_tab(get_data_global thy) - in (Symtab.lookup t cid) end - - -fun get_doc_class_local cid ctxt = - if cid = default_cid then error("default class access") (* TODO *) - else let val t = #docclass_tab(get_data ctxt) - in (Symtab.lookup t cid) end - - -fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) - in cid=default_cid orelse - Symtab.defined t (parse_cid ctxt cid) - end - -fun get_attributes_local cid ctxt = - if cid = default_cid then [] - else let val t = #docclass_tab(get_data ctxt) - val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) - in case Symtab.lookup t cid_long of - NONE => error("undefined class id for attributes: "^cid) - | (SOME ({inherits_from=NONE, - attribute_decl = X, ...})) => [(cid_long,X)] - | (SOME ({inherits_from=SOME(_,father), - attribute_decl = X, ...})) => - get_attributes_local father ctxt @ [(cid_long,X)] - end - -fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy) - - -fun get_all_attributes_local cid ctxt = - (tag_attr, get_attributes_local cid ctxt) - -fun get_all_attributes cid thy = get_all_attributes_local cid (Proof_Context.init_global thy) - - -type attributes_info = { def_occurrence : string, - def_pos : Position.T, - long_name : string, - typ : typ - } - -fun get_attribute_info_local (*long*)cid attr ctxt : attributes_info option= - let val hierarchy = get_attributes_local cid ctxt (* search in order *) - fun found (s,L) = case find_first (fn (bind,_,_) => Binding.name_of bind = attr) L of - NONE => NONE - | SOME X => SOME(s,X) - in case get_first found hierarchy of - NONE => NONE - | SOME (cid',(bind, ty,_)) => SOME({def_occurrence = cid, - def_pos = Binding.pos_of bind, - long_name = cid'^"."^(Binding.name_of bind), - typ = ty}) - end - -fun get_attribute_info (*long*)cid attr thy = - get_attribute_info_local cid attr (Proof_Context.init_global thy) - -fun get_attribute_defaults (* long*)cid thy = - let val attrS = flat(map snd (get_attributes cid thy)) - fun trans (_,_,NONE) = NONE - |trans (na,ty,SOME def) =SOME(na,ty, def) - in map_filter trans attrS end - -fun get_value_global oid thy = case get_object_global oid thy of - SOME{value=term,...} => SOME term - | NONE => NONE - -fun get_value_local oid ctxt = case get_object_local oid ctxt of - SOME{value=term,...} => SOME term - | NONE => NONE - -(* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun update_value_global oid upd_input_term upd_value thy = - case get_object_global oid thy of - SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} => - let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - 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) - - -val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) - -val doc_class_prefix = ISA_prefix ^ "doc_class_" - -fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s) - -fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE) - -fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE) - -fun is_class_ISA thy s = let val bname = Long_Name.base_name s - val qual = Long_Name.qualifier s - in - if String.isPrefix doc_class_prefix bname then - let - val class_name = - Long_Name.qualify qual (get_class_name_without_prefix bname) - in - is_defined_cid_global (class_name) thy end - else false end - -fun get_isa_global isa thy = - case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of - NONE => error("undefined inner syntax antiquotation: "^isa) - | SOME(bbb) => bbb - - -fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of - NONE => error("undefined inner syntax antiquotation: "^isa) - |SOME(bbb) => bbb - -fun update_isa map_data_fun (isa, trans) ctxt = - let - val bname = Long_Name.base_name isa; - val qual = Long_Name.qualifier isa; - val long_name = Long_Name.qualify qual (ISA_prefix ^ bname); - in map_data_fun (upd_ISA_transformers(Symtab.update(long_name, trans))) ctxt end - - fun update_isa_local (isa, trans) ctxt = update_isa map_data (isa, trans) ctxt - -fun update_isa_global (isa, trans) thy = update_isa map_data_global (isa, trans) thy - -fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy = - (* pre: term should be fully typed in order to allow type-related term-transformations *) - let val tab = #ISA_transformer_tab(get_data_global thy) - fun T(Const(s,ty) $ t) = if is_ISA s - then case Symtab.lookup tab s of - NONE => error("undefined inner syntax antiquotation: "^s) - | SOME({check=check, elaborate=elaborate}) => - case check thy (t,ty,pos) s of - NONE => Const(s,ty) $ t - (* checking isa, may raise error though. *) - | SOME t => if mk_elaboration - then elaborate thy s ty (SOME t) pos - else Const(s,ty) $ t - (* transforming isa *) - else (Const(s,ty) $ (T t)) - |T(t1 $ t2) = T(t1) $ T(t2) - |T(Const(s,ty)) = if is_ISA s - then case Symtab.lookup tab s of - NONE => error("undefined inner syntax antiquotation: "^s) - | SOME({elaborate=elaborate, ...}) => - if mk_elaboration - then elaborate thy s ty NONE pos - else Const(s, ty) - (* transforming isa *) - else Const(s, ty) - |T(Abs(s,ty,t)) = Abs(s,ty,T t) - |T t = t - in T term end - -fun elaborate_term ctxt term = transduce_term_global {mk_elaboration=true} - (term , Position.none) - (Proof_Context.theory_of ctxt) - -fun check_term ctxt term = transduce_term_global {mk_elaboration=false} - (term , Position.none) - (Proof_Context.theory_of ctxt) - -fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt) - in writeln (String.concatWith "," (Symtab.keys tab)) end - - -fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) - in writeln (String.concatWith "," (Symtab.keys tab)) 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) - fun is_class_son X (n, dc:docclass_struct) = (X = #inherits_from dc) - fun tree lev ([]:(string * docclass_struct)list) = "" - |tree lev ((n,R)::S) = (if P(lev,n) - then "."^Int.toString lev^" "^(T n)^"{...}.\n" - ^ (tree(lev + 1)(filter(is_class_son(SOME([],n)))class_tab)) - else "."^Int.toString lev^" ... \n") - ^ (tree lev S) - val roots = filter(is_class_son NONE) class_tab - in ".0 .\n" ^ tree 1 roots end - - -val (strict_monitor_checking, strict_monitor_checking_setup) - = Attrib.config_bool \<^binding>\strict_monitor_checking\ (K false); - -val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup) - = Attrib.config_bool \<^binding>\free_class_in_monitor_checking\ (K false); - -val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup) - = Attrib.config_bool \<^binding>\free_class_in_monitor_strict_checking\ (K false); - -val (invariants_checking, invariants_checking_setup) - = Attrib.config_bool \<^binding>\invariants_checking\ (K true); - -val (invariants_strict_checking, invariants_strict_checking_setup) - = Attrib.config_bool \<^binding>\invariants_strict_checking\ (K false); - -val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) - = Attrib.config_bool \<^binding>\invariants_checking_with_tactics\ (K false); - - -end (* struct *) - -\ - -setup\DOF_core.strict_monitor_checking_setup - #> DOF_core.free_class_in_monitor_checking_setup - #> DOF_core.free_class_in_monitor_strict_checking_setup - #> DOF_core.invariants_checking_setup - #> DOF_core.invariants_strict_checking_setup - #> DOF_core.invariants_checking_with_tactics_setup\ - section\ Syntax for Term Annotation Antiquotations (TA)\ text\Isabelle/DOF allows for annotations at the term level, for which an @@ -860,22 +66,6 @@ antiquotation syntax and semantics is defined at the inner syntax level. For the moment, only a fixed number of builtin TA's is supported, future versions might extend this feature substantially.\ -subsection\ Syntax \ - -datatype "doc_class" = mk string - -\ \and others in the future : file, http, thy, ...\ - -consts ISA_typ :: "string \ typ" ("@{typ _}") -consts ISA_term :: "string \ term" ("@{term _}") -consts ISA_term_repr :: "string \ term" ("@{termrepr _}") -datatype "thm" = ISA_thm string ("@{thm _}") | Thm_content ("proof":proofterm) -datatype "thms_of" = ISA_thms_of string ("@{thms-of _}") -datatype "file" = ISA_file string ("@{file _}") -datatype "thy" = ISA_thy string ("@{thy _}") -consts ISA_docitem :: "string \ 'a" ("@{docitem _}") -datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}") -consts ISA_trace_attribute :: "string \ (string * string) list" ("@{trace-attribute _}") \ \Dynamic setup of inner syntax cartouche\ @@ -963,433 +153,6 @@ declare [[cartouche_type = "char list"]] term "\Université\ :: char list" - -subsection\ Semantics \ - -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 _ = 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)); - in path end; - - -fun ML_isa_antiq check_file thy (name, _, pos) = - let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos); - in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end; - - -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 ML_isa_check_typ thy (term, _, pos) _ = - let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) - in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end - in ML_isa_check_generic check thy (term, pos) end - - -fun ML_isa_check_term thy (term, _, pos) _ = - let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) - in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end - in ML_isa_check_generic check thy (term, pos) end - - -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 - | SOME X => X - in ML_isa_check_generic check thy (term, pos) end - - -fun ML_isa_check_file thy (term, _, pos) _ = - let fun check thy (name, pos) = check_path (SOME File.check_file) - (Proof_Context.init_global thy) - (Path.current) - (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 - then case DOF_core.get_object_global name thy of - NONE => warning("oid declared, but not yet defined --- "^ - " type-check incomplete") - | SOME {pos=pos_decl,cid,id,...} => - let val ctxt = (Proof_Context.init_global thy) - val req_class = case req_ty of - \<^Type>\fun _ T\ => DOF_core.typ_to_cid T - | _ => error("can not infer type for: "^ name) - in if cid <> DOF_core.default_cid - andalso not(DOF_core.is_subclass ctxt cid req_class) - then error("reference ontologically inconsistent: " - ^cid^" vs. "^req_class^ Position.here pos_decl) - else () - end - else 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 - | SOME(_) => () - in ML_isa_check_generic check thy (term, pos) end - -fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = - case term_option of - NONE => error("Wrong term option. You must use a defined term") - | SOME term => Const (isa_name, ty) $ term - -fun reify_typ (Type (s, typ_list)) = - \<^Const>\Ty\ $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\typ\ (map reify_typ typ_list) - | reify_typ (TFree (name, sort)) = - \<^Const>\Tv\ $(\<^Const>\Free\ $ HOLogic.mk_literal name) - $ (HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort)) - | reify_typ (TVar (indexname, sort)) = - let val (name, index_value) = indexname - in \<^Const>\Tv\ - $ (\<^Const>\Var\ - $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value)) - $ (HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort)) end - -fun ML_isa_elaborate_typ (thy:theory) _ _ term_option _ = - case term_option of - NONE => error("Wrong term option. You must use a defined term") - | SOME term => let - val typ_name = HOLogic.dest_string term - val typ = Syntax.read_typ_global thy typ_name - in reify_typ typ end - -fun reify_term (Const (name, typ)) =\<^Const>\Ct\ $ HOLogic.mk_literal name $ reify_typ typ - | reify_term (Free (name, typ)) = - \<^Const>\Fv\ $ (\<^Const>\Free\ $ HOLogic.mk_literal name) $ reify_typ typ - | reify_term (Var (indexname, typ)) = - let val (name, index_value) = indexname - in \<^Const>\Fv\ - $ (\<^Const>\Var\ - $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value)) - $ reify_typ typ end - | reify_term (Bound i) = \<^Const>\Bv\ $ HOLogic.mk_nat i - | reify_term (Abs (_, typ, term)) = \<^Const>\Abs\ $ reify_typ typ $ reify_term term - | reify_term (Term.$ (t1, t2)) = \<^Const>\App\ $ reify_term t1 $ reify_term t2 - -fun ML_isa_elaborate_term (thy:theory) _ _ term_option _ = - case term_option of - NONE => error("Wrong term option. You must use a defined term") - | SOME term => let - val term_name = HOLogic.dest_string term - val term = Syntax.read_term_global thy term_name - in reify_term term end - -fun reify_proofterm (PBound i) =\<^Const>\PBound\ $ (HOLogic.mk_nat i) - | reify_proofterm (Abst (_, typ_option, proof)) = - \<^Const>\Abst\ $ reify_typ (the typ_option) $ reify_proofterm proof - | reify_proofterm (AbsP (_, term_option, proof)) = - \<^Const>\AbsP\ $ reify_term (the term_option) $ reify_proofterm proof - | reify_proofterm (op % (proof, term_option)) = - \<^Const>\Appt\ $ reify_proofterm proof $ reify_term (the term_option) - | reify_proofterm (op %% (proof1, proof2)) = - \<^Const>\AppP\ $ reify_proofterm proof1 $ reify_proofterm proof2 - | reify_proofterm (Hyp term) = \<^Const>\Hyp\ $ (reify_term term) - | reify_proofterm (PAxm (_, term, typ_list_option)) = - let - val tvars = rev (Term.add_tvars term []) - val meta_tvars = map (fn ((name, index_value), sort) => - HOLogic.mk_prod - (\<^Const>\Var\ - $ HOLogic.mk_prod - (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value) - , HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort))) tvars - val meta_typ_list = - HOLogic.mk_list @{typ "tyinst"} (map2 (fn x => fn y => HOLogic.mk_prod (x, y)) - meta_tvars (map reify_typ (the typ_list_option))) - in \<^Const>\PAxm\ $ reify_term term $ meta_typ_list end - | reify_proofterm (PClass (typ, class)) = - \<^Const>\OfClass\ $ reify_typ typ $ HOLogic.mk_literal class - | reify_proofterm (PThm ({prop = prop, types = types, ...}, _)) = - let - val tvars = rev (Term.add_tvars prop []) - val meta_tvars = map (fn ((name, index_value), sort) => - HOLogic.mk_prod - (\<^Const>\Var\ - $ HOLogic.mk_prod - (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value) - , HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort))) tvars - val meta_typ_list = - HOLogic.mk_list \<^typ>\tyinst\ (map2 (fn x => fn y => HOLogic.mk_prod (x, y)) - meta_tvars (map reify_typ (the types))) - in \<^Const>\PAxm\ $ reify_term prop $ meta_typ_list end - -fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos = - case term_option of - NONE => err ("Malformed term annotation") pos - | SOME term => - let - val thm_name = HOLogic.dest_string term - val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name - 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 - the option arguments (with a value NONE) of the proof datatype constructors, - at least for PAxm, with "SOME (typ/term)", - allowing us the use the projection function "the". - Maybe the function can deal with - 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 - (* 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. - Thm.reconstruct_proof_of seems sufficient to have a reifiable PAxm - in the metalogic. *) - val proof' = Thm.reconstruct_proof_of thm - (*in \<^Const>\Thm_content\ $ reify_proofterm prf end*) - (*in \<^Const>\Thm_content\ $ reify_proofterm proof end*) - in \<^Const>\Thm_content\ $ reify_proofterm proof' end - - -fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos = - case term_option of - NONE => err ("Malformed term annotation") pos - | SOME term => - let - val thm_name = HOLogic.dest_string term - val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm) - val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] [] - (*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*) - (*val all_proofs = map (Proof_Syntax.standard_proof_of - {full = true, expand_name = Thm.expand_name thm}) all_thms*) - (*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 - | SOME term => - let - val oid = HOLogic.dest_string term - val traces = 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) - in \<^Const>\Pair \<^typ>\string\ \<^typ>\string\\ $ HOLogic.mk_string s' $ S end - val traces' = map conv (HOLogic.dest_list traces) - in HOLogic.mk_list \<^Type>\prod \<^typ>\string\ \<^typ>\string\\ traces' end - -(* utilities *) - -fun property_list_dest ctxt X = - map (fn \<^Const_>\ISA_term for s\ => HOLogic.dest_string s - |\<^Const_>\ISA_term_repr for s\ => holstring_to_bstring ctxt (HOLogic.dest_string s)) - (HOLogic.dest_list X) - -end; (* struct *) - -\ - -ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ bool"} -val ty3 = ISA_core.reify_typ @{typ "prop"} -val ty4 = ISA_core.reify_typ @{typ "'a list"} -\ - -ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\x. x = 1"} -val t3 = ISA_core.reify_term @{term "[2, 3::int]"} -\ - -subsection\ Isar - Setup\ - -setup\DOF_core.update_isa_global("Isa_DOF.typ", - {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_typ}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term", - {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_term}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term_repr", - {check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.thm.thm", - {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thm}) \ -setup\DOF_core.update_isa_global("Isa_DOF.thms_of.thms_of", - {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thms_of}) \ -setup\DOF_core.update_isa_global("Isa_DOF.file.file", - {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.docitem", - {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.trace_attribute", - {check=ISA_core.ML_isa_check_trace_attribute, elaborate=ISA_core.ML_isa_elaborate_trace_attribute}) \ section\ Syntax for Annotated Documentation Commands (the '' View'' Part I) \ diff --git a/src/DOF/meta_interpretation/Deep_Interpretation.thy b/src/DOF/meta_interpretation/Deep_Interpretation.thy new file mode 100644 index 00000000..170076de --- /dev/null +++ b/src/DOF/meta_interpretation/Deep_Interpretation.thy @@ -0,0 +1,451 @@ +theory Deep_Interpretation + imports Isabelle_DOF.DOF_Core + Metalogic_ProofChecker.ProofTerm + +begin + +subsection\ Syntax \ + +datatype "doc_class" = mk string + +\ \and others in the future : file, http, thy, ...\ + +consts ISA_typ :: "string \ typ" ("@{typ _}") +consts ISA_term :: "string \ term" ("@{term _}") +consts ISA_term_repr :: "string \ term" ("@{termrepr _}") +datatype "thm" = ISA_thm string ("@{thm _}") | Thm_content ("proof":proofterm) +datatype "thms_of" = ISA_thms_of string ("@{thms-of _}") +datatype "file" = ISA_file string ("@{file _}") +datatype "thy" = ISA_thy string ("@{thy _}") +consts ISA_docitem :: "string \ 'a" ("@{docitem _}") +datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}") +consts ISA_trace_attribute :: "string \ (string * string) list" ("@{trace-attribute _}") + +subsection\ Semantics \ + +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 _ = 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)); + in path end; + + +fun ML_isa_antiq check_file thy (name, _, pos) = + let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos); + in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end; + + +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 ML_isa_check_typ thy (term, _, pos) _ = + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end + in ML_isa_check_generic check thy (term, pos) end + + +fun ML_isa_check_term thy (term, _, pos) _ = + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end + in ML_isa_check_generic check thy (term, pos) end + + +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 + | SOME X => X + in ML_isa_check_generic check thy (term, pos) end + + +fun ML_isa_check_file thy (term, _, pos) _ = + let fun check thy (name, pos) = check_path (SOME File.check_file) + (Proof_Context.init_global thy) + (Path.current) + (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 + then case DOF_core.get_object_global name thy of + NONE => warning("oid declared, but not yet defined --- "^ + " type-check incomplete") + | SOME {pos=pos_decl,cid,id,...} => + let val ctxt = (Proof_Context.init_global thy) + val req_class = case req_ty of + \<^Type>\fun _ T\ => DOF_core.typ_to_cid T + | _ => error("can not infer type for: "^ name) + in if cid <> DOF_core.default_cid + andalso not(DOF_core.is_subclass ctxt cid req_class) + then error("reference ontologically inconsistent: " + ^cid^" vs. "^req_class^ Position.here pos_decl) + else () + end + else 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 + | SOME(_) => () + in ML_isa_check_generic check thy (term, pos) end + +fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = + case term_option of + NONE => error("Wrong term option. You must use a defined term") + | SOME term => Const (isa_name, ty) $ term + +fun reify_typ (Type (s, typ_list)) = + \<^Const>\Ty\ $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\typ\ (map reify_typ typ_list) + | reify_typ (TFree (name, sort)) = + \<^Const>\Tv\ $(\<^Const>\Free\ $ HOLogic.mk_literal name) + $ (HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort)) + | reify_typ (TVar (indexname, sort)) = + let val (name, index_value) = indexname + in \<^Const>\Tv\ + $ (\<^Const>\Var\ + $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value)) + $ (HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort)) end + +fun ML_isa_elaborate_typ (thy:theory) _ _ term_option _ = + case term_option of + NONE => error("Wrong term option. You must use a defined term") + | SOME term => let + val typ_name = HOLogic.dest_string term + val typ = Syntax.read_typ_global thy typ_name + in reify_typ typ end + +fun reify_term (Const (name, typ)) =\<^Const>\Ct\ $ HOLogic.mk_literal name $ reify_typ typ + | reify_term (Free (name, typ)) = + \<^Const>\Fv\ $ (\<^Const>\Free\ $ HOLogic.mk_literal name) $ reify_typ typ + | reify_term (Var (indexname, typ)) = + let val (name, index_value) = indexname + in \<^Const>\Fv\ + $ (\<^Const>\Var\ + $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value)) + $ reify_typ typ end + | reify_term (Bound i) = \<^Const>\Bv\ $ HOLogic.mk_nat i + | reify_term (Abs (_, typ, term)) = \<^Const>\Abs\ $ reify_typ typ $ reify_term term + | reify_term (Term.$ (t1, t2)) = \<^Const>\App\ $ reify_term t1 $ reify_term t2 + +fun ML_isa_elaborate_term (thy:theory) _ _ term_option _ = + case term_option of + NONE => error("Wrong term option. You must use a defined term") + | SOME term => let + val term_name = HOLogic.dest_string term + val term = Syntax.read_term_global thy term_name + in reify_term term end + +fun reify_proofterm (PBound i) =\<^Const>\PBound\ $ (HOLogic.mk_nat i) + | reify_proofterm (Abst (_, typ_option, proof)) = + \<^Const>\Abst\ $ reify_typ (the typ_option) $ reify_proofterm proof + | reify_proofterm (AbsP (_, term_option, proof)) = + \<^Const>\AbsP\ $ reify_term (the term_option) $ reify_proofterm proof + | reify_proofterm (op % (proof, term_option)) = + \<^Const>\Appt\ $ reify_proofterm proof $ reify_term (the term_option) + | reify_proofterm (op %% (proof1, proof2)) = + \<^Const>\AppP\ $ reify_proofterm proof1 $ reify_proofterm proof2 + | reify_proofterm (Hyp term) = \<^Const>\Hyp\ $ (reify_term term) + | reify_proofterm (PAxm (_, term, typ_list_option)) = + let + val tvars = rev (Term.add_tvars term []) + val meta_tvars = map (fn ((name, index_value), sort) => + HOLogic.mk_prod + (\<^Const>\Var\ + $ HOLogic.mk_prod + (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value) + , HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort))) tvars + val meta_typ_list = + HOLogic.mk_list @{typ "tyinst"} (map2 (fn x => fn y => HOLogic.mk_prod (x, y)) + meta_tvars (map reify_typ (the typ_list_option))) + in \<^Const>\PAxm\ $ reify_term term $ meta_typ_list end + | reify_proofterm (PClass (typ, class)) = + \<^Const>\OfClass\ $ reify_typ typ $ HOLogic.mk_literal class + | reify_proofterm (PThm ({prop = prop, types = types, ...}, _)) = + let + val tvars = rev (Term.add_tvars prop []) + val meta_tvars = map (fn ((name, index_value), sort) => + HOLogic.mk_prod + (\<^Const>\Var\ + $ HOLogic.mk_prod + (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\int\ index_value) + , HOLogic.mk_set \<^typ>\class\ (map HOLogic.mk_literal sort))) tvars + val meta_typ_list = + HOLogic.mk_list \<^typ>\tyinst\ (map2 (fn x => fn y => HOLogic.mk_prod (x, y)) + meta_tvars (map reify_typ (the types))) + in \<^Const>\PAxm\ $ reify_term prop $ meta_typ_list end + +fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos = + case term_option of + NONE => err ("Malformed term annotation") pos + | SOME term => + let + val thm_name = HOLogic.dest_string term + val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name + 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 + the option arguments (with a value NONE) of the proof datatype constructors, + at least for PAxm, with "SOME (typ/term)", + allowing us the use the projection function "the". + Maybe the function can deal with + 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 + (* 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. + Thm.reconstruct_proof_of seems sufficient to have a reifiable PAxm + in the metalogic. *) + val proof' = Thm.reconstruct_proof_of thm + (*in \<^Const>\Thm_content\ $ reify_proofterm prf end*) + (*in \<^Const>\Thm_content\ $ reify_proofterm proof end*) + in \<^Const>\Thm_content\ $ reify_proofterm proof' end + + +fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos = + case term_option of + NONE => err ("Malformed term annotation") pos + | SOME term => + let + val thm_name = HOLogic.dest_string term + val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name + val body = Proofterm.strip_thm_body (Thm.proof_body_of thm) + val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] [] + (*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*) + (*val all_proofs = map (Proof_Syntax.standard_proof_of + {full = true, expand_name = Thm.expand_name thm}) all_thms*) + (*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 + | SOME term => + let + val oid = HOLogic.dest_string term + val traces = 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) + in \<^Const>\Pair \<^typ>\string\ \<^typ>\string\\ $ HOLogic.mk_string s' $ S end + val traces' = map conv (HOLogic.dest_list traces) + in HOLogic.mk_list \<^Type>\prod \<^typ>\string\ \<^typ>\string\\ traces' end + +(* utilities *) + +fun property_list_dest ctxt X = + map (fn \<^Const_>\ISA_term for s\ => HOLogic.dest_string s + |\<^Const_>\ISA_term_repr for s\ => holstring_to_bstring ctxt (HOLogic.dest_string s)) + (HOLogic.dest_list X) + +end; (* struct *) + +\ + +ML\ +val ty1 = ISA_core.reify_typ @{typ "int"} +val ty2 = ISA_core.reify_typ @{typ "int \ bool"} +val ty3 = ISA_core.reify_typ @{typ "prop"} +val ty4 = ISA_core.reify_typ @{typ "'a list"} +\ + +ML\ +val t1 = ISA_core.reify_term @{term "1::int"} +val t2 = ISA_core.reify_term @{term "\x. x = 1"} +val t3 = ISA_core.reify_term @{term "[2, 3::int]"} +\ + +subsection\ Isar - Setup\ + +setup\DOF_core.update_isa_global("Deep_Interpretation.typ", + {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_typ}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.term", + {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_term}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.term_repr", + {check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.thm.thm", + {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thm}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.thms_of.thms_of", + {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thms_of}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.file.file", + {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.docitem", + {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Deep_Interpretation.trace_attribute", + {check=ISA_core.ML_isa_check_trace_attribute, elaborate=ISA_core.ML_isa_elaborate_trace_attribute}) \ + +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 new file mode 100644 index 00000000..df88ffba --- /dev/null +++ b/src/DOF/meta_interpretation/Shallow_Interpretation.thy @@ -0,0 +1,311 @@ +theory Shallow_Interpretation + imports Isabelle_DOF.DOF_Core +begin + +subsection\ Syntax \ + +datatype "doc_class" = mk string + +\ \and others in the future : file, http, thy, ...\ + +datatype "typ" = ISA_typ string ("@{typ _}") +datatype "term" = ISA_term string ("@{term _}") +consts ISA_term_repr :: "string \ term" ("@{termrepr _}") +datatype "thm" = ISA_thm string ("@{thm _}") +datatype "file" = ISA_file string ("@{file _}") +datatype "thy" = ISA_thy string ("@{thy _}") +consts ISA_docitem :: "string \ 'a" ("@{docitem _}") +datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}") +consts ISA_trace_attribute :: "string \ (string * string) list" ("@{trace-attribute _}") + +subsection\ Semantics \ + +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 _ = 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)); + in path end; + + +fun ML_isa_antiq check_file thy (name, _, pos) = + let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos); + in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end; + + +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 ML_isa_check_typ thy (term, _, pos) _ = + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end + in ML_isa_check_generic check thy (term, pos) end + + +fun ML_isa_check_term thy (term, _, pos) _ = + let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy) + in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end + in ML_isa_check_generic check thy (term, pos) end + + +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 + | SOME X => X + in ML_isa_check_generic check thy (term, pos) end + + +fun ML_isa_check_file thy (term, _, pos) _ = + let fun check thy (name, pos) = check_path (SOME File.check_file) + (Proof_Context.init_global thy) + (Path.current) + (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 + then case DOF_core.get_object_global name thy of + NONE => warning("oid declared, but not yet defined --- "^ + " type-check incomplete") + | SOME {pos=pos_decl,cid,id,...} => + let val ctxt = (Proof_Context.init_global thy) + val req_class = case req_ty of + \<^Type>\fun _ T\ => DOF_core.typ_to_cid T + | _ => error("can not infer type for: "^ name) + in if cid <> DOF_core.default_cid + andalso not(DOF_core.is_subclass ctxt cid req_class) + then error("reference ontologically inconsistent: " + ^cid^" vs. "^req_class^ Position.here pos_decl) + else () + end + else 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 + | SOME(_) => () + in ML_isa_check_generic check thy (term, pos) end + +fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = + case term_option of + 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 + | SOME term => + let + val oid = HOLogic.dest_string term + val traces = 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) + in \<^Const>\Pair \<^typ>\string\ \<^typ>\string\\ $ HOLogic.mk_string s' $ S end + val traces' = map conv (HOLogic.dest_list traces) + in HOLogic.mk_list \<^Type>\prod \<^typ>\string\ \<^typ>\string\\ traces' end + +(* utilities *) + +fun property_list_dest ctxt X = + map (fn \<^Const_>\ISA_term for s\ => HOLogic.dest_string s + |\<^Const_>\ISA_term_repr for s\ => holstring_to_bstring ctxt (HOLogic.dest_string s)) + (HOLogic.dest_list X) + +end; (* struct *) + +\ + + +subsection\ Isar - Setup\ + +setup\DOF_core.update_isa_global("Shallow_Interpretation.typ.typ", + {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.term.term", + {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.term_repr", + {check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.thm.thm", + {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.file.file", + {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.docitem", + {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Shallow_Interpretation.trace_attribute", + {check=ISA_core.ML_isa_check_trace_attribute, elaborate=ISA_core.ML_isa_elaborate_trace_attribute}) \ + +end \ No newline at end of file diff --git a/src/ROOT b/src/ROOT index 5b586334..ca90a5b6 100644 --- a/src/ROOT +++ b/src/ROOT @@ -2,8 +2,10 @@ session "Isabelle_DOF" = "Functional-Automata" + options [document = pdf, document_output = "output", document_build = dof] sessions "Regular-Sets" + "Metalogic_ProofChecker" directories "DOF" + "DOF/meta_interpretation" "ontologies" "ontologies/CENELEC_50128" "ontologies/Conceptual" diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index fc7cc4fb..d132926e 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -44,7 +44,7 @@ doc_class text_section = type_synonym notion = string doc_class introduction = text_section + - uses :: "notion set" + "uses" :: "notion set" doc_class contribution_claim = introduction + based_on :: "notion list" diff --git a/src/tests/High_Level_Syntax_Invariants.thy b/src/tests/High_Level_Syntax_Invariants.thy index f275d0d6..1c6626f0 100644 --- a/src/tests/High_Level_Syntax_Invariants.thy +++ b/src/tests/High_Level_Syntax_Invariants.thy @@ -95,7 +95,7 @@ type_synonym notion = string doc_class introduction = text_section + authored_by :: "author set" <= "UNIV" - uses :: "notion set" + "uses" :: "notion set" invariant author_finite :: "finite (authored_by \)" and force_level :: "the (level \) > 1" @@ -119,7 +119,7 @@ doc_class result = technical + doc_class example = technical + referring_to :: "(notion + definition) set" <= "{}" -doc_class conclusion = text_section + +doc_class "conclusion" = text_section + establish :: "(claim \ result) set" invariant establish_defined :: "\ x. x \ Domain (establish \) \ (\ y \ Range (establish \). (x, y) \ establish \)" diff --git a/src/tests/Test_Reification.thy b/src/tests/Reification.thy similarity index 62% rename from src/tests/Test_Reification.thy rename to src/tests/Reification.thy index d2c93974..83461042 100644 --- a/src/tests/Test_Reification.thy +++ b/src/tests/Reification.thy @@ -1,19 +1,53 @@ -theory Test_Reification - imports "Main" Isabelle_DOF.Isa_DOF +theory Reification + imports "Isabelle_DOF.Conceptual" begin -(*ML\ +ML\ +val ty1 = ISA_core.reify_typ @{typ "int"} +val ty2 = ISA_core.reify_typ @{typ "int \ bool"} +val ty3 = ISA_core.reify_typ @{typ "prop"} +val ty4 = ISA_core.reify_typ @{typ "'a list"} +\ + +term*\@{typ \int\}\ +value*\@{typ \int\}\ +value*\@{typ \int \ bool\}\ +term*\@{typ \prop\}\ +value*\@{typ \prop\}\ +term*\@{typ \'a list\}\ +value*\@{typ \'a list\}\ + +ML\ +val t1 = ISA_core.reify_term @{term "1::int"} +val t2 = ISA_core.reify_term @{term "\x. x = 1"} +val t3 = ISA_core.reify_term @{term "[2, 3::int]"} +\ +term*\@{term \1::int\}\ +value*\@{term \1::int\}\ +term*\@{term \\x. x = 1\}\ +value*\@{term \\x. x = 1\}\ +term*\@{term \[2, 3::int]\}\ +value*\@{term \[2, 3::int]\}\ + +prf refl +full_prf refl + +term*\@{thm \HOL.refl\}\ +value*\proof @{thm \HOL.refl\}\ +value*\depth (proof @{thm \HOL.refl\})\ +value*\size (proof @{thm \HOL.refl\})\ +value*\fv_Proof (proof @{thm \HOL.refl\})\ +term*\@{thms-of \HOL.refl\}\ +value*\@{thms-of \HOL.refl\}\ + +ML\ val t_schematic = TVar(("'a",0), []) val t = @{term "Tv (Var (STR '''a'', 0)) {}"} val rt_schematic = ISA_core.reify_typ t_schematic val true = rt_schematic = t -\*) - -ML\ -val t = "\" -val tt = "\" \ + lemma test : "AAA \ BBB \ BBB \ AAA" by auto @@ -38,32 +72,10 @@ declare[[ML_print_depth = 20]] ML\ val full = true -val thm = @{thm "test"} -val standard_proof = Proof_Syntax.standard_proof_of - {full = full, expand_name = Thm.expand_name thm} thm -val term_of_proof = Proof_Syntax.term_of_proof standard_proof -\ -ML\ -val full = true -val thm = @{thm "test"} -val theory_of_thm = Thm.theory_of_thm thm -val prop_of = Thm.prop_of thm -(*val proof_of = Thm.proof_of thm*) -val reconstruct_proof_of = Thm.reconstruct_proof_of thm - - -\ - -ML\ -val full = true -val thm = @{thm "test"} -val theory_of_thm = Thm.theory_of_thm thm -val prop_of = Thm.prop_of thm -val proof_of = Thm.proof_of thm -val reconstruct_proof_of = Thm.reconstruct_proof_of thm -val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (proof_of % SOME prop_of); -val reconstruct_proof = Proofterm.reconstruct_proof theory_of_thm prop_of proof_of - +val thm = @{thm "test2"} +val hyps = Thm.hyps_of thm +val prems = Thm.prems_of thm +val reconstruct_proof = Thm.reconstruct_proof_of thm val standard_proof = Proof_Syntax.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm val term_of_proof = Proof_Syntax.term_of_proof standard_proof @@ -91,10 +103,10 @@ ML\ prf test full_prf test -term*\@{thm \Test_Reification.test\}\ -value*\@{thm \Test_Reification.test\}\ -(*term*\@{thms-of \TermAntiquotations.test\}\ -value*\@{thms-of \TermAntiquotations.test\}\*) +term*\@{thm \Reification.test\}\ +value*\@{thm \Reification.test\}\ +term*\@{thms-of \Reification.test\}\ +value*\@{thms-of \Reification.test\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\ @@ -138,8 +150,8 @@ ML\ prf test2 full_prf test2 -(*term*\@{thm \TermAntiquotations.test2\}\ -value*\proof @{thm \TermAntiquotations.test2\}\*) +term*\@{thm \Reification.test2\}\ +value*\proof @{thm \Reification.test2\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\ @@ -163,18 +175,8 @@ ML\ prf test2 full_prf test2 -(*term*\@{thm \TermAntiquotations.test3\}\ -value*\@{thm \TermAntiquotations.test3\}\*) - -ML\ -val full = false -val thm = @{thm "Pure.symmetric"} -val proof_of = Thm.proof_of thm - -val standard_proof = Proof_Syntax.standard_proof_of - {full = full, expand_name = Thm.expand_name thm} thm - -\ +term*\@{thm \Reification.test3\}\ +value*\@{thm \Reification.test3\}\ ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ ML\ @@ -201,7 +203,6 @@ full_prf symmetric term*\@{thm \Pure.symmetric\}\ value*\@{thm \Pure.symmetric\}\ -declare[[ML_print_depth = 20]] ML\ val full = true val thm = @{thm "Groups.minus_class.super"} @@ -218,8 +219,8 @@ val proof = Thm.proof_of thm prf Groups.minus_class.super full_prf Groups.minus_class.super -(*term*\@{thm \Groups.minus_class.super\}\ -value*\@{thm \Groups.minus_class.super\}\*) +term*\@{thm \Groups.minus_class.super\}\ +value*\@{thm \Groups.minus_class.super\}\ (*ML\ val full = true @@ -239,48 +240,6 @@ prf Homotopy.starlike_imp_contractible full_prf Homotopy.starlike_imp_contractible term*\@{thm \Homotopy.starlike_imp_contractible\}\ value*\@{thm \Homotopy.starlike_imp_contractible\}\*) -term\Field\ -find_consts name:"Domain" -find_theorems name:"Relation.Domain" -term\Domainp\ -find_consts name:"has_sort" -term\has_sort\ -ML\ -val t = replicate -val tt = HOLogic.dest_literal \<^term>\String.Literal True True True False False True False STR ''a''\ -\ -ML\ -val a_schematic = TVar(("'a",0), []) -val x = Var (("x", 0), a_schematic) -val y = Var (("y", 0), a_schematic) -val eq = \<^Const>\Pure.eq a_schematic\ -val imp = \<^Const>\Pure.imp \ -val term = \<^Const>\Pure.imp\ $ (eq $ x $ y) $ (eq $ y $ x) -val paxm = PAxm ("Pure.symmetric", term, SOME [\<^typ>\prop\]) -val paxm' = PAxm ("Pure.symmetric", term, NONE) -val t = ISA_core.reify_proofterm paxm -(*val tt = Value_Command.value \<^context> t*) -\ -ML\ -val t = @{thm "test"} -\ -ML\ -val a_schematic = TVar(("'a",0), []) -val x = Var (("x", 0), a_schematic) -val y = Var (("y", 0), a_schematic) -val eq = \<^Const>\Pure.eq a_schematic\ -val imp = \<^Const>\Pure.imp\ -val term = \<^Const>\Pure.imp\ $ (eq $ x $ y) $ (eq $ y $ x) -val paxm = PAxm ("Pure.symmetric", term, SOME [\<^typ>\prop\]) -val t = @{term "Tv (Var (STR '''a'', 0)) {}"} -val t = \<^term>\Tv (Var (STR '''a'', 0)) {}\ -val rt_schematic = ISA_core.reify_typ a_schematic -val true = rt_schematic = t -\ - -term\case_unit (1::int) ()\ -find_theorems name:"Sum*sumE" -find_theorems name:"case_unit" end \ No newline at end of file diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index dbf2ef2f..58e3d17b 100644 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -23,242 +23,6 @@ imports "Isabelle_DOF.Conceptual" begin -ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ bool"} -val ty3 = ISA_core.reify_typ @{typ "prop"} -val ty4 = ISA_core.reify_typ @{typ "'a list"} -\ - -term*\@{typ \int\}\ -value*\@{typ \int\}\ -value*\@{typ \int \ bool\}\ -term*\@{typ \prop\}\ -value*\@{typ \prop\}\ -term*\@{typ \'a list\}\ -value*\@{typ \'a list\}\ - -ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\x. x = 1"} -val t3 = ISA_core.reify_term @{term "[2, 3::int]"} -\ -term*\@{term \1::int\}\ -value*\@{term \1::int\}\ -term*\@{term \\x. x = 1\}\ -value*\@{term \\x. x = 1\}\ -term*\@{term \[2, 3::int]\}\ -value*\@{term \[2, 3::int]\}\ - -prf refl -full_prf refl - -term*\@{thm \HOL.refl\}\ -value*\proof @{thm \HOL.refl\}\ -value*\depth (proof @{thm \HOL.refl\})\ -value*\size (proof @{thm \HOL.refl\})\ -value*\fv_Proof (proof @{thm \HOL.refl\})\ -term*\@{thms-of \HOL.refl\}\ -value*\@{thms-of \HOL.refl\}\ - -ML\ -val t_schematic = TVar(("'a",0), []) -val t = @{term "Tv (Var (STR '''a'', 0)) {}"} -val rt_schematic = ISA_core.reify_typ t_schematic -val true = rt_schematic = t -\ - -lemma test : "AAA \ BBB \ BBB \ AAA" - by auto - -lemma test2 : "AAA \ BBB \ BBB \ AAA" - by auto - -lemma test3: "AAAAA \ BBBBB \ BBBBB \ AAAAA" -proof - assume "AAAAA \ BBBBB" - then obtain BBBBB and AAAAA .. - then show "BBBBB \ AAAAA" .. -qed - -lemma test4: - assumes "(AAA \ BBB)" - shows "BBB \ AAA" - apply (insert assms) - by auto - -declare[[show_sorts]] -declare[[ML_print_depth = 20]] - -ML\ -val full = true -val thm = @{thm "test"} -val standard_proof = Proof_Syntax.standard_proof_of - {full = full, expand_name = Thm.expand_name thm} thm -val term_of_proof = Proof_Syntax.term_of_proof standard_proof -\ - -ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ -ML\ - val thm = @{thm test}; - - (*proof body with digest*) - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); - - (*proof term only*) - val prf = Proofterm.proof_of body; - - (*clean output*) - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm); - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm); - - (*all theorems used in the graph of nested proofs*) - val all_thms = - Proofterm.fold_body_thms - (fn {name, ...} => insert (op =) name) [body] []; -\ - -prf test -full_prf test -term*\@{thm \TermAntiquotations.test\}\ -value*\@{thm \TermAntiquotations.test\}\ -term*\@{thms-of \TermAntiquotations.test\}\ -value*\@{thms-of \TermAntiquotations.test\}\ - -ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ -ML\ - val thm = @{thm test4}; - - (*proof body with digest*) - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); - - (*proof term only*) - val prf = Proofterm.proof_of body; - - (*clean output*) - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm); - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm); - - (*all theorems used in the graph of nested proofs*) - val all_thms = - Proofterm.fold_body_thms - (fn {name, ...} => insert (op =) name) [body] []; -\ - -ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ -ML\ - val thm = @{thm test2}; - - (*proof body with digest*) - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); - - (*proof term only*) - val prf = Proofterm.proof_of body; - - (*clean output*) - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm); - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm); - - (*all theorems used in the graph of nested proofs*) - val all_thms = - Proofterm.fold_body_thms - (fn {name, ...} => insert (op =) name) [body] []; -\ - -prf test2 -full_prf test2 -term*\@{thm \TermAntiquotations.test2\}\ -value*\proof @{thm \TermAntiquotations.test2\}\ - -ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ -ML\ - val thm = @{thm test3}; - - (*proof body with digest*) - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); - - (*proof term only*) - val prf = Proofterm.proof_of body; - - (*clean output*) - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm); - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm); - - (*all theorems used in the graph of nested proofs*) - val all_thms = - Proofterm.fold_body_thms - (fn {name, ...} => insert (op =) name) [body] []; -\ - -prf test2 -full_prf test2 -term*\@{thm \TermAntiquotations.test3\}\ -value*\@{thm \TermAntiquotations.test3\}\ - -ML\ (*See: *) \<^file>\~~/src/HOL/Proofs/ex/Proof_Terms.thy\\ -ML\ - val thm = @{thm Pure.symmetric}; - - (*proof body with digest*) - val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); - - (*proof term only*) - val prf = Proofterm.proof_of body; - - (*clean output*) - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm); - Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm); - - (*all theorems used in the graph of nested proofs*) - val all_thms = - Proofterm.fold_body_thms - (fn {name, ...} => insert (op =) name) [body] []; -\ - -prf symmetric -full_prf symmetric -term*\@{thm \Pure.symmetric\}\ -value*\@{thm \Pure.symmetric\}\ - -ML\ -val full = true -val thm = @{thm "Groups.minus_class.super"} -val standard_proof = Proof_Syntax.standard_proof_of - {full = full, expand_name = Thm.expand_name thm} thm -val term_of_proof = Proof_Syntax.term_of_proof standard_proof -\ - -ML\ -val thm = Proof_Context.get_thm \<^context> "Groups.minus_class.super" -val prop = Thm.prop_of thm -val proof = Thm.proof_of thm -\ - -prf Groups.minus_class.super -full_prf Groups.minus_class.super -term*\@{thm \Groups.minus_class.super\}\ -value*\@{thm \Groups.minus_class.super\}\ - -(*ML\ -val full = true -val thm = @{thm "Homotopy.starlike_imp_contractible"} -val standard_proof = Proof_Syntax.standard_proof_of - {full = full, expand_name = Thm.expand_name thm} thm -val term_of_proof = Proof_Syntax.term_of_proof standard_proof -\ - -ML\ -val thm = Proof_Context.get_thm \<^context> "Homotopy.starlike_imp_contractible" -val prop = Thm.prop_of thm -val proof = Thm.proof_of thm -\ - -prf Homotopy.starlike_imp_contractible -full_prf Homotopy.starlike_imp_contractible -term*\@{thm \Homotopy.starlike_imp_contractible\}\ -value*\@{thm \Homotopy.starlike_imp_contractible\}\*) - - text\Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring a fast read on the ``What's in Main''-documentation, but not additional knowledge on, say, SML --- an own syntax for references to types, terms, theorems, etc. are necessary. These are the