fun ctyp str = Type (str, []) ; val charT = ctyp "List.char" ; (* was "Main.char" *) val nibbleT = ctyp "List.nibble" ; (* was "Main.nibble" *) val boolT = ctyp "bool" ; fun listT ty = Type ("List.list", [ty]) ; fun setT ty = Type ("set", [ty]) ; fun pairT (t1, t2) = Type ("*", [t1, t2]) ; fun PairT (t1, t2) = [t1, t2] ---> pairT (t1, t2) ; fun ConsT ty = [ty, listT ty] ---> listT ty ; fun insertT ty = [ty, setT ty] ---> setT ty ; val CharT = [nibbleT, nibbleT] ---> charT ; val strT = ctyp "GDC.structr" ; val fmlT = ctyp "GDC.formula" ; val stringT = listT charT ; (* a lot of this is repeated from stringSyntax.ML, but with prefixes in Const names *) val zero = ord "0"; val ten = ord "A" - 10; (* dest_nib : term -> int *) fun dest_nib (Const (c, _)) = (case explode c of (* first four letters seem to be either Main or List *) [_, _, _, _, ".","n","i","b","b","l","e",".", "N", "i", "b", "b", "l", "e", h] => ord h - (if h <= "9" then zero else ten) | _ => raise Fail ("dest_nib, Const " ^ c)) | dest_nib _ = raise Fail "dest_nib, not Const" ; (* dest_nibs : term -> term -> string *) fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2); (* dest_char : term -> string *) fun dest_char (Const ("Main.char.Char", _) $ t1 $ t2) = dest_nibs t1 t2 | dest_char (Const ("List.char.Char", _) $ t1 $ t2) = dest_nibs t1 t2 | dest_char tm = raise TERM ("HOLinML.ML: dest_char", [tm]) ; (* dest_list : term -> term list *) fun dest_list (Const ("List.list.Nil", _)) = [] | dest_list (Const ("List.list.Cons", _) $ c $ cs) = c :: dest_list cs | dest_list tm = raise TERM ("HOLinML.ML: dest_list", [tm]) ; (* dest_ms : term -> term list members of literal multiset *) fun dest_ms (Const ("Multiset_no_le.single", _) $ e) = [e] | dest_ms (Const ("Multiset.single", _) $ e) = [e] | dest_ms (Const ("op +", _) $ ms1 $ ms2) = dest_ms ms1 @ dest_ms ms2 | dest_ms (Const ("0", _)) = [] | dest_ms (Const ("Multiset.Mempty", _)) = [] | dest_ms (Const ("Multiset_no_le.Mempty", _)) = [] | dest_ms tm = raise TERM ("HOLinML.ML: dest_ms", [tm]) ; (* dest_string : term -> string list *) fun dest_string (Const ("List.list.Nil", _)) = [] | dest_string (Const ("List.list.Cons", _) $ c $ cs) = dest_char c :: dest_string cs | dest_string tm = raise TERM ("HOLinML.ML: dest_string", [tm]) ; fun dest_string t = map dest_char (dest_list t) ; (* mk_nib and mk_char were Main. now List. (why?) *) (* mk_nib : int -> term *) fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then zero else ten)), nibbleT); (* mk_char : string -> term *) fun mk_char c = Const ("List.char.Char", CharT) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16); (* mk_string : term list -> term *) fun mk_string [] = Const ("List.list.Nil", listT charT) | mk_string (t :: ts) = Const ("List.list.Cons", ConsT charT) $ t $ mk_string ts; (* h2ml_str : term -> string ml2h_str : string -> term converts Isabelle/HOL string to ML string, and vice versa *) fun h2ml_str hstr = implode (dest_string hstr) ; fun ml2h_str str = mk_string (map mk_char (explode str)) ; (* stuff specifically for display logic *) fun SV hstr = Const ("GDC.structr.SV", listT charT --> strT) $ hstr ; fun FV hstr = Const ("GDC.formula.FV", listT charT --> fmlT) $ hstr ; val pSubstT = listT (pairT (stringT, stringT)) ; val fSubstT = listT (pairT (stringT, fmlT)) ; val sSubstT = listT (pairT (stringT, strT)) ; val pfSubstT = pairT (pSubstT, fSubstT) ; val fsSubstT = pairT (fSubstT, sSubstT) ; val pfsSubstT = pairT (pfSubstT, sSubstT) ; val ruleT = ctyp "GDC.rule" ; (* should be obsolete *) (* should be obsolete *) val ruleSubst = Const ("HOL_Sub.ruleSubst", [fsSubstT, ruleT] ---> ruleT) ; fun h2ml_list (Const ("List.list.Cons", _) $ h $ t) = h :: h2ml_list t | h2ml_list (Const ("List.list.Nil", _)) = [] | h2ml_list tm = raise TERM ("h2ml_list: term not recognized", [tm]) ; fun h2ml_set (Const ("op Un", _) $ s1 $ s2) = h2ml_set s1 @ h2ml_set s2 | h2ml_set (Const ("insert", _) $ h $ t) = h :: h2ml_set t | h2ml_set (Const ("{}", _)) = [] | h2ml_set tm = raise TERM ("h2ml_set: term not recognized", [tm]) ; fun h2ml_pair (Const ("Pair", _) $ s1 $ s2) = (s1, s2) | h2ml_pair tm = raise TERM ("h2ml_pair: term not recognized", [tm]) ; fun hset_nth 0 (Const ("insert", _) $ h $ t) = h | hset_nth n (Const ("insert", _) $ h $ t) = hset_nth (n-1) t | hset_nth _ tm = raise TERM ("hset_nth: term not recognized", [tm]) ; (* hset_append : term -> term -> term append of two HOL sets, s1 is {....} *) fun hset_append s1 s2 = let fun ha (Const ("{}", _)) = s2 | ha (f $ a) = ha f $ ha a | ha tm = tm ; in ha s1 end ; (* hset_sub : int -> term -> term -> term replace nth elt of set of form {...} with replacement set *) fun hset_sub 0 (Const ("insert", _) $ h $ t) ns = hset_append ns t | hset_sub n ((insh as Const ("insert", _) $ h) $ t) ns = insh $ hset_sub (n-1) t ns | hset_sub _ tm _ = raise TERM ("hset_sub: set not {x, ...}", [tm]) ; (* ml2h_list, ml2h_set : typ -> term list -> term tt is type of items in list *) fun ml2h_list tt ts = let fun cons x xs = Const ("List.list.Cons", ConsT tt) $ x $ xs fun m2h (y :: ys) = cons y (m2h ys) | m2h [] = Const ("List.list.Nil", listT tt) in m2h ts end ; fun ml2h_set tt ts = let fun cons x xs = Const ("insert", insertT tt) $ x $ xs fun m2h (y :: ys) = cons y (m2h ys) | m2h [] = Const ("{}", setT tt) in m2h ts end ; fun ml2h_pair (t1, t2) = Const ("Pair", PairT (type_of t1, type_of t2)) $ t1 $ t2 ; fun UnT ty = [setT ty, setT ty] ---> setT ty ; fun Un ty s1 s2 = Const ("op Un", UnT ty) $ s1 $ s2 ; fun subsetT ty = [setT ty, setT ty] ---> boolT ; fun subset' ty s1 s2 = Const ("op <=", subsetT ty) $ s1 $ s2 ; val Trueprop = Const ("Trueprop", boolT --> propT) ; (* warning - some of these are defined differently elsewhere *) (* mksub : typ -> string -> term mksubs : typ -> string list -> term make a substitution of one or more string variables to Isabelle vars *) fun mksub xT mlstr = ml2h_pair (ml2h_str mlstr, Var ((mlstr, 0), xT)) ; fun mksubs xT mlstrs = ml2h_list (pairT (stringT, xT)) (map (mksub xT) mlstrs) ; (* mkfssubs : {fv:string list, sv:string list} -> term make a HOL substitution, such as (([], [(''A'', ?A), (''B'', ?B)]), [(''X'', ?X), (''Y'', ?Y)]) *) fun mkfssubs {fv = fvstrs, sv = svstrs} = let val pfsub = ml2h_pair (mksubs stringT [], mksubs fmlT fvstrs) ; in ml2h_pair (pfsub, mksubs strT svstrs) end ; (* mkfssubs {fv = ["A", "B"], sv = ["X", "Y", "Z", "W"]} ; cterm_of (sign_of HOL_Sub.thy) it ; set show_types ; reset show_types ; *)