Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Solved type instantiation problem of future common value computation alg. 

Commented il slow-motion in MyCommentedIsabelle.
This commit is contained in:
Burkhart Wolff 2018-08-23 11:46:20 +02:00
parent 8fcc67978c
commit d04e09e24e
2 changed files with 22 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
MyCommentedIsabelle.thy
View File

@ -241,6 +241,9 @@ val true = Sign.typ_instance @{theory} (ty', generalize_typ ty)
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> Example:\<close>
ML\<open>val t = generalize_term @{term "[]"}\<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

67
test/conceptual/Attributes.thy
View File

@ -58,25 +58,24 @@ ML\<open>val Type(s,t) = @{typ "'a list"};
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 * 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
val generalize_term = Term.map_types (AnnoTextelemParser.generalize_typ 0)
fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t)
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: " ^Long_Name.base_name lhs^
" 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 --> typ) --> cid_ty --> cid_ty)
(typ --> typ)
--> cid_ty --> cid_ty)
val tyenv = Sign.typ_match thy ((AnnoTextelemParser.generalize_typ 0)(type_of rhs), lnt) (Vartab.empty);
val tyenv' = (map (fn (s,(t,u)) => ((s,t),u)) (Vartab.dest tyenv))
val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then ()
else error("illegal notation for attribute of "^cid_long)
fun join (ttt as @{typ "int"})
@ -91,67 +90,39 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
(* could be extended to bool, map, multisets, ... *)
in case opr of
"=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, generalize_term rhs)
$ Abs ("uu_", lnt, instantiate_term tyenv' (generalize_term rhs))
$ term
| "+=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, join lnt $ (Bound 0) $ (* generalize_term *) rhs)
$ Abs ("uu_", lnt, join lnt
$ (Bound 0)
$ instantiate_term tyenv'(generalize_term rhs))
$ term
| _ => error "corrupted syntax - oops - this should not occur"
end
in (* AnnoTextelemParser.infer_type thy*) (fold read_assn S term) end
in Sign.certify_term thy (fold read_assn S term) end
\<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
\<close>
ML\<open>
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)
val (tt, ty, n) = calc_update_term thy 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