preterm.ml

   1 (* ========================================================================= *)
   2 (* Preterms and pretypes; typechecking; translation to types and terms.      *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (*                 (c) Copyright, Marco Maggesi 2012                         *)
   9 (*               (c) Copyright, Vincent Aravantinos 2012                     *)
  10 (* ========================================================================= *)
  11
  12 needs "printer.ml";;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* Flag to say whether to treat varstruct "\const. bod" as variable.         *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let ignore_constant_varstruct = ref true;;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Flags controlling the treatment of invented type variables in quotations. *)
  22 (* It can be treated as an error, result in a warning, or neither of those.  *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let type_invention_warning = ref true;;
  26
  27 let type_invention_error = ref false;;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Implicit types or type schemes for non-constants.                         *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let the_implicit_types = ref ([]:(string*hol_type)list);;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* Overloading and interface mapping.                                        *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let make_overloadable s gty =
  40   if can (assoc s) (!the_overload_skeletons)
  41   then if assoc s (!the_overload_skeletons) = gty then ()
  42        else failwith "make_overloadable: differs from existing skeleton"
  43   else the_overload_skeletons := (s,gty)::(!the_overload_skeletons);;
  44
  45 let remove_interface sym =
  46   let interface = filter ((<>)sym o fst) (!the_interface) in
  47   the_interface := interface;;
  48
  49 let reduce_interface (sym,tm) =
  50   let namty = try dest_const tm with Failure _ -> dest_var tm in
  51   the_interface := filter ((<>) (sym,namty)) (!the_interface);;
  52
  53 let override_interface (sym,tm) =
  54   let namty = try dest_const tm with Failure _ -> dest_var tm in
  55   let interface = filter ((<>)sym o fst) (!the_interface) in
  56   the_interface := (sym,namty)::interface;;
  57
  58 let overload_interface (sym,tm) =
  59   let gty = try assoc sym (!the_overload_skeletons) with Failure _ ->
  60             failwith ("symbol \""^sym^"\" is not overloadable") in
  61   let (name,ty) as namty = try dest_const tm with Failure _ -> dest_var tm in
  62   if not (can (type_match gty ty) [])
  63   then failwith "Not an instance of type skeleton" else
  64   let interface = filter ((<>) (sym,namty)) (!the_interface) in
  65   the_interface := (sym,namty)::interface;;
  66
  67 let prioritize_overload ty =
  68   do_list
  69    (fun (s,gty) ->
  70       try let _,(n,t) = find
  71             (fun (s',(n,t)) -> s' = s & mem ty (map fst (type_match gty t [])))
  72             (!the_interface) in
  73           overload_interface(s,mk_var(n,t))
  74       with Failure _ -> ())
  75    (!the_overload_skeletons);;
  76
  77 (* ------------------------------------------------------------------------- *)
  78 (* Type abbreviations.                                                       *)
  79 (* ------------------------------------------------------------------------- *)
  80
  81 let new_type_abbrev,remove_type_abbrev,type_abbrevs =
  82   let the_type_abbreviations = ref ([]:(string*hol_type)list) in
  83   let remove_type_abbrev s =
  84     the_type_abbreviations :=
  85       filter (fun (s',_) -> s' <> s) (!the_type_abbreviations) in
  86   let new_type_abbrev(s,ty) =
  87     (remove_type_abbrev s;
  88      the_type_abbreviations := merge(<) [s,ty] (!the_type_abbreviations)) in
  89   let type_abbrevs() = !the_type_abbreviations in
  90   new_type_abbrev,remove_type_abbrev,type_abbrevs;;
  91
  92 (* ------------------------------------------------------------------------- *)
  93 (* Handle constant hiding.                                                   *)
  94 (* ------------------------------------------------------------------------- *)
  95
  96 let hide_constant,unhide_constant,is_hidden =
  97   let hcs = ref ([]:string list) in
  98   let hide_constant c = hcs := union [c] (!hcs)
  99   and unhide_constant c = hcs := subtract (!hcs) [c]
 100   and is_hidden c = mem c (!hcs) in
 101   hide_constant,unhide_constant,is_hidden;;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* The type of pretypes.                                                     *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 type pretype = Utv of string                   (* User type variable         *)
 108              | Ptycon of string * pretype list (* Type constructor           *)
 109              | Stv of int;;                    (* System type variable       *)
 110
 111 (* ------------------------------------------------------------------------- *)
 112 (* Dummy pretype for the parser to stick in before a proper typing pass.     *)
 113 (* ------------------------------------------------------------------------- *)
 114
 115 let dpty = Ptycon("",[]);;
 116
 117 (* ------------------------------------------------------------------------- *)
 118 (* Convert type to pretype.                                                  *)
 119 (* ------------------------------------------------------------------------- *)
 120
 121 let rec pretype_of_type ty =
 122   try let con,args = dest_type ty in
 123       Ptycon(con,map pretype_of_type args)
 124   with Failure _ -> Utv(dest_vartype ty);;
 125
 126 (* ------------------------------------------------------------------------- *)
 127 (* Preterm syntax.                                                           *)
 128 (* ------------------------------------------------------------------------- *)
 129
 130 type preterm = Varp of string * pretype       (* Variable           - v      *)
 131              | Constp of string * pretype     (* Constant           - c      *)
 132              | Combp of preterm * preterm     (* Combination        - f x    *)
 133              | Absp of preterm * preterm      (* Lambda-abstraction - \x. t  *)
 134              | Typing of preterm * pretype;;  (* Type constraint    - t : ty *)
 135
 136 (* ------------------------------------------------------------------------- *)
 137 (* Convert term to preterm.                                                  *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 let rec preterm_of_term tm =
 141   try let n,ty = dest_var tm in
 142       Varp(n,pretype_of_type ty)
 143   with Failure _ -> try
 144       let n,ty = dest_const tm in
 145       Constp(n,pretype_of_type ty)
 146   with Failure _ -> try
 147       let v,bod = dest_abs tm in
 148       Absp(preterm_of_term v,preterm_of_term bod)
 149   with Failure _ ->
 150       let l,r = dest_comb tm in
 151       Combp(preterm_of_term l,preterm_of_term r);;
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* Main pretype->type, preterm->term and retypechecking functions.           *)
 155 (* ------------------------------------------------------------------------- *)
 156
 157 let type_of_pretype,term_of_preterm,retypecheck =
 158   let tyv_num = ref 0 in
 159   let new_type_var() = let n = !tyv_num in (tyv_num := n + 1; Stv(n)) in
 160
 161   let pmk_cv(s,pty) =
 162     if can get_const_type s then Constp(s,pty)
 163     else Varp(s,pty) in
 164
 165   let pmk_numeral =
 166     let num_pty = Ptycon("num",[]) in
 167     let NUMERAL = Constp("NUMERAL",Ptycon("fun",[num_pty; num_pty]))
 168     and BIT0 = Constp("BIT0",Ptycon("fun",[num_pty; num_pty]))
 169     and BIT1 = Constp("BIT1",Ptycon("fun",[num_pty; num_pty]))
 170     and t_0 = Constp("_0",num_pty) in
 171     let rec pmk_numeral(n) =
 172       if n =/ num_0 then t_0 else
 173       let m = quo_num n (num_2) and b = mod_num n (num_2) in
 174       let op = if b =/ num_0 then BIT0 else BIT1 in
 175       Combp(op,pmk_numeral(m)) in
 176     fun n -> Combp(NUMERAL,pmk_numeral n) in
 177
 178   (* ----------------------------------------------------------------------- *)
 179   (* Pretype substitution for a pretype resulting from translation of type.  *)
 180   (* ----------------------------------------------------------------------- *)
 181
 182   let rec pretype_subst th ty =
 183     match ty with
 184       Ptycon(tycon,args) -> Ptycon(tycon,map (pretype_subst th) args)
 185     | Utv v -> rev_assocd ty th ty
 186     | _ -> failwith "pretype_subst: Unexpected form of pretype" in
 187
 188   (* ----------------------------------------------------------------------- *)
 189   (* Convert type to pretype with new Stvs for all type variables.           *)
 190   (* ----------------------------------------------------------------------- *)
 191
 192   let pretype_instance ty =
 193     let gty = pretype_of_type ty
 194     and tyvs = map pretype_of_type (tyvars ty) in
 195     let subs = map (fun tv -> new_type_var(),tv) tyvs in
 196     pretype_subst subs gty in
 197
 198   (* ----------------------------------------------------------------------- *)
 199   (* Get a new instance of a constant's generic type modulo interface.       *)
 200   (* ----------------------------------------------------------------------- *)
 201
 202   let get_generic_type cname =
 203     match filter ((=) cname o fst) (!the_interface) with
 204       [_,(c,ty)] -> ty
 205     | _::_::_ -> assoc cname (!the_overload_skeletons)
 206     | [] -> get_const_type cname in
 207
 208   (* ----------------------------------------------------------------------- *)
 209   (* Get the implicit generic type of a variable.                            *)
 210   (* ----------------------------------------------------------------------- *)
 211
 212   let get_var_type vname =
 213     assoc vname !the_implicit_types in
 214
 215   (* ----------------------------------------------------------------------- *)
 216   (* Unravel unifications and apply them to a type.                          *)
 217   (* ----------------------------------------------------------------------- *)
 218
 219   let rec solve env pty =
 220     match pty with
 221       Ptycon(f,args) -> Ptycon(f,map (solve env) args)
 222     | Stv(i) -> if defined env i then solve env (apply env i) else pty
 223     | _ -> pty in
 224
 225   (* ----------------------------------------------------------------------- *)
 226   (* Functions for display of preterms and pretypes, by converting them      *)
 227   (* to terms and types then re-using standard printing functions.           *)
 228   (* ----------------------------------------------------------------------- *)
 229
 230   let free_stvs =
 231     let rec free_stvs = function
 232     |Stv n -> [n]
 233     |Utv _ -> []
 234     |Ptycon(_,args) -> flat (map free_stvs args)
 235     in
 236     setify o free_stvs
 237   in
 238
 239   let string_of_pretype stvs =
 240     let rec type_of_pretype' ns = function
 241       |Stv n -> mk_vartype (if mem n ns then "?" ^ string_of_int n else "_")
 242       |Utv v -> mk_vartype v
 243       |Ptycon(con,args) -> mk_type(con,map (type_of_pretype' ns) args)
 244     in
 245     string_of_type o type_of_pretype' stvs
 246   in
 247
 248   let string_of_preterm =
 249     let rec untyped_t_of_pt = function
 250       |Varp(s,pty) -> mk_var(s,aty)
 251       |Constp(s,pty) -> mk_mconst(s,get_const_type s)
 252       |Combp(l,r) -> mk_comb(untyped_t_of_pt l,untyped_t_of_pt r)
 253       |Absp(v,bod) -> mk_gabs(untyped_t_of_pt v,untyped_t_of_pt bod)
 254       |Typing(ptm,pty) -> untyped_t_of_pt ptm
 255     in
 256     string_of_term o untyped_t_of_pt
 257   in
 258
 259   let string_of_ty_error env = function
 260     |None ->
 261         "unify: types cannot be unified "
 262         ^ "(you should not see this message, please report)"
 263     |Some(t,ty1,ty2) ->
 264         let ty1 = solve env ty1 and ty2 = solve env ty2 in
 265         let sty1 = string_of_pretype (free_stvs ty2) ty1 in
 266         let sty2 = string_of_pretype (free_stvs ty1) ty2 in
 267         let default_msg s =
 268           " " ^ s ^ " cannot have type " ^ sty1 ^ " and " ^ sty2
 269           ^ " simultaneously"
 270         in
 271         match t with
 272         |Constp(s,_) ->
 273             " " ^ s ^ " has type " ^ string_of_type (get_const_type s) ^ ", "
 274             ^ "it cannot be used with type " ^ sty2
 275         |Varp(s,_) -> default_msg s
 276         |t -> default_msg (string_of_preterm t)
 277   in
 278
 279   (* ----------------------------------------------------------------------- *)
 280   (* Unification of types                                                    *)
 281   (* ----------------------------------------------------------------------- *)
 282
 283   let rec istrivial ptm env x = function
 284     |Stv y as t ->
 285         y = x or defined env y & istrivial ptm env x (apply env y)
 286     |Ptycon(f,args) as t when exists (istrivial ptm env x) args ->
 287         failwith (string_of_ty_error env ptm)
 288     |(Ptycon _ | Utv _) -> false
 289   in
 290
 291   let unify ptm env ty1 ty2 =
 292     let rec unify env = function
 293     |[] -> env
 294     |(ty1,ty2,_)::oth when ty1 = ty2 -> unify env oth
 295     |(Ptycon(f,fargs),Ptycon(g,gargs),ptm)::oth ->
 296         if f = g & length fargs = length gargs
 297         then unify env (map2 (fun x y -> x,y,ptm) fargs gargs @ oth)
 298         else failwith (string_of_ty_error env ptm)
 299     |(Stv x,t,ptm)::oth ->
 300         if defined env x then unify env ((apply env x,t,ptm)::oth)
 301         else unify (if istrivial ptm env x t then env else (x|->t) env) oth
 302     |(t,Stv x,ptm)::oth -> unify env ((Stv x,t,ptm)::oth)
 303     |(_,_,ptm)::oth -> failwith (string_of_ty_error env ptm)
 304     in
 305     unify env [ty1,ty2,match ptm with None -> None | Some t -> Some(t,ty1,ty2)]
 306   in
 307
 308   (* ----------------------------------------------------------------------- *)
 309   (* Attempt to attach a given type to a term, performing unifications.      *)
 310   (* ----------------------------------------------------------------------- *)
 311
 312   let rec typify ty (ptm,venv,uenv) =
 313     match ptm with
 314     |Varp(s,_) when can (assoc s) venv ->
 315         let ty' = assoc s venv in
 316         Varp(s,ty'),[],unify (Some ptm) uenv ty' ty
 317     |Varp(s,_) when can num_of_string s ->
 318         let t = pmk_numeral(num_of_string s) in
 319         let ty' = Ptycon("num",[]) in
 320         t,[],unify (Some ptm) uenv ty' ty
 321     |Varp(s,_) ->
 322         warn (s <> "" & isnum s) "Non-numeral begins with a digit";
 323           if not(is_hidden s) & can get_generic_type s then
 324             let pty = pretype_instance(get_generic_type s) in
 325             let ptm = Constp(s,pty) in
 326             ptm,[],unify (Some ptm) uenv pty ty
 327           else
 328             let ptm = Varp(s,ty) in
 329             if not(can get_var_type s) then ptm,[s,ty],uenv
 330             else
 331               let pty = pretype_instance(get_var_type s) in
 332               ptm,[s,ty],unify (Some ptm) uenv pty ty
 333     |Combp(f,x) ->
 334         let ty'' = new_type_var() in
 335         let ty' = Ptycon("fun",[ty'';ty]) in
 336         let f',venv1,uenv1 = typify ty' (f,venv,uenv) in
 337         let x',venv2,uenv2 = typify ty'' (x,venv1@venv,uenv1) in
 338         Combp(f',x'),(venv1@venv2),uenv2
 339     |Typing(tm,pty) -> typify ty (tm,venv,unify (Some tm) uenv ty pty)
 340     |Absp(v,bod) ->
 341         let ty',ty'' =
 342           match ty with
 343           |Ptycon("fun",[ty';ty'']) -> ty',ty''
 344           |_ -> new_type_var(),new_type_var()
 345         in
 346         let ty''' = Ptycon("fun",[ty';ty'']) in
 347         let uenv0 = unify (Some ptm) uenv ty''' ty in
 348         let v',venv1,uenv1 =
 349           let v',venv1,uenv1 = typify ty' (v,[],uenv0) in
 350           match v' with
 351           |Constp(s,_) when !ignore_constant_varstruct ->
 352               Varp(s,ty'),[s,ty'],uenv0
 353           |_ -> v',venv1,uenv1
 354         in
 355         let bod',venv2,uenv2 = typify ty'' (bod,venv1@venv,uenv1) in
 356         Absp(v',bod'),venv2,uenv2
 357     |_ -> failwith "typify: unexpected constant at this stage"
 358   in
 359
 360   (* ----------------------------------------------------------------------- *)
 361   (* Further specialize type constraints by resolving overloadings.          *)
 362   (* ----------------------------------------------------------------------- *)
 363
 364   let rec resolve_interface ptm cont env =
 365     match ptm with
 366       Combp(f,x) -> resolve_interface f (resolve_interface x cont) env
 367     | Absp(v,bod) -> resolve_interface v (resolve_interface bod cont) env
 368     | Varp(_,_) -> cont env
 369     | Constp(s,ty) ->
 370           let maps = filter (fun (s',_) -> s' = s) (!the_interface) in
 371           if maps = [] then cont env else
 372           tryfind (fun (_,(_,ty')) ->
 373             let ty' = pretype_instance ty' in
 374             cont(unify (Some ptm) env ty' ty)) maps
 375   in
 376
 377   (* ----------------------------------------------------------------------- *)
 378   (* Hence apply throughout a preterm.                                       *)
 379   (* ----------------------------------------------------------------------- *)
 380
 381   let rec solve_preterm env ptm =
 382     match ptm with
 383       Varp(s,ty) -> Varp(s,solve env ty)
 384     | Combp(f,x) -> Combp(solve_preterm env f,solve_preterm env x)
 385     | Absp(v,bod) -> Absp(solve_preterm env v,solve_preterm env bod)
 386     | Constp(s,ty) -> let tys = solve env ty in
 387           try let _,(c',_) = find
 388                 (fun (s',(c',ty')) ->
 389                    s = s' & can (unify None env (pretype_instance ty')) ty)
 390                 (!the_interface) in
 391               pmk_cv(c',tys)
 392           with Failure _ -> Constp(s,tys)
 393   in
 394
 395   (* ----------------------------------------------------------------------- *)
 396   (* Flag to indicate that Stvs were translated to real type variables.      *)
 397   (* ----------------------------------------------------------------------- *)
 398
 399   let stvs_translated = ref false in
 400
 401   (* ----------------------------------------------------------------------- *)
 402   (* Pretype <-> type conversion; -> flags system type variable translation. *)
 403   (* ----------------------------------------------------------------------- *)
 404
 405   let rec type_of_pretype ty =
 406     match ty with
 407       Stv n -> stvs_translated := true;
 408                let s = "?"^(string_of_int n) in
 409                mk_vartype(s)
 410     | Utv(v) -> mk_vartype(v)
 411     | Ptycon(con,args) -> mk_type(con,map type_of_pretype args) in
 412
 413   (* ----------------------------------------------------------------------- *)
 414   (* Maps preterms to terms.                                                 *)
 415   (* ----------------------------------------------------------------------- *)
 416
 417   let term_of_preterm =
 418     let rec term_of_preterm ptm =
 419       match ptm with
 420         Varp(s,pty) -> mk_var(s,type_of_pretype pty)
 421       | Constp(s,pty) -> mk_mconst(s,type_of_pretype pty)
 422       | Combp(l,r) -> mk_comb(term_of_preterm l,term_of_preterm r)
 423       | Absp(v,bod) -> mk_gabs(term_of_preterm v,term_of_preterm bod)
 424       | Typing(ptm,pty) -> term_of_preterm ptm in
 425     let report_type_invention () =
 426       if !stvs_translated then
 427         if !type_invention_error
 428         then failwith "typechecking error (cannot infer type of variables)"
 429         else warn !type_invention_warning "inventing type variables" in
 430     fun ptm -> stvs_translated := false;
 431                let tm = term_of_preterm ptm in
 432                report_type_invention (); tm in
 433
 434   (* ----------------------------------------------------------------------- *)
 435   (* Overall typechecker: initial typecheck plus overload resolution pass.   *)
 436   (* ----------------------------------------------------------------------- *)
 437
 438   let retypecheck venv ptm =
 439     let ty = new_type_var() in
 440     let ptm',_,env =
 441       try typify ty (ptm,venv,undefined)
 442       with Failure e -> failwith
 443        ("typechecking error (initial type assignment):" ^ e) in
 444     let env' =
 445       try resolve_interface ptm' (fun e -> e) env
 446       with Failure _ -> failwith "typechecking error (overload resolution)" in
 447     let ptm'' = solve_preterm env' ptm' in
 448     ptm'' in
 449
 450   type_of_pretype,term_of_preterm,retypecheck;;