typeSystem.lem

open import Pervasives_extra
open import Lib
open import Ast
open import Namespace
open import SemanticPrimitives

(* 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

(* 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 * tid_or_exn)
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

type decls =
  <| defined_mods : set (list modN);
     defined_types : set (id modN typeN);
     defined_exns : set (id modN conN) |>

val empty_decls : decls
let empty_decls = <|defined_mods = {}; defined_types = {}; defined_exns = {}|>

val union_decls : decls -> decls -> decls
let union_decls d1 d2 =
  <| defined_mods = d1.defined_mods union d2.defined_mods;
     defined_types = d1.defined_types union d2.defined_types;
     defined_exns = d1.defined_exns union d2.defined_exns |>

(* Check a declaration and update the top-level environments
 * The arguments are in order:
 * - the module that the declaration is in
 * - the set of all modules, and types, and exceptions that have been previously declared
 * - the type environment
 * - the declaration
 * - the set of all modules, and types, and exceptions that are declared here
 * - the environment of new stuff declared here *)

val type_d : bool -> list modN -> decls -> type_env -> dec -> decls -> type_env -> bool

val type_ds : bool -> list modN -> decls -> type_env -> list dec -> decls -> type_env -> bool
val check_signature : list modN -> tenv_abbrev -> decls -> type_env -> maybe specs -> decls -> type_env -> bool
val type_specs : list modN -> tenv_abbrev -> specs -> decls -> type_env -> bool
val type_prog : bool -> decls -> type_env -> list top -> decls -> 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, [Tapp [t2'; t3'] TC_fn; t2]) -> (t2 = t2') && (t = t3')
    | (Opn _, [Tapp [] TC_int; Tapp [] TC_int]) -> (t = Tint)
    | (Opb _, [Tapp [] TC_int; Tapp [] TC_int]) -> (t = Tapp [] (TC_name (Short "bool")))
    | (Opw W8 _, [Tapp [] TC_word8; Tapp [] TC_word8]) -> (t = Tapp [] TC_word8)
    | (Opw W64 _, [Tapp [] TC_word64; Tapp [] TC_word64]) -> (t = Tapp [] TC_word64)
    | (FP_bop _, [Tapp [] TC_word64; Tapp [] TC_word64] ) -> (t = Tapp [] TC_word64)
    | (FP_uop _, [Tapp [] TC_word64] ) -> (t = Tapp [] TC_word64)
    | (FP_cmp _, [Tapp [] TC_word64; Tapp [] TC_word64] ) -> (t = Tapp [] (TC_name (Short "bool")))
    | (Shift W8 _ _, [Tapp [] TC_word8]) -> (t = Tapp [] TC_word8)
    | (Shift W64 _ _, [Tapp [] TC_word64]) -> (t = Tapp [] TC_word64)
    | (Equality, [t1; t2]) -> (t1 = t2) && (t = Tapp [] (TC_name (Short "bool")))
    | (Opassign, [Tapp [t1] TC_ref; t2]) -> (t1 = t2) && (t = Tapp [] TC_tup)
    | (Opref, [t1]) -> (t = Tapp [t1] TC_ref)
    | (Opderef, [Tapp [t1] TC_ref]) -> (t = t1)
    | (Aw8alloc, [Tapp [] TC_int; Tapp [] TC_word8]) -> (t = Tapp [] TC_word8array)
    | (Aw8sub, [Tapp [] TC_word8array; Tapp [] TC_int]) -> (t = Tapp [] TC_word8)
    | (Aw8length, [Tapp [] TC_word8array]) -> (t = Tapp [] TC_int)
    | (Aw8update, [Tapp [] TC_word8array; Tapp [] TC_int; Tapp [] TC_word8]) -> t = Tapp [] TC_tup
    | (WordFromInt W8, [Tapp [] TC_int]) -> t = Tapp [] TC_word8
    | (WordToInt W8, [Tapp [] TC_word8]) -> t = Tapp [] TC_int
    | (WordFromInt W64, [Tapp [] TC_int]) -> t = Tapp [] TC_word64
    | (WordToInt W64, [Tapp [] TC_word64]) -> t = Tapp [] TC_int
    | (CopyStrStr, [Tapp [] TC_string; Tapp [] TC_int; Tapp [] TC_int]) -> t = Tapp [] TC_string
    | (CopyStrAw8, [Tapp [] TC_string; Tapp [] TC_int; Tapp [] TC_int; Tapp [] TC_word8array; Tapp [] TC_int]) -> t = Tapp [] TC_tup
    | (CopyAw8Str, [Tapp [] TC_word8array; Tapp [] TC_int; Tapp [] TC_int]) -> t = Tapp [] TC_string
    | (CopyAw8Aw8, [Tapp [] TC_word8array; Tapp [] TC_int; Tapp [] TC_int; Tapp [] TC_word8array; Tapp [] TC_int]) -> t = Tapp [] TC_tup
    | (Chr, [Tapp [] TC_int]) -> (t = Tchar)
    | (Ord, [Tapp [] TC_char]) -> (t = Tint)
    | (Chopb _, [Tapp [] TC_char; Tapp [] TC_char]) -> (t = Tapp [] (TC_name (Short "bool")))
    | (Implode, [Tapp [Tapp [] TC_char] (TC_name (Short "list"))]) -> t = Tapp [] TC_string
    | (Strsub, [Tapp [] TC_string; Tapp [] TC_int]) -> t = Tchar
    | (Strlen, [Tapp [] TC_string]) -> t = Tint
    | (Strcat, [Tapp [Tapp [] TC_string] (TC_name (Short "list"))]) -> t = Tapp [] TC_string
    | (ListAppend, [Tapp [t1] (TC_name (Short "list")); Tapp [t2] (TC_name (Short "list"))]) -> (t1 = t2) && t = Tapp [t1] (TC_name (Short "list"))
    | (VfromList, [Tapp [t1] (TC_name (Short "list"))]) -> t = Tapp [t1] TC_vector
    | (Vsub, [Tapp [t1] TC_vector; Tapp [] TC_int]) -> t = t1
    | (Vlength, [Tapp [t1] TC_vector]) -> (t = Tapp [] TC_int)
    | (Aalloc, [Tapp [] TC_int; t1]) -> t = Tapp [t1] TC_array
    | (AallocEmpty, [Tapp [] TC_tup]) -> exists t1. t = Tapp [t1] TC_array
    | (Asub, [Tapp [t1] TC_array; Tapp [] TC_int]) -> t = t1
    | (Alength, [Tapp [t1] TC_array]) -> t = Tapp [] TC_int
    | (Aupdate, [Tapp [t1] TC_array; Tapp [] TC_int; t2]) -> t1 = t2 && t = Tapp [] TC_tup
    | (ConfigGC, [Tapp [] TC_int; Tapp [] TC_int]) -> t = Tapp [] TC_tup
    | (FFI n, [Tapp [] TC_string; Tapp [] TC_word8array]) -> t = Tapp [] TC_tup
    | _ -> false
  end

