nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Resolved the type inference riddle and worked out 

a solution (type matching and instantiation.)
Documented the interface to the type interface
in MyCommentedIsabelle with an example.
This commit is contained in:
Burkhart Wolff 2018-08-22 22:06:15 +02:00
parent 8e09644e5c
commit 8fcc67978c
4 changed files with 197 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
Isa_DOF.thy
View File

@ -332,6 +332,7 @@ fun get_attributes_local cid ctxt =
fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy)
(* deprecated ?
fun get_default_local cid attr ctxt =
let val hierarchy_rev = rev(get_attributes_local cid ctxt) (* search in reverse order *)
fun found (_,L) = find_first (fn (bind,_,SOME(term)) => Binding.name_of bind = attr
@ -342,8 +343,10 @@ fun get_default_local cid attr ctxt =
end
fun get_default cid attr thy = get_default_local cid attr (Proof_Context.init_global thy)
*)
type attributes_info = { def_occurrence : string,
def_pos : Position.T,
long_name : string,
typ : typ
}
@ -356,6 +359,7 @@ fun get_attribute_info_local (*long*)cid attr ctxt : attributes_info option=
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
@ -412,7 +416,7 @@ fun print_doc_classes b ctxt =
| SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + ");
writeln (" name: "^(Binding.print name));
writeln (" origin: "^thy_name);
writeln (" attrs: " ^ commas (map print_attr attribute_decl))
writeln (" attrs: "^commas (map print_attr attribute_decl))
);
in map print_class (Symtab.dest y);
writeln "=====================================\n\n\n"
@ -433,7 +437,6 @@ val _ =
end (* struct *)
*}
print_antiquotations
section{* Syntax for Annotated Documentation Commands (the '' View'' Part I) *}
@ -497,10 +500,12 @@ fun convert((Const(s,ty),_), t) X = Const(s^"_update", dummyT)
$ Abs("uuu_", type_of t, t) $ X
|convert _ _ = error("Left-hand side not a doc_class attribute.")
fun base_default cid_long =
if cid_long = DOF_core.default_cid then Const(@{const_name "undefined"},@{typ "unit"})
else let val ty_name = cid_long^"."^ Long_Name.base_name cid_long^"_ext"
in Const(@{const_name "undefined"},Type(ty_name, [@{typ "unit"}])) end
fun cid_2_cidType cid_long =
if cid_long = DOF_core.default_cid then @{typ "unit"}
else let val ty_name = cid_long^"."^ Long_Name.base_name cid_long^"_ext"
in Type(ty_name, [@{typ "unit"}]) end
fun base_default_term cid_long = Const(@{const_name "undefined"},cid_2_cidType cid_long)
fun check_classref (SOME(cid,pos')) thy =
let val _ = if not (DOF_core.is_defined_cid_global cid thy)
@ -517,7 +522,7 @@ fun check_classref (SOME(cid,pos')) thy =
fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort));
fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term])
fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks:Input.source)
@ -529,7 +534,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta
this label is used as jump-target for point-and-click feature. *)
fun enrich_trans thy =
let val cid_long = check_classref cid_pos thy
val count = Unsynchronized.ref (0 - 1);
val count = Unsynchronized.ref (~1);
fun incr () = Unsynchronized.inc count
val generalize_term = let val n = incr () in Term.map_types (generalize_typ n) end
fun read_assn ((lhs, pos), rhs) =
@ -538,7 +543,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta
val assns = map read_assn doc_attrs
val _ = (SPY:=assns)
val _ = (SPY2 := Input.source_explode toks)
val defaults = base_default cid_long (* this calculation ignores the defaults *)
val defaults = base_default_term cid_long (* this calculation ignores the defaults *)
val value_term = (fold convert assns defaults) |> (infer_type thy)
val name = Context.theory_name thy
in thy |> DOF_core.define_object_global (oid, {pos=pos,
@ -623,12 +628,12 @@ val _ =
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("figure*", @{here}) "paragraph heading"
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "paragraph heading"
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
@ -853,7 +858,7 @@ fun calculate_attr_access_check ctxt attr oid = (* template *)
SOME term => let val ctxt = Context.the_proof ctxt
val SOME{cid,...} = DOF_core.get_object_local oid ctxt
val (* (long_cid, attr_b,ty) = *)
{def_occurrence, long_name, typ=ty} =
{def_occurrence, 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 ref"^ oid)
@ -939,7 +944,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
fun check_n_filter thy (bind,ty,mf) =
case DOF_core.get_attribute_info parent_cid_long (Binding.name_of bind) thy of
NONE => (* no prior declaration *) SOME(bind,ty,mf)
| SOME{def_occurrence, long_name, typ} => if ty = typ
| SOME{def_occurrence,long_name,typ,def_pos} => if ty = typ
then (warning("overriding attribute:"^long_name^
" in doc class:" ^ def_occurrence);
SOME(bind,ty,mf))

102
MyCommentedIsabelle.thy
View File

@ -184,23 +184,98 @@ subsection{* Type-Certification (=checking that a type annotation is consistent)
ML{*
Sign.typ_instance: theory -> typ * typ -> bool;
Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv;
Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int;
Sign.const_type: theory -> string -> typ option;
Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*)
Sign.cert_term: theory -> term -> term; (* short-cut for the latter *)
Sign.tsig_of: theory -> Type.tsig (* projects the type signature *)
*}
text{* @{ML "Sign.certify_term"} is actually an abstract wrapper on the structure Type
which contains the heart of the type inference. *}
text{* Type generalization is no longer part of the standard API. Here is a way to
overcome this by a self-baked generalization function:*}
text{*
@{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure
@{ML_structure "Type"}
which contains the heart of the type inference.
It also contains the type substitution type @{ML_type "Type.tyenv"} which is
is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"}
which in itself is a synonym for @{ML_type "'a Symtab.table"}, so
possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. *}
ML{*
text\<open>Note that @{emph \<open>polymorphic variables\<close>} are treated like constant symbols
in the type inference; thus, the following test, that one type is an instance of the
other, yields false:
\<close>
ML\<open>
val ty = @{typ "'a option"};
val ty' = @{typ "int option"};
Sign.typ_instance @{theory}(ty', ty);
val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *)
val false = Sign.typ_instance @{theory}(ty', ty);
\<close>
text\<open>In order to make the type inference work, one has to consider @{emph \<open>schematic\<close>}
type variables, which are more and more hidden from the Isar interface. Consequently,
the typ antiquotation above will not work for schematic type variables and we have
to construct them by hand on the SML level: \<close>
ML\<open>
val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]);
\<close>
text\<open> MIND THE "'" !!!\<close>
text \<open>On this basis, the following @{ML_type "Type.tyenv"} is constructed: \<close>
ML\<open>
val tyenv = Sign.typ_match ( @{theory})
(t_schematic, @{typ "int list"})
(Vartab.empty);
val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv;
\<close>
text{* Type generalization --- the conversion between free type variables and schematic
type variables --- is apparently no longer part of the standard API (there is a slightly
more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to
overcome this by a self-baked generalization function:*}
ML\<open>
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
Sign.typ_instance @{theory} (ty', generalize_typ ty)
*}
val generalize_term = Term.map_types generalize_typ;
val true = Sign.typ_instance @{theory} (ty', generalize_typ ty)
\<close>
text\<open>... or more general variants thereof that are parameterized by the indexes for schematic
type variables instead of assuming just @{ML "0"}. \<close>
text
\<open>Now we turn to the crucial issue of type-instantiation and with a given type environment
@{ML "tyenv"}. For this purpose, one has to switch to the low-level interface
@{ML_structure "Term_Subst"}.
\<close>
ML\<open>
Term_Subst.map_types_same : (typ -> typ) -> term -> term;
Term_Subst.map_aterms_same : (term -> term) -> term -> term;
Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term;
Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ;
Term_Subst.generalizeT: string list -> int -> typ -> typ;
(* this is the standard type generalisation function !!!
only type-frees in the string-list were taken into account. *)
Term_Subst.generalize: string list * string list -> int -> term -> term
(* this is the standard term generalisation function !!!
only type-frees and frees in the string-lists were taken
into account. *)
\<close>
text \<open>Apparently, a bizarre conversion between the old-style interface and
the new-style @{ML "tyenv"} is necessary. See the following example.\<close>
ML\<open>
val S = Vartab.dest tyenv;
val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
(* it took me quite some time to find out that these two type representations,
obscured by a number of type-synonyms, where actually identical. *)
val ty = t_schematic;
val ty' = Term_Subst.instantiateT S' t_schematic;
val t = (generalize_term @{term "[]"});
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
(* or alternatively : *)
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
\<close>
subsection{* Type-Inference (= inferring consistent type information if possible) *}
@ -211,7 +286,16 @@ ML{*
Type_Infer_Context.infer_types: Proof.context -> term list -> term list
*}
subsection{* Theories *}
subsection{* thy and the signature interface*}
ML\<open>
Sign.tsig_of: theory -> Type.tsig;
Sign.syn_of : theory -> Syntax.syntax;
Sign.of_sort : theory -> typ * sort -> bool ;
\<close>
subsection{* Theories *}
text \<open> This structure yields the datatype \verb*thy* which becomes the content of
\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
which inspired me (bu) to this naming. \<close>

7
examples/scholarly/IsaDofApplications.thy
View File

@ -605,8 +605,9 @@ Clicking on a document class identifier permits to hyperlink into the correspond
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
\<close>
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''"
(*
side_by_s ide_figure*["text-elements"::side_by_side_figure,
side_by_side_figure.anchor="''fig-Dogfood-II-bgnd1''"
,caption="''Exploring a Reference of a Text-Element.''"
,relative_width="''48''"
,src="''figures/Dogfood-II-bgnd1''"
@ -625,6 +626,8 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
,relative_width2="''47''"
,src2="''figures/Dogfood-III-bgnd-text_section''"
]\<open> Hyperlinks. \<close>
*)
declare_reference*["figDogfoodVIlinkappl"::figure]
text\<open> An ontological reference application in

106
test/conceptual/Attributes.thy
View File

@ -3,9 +3,13 @@ theory Attributes
begin
text*[dfgdfg::B, y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl}}\<close>
text*[dfgdfg::B, B.x = "''f''", y = "[''s'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
text\<open> @{docitem_ref \<open>dfgdfg\<close>} }\<close>
(*
text*[dfgdfg2::C, C.z = "None"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
*)
text\<open> @{docitem_ref \<open>dfgdfg\<close>} \<close>
print_doc_classes
@ -22,12 +26,12 @@ term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
term "C.z ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
ML\<open>
val SOME {def_occurrence = "Conceptual.A", long_name = "Conceptual.A.x", typ = t}
val SOME {def_occurrence = "Conceptual.A", long_name = "Conceptual.A.x", typ = t, def_pos}
= DOF_core.get_attribute_info "Conceptual.A" "x" @{theory};
DOF_core.get_attribute_info "Conceptual.B" "x" @{theory};
DOF_core.get_attribute_info "Conceptual.B" "y" @{theory};
DOF_core.get_attribute_info "Conceptual.C" "x" @{theory};
val SOME {def_occurrence = "Conceptual.C", long_name = "Conceptual.B.y", typ = t'}
val SOME {def_occurrence = "Conceptual.C", long_name = "Conceptual.B.y", typ = t', def_pos}
= DOF_core.get_attribute_info "Conceptual.C" "y" @{theory};
(* this is the situation where an attribute is defined in C, but due to inheritance
from B, where it is firstly declared which results in a different long_name. *)
@ -35,16 +39,7 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
\<close>
ML\<open>
DOF_core.get_default_local "Conceptual.A" "x" @{context};
DOF_core.get_default_local "Conceptual.B" "x" @{context};
DOF_core.get_default_local "Conceptual.B" "y" @{context};
DOF_core.get_default_local "Conceptual.C" "x" @{context};
DOF_core.get_default_local "Conceptual.C" "y" @{context};
DOF_core.get_default_local "Conceptual.C" "z" @{context};
\<close>
ML\<open>
DOF_core.get_value_local "sdf" @{context};
@ -57,25 +52,33 @@ ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::d
(* separate checking and term construction ?*)
ML\<open>val Type(s,t) = @{typ "'a list"}; fold\<close>
ML\<open>val Type(s,t) = @{typ "'a list"};
val tt = @{term "(undefined::B)\<lparr>B.x := '''' , B.y := []\<rparr>"};
val tt' = AnnoTextelemParser.infer_type @{theory} tt;
val tt'' = Sign.certify_term @{theory} tt;
\<close>
ML\<open>Variable.names_of @{context};
Name.is_bound\<close>
ML\<open>
fun calc_update_term thy cid_long (S:(((string * Position.T) * string) * string)list) term =
let val count = Unsynchronized.ref (0 - 1);
fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) term =
let val cid_ty = AnnoTextelemParser.cid_2_cidType cid_long
val count = Unsynchronized.ref (0);
fun incr () = Unsynchronized.inc count
val generalize_term = let val n = incr ()
in Term.map_types (AnnoTextelemParser.generalize_typ n) end
fun read_assn (((lhs, pos), opr), rhs) term =
fun read_assn (lhs, pos, opr, rhs) term =
let val info_opt = DOF_core.get_attribute_info cid_long
(Long_Name.base_name lhs) thy
val (ln,lnt,lnu,lnut) = case info_opt of
NONE => error ("unknown attribute in class: "^cid_long)
NONE => error ("unknown attribute: " ^Long_Name.base_name lhs^
" in class: "^cid_long)
| SOME{long_name, typ, ...} => (long_name, typ,
long_name ^"_update",
typ --> dummyT --> dummyT)
(typ --> typ) --> cid_ty --> cid_ty)
val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then ()
else error("illegal notation for attribute of "^cid_long)
val rhs' = Syntax.read_term_global thy rhs |> generalize_term
fun join (ttt as @{typ "int"})
= Const (@{const_name "plus"}, ttt --> ttt --> ttt)
|join (ttt as @{typ "string"})
@ -84,18 +87,71 @@ fun calc_update_term thy cid_long (S:(((string * Position.T) * string) * string)
= Const (@{const_name "sup"}, ttt --> ttt --> ttt)
|join (ttt as Type(@{type_name "list"},_))
= Const (@{const_name "append"}, ttt --> ttt --> ttt)
|join _ = error("implicit fusion operation not defined on attribute: "^ lhs)
|join _ = error("implicit fusion operation not defined for attribute: "^ lhs)
(* could be extended to bool, map, multisets, ... *)
in case opr of
"=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, rhs')
$ Abs ("uu_", lnt, generalize_term rhs)
$ term
| "+=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, join lnt $ (Bound 0) $ rhs')
$ Abs ("uu_", lnt, join lnt $ (Bound 0) $ (* generalize_term *) rhs)
$ term
| _ => error "corrupted syntax - oops - this should not occur"
end
in fold read_assn S term end
in (* AnnoTextelemParser.infer_type thy*) (fold read_assn S term) end
\<close>
ML\<open>\<close>
ML\<open>val t = @{term "Conceptual.B.y_update"}\<close>
declare [[ML_print_depth=30]]
ML\<open>;
@{theory};
open Sign;
Sign.typ_match;
\<close>
ML\<open>
val Type("List.list",[S]) = @{typ "('a) list"};
val ttt = Type("List.list",[TVar(("'a",0),@{sort "type"})]);
(* hint : the antiquotation 'typ' throws an exception for scheatic variables.... *)
Type.could_unify;
val tyenv = Type.typ_match (Sign.tsig_of @{theory})
(ttt, @{typ "int list"})
(Vartab.empty);
val tyenv = Sign.typ_match ( @{theory})
(ttt, @{typ "int list"})
(Vartab.empty);
Vartab.dest tyenv;\<close>
ML\<open>
fun get_attribute_defaults (* long*)cid thy =
let val attrS = flat(map snd (DOF_core.get_attributes cid thy))
fun trans (_,_,NONE) = NONE
|trans (na,ty,SOME def) =SOME(na,ty, def)
in map_filter trans attrS end
val cid_long = "Conceptual.B"
val attr_name = "dfgdfg"
val thy = @{theory};
Thm.generalize;
Term_Subst.generalize;
val XXX = DOF_core.get_value_global attr_name thy
val S = get_attribute_defaults cid_long thy;
fun conv (na, _ (* ty *), term) = (Binding.name_of na, Binding.pos_of na, "=", term);
val tt = calc_update_term @{theory} cid_long (map conv S)
(the(DOF_core.get_value_global attr_name thy));
\<close>
ML\<open>
AnnoTextelemParser.infer_type @{theory} tt;
\<close>
ML\<open> val t = @{term "None"}
val Const(s,tt) = t
val Type(m,[TFree(d,s)]) = tt
\<close>
end