1structure Pretype :> Pretype = 2struct 3 4open HolKernel errormonad Pretype_dtype; 5infix >> >-; 6 7 8val TCERR = mk_HOL_ERR "Pretype"; 9 10structure Env = 11struct 12 type t = ((int,pretype) Binarymap.dict * int) 13 fun lookup (d,c) i = Binarymap.peek(d,i) 14 fun update (i,pty) (d,c) = (Binarymap.insert(d,i,pty), c) 15 val empty : t = (Binarymap.mkDict Int.compare, 0) 16 fun new (d,c) = ((d,c+1), c) 17 fun toList (d,c) = List.tabulate(c, fn i => (i, Binarymap.peek(d,i))) 18end 19 20open typecheck_error 21type 'a in_env = (Env.t,'a,error) errormonad.t 22 23fun fail s = error (Misc s, locn.Loc_Unknown) 24 25fun boundcase i (n:'a in_env) (sf : pretype -> 'a in_env) : 'a in_env = fn e => 26 case Env.lookup e i of 27 NONE => n e 28 | SOME pty => sf pty e 29 30fun tyvars t = 31 case t of 32 Vartype s => return [s] 33 | Tyop{Args,...} => 34 List.foldl (fn (t, set) => lift2 Lib.union (tyvars t) set) 35 (return []) 36 Args 37 | UVar i => boundcase i (return []) tyvars 38 39fun mk_fun_ty (dom,rng) = Tyop{Thy="min", Tyop="fun", Args = [dom,rng]} 40 41val new_uvar = lift UVar (Some o Env.new) 42fun update arg E = 43 let 44 val E' = Env.update arg E 45 in 46 Some (E', ()) 47 end 48 49infix ref_occurs_in 50 51fun (r:int) ref_occurs_in (value:pretype) : bool in_env= 52 case value of 53 Vartype _ => return false 54 | Tyop {Args = ts : pretype list,...} => refoccl r ts 55 | UVar i => boundcase i (return (r = i)) (fn pty => r ref_occurs_in pty) 56and refoccl r [] = return false 57 | refoccl r ((t:pretype)::ts) = 58 r ref_occurs_in t >- (fn b => if b then return b else refoccl r ts) 59 60 61infix ref_equiv 62fun r ref_equiv value = 63 case value of 64 Vartype _ => return false 65 | Tyop _ => return false 66 | UVar r' => boundcase r' 67 (return (r = r')) 68 (fn pty => if r = r' then return true 69 else r ref_equiv pty) 70 71fun bind i pty : unit in_env = 72 case pty of 73 UVar j => if i = j then ok 74 else boundcase j (update(i,pty)) (bind i) 75 | _ => (i ref_occurs_in pty) >- 76 (fn b => if b then fail "Circular binding in unification" 77 else update(i,pty)) 78 79fun unify t1 t2 = 80 case (t1, t2) of 81 (UVar r, _) => 82 boundcase r (bind r t2) (fn t1' => unify t1' t2) 83 | (_, UVar r) => boundcase r (bind r t1) (fn t2' => unify t1 t2') 84 | (Vartype v1, Vartype v2) => 85 if v1 = v2 then ok 86 else fail ("Attempt to unify fixed variable types "^v1^" and " ^ v2) 87 | (Vartype v, Tyop {Thy,Tyop=s,...}) => 88 fail ("Attempt to unify fixed variable type "^v^" with operator "^ 89 Thy^"$"^s) 90 | (Tyop {Thy,Tyop=s,...}, Vartype v) => 91 fail ("Attempt to unify fixed variable type "^v^" with operator "^ 92 Thy^"$"^s) 93 | (Tyop{Args=as1, Tyop=op1, Thy=thy1}, Tyop{Args=as2, Tyop=op2, Thy=thy2})=> 94 if thy1 <> thy2 orelse op1 <> op2 then 95 fail ("Attempt to unify different type operators: " ^ 96 thy1 ^ "$" ^ op1^ " and " ^ thy2 ^ "$" ^ op2) 97 else unifyl as1 as2 98and unifyl [] [] = ok 99 | unifyl [] _ = fail "Same tyop with different # of arguments?" 100 | unifyl _ [] = fail "Same tyop with different # of arguments?" 101 | unifyl (t1::t1s) (t2::t2s) = unify t1 t2 >> unifyl t1s t2s 102 103fun can_unify pty1 pty2 : bool in_env = fn e => 104 case unify pty1 pty2 e of 105 Error _ => Some (e, false) 106 | _ => Some (e, true) 107 108fun apply_subst E pty = 109 case pty of 110 Vartype _ => pty 111 | Tyop{Tyop = s, Thy = t, Args = args} => 112 Tyop{Tyop = s, Thy = t, Args = map (apply_subst E) args} 113 | UVar i => case Env.lookup E i of 114 NONE => pty 115 | SOME pty => apply_subst E pty 116 117(* ---------------------------------------------------------------------- 118 Passes over a type, turning all of the type variables not in the 119 avoids list into fresh UVars, but doing so consistently by using 120 an env, which is an alist from variable names to type variable 121 refs. 122 ---------------------------------------------------------------------- *) 123 124local 125 fun replace s (env as (E, alist)) = 126 case Lib.assoc1 s alist of 127 NONE => (case new_uvar E of 128 Some (E', pty) => Some ((E',(s,pty) :: alist), pty) 129 | Error e => Error e (* should never happen *)) 130 | SOME (_, pty) => Some (env, pty) 131in 132fun rename_tv avds ty = 133 case ty of 134 Vartype s => if mem s avds then return ty else replace s 135 | Tyop{Tyop = s, Thy = thy, Args = args} => 136 mmap (rename_tv avds) args >- 137 (fn args' => return (Tyop{Tyop = s, Thy = thy, Args = args'})) 138 | x => return x 139 140fun rename_typevars avds ty : pretype in_env = fn e => 141 case rename_tv avds ty (e, []) of 142 Some ((e', _), pty) => Some (e', pty) 143 | Error e => Error e 144 145end 146 147fun fromType t = 148 if Type.is_vartype t then Vartype (Type.dest_vartype t) 149 else let val {Tyop = tyop, Args, Thy} = Type.dest_thy_type t 150 in Tyop{Tyop = tyop, Args = map fromType Args, Thy = Thy} 151 end 152 153fun remove_made_links ty = 154 case ty of 155 UVar i => boundcase i (return ty) remove_made_links 156 | Tyop{Tyop = s, Thy, Args} => 157 lift (fn args => Tyop {Tyop = s, Thy = Thy, Args = args}) 158 (mmap remove_made_links Args) 159 | _ => return ty 160 161val tyvariant = Lexis.gen_variant Lexis.tyvar_vary 162 163fun replace_null_links ty : (Env.t * string list, pretype, error) t = 164 case ty of 165 UVar r => (fn (e,used) => 166 case Env.lookup e r of 167 SOME pty => replace_null_links pty (e,used) 168 | NONE => 169 let 170 val nm = tyvariant used "'a" 171 val res = Vartype nm 172 in 173 Some ((Env.update (r,res) e, nm::used), res) 174 end) 175 | Tyop {Args,Thy,Tyop=s} => 176 lift (fn args => Tyop{Tyop=s,Args=args,Thy=Thy}) 177 (mmap replace_null_links Args) 178 | Vartype _ => return ty 179 180fun clean ty = 181 case ty of 182 Vartype s => Type.mk_vartype s 183 | Tyop{Tyop = s, Args, Thy} => 184 Type.mk_thy_type{Tyop = s, Thy = Thy, Args = map clean Args} 185 | _ => raise Fail "Don't expect to see links remaining at this stage" 186 187fun toTypeM ty : Type.hol_type in_env = 188 remove_made_links ty >- 189 (fn ty => tyvars ty >- 190 (fn vs => lift (clean o #2) (addState vs (replace_null_links ty)))) 191 192fun toType pty = 193 case toTypeM pty Env.empty of 194 Error e => raise mkExn e 195 | Some (_, ty) => ty 196 197fun chase (Tyop{Tyop = "fun", Thy = "min", Args = [_, ty]}) = return ty 198 | chase (UVar i) = 199 boundcase i (fail ("chase: uvar "^Int.toString i^" unbound")) chase 200 | chase (Vartype s) = fail ("chase: can't chase variable type "^s) 201 | chase (Tyop{Tyop=s, Thy, ...}) = 202 fail ("chase: can't chase through "^Thy^"$"^s) 203 204 205datatype pp_pty_state = none | left | right | uvar 206 207fun pp_pretype pty = let 208 open HOLPP 209 fun pp_pty state pty = let 210 in 211 case pty of 212 Vartype s => [add_string ("V("^s^")")] 213 | Tyop {Thy,Tyop = tyop,Args} => 214 let 215 val qid = if Thy = "bool" orelse Thy = "min" then add_string tyop 216 else add_string (Thy ^ "$" ^ tyop) 217 in 218 if Thy = "min" andalso tyop = "fun" then 219 let 220 val wrap = 221 case state of 222 none => (fn ps => [block INCONSISTENT 0 ps]) 223 | right => I 224 | _ (* left or uvar *) => 225 fn ps => [add_string "(", block INCONSISTENT 0 ps, 226 add_string ")"] 227 val core = 228 pp_pty left (hd Args) @ 229 [add_string " ", add_string "->", add_break (1,0)] @ 230 pp_pty right (hd (tl Args)) 231 in 232 wrap core 233 end 234 else 235 case Args of 236 [] => [qid] 237 | _ => [ 238 add_string "(", 239 block INCONSISTENT 0 ( 240 pr_list (block INCONSISTENT 0 o pp_pty none) [add_string ","] 241 Args 242 ), 243 add_string ")", 244 qid 245 ] 246 end 247 | UVar r => [add_string ("U("^Int.toString r^")")] 248 end 249in 250 block INCONSISTENT 0 (pp_pty none pty) 251end 252 253fun remove_ty_aq t = 254 if parse_type.is_ty_antiq t then parse_type.dest_ty_antiq t 255 else raise mk_HOL_ERR "Parse" "type parser" "antiquotation is not of a type" 256 257fun tyop_to_qtyop ((tyop,locn), args) = 258 case Type.decls tyop of 259 [] => raise mk_HOL_ERRloc "Parse" "type parser" locn 260 (tyop^" not a known type operator") 261 | {Thy,Tyop = tyop} :: _ => Tyop{Thy = Thy, Tyop = tyop, Args = args} 262 263fun do_qtyop {Thy,Tyop=tyop,Locn,Args} = Tyop {Thy=Thy,Tyop=tyop,Args=Args} 264 265val termantiq_constructors = 266 {vartype = fn x => Vartype (fst x), qtyop = do_qtyop, 267 tyop = tyop_to_qtyop, 268 antiq = fn x => fromType (remove_ty_aq x)} 269 270val typantiq_constructors = 271 {vartype = fn x => Vartype (fst x), qtyop = do_qtyop, 272 tyop = tyop_to_qtyop, 273 antiq = fromType} 274 275fun has_unbound_uvar pty = 276 case pty of 277 Vartype _ => return false 278 | UVar r => boundcase r (return true) has_unbound_uvar 279 | Tyop{Args,...} => huul Args 280and huul [] = return false 281 | huul (ty1 :: tys) = 282 has_unbound_uvar ty1 >- (fn b => if b then return true 283 else huul tys) 284 285end; 286