typeSystem.lem

(*
  Specification of CakeML's type system.
*)
open import Pervasives_extra
open import Lib
open import Ast
open import Namespace
open import SemanticPrimitives


type type_ident = nat

(* Types *)
type t =
  (* Type variables that the user writes down ('a, 'b, etc.) *)
  | Tvar of tvarN
  (* deBruijn indexed type variables. *)
  | Tvar_db of nat
  (* The two numbers represent the identity of the type constructor. The first
     is the identity of the compilation unit that it was defined in, and the
     second is its identity inside of that unit *)
  | Tapp of list t * type_ident

(* Some abbreviations *)
let Tarray_num : type_ident = 0
let Tbool_num : type_ident = 1
let Tchar_num : type_ident = 2
let Texn_num : type_ident = 3
let Tfn_num : type_ident = 4
let Tint_num : type_ident = 5
let Tlist_num : type_ident = 6
let Tref_num : type_ident = 7
let Tstring_num : type_ident = 8
let Ttup_num : type_ident = 9
let Tvector_num : type_ident = 10
let Tword64_num : type_ident = 11
let Tword8_num : type_ident = 12
let Tword8array_num : type_ident = 13

(* The numbers for the primitive types *)
let prim_type_nums =
  [Tarray_num; Tchar_num; Texn_num; Tfn_num; Tint_num; Tref_num; Tstring_num; Ttup_num;
   Tvector_num; Tword64_num; Tword8_num; Tword8array_num]

let Tarray t = Tapp [t] Tarray_num
let Tbool = Tapp [] Tbool_num
let Tchar = Tapp [] Tchar_num
let Texn = Tapp [] Texn_num
let Tfn t1 t2 = Tapp [t1;t2] Tfn_num
let Tint = Tapp [] Tint_num
let Tlist t = Tapp [t] Tlist_num
let Tref t = Tapp [t] Tref_num
let Tstring = Tapp [] Tstring_num
let Ttup ts = Tapp ts Ttup_num
let Tvector t = Tapp [t] Tvector_num
let Tword64 = Tapp [] Tword64_num
let Tword8 = Tapp [] Tword8_num
let Tword8array = Tapp [] Tword8array_num

(* Check that the free type variables are in the given list. Every deBruijn
 * variable must be smaller than the first argument. So if it is 0, no deBruijn
 * indices are permitted. *)
val check_freevars : nat -> list tvarN -> t -> bool
let rec
check_freevars dbmax tvs (Tvar tv) =
  elem tv tvs
and
check_freevars dbmax tvs (Tapp ts tn) =
  List.all (check_freevars dbmax tvs) ts
and
check_freevars dbmax tvs (Tvar_db n) = n < dbmax

val check_freevars_ast : list tvarN -> ast_t -> bool
let rec
check_freevars_ast tvs (Atvar tv) =
  elem tv tvs
and
check_freevars_ast tvs (Attup ts) =
  List.all (check_freevars_ast tvs) ts
and
check_freevars_ast tvs (Atfun t1 t2) =
  check_freevars_ast tvs t1 && check_freevars_ast tvs t2
and
check_freevars_ast tvs (Atapp ts tn) =
  List.all (check_freevars_ast tvs) ts


(* Simultaneous substitution of types for type variables in a type *)
val type_subst : Map.map tvarN t -> t -> t
let rec
type_subst s (Tvar tv) =
  match Map.lookup tv s with
    | Nothing -> Tvar tv
    | Just(t) -> t
  end
and
type_subst s (Tapp ts tn) =
  Tapp (List.map (type_subst s) ts) tn
and
type_subst s (Tvar_db n) = Tvar_db n

(* Increment the deBruijn indices in a type by n levels, skipping all levels
 * less than skip. *)
val deBruijn_inc : nat -> nat -> t -> t
let rec
deBruijn_inc skip n (Tvar tv) = Tvar tv
and
deBruijn_inc skip n (Tvar_db m) =
  if m < skip then
    Tvar_db m
  else
    Tvar_db (m + n)
and
deBruijn_inc skip n (Tapp ts tn) = Tapp (List.map (deBruijn_inc skip n) ts) tn

(* skip the lowest given indices and replace the next (LENGTH ts) with the given types and reduce all the higher ones *)
val deBruijn_subst : nat -> list t -> t -> t
let rec
deBruijn_subst skip ts (Tvar tv) = Tvar tv
and
deBruijn_subst skip ts (Tvar_db n) =
  if not (n < skip) && (n < List.length ts + skip) then
    List_extra.nth ts (n - skip)
  else if not (n < skip) then
    Tvar_db (n - List.length ts)
  else
    Tvar_db n
