58 |
58 |
59 (* make distinct names out of the type list, |
59 (* make distinct names out of the type list, |
60 forbidding "o", "x..","f..","P.." as names *) |
60 forbidding "o", "x..","f..","P.." as names *) |
61 (* a number string is added if necessary *) |
61 (* a number string is added if necessary *) |
62 fun mk_var_names types : string list = let |
62 fun mk_var_names types : string list = let |
|
63 fun strip ss = drop (find ("'", ss)+1, ss); |
63 fun typid (Type (id,_) ) = hd (explode (Sign.base_name id)) |
64 fun typid (Type (id,_) ) = hd (explode (Sign.base_name id)) |
64 | typid (TFree (id,_) ) = hd (tl (explode (Sign.base_name id))) |
65 | typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id)))) |
65 | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id))); |
66 | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id))); |
66 fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s; |
67 fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s; |
67 fun index_vnames(vn::vns,occupied) = |
68 fun index_vnames(vn::vns,occupied) = |
68 (case assoc(occupied,vn) of |
69 (case assoc(occupied,vn) of |
69 None => if vn mem vns |
70 None => if vn mem vns |
108 |
109 |
109 fun mk_tvar s = TFree("'"^s,pcpoS); |
110 fun mk_tvar s = TFree("'"^s,pcpoS); |
110 fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T])); |
111 fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T])); |
111 infixr 5 -->; |
112 infixr 5 -->; |
112 infixr 6 ~>; val op ~> = mk_typ "->"; |
113 infixr 6 ~>; val op ~> = mk_typ "->"; |
|
114 val cfun_arrow = fst (rep_Type (dummyT ~> dummyT)); |
113 val NoSyn' = ThyOps.Mixfix NoSyn; |
115 val NoSyn' = ThyOps.Mixfix NoSyn; |
114 |
116 |
115 (* ----- support for term expressions ----- *) |
117 (* ----- support for term expressions ----- *) |
116 |
118 |
117 fun % s = Free(s,dummyT); |
119 fun % s = Free(s,dummyT); |