forked from Isabelle_DOF/Isabelle_DOF
Update file hierarchy for meta-interpretation
Restructure theory files to allow multiple meta-interpretation of term antiquotations
This commit is contained in:
Nicolas Méric
parent
f5a2b6fe1b
commit
1ec6dacd6e
|
|
@ -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"]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||
Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) 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. \<close>
|
||||
|
||||
|
||||
section*[conclusion::conclusion]\<open> Conclusion and Related Work\<close>
|
||||
section*["conclusion"::"conclusion"]\<open> Conclusion and Related Work\<close>
|
||||
text\<open> 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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
\<close>
|
||||
|
||||
section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\<open>Conclusion\<close>
|
||||
section*["conclusion"::"conclusion",main_author="Some(@{docitem ''bu''}::author)"]\<open>Conclusion\<close>
|
||||
text\<open>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
|
||||
|
|
|
|||
|
|
@ -2310,7 +2310,7 @@ term "\<open>A \<Longrightarrow> B\<close> = ''''"
|
|||
|
||||
|
||||
|
||||
chapter*[c::conclusion]\<open>Conclusion\<close>
|
||||
chapter*[c::"conclusion"]\<open>Conclusion\<close>
|
||||
text\<open> 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
|
||||
|
|
|
|||
|
|
@ -0,0 +1,800 @@
|
|||
theory DOF_Core
|
||||
imports Main
|
||||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||
|
||||
begin
|
||||
|
||||
section\<open>Primitive Markup Generators\<close>
|
||||
ML\<open>
|
||||
|
||||
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 = "\<sigma>"
|
||||
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
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open> Utilities\<close>
|
||||
|
||||
ML\<open>
|
||||
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)
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
|
||||
|
||||
ML\<open>
|
||||
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>\<open>tag_attribute\<close>, \<^Type>\<open>int\<close>, 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>\<open>unit\<close>])) = 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>\<open>strict_monitor_checking\<close> (K false);
|
||||
|
||||
val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_checking\<close> (K false);
|
||||
|
||||
val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_strict_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking, invariants_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K true);
|
||||
|
||||
val (invariants_strict_checking, invariants_strict_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_strict_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
|
||||
|
||||
|
||||
end (* struct *)
|
||||
|
||||
\<close>
|
||||
|
||||
setup\<open>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\<close>
|
||||
|
||||
end
|
||||
1239
src/DOF/Isa_DOF.thy
1239
src/DOF/Isa_DOF.thy
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,451 @@
|
|||
theory Deep_Interpretation
|
||||
imports Isabelle_DOF.DOF_Core
|
||||
Metalogic_ProofChecker.ProofTerm
|
||||
|
||||
begin
|
||||
|
||||
subsection\<open> Syntax \<close>
|
||||
|
||||
datatype "doc_class" = mk string
|
||||
|
||||
\<comment> \<open>and others in the future : file, http, thy, ...\<close>
|
||||
|
||||
consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||
consts ISA_term_repr :: "string \<Rightarrow> 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 \<Rightarrow> 'a" ("@{docitem _}")
|
||||
datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}")
|
||||
consts ISA_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")
|
||||
|
||||
subsection\<open> Semantics \<close>
|
||||
|
||||
ML\<open>
|
||||
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>\<open>fun _ T\<close> => 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>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
|
||||
| reify_typ (TFree (name, sort)) =
|
||||
\<^Const>\<open>Tv\<close> $(\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name)
|
||||
$ (HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))
|
||||
| reify_typ (TVar (indexname, sort)) =
|
||||
let val (name, index_value) = indexname
|
||||
in \<^Const>\<open>Tv\<close>
|
||||
$ (\<^Const>\<open>Var\<close>
|
||||
$ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
|
||||
$ (HOLogic.mk_set \<^typ>\<open>class\<close> (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>\<open>Ct\<close> $ HOLogic.mk_literal name $ reify_typ typ
|
||||
| reify_term (Free (name, typ)) =
|
||||
\<^Const>\<open>Fv\<close> $ (\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name) $ reify_typ typ
|
||||
| reify_term (Var (indexname, typ)) =
|
||||
let val (name, index_value) = indexname
|
||||
in \<^Const>\<open>Fv\<close>
|
||||
$ (\<^Const>\<open>Var\<close>
|
||||
$ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
|
||||
$ reify_typ typ end
|
||||
| reify_term (Bound i) = \<^Const>\<open>Bv\<close> $ HOLogic.mk_nat i
|
||||
| reify_term (Abs (_, typ, term)) = \<^Const>\<open>Abs\<close> $ reify_typ typ $ reify_term term
|
||||
| reify_term (Term.$ (t1, t2)) = \<^Const>\<open>App\<close> $ 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>\<open>PBound\<close> $ (HOLogic.mk_nat i)
|
||||
| reify_proofterm (Abst (_, typ_option, proof)) =
|
||||
\<^Const>\<open>Abst\<close> $ reify_typ (the typ_option) $ reify_proofterm proof
|
||||
| reify_proofterm (AbsP (_, term_option, proof)) =
|
||||
\<^Const>\<open>AbsP\<close> $ reify_term (the term_option) $ reify_proofterm proof
|
||||
| reify_proofterm (op % (proof, term_option)) =
|
||||
\<^Const>\<open>Appt\<close> $ reify_proofterm proof $ reify_term (the term_option)
|
||||
| reify_proofterm (op %% (proof1, proof2)) =
|
||||
\<^Const>\<open>AppP\<close> $ reify_proofterm proof1 $ reify_proofterm proof2
|
||||
| reify_proofterm (Hyp term) = \<^Const>\<open>Hyp\<close> $ (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>\<open>Var\<close>
|
||||
$ HOLogic.mk_prod
|
||||
(HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
|
||||
, HOLogic.mk_set \<^typ>\<open>class\<close> (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>\<open>PAxm\<close> $ reify_term term $ meta_typ_list end
|
||||
| reify_proofterm (PClass (typ, class)) =
|
||||
\<^Const>\<open>OfClass\<close> $ 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>\<open>Var\<close>
|
||||
$ HOLogic.mk_prod
|
||||
(HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
|
||||
, HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))) tvars
|
||||
val meta_typ_list =
|
||||
HOLogic.mk_list \<^typ>\<open>tyinst\<close> (map2 (fn x => fn y => HOLogic.mk_prod (x, y))
|
||||
meta_tvars (map reify_typ (the types)))
|
||||
in \<^Const>\<open>PAxm\<close> $ 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>\<open>Thm_content\<close> $ reify_proofterm prf end*)
|
||||
(*in \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof end*)
|
||||
in \<^Const>\<open>Thm_content\<close> $ 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>\<open>thm\<close> (map (fn proof => \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof) all_proofs) end*)
|
||||
in HOLogic.mk_list \<^typ>\<open>string\<close> (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>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
|
||||
$ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
|
||||
let val s' = DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s)
|
||||
in \<^Const>\<open>Pair \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> $ HOLogic.mk_string s' $ S end
|
||||
val traces' = map conv (HOLogic.dest_list traces)
|
||||
in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest ctxt X =
|
||||
map (fn \<^Const_>\<open>ISA_term for s\<close> => HOLogic.dest_string s
|
||||
|\<^Const_>\<open>ISA_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X)
|
||||
|
||||
end; (* struct *)
|
||||
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val ty1 = ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = ISA_core.reify_typ @{typ "'a list"}
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val t1 = ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
\<close>
|
||||
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.typ",
|
||||
{check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_typ}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.term",
|
||||
{check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_term}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.term_repr",
|
||||
{check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.thm.thm",
|
||||
{check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_thm}) \<close>
|
||||
setup\<open>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}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.file.file",
|
||||
{check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Deep_Interpretation.docitem",
|
||||
{check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>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}) \<close>
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,311 @@
|
|||
theory Shallow_Interpretation
|
||||
imports Isabelle_DOF.DOF_Core
|
||||
begin
|
||||
|
||||
subsection\<open> Syntax \<close>
|
||||
|
||||
datatype "doc_class" = mk string
|
||||
|
||||
\<comment> \<open>and others in the future : file, http, thy, ...\<close>
|
||||
|
||||
datatype "typ" = ISA_typ string ("@{typ _}")
|
||||
datatype "term" = ISA_term string ("@{term _}")
|
||||
consts ISA_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
datatype "thm" = ISA_thm string ("@{thm _}")
|
||||
datatype "file" = ISA_file string ("@{file _}")
|
||||
datatype "thy" = ISA_thy string ("@{thy _}")
|
||||
consts ISA_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
|
||||
datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}")
|
||||
consts ISA_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")
|
||||
|
||||
subsection\<open> Semantics \<close>
|
||||
|
||||
ML\<open>
|
||||
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>\<open>fun _ T\<close> => 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>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
|
||||
$ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
|
||||
let val s' = DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s)
|
||||
in \<^Const>\<open>Pair \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> $ HOLogic.mk_string s' $ S end
|
||||
val traces' = map conv (HOLogic.dest_list traces)
|
||||
in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest ctxt X =
|
||||
map (fn \<^Const_>\<open>ISA_term for s\<close> => HOLogic.dest_string s
|
||||
|\<^Const_>\<open>ISA_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X)
|
||||
|
||||
end; (* struct *)
|
||||
|
||||
\<close>
|
||||
|
||||
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.typ.typ",
|
||||
{check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.term.term",
|
||||
{check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.term_repr",
|
||||
{check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.thm.thm",
|
||||
{check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.file.file",
|
||||
{check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Shallow_Interpretation.docitem",
|
||||
{check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>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}) \<close>
|
||||
|
||||
end
|
||||
2
src/ROOT
2
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"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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 \<sigma>)"
|
||||
and force_level :: "the (level \<sigma>) > 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 \<times> result) set"
|
||||
invariant establish_defined :: "\<forall> x. x \<in> Domain (establish \<sigma>)
|
||||
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
|
||||
|
|
|
|||
|
|
@ -1,19 +1,53 @@
|
|||
theory Test_Reification
|
||||
imports "Main" Isabelle_DOF.Isa_DOF
|
||||
theory Reification
|
||||
imports "Isabelle_DOF.Conceptual"
|
||||
|
||||
begin
|
||||
|
||||
(*ML\<open>
|
||||
ML\<open>
|
||||
val ty1 = ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = ISA_core.reify_typ @{typ "'a list"}
|
||||
\<close>
|
||||
|
||||
term*\<open>@{typ \<open>int\<close>}\<close>
|
||||
value*\<open>@{typ \<open>int\<close>}\<close>
|
||||
value*\<open>@{typ \<open>int \<Rightarrow> bool\<close>}\<close>
|
||||
term*\<open>@{typ \<open>prop\<close>}\<close>
|
||||
value*\<open>@{typ \<open>prop\<close>}\<close>
|
||||
term*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
value*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
val t1 = ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
\<close>
|
||||
term*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
value*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
term*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
|
||||
value*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
|
||||
term*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
|
||||
value*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
|
||||
|
||||
prf refl
|
||||
full_prf refl
|
||||
|
||||
term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>proof @{thm \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>depth (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
value*\<open>size (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
value*\<open>fv_Proof (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
term*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
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
|
||||
\<close>*)
|
||||
|
||||
ML\<open>
|
||||
val t = "\<bullet>"
|
||||
val tt = "\<cdot>"
|
||||
\<close>
|
||||
|
||||
lemma test : "AAA \<and> BBB \<longrightarrow> BBB \<and> AAA"
|
||||
by auto
|
||||
|
||||
|
|
@ -38,32 +72,10 @@ declare[[ML_print_depth = 20]]
|
|||
|
||||
ML\<open>
|
||||
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
|
||||
\<close>
|
||||
ML\<open>
|
||||
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
|
||||
|
||||
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
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\<open>
|
|||
|
||||
prf test
|
||||
full_prf test
|
||||
term*\<open>@{thm \<open>Test_Reification.test\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Test_Reification.test\<close>}\<close>
|
||||
(*term*\<open>@{thms-of \<open>TermAntiquotations.test\<close>}\<close>
|
||||
value*\<open>@{thms-of \<open>TermAntiquotations.test\<close>}\<close>*)
|
||||
term*\<open>@{thm \<open>Reification.test\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Reification.test\<close>}\<close>
|
||||
term*\<open>@{thms-of \<open>Reification.test\<close>}\<close>
|
||||
value*\<open>@{thms-of \<open>Reification.test\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
|
|
@ -138,8 +150,8 @@ ML\<open>
|
|||
|
||||
prf test2
|
||||
full_prf test2
|
||||
(*term*\<open>@{thm \<open>TermAntiquotations.test2\<close>}\<close>
|
||||
value*\<open>proof @{thm \<open>TermAntiquotations.test2\<close>}\<close>*)
|
||||
term*\<open>@{thm \<open>Reification.test2\<close>}\<close>
|
||||
value*\<open>proof @{thm \<open>Reification.test2\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
|
|
@ -163,18 +175,8 @@ ML\<open>
|
|||
|
||||
prf test2
|
||||
full_prf test2
|
||||
(*term*\<open>@{thm \<open>TermAntiquotations.test3\<close>}\<close>
|
||||
value*\<open>@{thm \<open>TermAntiquotations.test3\<close>}\<close>*)
|
||||
|
||||
ML\<open>
|
||||
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
|
||||
|
||||
\<close>
|
||||
term*\<open>@{thm \<open>Reification.test3\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Reification.test3\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
|
|
@ -201,7 +203,6 @@ full_prf symmetric
|
|||
term*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
|
||||
|
||||
declare[[ML_print_depth = 20]]
|
||||
ML\<open>
|
||||
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*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>*)
|
||||
term*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
|
||||
|
||||
(*ML\<open>
|
||||
val full = true
|
||||
|
|
@ -239,48 +240,6 @@ prf Homotopy.starlike_imp_contractible
|
|||
full_prf Homotopy.starlike_imp_contractible
|
||||
term*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>*)
|
||||
term\<open>Field\<close>
|
||||
find_consts name:"Domain"
|
||||
find_theorems name:"Relation.Domain"
|
||||
term\<open>Domainp\<close>
|
||||
find_consts name:"has_sort"
|
||||
term\<open>has_sort\<close>
|
||||
ML\<open>
|
||||
val t = replicate
|
||||
val tt = HOLogic.dest_literal \<^term>\<open>String.Literal True True True False False True False STR ''a''\<close>
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val a_schematic = TVar(("'a",0), [])
|
||||
val x = Var (("x", 0), a_schematic)
|
||||
val y = Var (("y", 0), a_schematic)
|
||||
val eq = \<^Const>\<open>Pure.eq a_schematic\<close>
|
||||
val imp = \<^Const>\<open>Pure.imp \<close>
|
||||
val term = \<^Const>\<open>Pure.imp\<close> $ (eq $ x $ y) $ (eq $ y $ x)
|
||||
val paxm = PAxm ("Pure.symmetric", term, SOME [\<^typ>\<open>prop\<close>])
|
||||
val paxm' = PAxm ("Pure.symmetric", term, NONE)
|
||||
val t = ISA_core.reify_proofterm paxm
|
||||
(*val tt = Value_Command.value \<^context> t*)
|
||||
\<close>
|
||||
ML\<open>
|
||||
val t = @{thm "test"}
|
||||
\<close>
|
||||
ML\<open>
|
||||
val a_schematic = TVar(("'a",0), [])
|
||||
val x = Var (("x", 0), a_schematic)
|
||||
val y = Var (("y", 0), a_schematic)
|
||||
val eq = \<^Const>\<open>Pure.eq a_schematic\<close>
|
||||
val imp = \<^Const>\<open>Pure.imp\<close>
|
||||
val term = \<^Const>\<open>Pure.imp\<close> $ (eq $ x $ y) $ (eq $ y $ x)
|
||||
val paxm = PAxm ("Pure.symmetric", term, SOME [\<^typ>\<open>prop\<close>])
|
||||
val t = @{term "Tv (Var (STR '''a'', 0)) {}"}
|
||||
val t = \<^term>\<open>Tv (Var (STR '''a'', 0)) {}\<close>
|
||||
val rt_schematic = ISA_core.reify_typ a_schematic
|
||||
val true = rt_schematic = t
|
||||
\<close>
|
||||
|
||||
term\<open>case_unit (1::int) ()\<close>
|
||||
find_theorems name:"Sum*sumE"
|
||||
find_theorems name:"case_unit"
|
||||
|
||||
end
|
||||
|
|
@ -23,242 +23,6 @@ imports
|
|||
"Isabelle_DOF.Conceptual"
|
||||
begin
|
||||
|
||||
ML\<open>
|
||||
val ty1 = ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = ISA_core.reify_typ @{typ "'a list"}
|
||||
\<close>
|
||||
|
||||
term*\<open>@{typ \<open>int\<close>}\<close>
|
||||
value*\<open>@{typ \<open>int\<close>}\<close>
|
||||
value*\<open>@{typ \<open>int \<Rightarrow> bool\<close>}\<close>
|
||||
term*\<open>@{typ \<open>prop\<close>}\<close>
|
||||
value*\<open>@{typ \<open>prop\<close>}\<close>
|
||||
term*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
value*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
val t1 = ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
\<close>
|
||||
term*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
value*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
term*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
|
||||
value*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
|
||||
term*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
|
||||
value*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
|
||||
|
||||
prf refl
|
||||
full_prf refl
|
||||
|
||||
term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>proof @{thm \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>depth (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
value*\<open>size (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
value*\<open>fv_Proof (proof @{thm \<open>HOL.refl\<close>})\<close>
|
||||
term*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
|
||||
value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
lemma test : "AAA \<and> BBB \<longrightarrow> BBB \<and> AAA"
|
||||
by auto
|
||||
|
||||
lemma test2 : "AAA \<and> BBB \<Longrightarrow> BBB \<and> AAA"
|
||||
by auto
|
||||
|
||||
lemma test3: "AAAAA \<and> BBBBB \<longrightarrow> BBBBB \<and> AAAAA"
|
||||
proof
|
||||
assume "AAAAA \<and> BBBBB"
|
||||
then obtain BBBBB and AAAAA ..
|
||||
then show "BBBBB \<and> AAAAA" ..
|
||||
qed
|
||||
|
||||
lemma test4:
|
||||
assumes "(AAA \<and> BBB)"
|
||||
shows "BBB \<and> AAA"
|
||||
apply (insert assms)
|
||||
by auto
|
||||
|
||||
declare[[show_sorts]]
|
||||
declare[[ML_print_depth = 20]]
|
||||
|
||||
ML\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
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] [];
|
||||
\<close>
|
||||
|
||||
prf test
|
||||
full_prf test
|
||||
term*\<open>@{thm \<open>TermAntiquotations.test\<close>}\<close>
|
||||
value*\<open>@{thm \<open>TermAntiquotations.test\<close>}\<close>
|
||||
term*\<open>@{thms-of \<open>TermAntiquotations.test\<close>}\<close>
|
||||
value*\<open>@{thms-of \<open>TermAntiquotations.test\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
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] [];
|
||||
\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
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] [];
|
||||
\<close>
|
||||
|
||||
prf test2
|
||||
full_prf test2
|
||||
term*\<open>@{thm \<open>TermAntiquotations.test2\<close>}\<close>
|
||||
value*\<open>proof @{thm \<open>TermAntiquotations.test2\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
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] [];
|
||||
\<close>
|
||||
|
||||
prf test2
|
||||
full_prf test2
|
||||
term*\<open>@{thm \<open>TermAntiquotations.test3\<close>}\<close>
|
||||
value*\<open>@{thm \<open>TermAntiquotations.test3\<close>}\<close>
|
||||
|
||||
ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
|
||||
ML\<open>
|
||||
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] [];
|
||||
\<close>
|
||||
|
||||
prf symmetric
|
||||
full_prf symmetric
|
||||
term*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val thm = Proof_Context.get_thm \<^context> "Groups.minus_class.super"
|
||||
val prop = Thm.prop_of thm
|
||||
val proof = Thm.proof_of thm
|
||||
\<close>
|
||||
|
||||
prf Groups.minus_class.super
|
||||
full_prf Groups.minus_class.super
|
||||
term*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
|
||||
|
||||
(*ML\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val thm = Proof_Context.get_thm \<^context> "Homotopy.starlike_imp_contractible"
|
||||
val prop = Thm.prop_of thm
|
||||
val proof = Thm.proof_of thm
|
||||
\<close>
|
||||
|
||||
prf Homotopy.starlike_imp_contractible
|
||||
full_prf Homotopy.starlike_imp_contractible
|
||||
term*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>
|
||||
value*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>*)
|
||||
|
||||
|
||||
text\<open>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
|
||||
|
|
|
|||
Loading…
Reference in New Issue