From 8fcc67978c63448658923607c62a253262bca618 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 22 Aug 2018 22:06:15 +0200 Subject: [PATCH] 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. --- Isa_DOF.thy | 31 ++++--- MyCommentedIsabelle.thy | 102 +++++++++++++++++++-- examples/scholarly/IsaDofApplications.thy | 7 +- test/conceptual/Attributes.thy | 106 +++++++++++++++++----- 4 files changed, 197 insertions(+), 49 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 99baa874..4fe3c646 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -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)) diff --git a/MyCommentedIsabelle.thy b/MyCommentedIsabelle.thy index fa1aa7e7..3a22d485 100644 --- a/MyCommentedIsabelle.thy +++ b/MyCommentedIsabelle.thy @@ -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\Note that @{emph \polymorphic variables\} are treated like constant symbols +in the type inference; thus, the following test, that one type is an instance of the +other, yields false: +\ +ML\ 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); +\ +text\In order to make the type inference work, one has to consider @{emph \schematic\} +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: \ +ML\ +val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); +\ +text\ MIND THE "'" !!!\ +text \On this basis, the following @{ML_type "Type.tyenv"} is constructed: \ +ML\ +val tyenv = Sign.typ_match ( @{theory}) + (t_schematic, @{typ "int list"}) + (Vartab.empty); +val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv; +\ + +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\ 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) +\ +text\... or more general variants thereof that are parameterized by the indexes for schematic +type variables instead of assuming just @{ML "0"}. \ + +text +\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"}. +\ + +ML\ +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. *) +\ + +text \Apparently, a bizarre conversion between the old-style interface and +the new-style @{ML "tyenv"} is necessary. See the following example.\ +ML\ +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) +\ 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\ +Sign.tsig_of: theory -> Type.tsig; +Sign.syn_of : theory -> Syntax.syntax; +Sign.of_sort : theory -> typ * sort -> bool ; +\ + +subsection{* Theories *} + + text \ 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. \ diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index e61d22cf..033b9c0a 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -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}). \ - -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''" ]\ Hyperlinks. \ +*) + declare_reference*["figDogfoodVIlinkappl"::figure] text\ An ontological reference application in diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index d2e5eddc..7459a59a 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -3,9 +3,13 @@ theory Attributes begin -text*[dfgdfg::B, y = "[''sdf'']"]\ sdfsdfs sdfsdf sdfsdf @{thm refl}}\ +text*[dfgdfg::B, B.x = "''f''", y = "[''s'']"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ -text\ @{docitem_ref \dfgdfg\} }\ +(* +text*[dfgdfg2::C, C.z = "None"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ +*) + +text\ @{docitem_ref \dfgdfg\} \ print_doc_classes @@ -22,12 +26,12 @@ term "B.x ((undefined::C)\B.y := [''sdf'']\)" term "C.z ((undefined::C)\B.y := [''sdf'']\)" ML\ -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}; \ -ML\ -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}; -\ ML\ DOF_core.get_value_local "sdf" @{context}; @@ -57,25 +52,33 @@ ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::d (* separate checking and term construction ?*) -ML\val Type(s,t) = @{typ "'a list"}; fold\ +ML\val Type(s,t) = @{typ "'a list"}; + val tt = @{term "(undefined::B)\B.x := '''' , B.y := []\"}; + val tt' = AnnoTextelemParser.infer_type @{theory} tt; + val tt'' = Sign.certify_term @{theory} tt; + \ + +ML\Variable.names_of @{context}; +Name.is_bound\ ML\ -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 \ -ML\\ +ML\val t = @{term "Conceptual.B.y_update"}\ +declare [[ML_print_depth=30]] + +ML\; +@{theory}; +open Sign; +Sign.typ_match; + +\ + + +ML\ +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;\ +ML\ + +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)); +\ +ML\ +AnnoTextelemParser.infer_type @{theory} tt; +\ + +ML\ val t = @{term "None"} + val Const(s,tt) = t + val Type(m,[TFree(d,s)]) = tt + \ + end \ No newline at end of file