val check_type_names : tenv_abbrev -> t -> bool
let rec
check_type_names tenvT (Tvar tv) =
  true
and
check_type_names tenvT (Tapp ts tn) =
  match tn with
     TC_name tn ->
       match nsLookup tenvT tn with
         | Just (tvs, t) -> List.length tvs = List.length ts
         | Nothing -> false
       end
   | _ -> true
  end &&
  List.all (check_type_names tenvT) ts
and
check_type_names tenvT (Tvar_db n) =
  true

(* Substitution of type names for the type they abbreviate *)
val type_name_subst : tenv_abbrev -> t -> t
let rec
type_name_subst tenvT (Tvar tv) = Tvar tv
and
type_name_subst tenvT (Tapp ts tc) =
  let args = List.map (type_name_subst tenvT) ts in
    match tc with
      | TC_name tn ->
          match nsLookup tenvT tn with
            | Just (tvs, t) -> type_subst (alistToFmap (List_extra.zipSameLength tvs args)) t
            | Nothing -> Tapp args tc
          end
      | _ -> Tapp args tc
    end
and
type_name_subst tenvT (Tvar_db n) = Tvar_db n

(* 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 t)) -> bool
let check_ctor_tenv tenvT tds =
  check_dup_ctors tds &&
  List.all
    (fun (tvs,tn,ctors) ->
       List.allDistinct tvs &&
       List.all
         (fun (cn,ts) -> List.all (check_freevars 0 tvs) ts && List.all (check_type_names tenvT) ts)
         ctors)
    tds &&
  List.allDistinct (List.map (fun (_,tn,_) -> tn) tds)

val build_ctor_tenv : list modN -> tenv_abbrev -> list (list tvarN * typeN * list (conN * list t)) -> tenv_ctor
let build_ctor_tenv mn tenvT tds =
  alist_to_ns
    (List.reverse
      (List.concat
        (List.map
           (fun (tvs,tn,ctors) ->
              List.map (fun (cn,ts) -> (cn,(tvs,List.map (type_name_subst tenvT) ts, TypeId (mk_id mn tn)))) ctors)
           tds)))