and
deBruijn_subst skip ts (Tapp ts' tn) =
  Tapp (List.map (deBruijn_subst skip ts) ts') tn

(* Type environments *)
type tenv_val_exp =
  | Empty
  (* Binds several de Bruijn type variables *)
  | Bind_tvar of nat * tenv_val_exp
  (* The number is how many de Bruijn type variables the typescheme binds *)
  | Bind_name of varN * nat * t * tenv_val_exp

val bind_tvar : nat -> tenv_val_exp -> tenv_val_exp
let bind_tvar tvs tenvE = if tvs = 0 then tenvE else Bind_tvar tvs tenvE

val opt_bind_name : maybe varN -> nat -> t -> tenv_val_exp -> tenv_val_exp
let opt_bind_name n tvs t tenvE =
  match n with
    | Nothing -> tenvE
    | Just n' -> Bind_name n' tvs t tenvE
  end

val tveLookup : varN -> nat -> tenv_val_exp -> maybe (nat * t)
let rec
tveLookup n inc Empty = Nothing
and
tveLookup n inc (Bind_tvar tvs tenvE) = tveLookup n (inc + tvs) tenvE
and
tveLookup n inc (Bind_name n' tvs t tenvE) =
  if n' = n then
    Just (tvs, deBruijn_inc tvs inc t)
  else
    tveLookup n inc tenvE
declare termination_argument tveLookup = automatic

type tenv_abbrev = namespace modN typeN (list tvarN * t)
type tenv_ctor = namespace modN conN (list tvarN * list t * type_ident)
type tenv_val = namespace modN varN (nat * t)

type type_env =
  <| v : tenv_val
   ; c : tenv_ctor
   ; t : tenv_abbrev
   |>

val extend_dec_tenv : type_env -> type_env -> type_env
let extend_dec_tenv tenv' tenv =
  <| v = nsAppend tenv'.v tenv.v;
     c = nsAppend tenv'.c tenv.c;
     t = nsAppend tenv'.t tenv.t |>

val lookup_varE : id modN varN -> tenv_val_exp -> maybe (nat * t)
let lookup_varE id tenvE =
  match id with
  | Short x -> tveLookup x 0 tenvE
  | _ -> Nothing
  end

val lookup_var : id modN varN -> tenv_val_exp -> type_env -> maybe (nat * t)
let lookup_var id tenvE tenv =
  match lookup_varE id tenvE with
  | Just x -> Just x
  | Nothing -> nsLookup tenv.v id
  end

val num_tvs : tenv_val_exp -> nat
let rec
num_tvs Empty = 0
and
num_tvs (Bind_tvar tvs tenvE) = tvs + num_tvs tenvE
and
num_tvs (Bind_name n tvs t tenvE) = num_tvs tenvE

declare termination_argument num_tvs = automatic

val bind_var_list : nat -> list (varN * t) -> tenv_val_exp -> tenv_val_exp
let rec
bind_var_list tvs [] tenvE = tenvE
and
bind_var_list tvs ((n,t)::binds) tenvE =
  Bind_name n tvs t (bind_var_list tvs binds tenvE)

declare termination_argument bind_var_list = automatic

(* A pattern matches values of a certain type and extends the type environment
 * with the pattern's binders. The number is the maximum deBruijn type variable
 * allowed. *)
val type_p : nat -> type_env -> pat -> t -> list (varN * t) -> bool

(* An expression has a type *)
val type_e : type_env -> tenv_val_exp -> exp -> t -> bool

(* A list of expressions has a list of types *)
val type_es : type_env -> tenv_val_exp -> list exp -> list t -> bool

(* Type a mutually recursive bundle of functions.  Unlike pattern typing, the
 * resulting environment does not extend the input environment, but just
 * represents the functions *)
val type_funs : type_env -> tenv_val_exp -> list (varN * varN * exp) -> list (varN * t) -> bool

(* Check a declaration and update the top-level environments
 * The arguments are in order:
 * - whether to do extra checks
 * - the type environment
 * - the declaration
 * - the set of type identity stamps defined here
 * - the environment of new stuff declared here *)

val type_d : bool -> type_env -> dec -> set nat -> type_env -> bool
val type_ds : bool -> type_env -> list dec -> set nat -> type_env -> bool

(* Check that the operator can have type (t1 -> ... -> tn -> t) *)
val type_op : op -> list t -> t -> bool
let type_op op ts t =
  match (op,ts) with
    | (Opapp, [t1; t2]) -> t1 = Tfn t2 t
    | (Opn _, [t1; t2]) -> t1 = Tint && t2 = Tint && t = Tint
    | (Opb _, [t1; t2]) -> t1 = Tint && t2 = Tint && t = Tbool
    | (Opw W8 _, [t1; t2]) -> t1 = Tword8 && t2 = Tword8 && t = Tword8
    | (Opw W64 _, [t1; t2]) -> t1 = Tword64 && t2 = Tword64 && t = Tword64
    | (FP_bop _, [t1; t2]) -> t1 = Tword64 && t2 = Tword64 && t = Tword64
    | (FP_uop _, [t1]) ->  t1 = Tword64 && t = Tword64
    | (FP_cmp _, [t1; t2]) ->  t1 = Tword64 && t2 = Tword64 && t = Tbool
    | (Shift W8 _ _, [t1]) -> t1 = Tword8 && t = Tword8
    | (Shift W64 _ _, [t1]) -> t1 = Tword64 && t = Tword64
    | (Equality, [t1; t2]) -> t1 = t2 && t = Tbool
    | (Opassign, [t1; t2]) -> t1 = Tref t2 && t = Ttup []
    | (Opref, [t1]) -> t = Tref t1
    | (Opderef, [t1]) -> t1 = Tref t
    | (Aw8alloc, [t1; t2]) -> t1 = Tint && t2 = Tword8 && t = Tword8array
    | (Aw8sub, [t1; t2]) -> t1 = Tword8array && t2 = Tint && t = Tword8
    | (Aw8length, [t1]) -> t1 = Tword8array && t = Tint
    | (Aw8update, [t1; t2; t3]) -> t1 = Tword8array && t2 = Tint && t3 = Tword8 && t = Ttup []
    | (WordFromInt W8, [t1]) -> t1 = Tint && t = Tword8
    | (WordToInt W8, [t1]) -> t1 = Tword8 && t = Tint
    | (WordFromInt W64, [t1]) -> t1 = Tint && t = Tword64
    | (WordToInt W64, [t1]) -> t1 = Tword64 && t = Tint
    | (CopyStrStr, [t1; t2; t3]) -> t1 = Tstring && t2 = Tint && t3 = Tint && t = Tstring
    | (CopyStrAw8, [t1; t2; t3; t4; t5]) ->
      t1 = Tstring && t2 = Tint && t3 = Tint && t4 = Tword8array && t5 = Tint && t = Ttup []
    | (CopyAw8Str, [t1; t2; t3]) -> t1 = Tword8array && t2 = Tint && t3 = Tint && t = Tstring
    | (CopyAw8Aw8, [t1; t2; t3; t4; t5]) ->
      t1 = Tword8array && t2 = Tint && t3 = Tint && t4 = Tword8array && t5 = Tint && t = Ttup []
    | (Chr, [t1]) -> t1 = Tint && t = Tchar
    | (Ord, [t1]) -> t1 = Tchar && t = Tint
    | (Chopb _, [t1; t2]) -> t1 = Tchar && t2 = Tchar && t = Tbool
    | (Implode, [t1]) -> t1 = Tlist Tchar && t = Tstring
    | (Strsub, [t1; t2]) -> t1 = Tstring && t2 = Tint && t = Tchar
    | (Strlen, [t1]) -> t1 = Tstring && t = Tint
    | (Strcat, [t1]) -> t1 = Tlist Tstring && t = Tstring
    | (VfromList, [Tapp [t1] ctor]) -> ctor = Tlist_num && t = Tvector t1
    | (Vsub, [t1; t2]) -> t2 = Tint && Tvector t = t1
    | (Vlength, [Tapp [t1] ctor]) -> ctor = Tvector_num && t = Tint
    | (Aalloc, [t1; t2]) -> t1 = Tint && t = Tarray t2
    | (AallocEmpty, [t1]) -> t1 = Ttup [] && exists t2. t = Tarray t2
    | (Asub, [t1; t2]) -> t2 = Tint && Tarray t = t1
    | (Alength, [Tapp [t1] ctor]) -> ctor = Tarray_num && t = Tint
    | (Aupdate, [t1; t2; t3]) -> t1 = Tarray t3 && t2 = Tint && t = Ttup []
    | (ConfigGC, [t1;t2]) -> t1 = Tint && t2 = Tint && t = Ttup []
    | (FFI n, [t1;t2]) -> t1 = Tstring && t2 = Tword8array && t = Ttup []
    | (ListAppend, [Tapp [t1] ctor; t2]) -> ctor = Tlist_num && t2 = Tapp [t1] ctor && t = t2
    | _ -> false
  end

val check_type_names : tenv_abbrev -> ast_t -> bool
let rec
check_type_names tenvT (Atvar tv) =
  true
and
check_type_names tenvT (Attup ts) =
  List.all (check_type_names tenvT) ts
and
check_type_names tenvT (Atfun t1 t2) =
  check_type_names tenvT t1 && check_type_names tenvT t2
and
check_type_names tenvT (Atapp ts tn) =
  match nsLookup tenvT tn with
  | Just (tvs, _) -> List.length tvs = List.length ts
  | Nothing -> false
  end &&
  List.all (check_type_names tenvT) ts

(* Substitution of type names for the type they abbreviate *)
val type_name_subst : tenv_abbrev -> ast_t -> t
let rec
type_name_subst tenvT (Atvar tv) = Tvar tv
and
type_name_subst tenvT (Attup ts) =
  Ttup (List.map (type_name_subst tenvT) ts)
and
type_name_subst tenvT (Atfun t1 t2) =
  Tfn (type_name_subst tenvT t1) (type_name_subst tenvT t2)
and
type_name_subst tenvT (Atapp ts tc) =
  let args = List.map (type_name_subst tenvT) ts in
  match nsLookup tenvT tc with
  | Just (tvs, t) -> type_subst (alistToFmap (List_extra.zipSameLength tvs args)) t
  | Nothing -> Ttup args (* can't happen, for a type that passes the check *)
  end

(* Check that a type definition defines no already defined types or duplicate
 * constructors, and that the free type variables of each constructor argument
 * type are included in the type's type parameters. Also check that all of the
 * types mentioned are in scope. *)
val check_ctor_tenv : tenv_abbrev -> list (list tvarN * typeN * list (conN * list ast_t)) -> bool
let rec check_ctor_tenv tenvT [] = true
and check_ctor_tenv tenvT ((tvs,tn,ctors)::tds) =
  check_dup_ctors (tvs,tn,ctors) &&
  List.allDistinct tvs &&
  List.all
    (fun (cn,ts) -> List.all (check_freevars_ast tvs) ts && List.all (check_type_names tenvT) ts)
    ctors &&
  not (List.elem tn (List.map (fun (_,tn,_) -> tn) tds)) &&
  check_ctor_tenv tenvT tds
declare termination_argument check_ctor_tenv = automatic

val build_ctor_tenv : tenv_abbrev -> list (list tvarN * typeN * list (conN * list ast_t)) -> list nat -> tenv_ctor
let rec build_ctor_tenv tenvT [] [] = alist_to_ns []
and build_ctor_tenv tenvT ((tvs,tn,ctors)::tds) (id::ids) =
  nsAppend
    (build_ctor_tenv tenvT tds ids)
    (alist_to_ns
      (List.reverse
        (List.map
          (fun (cn,ts) -> (cn,(tvs,List.map (type_name_subst tenvT) ts, id)))
          ctors)))
and build_ctor_tenv tenvT _ _ = alist_to_ns []
declare termination_argument build_ctor_tenv = automatic

(* For the value restriction on let-based polymorphism *)
val is_value : exp -> bool
let rec
is_value (Lit _) = true
and
is_value (Con _ es) = List.all is_value es
and
is_value (Var _) = true
and
is_value (Fun _ _) = true
and
is_value (Tannot e _) = is_value e
and
is_value (Lannot e _) = is_value e
and
is_value _ = false

indreln [type_p : nat -> type_env -> pat -> t -> list (varN * t) -> bool]
and [type_ps : nat -> type_env -> list pat -> list t -> list (varN * t) -> bool]

pany : forall tvs tenv t.
check_freevars tvs [] t
==>
type_p tvs tenv Pany t []

and

pvar : forall tvs tenv n t.
check_freevars tvs [] t
==>
type_p tvs tenv (Pvar n) t [(n,t)]

and

plit_int : forall tvs tenv n.
true
==>
type_p tvs tenv (Plit (IntLit n)) Tint []

and

plit_char : forall tvs tenv c.
true
==>
type_p tvs tenv (Plit (Char c)) Tchar []

and

plit_string : forall tvs tenv s.
true
==>
type_p tvs tenv (Plit (StrLit s)) Tstring []

and

plit_word8 : forall tvs tenv w.
true
==>
type_p tvs tenv (Plit (Word8 w)) Tword8 []

and

plit_word64 : forall tvs tenv w.
true
==>
type_p tvs tenv (Plit (Word64 w)) Tword64 []

and

pcon_some : forall tvs tenv cn ps ts tvs' tn ts' bindings.
List.all (check_freevars tvs []) ts' &&
List.length ts' = List.length tvs' &&
type_ps tvs tenv ps (List.map (type_subst (alistToFmap (List_extra.zipSameLength tvs' ts'))) ts) bindings &&
nsLookup tenv.c cn = Just (tvs', ts, tn)
==>
type_p tvs tenv (Pcon (Just cn) ps) (Tapp ts' tn) bindings

and

pcon_none : forall tvs tenv ps ts bindings.
type_ps tvs tenv ps ts bindings
==>
type_p tvs tenv (Pcon Nothing ps) (Ttup ts) bindings

and

pref : forall tvs tenv p t bindings.
type_p tvs tenv p t bindings
==>
type_p tvs tenv (Pref p) (Tref t) bindings

and

ptypeannot : forall tvs tenv p t bindings.
check_freevars_ast [] t &&
check_type_names tenv.t t &&
type_p tvs tenv p (type_name_subst tenv.t t) bindings
==>
type_p tvs tenv (Ptannot p t) (type_name_subst tenv.t t) bindings

and

empty : forall tvs tenv.
true
==>
type_ps tvs tenv [] [] []

and

cons : forall tvs tenv p ps t ts bindings bindings'.
type_p tvs tenv p t bindings &&
type_ps tvs tenv ps ts bindings'
==>
type_ps tvs tenv (p::ps) (t::ts) (bindings'++bindings)

indreln [type_e : type_env -> tenv_val_exp -> exp -> t -> bool]
and [type_es : type_env -> tenv_val_exp -> list exp -> list t -> bool]
and [type_funs : type_env -> tenv_val_exp -> list (varN * varN * exp) -> list (varN * t) -> bool]

lit_int : forall tenv tenvE n.
true
==>
type_e tenv tenvE (Lit (IntLit n)) Tint

and

lit_char : forall tenv tenvE c.
true
==>
type_e tenv tenvE (Lit (Char c)) Tchar

and

lit_string : forall tenv tenvE s.
true
==>
type_e tenv tenvE (Lit (StrLit s)) Tstring

and

lit_word8 : forall tenv tenvE w.
true
==>
type_e tenv tenvE (Lit (Word8 w)) Tword8

and

lit_word64 : forall tenv tenvE w.
true
==>
type_e tenv tenvE (Lit (Word64 w)) Tword64

and

raise : forall tenv tenvE e t.
check_freevars (num_tvs tenvE) [] t &&
type_e tenv tenvE e Texn
==>
type_e tenv tenvE (Raise e) t


and

handle : forall tenv tenvE e pes t.
type_e tenv tenvE e t &&
pes <> [] &&
(forall ((p,e) MEM pes). exists bindings.
   List.allDistinct (pat_bindings p []) &&
   type_p (num_tvs tenvE) tenv p Texn bindings &&
   type_e tenv (bind_var_list 0 bindings tenvE) e t)
==>
type_e tenv tenvE (Handle e pes) t

and

con_some : forall tenv tenvE cn es tvs tn ts' ts.
List.all (check_freevars (num_tvs tenvE) []) ts' &&
List.length tvs = List.length ts' &&
type_es tenv tenvE es (List.map (type_subst (alistToFmap (List_extra.zipSameLength tvs ts'))) ts) &&
nsLookup tenv.c cn = Just (tvs, ts, tn)
==>
type_e tenv tenvE (Con (Just cn) es) (Tapp ts' tn)

and

con_none : forall tenv tenvE es ts.
type_es tenv tenvE es ts
==>
type_e tenv tenvE (Con Nothing es) (Ttup ts)

and

var : forall tenv tenvE n t targs tvs.
tvs = List.length targs &&
List.all (check_freevars (num_tvs tenvE) []) targs &&
lookup_var n tenvE tenv = Just (tvs,t)
==>
type_e tenv tenvE (Var n) (deBruijn_subst 0 targs t)

and

fn : forall tenv tenvE n e t1 t2.
check_freevars (num_tvs tenvE) [] t1 &&
type_e tenv (Bind_name n 0 t1 tenvE) e t2
==>
type_e tenv tenvE (Fun n e) (Tfn t1 t2)

and

app : forall tenv tenvE op es ts t.
type_es tenv tenvE es ts &&
type_op op ts t &&
check_freevars (num_tvs tenvE) [] t
==>
type_e tenv tenvE (App op es) t

and

log : forall tenv tenvE l e1 e2.
type_e tenv tenvE e1 Tbool &&
type_e tenv tenvE e2 Tbool
==>
type_e tenv tenvE (Log l e1 e2) Tbool

and

if' : forall tenv tenvE e1 e2 e3 t.
type_e tenv tenvE e1 Tbool &&
type_e tenv tenvE e2 t &&
type_e tenv tenvE e3 t
==>
type_e tenv tenvE (If e1 e2 e3) t

and

mat : forall tenv tenvE e pes t1 t2.
type_e tenv tenvE e t1 &&
pes <> [] &&
(forall ((p,e) MEM pes) . exists bindings.
   List.allDistinct (pat_bindings p []) &&
   type_p (num_tvs tenvE) tenv p t1 bindings &&
   type_e tenv (bind_var_list 0 bindings tenvE) e t2)
==>
type_e tenv tenvE (Mat e pes) t2

and

(*
let_poly : forall tenv tenvE n e1 e2 t1 t2 tvs.
is_value e1 &&
type_e tenv (bind_tvar tvs tenvE) e1 t1 &&
type_e tenv (opt_bind_name n tvs t1 tenvE) e2 t2
==>
type_e tenv tenvE (Let n e1 e2) t2

and
*)

let_mono : forall tenv tenvE n e1 e2 t1 t2.
type_e tenv tenvE e1 t1 &&
type_e tenv (opt_bind_name n 0 t1 tenvE) e2 t2
==>
type_e tenv tenvE (Let n e1 e2) t2

(*
and

letrec : forall tenv tenvE funs e t tenv' tvs.
type_funs tenv (bind_var_list 0 tenv' (bind_tvar tvs tenvE)) funs tenv' &&
type_e tenv (bind_var_list tvs tenv' tenvE) e t
==>
type_e tenv tenvE (Letrec funs e) t
*)

and

letrec : forall tenv tenvE funs e t bindings.
type_funs tenv (bind_var_list 0 bindings tenvE) funs bindings &&
type_e tenv (bind_var_list 0 bindings tenvE) e t
==>
type_e tenv tenvE (Letrec funs e) t

and

typeannot: forall tenv tenvE e t.
check_freevars_ast [] t &&
check_type_names tenv.t t &&
type_e tenv tenvE e (type_name_subst tenv.t t)
==>
type_e tenv tenvE (Tannot e t) (type_name_subst tenv.t t)

and

locannot: forall tenv tenvE e l t.
type_e tenv tenvE e t
==>
type_e tenv tenvE (Lannot e l) t

and

empty : forall tenv tenvE.
true
==>
type_es tenv tenvE [] []

and

cons : forall tenv tenvE e es t ts.
type_e tenv tenvE e t &&
type_es tenv tenvE es ts
==>
type_es tenv tenvE (e::es) (t::ts)

and

no_funs : forall tenv tenvE.
true
==>
type_funs tenv tenvE [] []

and

funs : forall tenv tenvE fn n e funs bindings t1 t2.
check_freevars (num_tvs tenvE) [] (Tfn t1 t2) &&
type_e tenv (Bind_name n 0 t1 tenvE) e t2 &&
type_funs tenv tenvE funs bindings &&
lookup fn bindings = Nothing
==>
type_funs tenv tenvE ((fn, n, e)::funs) ((fn, Tfn t1 t2)::bindings)

val tenv_add_tvs : nat -> alist varN t -> alist varN (nat * t)
let tenv_add_tvs tvs bindings =
  List.map (fun (n,t) -> (n,(tvs,t))) bindings

val type_pe_determ : type_env -> tenv_val_exp -> pat -> exp -> bool
let type_pe_determ tenv tenvE p e =
  forall t1 tenv1 t2 tenv2.
    type_p 0 tenv p t1 tenv1 && type_e tenv tenvE e t1 &&
    type_p 0 tenv p t2 tenv2 && type_e tenv tenvE e t2
    -->
    tenv1 = tenv2

val tscheme_inst : (nat * t) -> (nat * t) -> bool
let tscheme_inst (tvs_spec, t_spec) (tvs_impl, t_impl) =
  exists subst.
    List.length subst = tvs_impl &&
    check_freevars tvs_impl [] t_impl &&
    List.all (check_freevars tvs_spec []) subst &&
    deBruijn_subst 0 subst t_impl = t_spec

let tenvLift mn tenv =
  <| v = nsLift mn tenv.v; c = nsLift mn tenv.c; t = nsLift mn tenv.t; |>

indreln [type_d : bool -> type_env -> dec -> set nat -> type_env -> bool] and
        [type_ds : bool -> type_env -> list dec -> set nat -> type_env -> bool]

dlet_poly : forall extra_checks tvs tenv p e t bindings locs.
is_value e &&
List.allDistinct (pat_bindings p []) &&
type_p tvs tenv p t bindings &&
type_e tenv (bind_tvar tvs Empty) e t &&
(extra_checks -->
  forall tvs' bindings' t'.
    type_p tvs' tenv p t' bindings' &&
    type_e tenv (bind_tvar tvs' Empty) e t' -->
      all2 tscheme_inst (List.map snd (tenv_add_tvs tvs' bindings')) (List.map snd (tenv_add_tvs tvs bindings)))
==>
type_d extra_checks tenv (Dlet locs p e)
  {}
  <| v = alist_to_ns (tenv_add_tvs tvs bindings); c = nsEmpty; t = nsEmpty |>

and

dlet_mono : forall extra_checks tenv p e t bindings locs.
(* The following line makes sure that when the value restriction prohibits
   generalisation, a type error is given rather than picking an arbitrary
   instantiation. However, we should only do the check when the extra_checks
   argument tells us to. *)
(extra_checks --> not (is_value e) && type_pe_determ tenv Empty p e) &&
List.allDistinct (pat_bindings p []) &&
type_p 0 tenv p t bindings &&
type_e tenv Empty e t
==>
type_d extra_checks tenv (Dlet locs p e)
  {} <| v = alist_to_ns (tenv_add_tvs 0 bindings); c = nsEmpty; t = nsEmpty |>

and

dletrec : forall extra_checks tenv funs bindings tvs locs.
type_funs tenv (bind_var_list 0 bindings (bind_tvar tvs Empty)) funs bindings &&
(extra_checks -->
  forall tvs' bindings'.
    type_funs tenv (bind_var_list 0 bindings' (bind_tvar tvs' Empty)) funs bindings' -->
      all2 tscheme_inst (List.map snd (tenv_add_tvs tvs' bindings')) (List.map snd (tenv_add_tvs tvs bindings)))
==>
type_d extra_checks tenv (Dletrec locs funs)
  {} <| v = alist_to_ns (tenv_add_tvs tvs bindings); c = nsEmpty; t = nsEmpty |>

and

dtype : forall extra_checks tenv tdefs type_identities tenvT locs.
List.allDistinct type_identities &&
disjoint (Set.fromList type_identities)
         (Set.fromList (Tlist_num :: Tbool_num :: prim_type_nums)) &&
check_ctor_tenv (nsAppend tenvT tenv.t) tdefs &&
List.length type_identities = List.length tdefs &&
tenvT = alist_to_ns (Lib.map2
                      (fun (tvs,tn,ctors) i ->
                        (tn, (tvs, Tapp (List.map Tvar tvs) i)))
                      tdefs type_identities)
==>
type_d extra_checks tenv (Dtype locs tdefs)
  (Set.fromList type_identities)
  <| v = nsEmpty; c = build_ctor_tenv (nsAppend tenvT tenv.t) tdefs type_identities; t = tenvT |>

and

dtabbrev : forall extra_checks tenv tvs tn t locs.
check_freevars_ast tvs t &&
check_type_names tenv.t t &&
List.allDistinct tvs
==>
type_d extra_checks tenv (Dtabbrev locs tvs tn t)
  {}
  <| v = nsEmpty; c = nsEmpty; t = nsSing tn (tvs,type_name_subst tenv.t t) |>

and

dexn : forall extra_checks tenv cn ts locs.
List.all (check_freevars_ast []) ts &&
List.all (check_type_names tenv.t) ts
==>
type_d extra_checks tenv (Dexn locs cn ts)
  {}
  <| v = nsEmpty;
     c = nsSing cn ([], List.map (type_name_subst tenv.t) ts, Texn_num);
     t = nsEmpty |>

and

dexn : forall extra_checks tenv mn ds decls tenv'.
type_ds extra_checks tenv ds decls tenv'
==>
type_d extra_checks tenv (Dmod mn ds) decls (tenvLift mn tenv')

and

empty : forall extra_checks tenv.
true
==>
type_ds extra_checks tenv []
  {}
  <| v = nsEmpty; c = nsEmpty; t = nsEmpty |>

and

cons : forall extra_checks tenv d ds tenv1 tenv2 decls1 decls2.
type_d extra_checks tenv d decls1 tenv1 &&
type_ds extra_checks (extend_dec_tenv tenv1 tenv) ds decls2 tenv2 &&
disjoint decls1 decls2
==>
type_ds extra_checks tenv (d::ds)
  (decls1 union decls2) (extend_dec_tenv tenv2 tenv1)

(*
indreln [type_specs : list modN -> tenv_abbrev -> specs -> decls -> type_env -> bool]

empty : forall mn tenvT.
true
==>
type_specs mn tenvT []
  empty_decls <| v = nsEmpty; c = nsEmpty; t = nsEmpty |>

and

sval : forall mn tenvT x t specs tenv fvs decls subst.
check_freevars 0 fvs t &&
check_type_names tenvT t &&
type_specs mn tenvT specs decls tenv &&
subst = alistToFmap (List_extra.zipSameLength fvs (List.map Tvar_db (genlist (fun x -> x) (List.length fvs))))
==>
type_specs mn tenvT (Sval x t :: specs)
  decls
  (extend_dec_tenv tenv
    <| v = nsSing x (List.length fvs, type_subst subst (type_name_subst tenvT t));
       c = nsEmpty;
       t = nsEmpty |>)

and

stype : forall mn tenvT tenv td specs decls' decls tenvT'.
tenvT' = alist_to_ns (List.map (fun (tvs,tn,ctors) -> (tn, (tvs, Tapp (List.map Tvar tvs) (TC_name (mk_id mn tn))))) td) &&
check_ctor_tenv (nsAppend tenvT' tenvT) td &&
type_specs mn (nsAppend tenvT' tenvT) specs decls tenv &&
decls' = <| defined_mods = {};
            defined_types = Set.fromList (List.map (fun (tvs,tn,ctors) -> (mk_id mn tn)) td);
            defined_exns = {} |>
==>
type_specs mn tenvT (Stype td :: specs)
  (union_decls decls decls')
  (extend_dec_tenv tenv
   <| v = nsEmpty;
      c = build_ctor_tenv mn (nsAppend tenvT' tenvT) td;
      t = tenvT' |>)

and

stabbrev : forall mn tenvT tenvT' tvs tn t specs decls tenv.
List.allDistinct tvs &&
check_freevars 0 tvs t &&
check_type_names tenvT t &&
tenvT' = nsSing tn (tvs,type_name_subst tenvT t) &&
type_specs mn (nsAppend tenvT' tenvT) specs decls tenv
==>
type_specs mn tenvT (Stabbrev tvs tn t :: specs)
  decls (extend_dec_tenv tenv <| v = nsEmpty; c = nsEmpty; t = tenvT' |>)

and

sexn : forall mn tenvT tenv cn ts specs decls.
check_exn_tenv mn cn ts &&
type_specs mn tenvT specs decls tenv &&
List.all (check_type_names tenvT) ts
==>
type_specs mn tenvT (Sexn cn ts :: specs)
  (union_decls decls <| defined_mods = {}; defined_types = {}; defined_exns = {mk_id mn cn} |>)
  (extend_dec_tenv tenv
   <| v = nsEmpty;
      c = nsSing cn ([], List.map (type_name_subst tenvT) ts, TypeExn (mk_id mn cn));
      t = nsEmpty |>)

and

stype_opq : forall mn tenvT tenv tn specs tvs decls tenvT'.
List.allDistinct tvs &&
tenvT' = nsSing tn (tvs, Tapp (List.map Tvar tvs) (TC_name (mk_id mn tn))) &&
type_specs mn (nsAppend tenvT' tenvT) specs decls tenv
==>
type_specs mn tenvT (Stype_opq tvs tn :: specs)
  (union_decls decls <| defined_mods = {}; defined_types = {mk_id mn tn}; defined_exns = {} |>)
  (extend_dec_tenv tenv <| v = nsEmpty; c = nsEmpty; t = tenvT' |>)

val weak_decls : decls -> decls -> bool
let weak_decls decls_impl decls_spec =
  decls_impl.defined_mods = decls_spec.defined_mods &&
  decls_spec.defined_types subset decls_impl.defined_types &&
  decls_spec.defined_exns subset decls_impl.defined_exns
   *)

(*
val weak_tenvT : id modN typeN -> (list tvarN * t) -> (list tvarN * t) -> bool
let weak_tenvT n (tvs_spec, t_spec) (tvs_impl, t_impl) =
  (* For simplicity, we reject matches that differ only by renaming of bound type variables *)
  tvs_spec = tvs_impl &&
  (t_spec = t_impl ||
   (* The specified type is opaque *)
   t_spec = Tapp (List.map Tvar tvs_spec) (TC_name n))
   *)

let tscheme_inst2 _ ts1 ts2 = tscheme_inst ts1 ts2

val weak_tenv : type_env -> type_env -> bool
let weak_tenv tenv_impl tenv_spec =
  nsSub tscheme_inst2 tenv_spec.v tenv_impl.v &&
  nsSub (fun _ x y -> x = y) tenv_spec.c tenv_impl.c(* &&
  nsSub weak_tenvT tenv_spec.t tenv_impl.t*)

(*
indreln [check_signature : list modN -> tenv_abbrev -> decls -> type_env -> maybe specs -> decls -> type_env -> bool]

none : forall mn tenvT decls tenv.
true
==>
check_signature mn tenvT decls tenv Nothing decls tenv

and

some : forall mn specs tenv_impl tenv_spec decls_impl decls_spec tenvT.
weak_tenv tenv_impl tenv_spec &&
weak_decls decls_impl decls_spec &&
type_specs mn tenvT specs decls_spec tenv_spec
==>
check_signature mn tenvT decls_impl tenv_impl (Just specs) decls_spec tenv_spec

let tenvLift mn tenv =
  <| v = nsLift mn tenv.v; c = nsLift mn tenv.c; t = nsLift mn tenv.t; |>

indreln [type_top : bool -> decls -> type_env -> top -> decls -> type_env -> bool]

tdec : forall extra_checks tenv d tenv' decls decls'.
type_d extra_checks [] decls tenv d decls' tenv'
==>
type_top extra_checks decls tenv (Tdec d) decls' tenv'

and

tmod : forall extra_checks tenv mn spec ds tenv_impl tenv_spec decls decls_impl decls_spec.
not ([mn] IN decls.defined_mods) &&
type_ds extra_checks [mn] decls tenv ds decls_impl tenv_impl &&
check_signature [mn] tenv.t decls_impl tenv_impl spec decls_spec tenv_spec
==>
type_top extra_checks decls tenv (Tmod mn spec ds)
  (union_decls <| defined_mods = {[mn]}; defined_types = {}; defined_exns = {} |> decls_spec)
  (tenvLift mn tenv_spec)

indreln [type_prog : bool -> decls -> type_env -> list top -> decls -> type_env -> bool]

empty : forall extra_checks tenv decls.
true
==>
type_prog extra_checks decls tenv [] empty_decls <| v = nsEmpty; c = nsEmpty; t = nsEmpty |>

and

cons : forall extra_checks tenv top tops tenv1 tenv2 decls decls1 decls2.
type_top extra_checks decls tenv top decls1 tenv1 &&
type_prog extra_checks (union_decls decls1 decls) (extend_dec_tenv tenv1 tenv) tops decls2 tenv2
==>
type_prog extra_checks decls tenv (top :: tops)
  (union_decls decls2 decls1) (extend_dec_tenv tenv2 tenv1)
  *)