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