(* Check that an exception definition defines no already defined (or duplicate)
 * constructors, and that the arguments have no free type variables. *)
val check_exn_tenv : list modN -> conN -> list t -> bool
let check_exn_tenv mn cn ts =
  List.all (check_freevars 0 []) ts

(* 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

val tid_exn_to_tc : tid_or_exn -> tctor
let tid_exn_to_tc t =
  match t with
    | TypeId tid -> TC_name tid
    | TypeExn _ -> TC_exn
  end

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' (tid_exn_to_tc 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) (Tapp ts TC_tup) 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 0 [] 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' (tid_exn_to_tc tn))

and

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

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 (Tapp [] (TC_name (Short "bool"))) &&
type_e tenv tenvE e2 (Tapp [] (TC_name (Short "bool")))
==>
type_e tenv tenvE (Log l e1 e2) (Tapp [] (TC_name (Short "bool")))

and

if' : forall tenv tenvE e1 e2 e3 t.
type_e tenv tenvE e1 (Tapp [] (TC_name (Short "bool"))) &&
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 0 [] 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

indreln [type_d : bool -> list modN -> decls -> type_env -> dec -> decls -> type_env -> bool]

dlet_poly : forall extra_checks tvs mn tenv p e t bindings decls 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 mn decls tenv (Dlet locs p e)
  empty_decls <| v = alist_to_ns (tenv_add_tvs tvs bindings); c = nsEmpty; t = nsEmpty |>

and

dlet_mono : forall extra_checks mn tenv p e t bindings decls 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 mn decls tenv (Dlet locs p e)
  empty_decls <| v = alist_to_ns (tenv_add_tvs 0 bindings); c = nsEmpty; t = nsEmpty |>

and

dletrec : forall extra_checks mn tenv funs bindings tvs decls 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 mn decls tenv (Dletrec locs funs)
  empty_decls <| v = alist_to_ns (tenv_add_tvs tvs bindings); c = nsEmpty; t = nsEmpty |>

and

dtype : forall extra_checks mn tenv tdefs decls defined_types' decls' tenvT locs.
check_ctor_tenv (nsAppend tenvT tenv.t) tdefs &&
defined_types' = Set.fromList (List.map (fun (tvs,tn,ctors) -> (mk_id mn tn)) tdefs) &&
disjoint defined_types' decls.defined_types &&
tenvT = alist_to_ns (List.map (fun (tvs,tn,ctors) -> (tn, (tvs, Tapp (List.map Tvar tvs) (TC_name (mk_id mn tn))))) tdefs) &&
decls' = <| defined_mods = {}; defined_types = defined_types'; defined_exns = {} |>
==>
type_d extra_checks mn decls tenv (Dtype locs tdefs)
  decls' <| v = nsEmpty; c = build_ctor_tenv mn (nsAppend tenvT tenv.t) tdefs; t = tenvT |>

and

dtabbrev : forall extra_checks mn decls tenv tvs tn t locs.
check_freevars 0 tvs t &&
check_type_names tenv.t t &&
List.allDistinct tvs
==>
type_d extra_checks mn decls tenv (Dtabbrev locs tvs tn t)
  empty_decls <| v = nsEmpty; c = nsEmpty;
                 t = nsSing tn (tvs,type_name_subst tenv.t t) |>

and

dexn : forall extra_checks mn tenv cn ts decls decls' locs.
check_exn_tenv mn cn ts &&
not (mk_id mn cn IN decls.defined_exns) &&
List.all (check_type_names tenv.t) ts &&
decls' = <| defined_mods = {}; defined_types = {}; defined_exns = {mk_id mn cn} |>
==>
type_d extra_checks mn decls tenv (Dexn locs cn ts)
  decls' <| v = nsEmpty;
            c = nsSing cn ([], List.map (type_name_subst tenv.t) ts, TypeExn (mk_id mn cn));
            t = nsEmpty |>

indreln [ type_ds : bool -> list modN -> decls -> type_env -> list dec -> decls -> type_env -> bool]

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

and

cons : forall extra_checks mn tenv d ds tenv1 tenv2 decls decls1 decls2.
type_d extra_checks mn decls tenv d decls1 tenv1 &&
type_ds extra_checks mn (union_decls decls1 decls) (extend_dec_tenv tenv1 tenv) ds decls2 tenv2
==>
type_ds extra_checks mn decls tenv (d::ds)
  (union_decls decls2 decls1) (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)