Lem User’s Manual:
version 0.2

Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell

http://www.cl.cam.ac.uk/~so294/lem/


Lem is a lightweight tool for writing, managing, and publishing large scale semantic definitions. It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems (such as Coq, HOL4, and Isabelle).

It resembles a pure subset of Objective Caml, supporting typical functional programming constructs, including top-level parametric polymorphism, datatypes, records, higher-order functions, and pattern matching. It also supports common logical mechanisms including list and set comprehensions, universal and existential quantifiers, and inductively defined relations. From this, Lem generates OCaml, HOL4 and Isabelle code; the OCaml backend uses a finite set library (and does not yet support inductive relations). A Coq backend is in development.

This is a preliminary release of Lem which is not yet feature complete (see Section 5). It is currently released under a restrictive license, but we intend to use an open source or free software license release for later, more complete releases.

1  Installing Lem

Lem depends on OCaml (http://caml.inria.fr/), and the Batteries Included library (http://batteries.forge.ocamlcore.org/) Batteries Included in turn depends on findlib (http://projects.camlcity.org/projects/findlib.html) and Camomile (http://camomile.sourceforge.net/). Lem is tested against OCaml 3.12.1, Batteries Included 1.4.0, findlib 1.2.7 and Camomile 0.8.3. Earlier versions have a good chance of working, but not OCaml prior to 3.12.0.

To build Lem run make in Lem’s top-level directory. This builds the executable lem, and places a symbolic link to it in Lem’s root directory. Now set the LEMLIB environment variable to path_to_lem/library, or alternately pass the -lib path_to_lem/library flag to lem when you run it. This tells Lem where to find its library of types for HOL/Isabelle/OCaml/Coq built-in functions.

2  Invoking Lem

Lem processes and type checks its .lem file arguments in order. Each of the -hol, -isa, -tex, -coq, and -ocaml flags cause Lem to produce output for the corresponding system, one output file per input file. For example,

lem name1.lem name2.lem -ocaml -hol -isa 

creates 6 files (assuming there are no type errors in the source files), name1.ml, name2.ml, Name1Script.sml, Name2Script.sml, Name1.thy, and Name2.thy.

Lem-generated OCaml relies on the files in ocaml_lib, and so they must be compiled to link with path_to_lem/ocaml-lib/_build/extract.cma (or extract.cmxa). For example,

ocamlc -I path_to_lem/ocaml-lib/_build -o name extract.cma name1.ml

If the -tex option is specified, then for each input file name.lem the tool will create both a stand-alone LaTeX file name.tex that typesets the whole of that file and a file name-inc.tex of LaTeX definitions, one for each top-level Lem definition, that can be included in the preamble of another document, so that particular top-level Lem definitions can be quoted within it. Additionally, Lem will create a single alldoc.tex and alldoc-inc.tex with the content of all the Lem input files. Lem-generated LATEX makes use of macros defined in path_to_lem/tex-lib/lem.sty.

3  Syntax

Lem generally follows the syntax of the pure functional fragment of OCaml, with the following notable differences:

3.1  Literals

A literal constant lit is either

3.2  Variables and other names

A name x is a non-empty sequence of characters starting with a letter or the _ character, followed by letters, numbers and the _ and characters.

An identifier   id   is a non-empty sequence of names separated by the . character. An identifier is a module path, so all but the last name must refer to modules, and hence begin with capital letters.

A constructor name C is an identifier that refers to the definition of a data constructor.

A field name fn is an identifier that refers to a field of a defined record type.

An infix name ix is a non-empty sequence of symbolic characters: !$%&*+-./:<=>?@|~^ (except for sequences that are otherwise used as keywords, such as ->).

Infix operators are parsed in precedence on their first character in the following order, from tightest binding to weakest:

3.3  Patterns

As in OCaml, most binding forms in Lem use patterns which match against a value and can bind multiple names to various of its sub-values.

A pattern pat is either

3.4  Expressions

An expression exp is either

Quantification bindings support quantifying over and comprehending over a restricted domain. In a list of quantification bindings, no variable can be appear twice as a binder; however, later expressions can refer to earlier bindings. If a given pattern does not match all variables, then in a comprehension or forall context they are ignored. In an exist context, the witness must match the pattern.

A quantification binding qbind is either

3.5  Definitions

Several of the definition forms are parameterized by an optional targetopt that specifies a set of targets that the definition should be used for. This allows different definitions of a particular function to be used for the different targets.

3.5.1  Type definitions

Lem supports the definition of algebraic datatypes, record types, and type abbreviations. Each top-level type definition is a sequence of type definition expressions td:
type   td1   and   ...   and   tdn
where a type definition expression td is either

A constructor definition   ctor_def is either

tyvars is either

3.5.2  Inductive relations

An inductive relation is defined with a sequence of rules
indreln   targets?   rule1   and   ...   and   rulen
where each rulei is

3.5.3  Other definitions

A definition is either

3.6  Types

A   typ is either:

4  Libraries

4.1  Pervasives

4.2  List

4.3  Set

4.4  Pmap

5  Status

5.1  Working features

5.2  Features in development

6  Formal syntax

The l decorations on the grammar correspond to where the implementation records source type information; they cannot appear in source programs.


l ::=  Source locations
  |    
xl , yl , zl ::=  Location-annotated names
  |x   l   
  |( ix ) l  Remove infix status
ixl ::=  Location-annotated infix names
  |ix   l   
  |xl  Add infix status
α ::=  Type variables
  |x   
αl ::=  Location-annotated type variables
  |α   l   
id ::=  Long identifers
  |x1l .   ..   xnl . xl   l   
tyvars ::=  Type variable lists
  |( α1l ,   ..   , αnl )  Must have >1 type variables
  |αlS   
  | S   
typ_aux ::=  Types
  |_  Unspecified type
  |αl  Type variables
  |typ1typ2  Function types
  |typ1 *   ....   * typn  Tuple types
  |( typ1 ,   ..   , typn ) id  Type applications, must have >1 type arguments
  |typ   idS  Type applications (single argument)
  |idS  Type applications (no argument)
  |( typ )   
typ ::=  Location-annotated types
  |typ_aux   l   
lit_aux ::=  Literal constants
  |true   
  |false   
  |num   
  |string   
  |( )   
lit ::=   
  |lit_aux   l  Location-annotated literal constants
;? ::=  Optional semi-colons
  |    
  |;   
pat_aux ::=  Patterns
  |_  Wildcards
  |pat   as   xl  Named patterns
  |( pat : typ )  Typed patterns
  |id   pat1   ..   patn  Single variable and constructor patterns
  |⟨| fpat1 ;   ...   ; fpatn   ;? |⟩  Record patterns
  |( pat1 ,   ....   , patn )  Tuple patterns
  |[ pat1 ;   ..   ; patn   ;? ]  List patterns
  |( pat )   
  |pat1 :: pat2  Cons patterns
  |lit  Literal constant patterns
pat ::=  Location-annotated patterns
  |pat_aux   l   
fpat ::=  Field patterns
  |id = pat   l   
|? ::=  Optional bars
  |    
  |   
exp_aux ::=  Expressions
  |id  Identifiers
  |fun   psexp  Curried functions
  |function   |?   pexp1 ∣   ...   ∣ pexpn   end  Functions with pattern matching
  |exp1   exp2  Function applications
  |exp1   ixl   exp2  Infix applications
  |⟨| fexps |⟩  Records
  |⟨| exp   with   fexps |⟩  Functional update for records
  |exp . id  Field projection for records
  |match   exp   with   |?   pexp1 ∣   ...   ∣ pexpn   l   end  Pattern matching expressions
  |( exp : typ )  Type-annotated expressions
  |let   letbind   in   exp  Let expressions
  |( exp1 ,   ....   , expn )  Tuples
  |[ exp1 ;   ..   ; expn   ;? ]  Lists
  |( exp )   
  |begin   exp   end  Alternate syntax for (exp)
  |if   exp1   then   exp2   else   exp3  Conditionals
  |exp1 :: exp2  Cons expressions
  |lit  Literal constants
  |{ exp1exp2 }  Set comprehensions
  |{ exp1 ∣   forall   qbind1   ..   qbindnexp2 }  Set comprehensions with explicit binding
  |{ exp1 ;   ..   ; expn   ;? }  Sets
  |q   qbind1   ...   qbindn . exp  Logical quantifications
  |[ exp1 ∣   forall   qbind1   ..   qbindnexp2 ]  List comprehensions (all binders must be quantified)
exp ::=  Location-annotated expressions
  |exp_aux   l   
q ::=  Quantifiers
  |forall   
  |exist   
qbind ::=  Bindings for quantifiers
  |xl   
  |( pat   IN   exp )  Restricted quantifications over sets
  |( pat   MEM   exp )  Restricted quantifications over lists
fexp ::=  Field-expressions
  |id = exp   l   
fexps ::=  Field-expression lists
  |fexp1 ;   ...   ; fexpn   ;?   l   
pexp ::=  Pattern matches
  |patexp   l   
psexp ::=  Multi-pattern matches
  |pat1   ...   patnexp   l   
tannot? ::=  Optional type annotations
  |    
  |: typ   
funcl_aux ::=  Function clauses
  |xl   pat1   ...   patn   tannot? = exp   
letbind_aux ::=  Let bindings
  |pat   tannot? = exp  Value bindings
  |funcl_aux  Function bindings
letbind ::=  Location-annotated let bindings
  |letbind_aux   l   
funcl ::=  Location-annotated function clauses
  |funcl_aux   l   
rule_aux ::=  Inductively defined relation clauses
  |forall   x1l   ..   xnl . exp =⇒ xl   exp1   ..   expi   
rule ::=  Location-annotated inductively defined relation clauses
  |rule_aux   l   
typs ::=  Type lists
  |typ1 *   ...   * typn   
ctor_def ::=  Datatype definition clauses
  |xl   of   typs   
  |xlS  Constant constructors
texp ::=  Type definition bodies
  |typ  Type abbreviations
  |⟨| x1l : typ1 ;   ...   ; xnl : typn   ;? |⟩  Record types
  ||?   ctor_def1 ∣   ...   ∣ ctor_defn  Variant types
td ::=  Type definitions
  |tyvars   xl = texp   
  |tyvars   xl  Definitions of opaque types
c ::=  Typeclass constraints
  |( id   αl )   
cs ::=  Typeclass constraint lists
  |    
  |c1   ..   ci  Must have >0 constraints
c_pre ::=  Type and instance scheme prefixes
  |    
  |forall   α1l   ..   αnl . cs  Must have >0 type variables
typschm ::=  Type schemes
  |c_pre   typ   
instschm ::=  Instance schemes
  |c_pre ( id   typ )   
target ::=  Backend target names
  |hol   
  |isabelle   
  |ocaml   
  |coq   
  |tex   
targets ::=  Backend target name lists
  |{ target1 ;   ...   ; targetn }   
targets? ::=  Optional targets
  |    
  |targets   
val_def ::=  Value definitions
  |let   targets?   letbind  Non-recursive value definitions
  |let   rec   targets?   funcl1   and   ...   and   funcln  Recursive function definitions
val_spec ::=  Value type specifications
  |val   xl : typschm   
def_aux ::=  Top-level definitions
  |type   td1   and   ...   and   tdn  Type definitions
  |val_def  Value definitions
  |module   xl =   struct   defs   end  Module definitions
  |module   xl = id  Module renamings
  |open   id  Opening modules
  |indreln   targets?   rule1   and   ...   and   rulen  Inductively defined relations
  |val_spec  Top-level type constraints
  |sub   [ target ] xl   x1l   ..   xil = exp  Target-specific functions to inline
  |class   ( xl   αl )   val   x1l : typ1   l1   ...   val   xnl : typn   ln   end  Typeclass definitions
  |instance   instschm   val_def1   l1   ...   val_defn   ln   end  Typeclass instantiations
def ::=  Location-annotated definitions
  |def_aux   l   
;;? ::=  Optional double-semi-colon
  |    
  |;;   
defs ::=  Definition sequences
  |def1   ;;1?   ..   defn   ;;n?   

7  Formal type system


p ::=  Unique paths
  |x1 .   ..   xn . x   
  | __list   
  | __bool   
  | __num   
  | __set   
  | __string   
  | __unit   
σ ::=  Type variable substitutions
  |{ α1t1   ..   αntn }   
t , u ::=  Internal types
  |α   
  |t1t2   
  |t1 *   ....   * tn   
  |t_args   p   
  |σ ( t )M  Multiple substitutions
  |curry   ( t_multi , t )M  Curried, multiple argument functions
t_args ::=  Lists of types
  |( t1 ,   ..   , tn )   
  |σ ( t_args )M  Multiple substitutions
t_multi ::=  Lists of types
  |( t1 *   ..   * tn )   
  |σ ( t_multi )M  Multiple substitutions
tvs ::=  Type variable lists
  |α1   ..   αn   
names ::=  Sets of names
  |{ x1 ,   ..   , xn }   
C  ::=  Typeclass constraint lists
  |( p1   α1 )   ..   ( pn   αn )   
v_desc ::=  Value descriptions
  |⟨   forall   tvs . t_multip , ( x   of   names ) ⟩  Constructors
  |⟨   forall   tvs . pt , ( x   of   names ) ⟩  Fields
  |forall   tvs . Ct  Values
kind ::=  Sorts of value bindings
  |ctor   
  |field   
  |mthd   
  |let   
  |spec   
  |target   
κ ::=   
  |{ kind1 ;   ..   ; kindn }   
  |κ1   ∪   κ2M   
Σ ::=  Typeclass constraints
  |{ ( p1   t1 ) ,   ..   , ( pn   tn ) }   
  |Σ1   ∪   ..   ∪   ΣnM   
E ::=  Environments
  |Em , Ep , Ex   
  |E1E2M   
  |єM   
Ex  ::=  Value environments
  |{ x1 ↦ κ1   v_desc1 ,   ..   , xn ↦ κn   v_descn }   
  |E1x ⊎   ..   ⊎ Enx M   
Em  ::=  Module environments
  |{ x1E1 ,   ..   , xnEn }   
Ep  ::=  Path environments
  |{ x1p1 ,   ..   , xnpn }   
  |E1p ⊎   ..   ⊎ Enp M   
El  ::=  Lexical bindings
  |{ x1t1 ,   ..   , xntn }   
  |E1l ⊎   ..   ⊎ Enl M   
tc_abbrev ::=  Type abbreviations
  |. t   
  |    
tc_def ::=  Type and class constructor definitions
  |tvs   tc_abbrev  Type constructors
Δ ::=  Type constructor definitions
  |{ p1tc_def1 ,   ..   , pntc_defn }   
  |Δ1 ⊎ Δ2M   
δ ::=  Typeclass definitions
  |{ p1xs1 ,   ..   , pnxsn }   
  |δ1 ⊎ δ2M   
inst ::=  A typeclass instance, t must not contain nested types
  |C ⇒ ( p   t )   
I ::=  Global instances
  |{ inst1 ,   ..   , instn }   
  |I1   ∪   I2M   
D ::=  Global type definition store
  |⟨ Δ , δ , I   
  |D1D2M   
  |єM   
xs ::=   
  |x1   ..   xn   
formula ::=   
  |judgement   
  |formula1    ..    formulan   
  |Em ( x )   ▷   E  Module lookup
  |Ep ( x )   ▷   p  Path lookup
  |Ex ( x )   ▷   κ   v_desc  Value lookup
  |El ( x )   ▷   t  Lexical binding lookup
  |Δ ( p )   ▷   tc_def  Type constructor lookup
  |δ ( p )   ▷   xs  Type constructor lookup
  |dom   ( E1m )   ∩   dom   ( E2m ) =   ∅   
  |dom   ( E1x )   ∩   dom   ( E2x ) =   ∅   
  |dom   ( E1p )   ∩   dom   ( E2p ) =   ∅   
  |disjoint   doms   ( E1l ,   ..   , Enl )  Pairwise disjoint domains
  |disjoint   doms   ( E1x ,   ..   , Enx )  Pairwise disjoint domains
  |compatible   overlap   ( { x1t1 } ,   ..   , { xntn } )  (xi = xj) =⇒ (ti = tj)
  |duplicates   ( tvs ) =   ∅   
  |duplicates   ( x1 ,   ..   , xn ) =   ∅   
  |x   ∉   dom   ( El )   
  |x   ∉   dom   ( Ex )   
  |p   ∉   dom   ( δ )   
  |p   ∉   dom   ( Δ )   
  |kind   ∉   κ   
  | kind ∈ κ   
  |κ1   ∩   κ2 =   ∅   
  |κ1   ≠   κ2   
  |FV   ( t )   ⊂   tvs  Free type variables
  |FV   ( t_multi )   ⊂   tvs  Free type variables
  |FV   ( C )   ⊂   tvs  Free type variables
  |inst   IN   I   
  |( p   t )   ∉   I   
  |E1l = E2l   
  |E1x = E2x   
  |E1 = E2   
  |Δ1 = Δ2   
  |δ1 = δ2   
  |I1 = I2   
  |names1 = names2   
  |t1 = t2   
  |σ1 = σ2   
  |p1 = p2   
  |xs1 = xs2   
  |tvs1 = tvs2   

tyvarstvs   

(  α1   l1  ,   ..   ,  αn   ln  )  ↝  α1   ..   αn
  convert_tvs_none

E1 ( x1l   ..   xnl )   ▷   E2   Name path lookup

E  (     )   ▷   E
  look_m_none
 Em   (  x  )   ▷   E1 
 E1  (  y1l   ..   ynl  )   ▷   E2 
⟨  Em   ,  Ep   ,  Ex   ⟩  (  x   l   y1l   ..   ynl  )   ▷   E2
  look_m_some

E1 ( id )   ▷   E2   Module identifier lookup

 E1  (  y1l   ..   ynl   x   l1  )   ▷   E2 
E1  (  y1l  .   ..   ynl  .  x   l1   l2  )   ▷   E2
  look_m_id_all

E ( id )   ▷   p   Path identifier lookup

 E  (  y1l   ..   ynl  )   ▷   ⟨  Em   ,  Ep   ,  Ex   ⟩ 
 Ep   (  x  )   ▷   p 
E  (  y1l  .   ..   ynl  .  x   l1   l2  )   ▷   p
  look_tc_all

E ( id )   ▷   κ   v_desc   Value identifier lookup

 E  (  y1l   ..   ynl  )   ▷   ⟨  Em   ,  Ep   ,  Ex   ⟩ 
 Ex   (  x  )   ▷   κ   v_desc 
E  (  y1l  .   ..   ynl  .  x   l1   l2  )   ▷   κ   v_desc
  look_var_all

Δ ⊢ t   ok   Well-formed types

Δ  ⊢  α   ok
  check_t_var
 Δ  ⊢  t1   ok 
 Δ  ⊢  t2   ok 
Δ  ⊢  t1  →  t2   ok
  check_t_fn
 Δ  ⊢  t1   ok    ....    Δ  ⊢  tn   ok 
Δ  ⊢  t1  *   ....   *  tn   ok
  check_t_tup
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
 Δ  (  p  )   ▷   α1   ..   αn   tc_abbrev 
Δ  ⊢  (  t1  ,   ..   ,  tn  )   p   ok
  check_t_app

Δ ⊢ t1 = t2   Type equality

 Δ  ⊢  t   ok 
Δ  ⊢  t  =  t
  teq_refl
 Δ  ⊢  t2  =  t1 
Δ  ⊢  t1  =  t2
  teq_sym
 Δ  ⊢  t1  =  t2 
 Δ  ⊢  t2  =  t3 
Δ  ⊢  t1  =  t3
  teq_trans
 Δ  ⊢  t1  =  t3 
 Δ  ⊢  t2  =  t4 
Δ  ⊢  t1  →  t2  =  t3  →  t4
  teq_arrow
 Δ  ⊢  t1  =  u1    ....    Δ  ⊢  tn  =  un 
Δ  ⊢  t1  *   ....   *  tn  =  u1  *   ....   *  un
  teq_tup
 Δ  ⊢  t1  =  u1    ..    Δ  ⊢  tn  =  un 
Δ  ⊢  (  t1  ,   ..   ,  tn  )   p  =  (  u1  ,   ..   ,  un  )   p
  teq_app
 Δ  (  p  )   ▷   α1   ..   αn   .  u 
Δ  ⊢  (  t1  ,   ..   ,  tn  )   p  =  {  α1  ↦  t1   ..   αn  ↦  tn  }  (  u  )
  teq_expand

Δ , Etypt   Convert source types to internal types

Δ  ,  E  ⊢  α   l   l  ↝  α
  convert_typ_var
 Δ  ,  E  ⊢  typ1  ↝  t1 
 Δ  ,  E  ⊢  typ2  ↝  t2 
Δ  ,  E  ⊢  typ1  →  typ2   l  ↝  t1  →  t2
  convert_typ_fn
 Δ  ,  E  ⊢  typ1  ↝  t1    ....    Δ  ,  E  ⊢  typn  ↝  tn 
Δ  ,  E  ⊢  typ1  *   ....   *  typn   l  ↝  t1  *   ....   *  tn
  convert_typ_tup
 Δ  ,  E  ⊢  typ1  ↝  t1    ..    Δ  ,  E  ⊢  typn  ↝  tn 
 E  (  id  )   ▷   p 
 Δ  (  p  )   ▷   α1   ..   αn   tc_abbrev 
Δ  ,  E  ⊢  (  typ1  ,   ..   ,  typn  )  id   l  ↝  (  t1  ,   ..   ,  tn  )   p
  convert_typ_app
 Δ  ,  E  ⊢  typ  ↝  t 
Δ  ,  E  ⊢  (  typ  )   l  ↝  t
  convert_typ_paren
 Δ  ,  E  ⊢  typ  ↝  t1 
 Δ  ⊢  t1  =  t2 
Δ  ,  E  ⊢  typ  ↝  t2
  convert_typ_eq

Δ , Etypst_multi   

 Δ  ,  E  ⊢  typ1  ↝  t1    ..    Δ  ,  E  ⊢  typn  ↝  tn 
Δ  ,  E  ⊢  typ1  *   ..   *  typn  ↝  (  t1  *   ..   *  tn  )
  convert_typs_all

lit : t   Typing literal constants

⊢  true   l  :  (     )    __bool 
  check_lit_true
⊢  false   l  :  (     )    __bool 
  check_lit_false
⊢  num   l  :  (     )    __num 
  check_lit_num
⊢  string   l  :  (     )    __string 
  check_lit_string
⊢  (  )   l  :  (     )    __unit 
  check_lit_unit

Δ , E ⊢   field   id : t_args   pt   ▷   ( x   of   names )   Field typing (also returns canonical field names)

 E  (  id  )   ▷   {  field  }   ⟨   forall   α1   ..   αn  .  p  →  t  ,  (  x   of   names  )  ⟩ 
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
Δ  ,  E  ⊢   field   id  :  (  t1  ,   ..   ,  tn  )   p  →  {  α1  ↦  t1   ..   αn  ↦  tn  }  (  t  )   ▷   (  x   of   names  )
  inst_field_all

Δ , E ⊢   ctor   id : t_multit_args   p   ▷   ( x   of   names )   Data constructor typing (also returns canonical constructor names)

 E  (  id  )   ▷   {  ctor  }   ⟨   forall   α1   ..   αn  .  t_multi  →  p  ,  (  x   of   names  )  ⟩ 
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
Δ  ,  E  ⊢   ctor   id  :  {  α1  ↦  t1   ..   αn  ↦  tn  }  (  t_multi  )  →  (  t1  ,   ..   ,  tn  )   p   ▷   (  x   of   names  )
  inst_ctor_all

Δ , E ⊢   val   id : t   ▷   Σ   Typing top-level bindings, collecting typeclass constraints

 E  (  id  )   ▷   κ   forall   α1   ..   αn  .  (  p1   α′1  )   ..   (  pi   α′i  )  ⇒  t 
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
 σ  =  {  α1  ↦  t1   ..   αn  ↦  tn  } 
 κ   ≠   {  spec  } 
Δ  ,  E  ⊢   val   id  :  σ  (  t  )   ▷   {  (  p1   σ  (  α′1  )  )  ,   ..   ,  (  pi   σ  (  α′i  )  )  }
  inst_val_all

E , El x   not   ctor   v is not bound to a data constructor

 El   (  x  )   ▷   t 
E  ,  El   ⊢  x   not   ctor
  not_ctor_val
 x   ∉   dom   (  Ex   ) 
⟨  Em   ,  Ep   ,  Ex   ⟩  ,  El   ⊢  x   not   ctor
  not_ctor_unbound
 Ex   (  x  )   ▷   κ   v_desc 
 ctor   ∉   κ 
⟨  Em   ,  Ep   ,  Ex   ⟩  ,  El   ⊢  x   not   ctor
  not_ctor_bound

El id   not   shadowed   id is not lexically shadowed

 x   ∉   dom   (  El   ) 
El   ⊢     x   l1   l2   not   shadowed
  not_shadowed_sing
El   ⊢  x1l  .   ..   xnl  .  yl  .  zl   l   not   shadowed
  not_shadowed_multi

Δ , E , E1l pat : t   ▷   E2l   Typing patterns, building their binding environment

 Δ  ,  E  ,  E1l   ⊢  pat_aux  :  t   ▷   E2l  
Δ  ,  E  ,  E1l   ⊢  pat_aux   l  :  t   ▷   E2l 
  check_pat_all

Δ , E , E1l pat_aux : t   ▷   E2l   Typing patterns, building their binding environment

 Δ  ⊢  t   ok 
Δ  ,  E  ,  El   ⊢  _  :  t   ▷   {     }
  check_pat_aux_wild
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E2l  
 x   ∉   dom   (  E2l   ) 
Δ  ,  E  ,  E1l   ⊢  pat   as   x   l  :  t   ▷   E2l   ⊎  {  x  ↦  t  }
  check_pat_aux_as
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E2l  
 Δ  ,  E  ⊢  typ  ↝  t 
Δ  ,  E  ,  E1l   ⊢  (  pat  :  typ  )  :  t   ▷   E2l 
  check_pat_aux_typ
 Δ  ,  E  ⊢   ctor   id  :  (  t1  *   ..   *  tn  )  →  t_args   p   ▷   (  x   of   names  ) 
 El   ⊢  id   not   shadowed 
 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ..    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 disjoint   doms   (  E1l   ,   ..   ,  Enl   ) 
Δ  ,  E  ,  El   ⊢  id   pat1   ..   patn  :  t_args   p   ▷   E1l   ⊎   ..   ⊎  Enl 
  check_pat_aux_ident_constr
 Δ  ⊢  t   ok 
 E  ,  El   ⊢  x   not   ctor 
Δ  ,  E  ,  El   ⊢     x   l1   l2     :  t   ▷   {  x  ↦  t  }
  check_pat_aux_var
 El   ⊢  id1   not   shadowed    ...    El   ⊢  idn   not   shadowed 
 Δ  ,  E  ⊢   field   id1  :  t_args   p  →  t1   ▷   (  x1   of   names  )    ...    Δ  ,  E  ⊢   field   idn  :  t_args   p  →  tn   ▷   (  xn   of   names  ) 
 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 disjoint   doms   (  E1l   ,   ...   ,  Enl   ) 
 duplicates   (  x1  ,   ...   ,  xn  )  =   ∅ 
Δ  ,  E  ,  El   ⊢  ⟨|  id1  =  pat1   l1  ;   ...   ;  idn  =  patn   ln   ;?  |⟩  :  t_args   p   ▷   E1l   ⊎   ...   ⊎  Enl 
  check_pat_aux_record
 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ....    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 disjoint   doms   (  E1l   ,   ....   ,  Enl   ) 
Δ  ,  E  ,  El   ⊢  (  pat1  ,   ....   ,  patn  )  :  t1  *   ....   *  tn   ▷   E1l   ⊎   ....   ⊎  Enl 
  check_pat_aux_tup
 Δ  ⊢  t   ok 
 Δ  ,  E  ,  El   ⊢  pat1  :  t   ▷   E1l     ..    Δ  ,  E  ,  El   ⊢  patn  :  t   ▷   Enl  
 disjoint   doms   (  E1l   ,   ..   ,  Enl   ) 
Δ  ,  E  ,  El   ⊢  [  pat1  ;   ..   ;  patn   ;?  ]  :  (  t  )    __list    ▷   E1l   ⊎   ..   ⊎  Enl 
  check_pat_aux_list
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E2l  
Δ  ,  E  ,  E1l   ⊢  (  pat  )  :  t   ▷   E2l 
  check_pat_aux_paren
 Δ  ,  E  ,  E1l   ⊢  pat1  :  t   ▷   E2l  
 Δ  ,  E  ,  E1l   ⊢  pat2  :  (  t  )    __list    ▷   E3l  
 disjoint   doms   (  E2l   ,  E3l   ) 
Δ  ,  E  ,  E1l   ⊢  pat1  ::  pat2  :  t   ▷   E2l   ⊎  E3l 
  check_pat_aux_cons
 ⊢  lit  :  t 
Δ  ,  E  ,  El   ⊢  lit  :  t   ▷   {     }
  check_pat_aux_lit

Δ , E , El exp : t   ▷   Σ   Typing expressions, collecting typeclass constraints

 Δ  ,  E  ,  El   ⊢  exp_aux  :  t   ▷   Σ 
Δ  ,  E  ,  El   ⊢  exp_aux   l  :  t   ▷   Σ
  check_exp_all

Δ , E , El exp_aux : t   ▷   Σ   Typing expressions, collecting typeclass constraints

 El   (  x  )   ▷   t 
Δ  ,  E  ,  El   ⊢     x   l1   l2  :  t   ▷   {     }
  check_exp_aux_ident_val
 Δ  ,  E  ⊢   ctor   id  :  t_multi  →  t_args   p   ▷   (  x   of   names  ) 
 El   ⊢  id   not   shadowed 
Δ  ,  E  ,  El   ⊢  id  :  curry   (  t_multi  ,  t_args   p  )   ▷   {     }
  check_exp_aux_ident_constr
 Δ  ,  E  ⊢   val   id  :  t   ▷   Σ 
 El   ⊢  id   not   shadowed 
Δ  ,  E  ,  El   ⊢  id  :  t   ▷   Σ
  check_exp_aux_ident_const
 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 Δ  ,  E  ,  El   ⊎  E1l   ⊎   ...   ⊎  Enl   ⊢  exp  :  u   ▷   Σ 
 disjoint   doms   (  E1l   ,   ...   ,  Enl   ) 
Δ  ,  E  ,  El   ⊢  fun   pat1   ...   patn  →  exp   l  :  curry   (  (  t1  *   ...   *  tn  )  ,  u  )   ▷   Σ
  check_exp_aux_fn
 Δ  ,  E  ,  El   ⊢  pat1  :  t   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  t   ▷   Enl  
 Δ  ,  E  ,  El   ⊎  E1l   ⊢  exp1  :  u   ▷   Σ1    ...    Δ  ,  E  ,  El   ⊎  Enl   ⊢  expn  :  u   ▷   Σn 
Δ  ,  E  ,  El   ⊢  function   |?   pat1  →  exp1   l1  ∣   ...   ∣  patn  →  expn   ln   end  :  t  →  u   ▷   Σ1   ⋃   ...   ⋃   Σn
  check_exp_aux_function
 Δ  ,  E  ,  El   ⊢  exp1  :  t1  →  t2   ▷   Σ1 
 Δ  ,  E  ,  El   ⊢  exp2  :  t1   ▷   Σ2 
Δ  ,  E  ,  El   ⊢  exp1   exp2  :  t2   ▷   Σ1   ⋃   Σ2
  check_exp_aux_app
 Δ  ,  E  ,  El   ⊢     (  ix  )       :  t1  →  t2  →  t3   ▷   Σ1 
 Δ  ,  E  ,  El   ⊢  exp1  :  t1   ▷   Σ2 
 Δ  ,  E  ,  El   ⊢  exp2  :  t2   ▷   Σ3 
Δ  ,  E  ,  El   ⊢  exp1   ix   l   exp2  :  t3   ▷   Σ1   ⋃   Σ2   ⋃   Σ3
  check_exp_aux_infix_app1
 Δ  ,  E  ,  El   ⊢     x        :  t1  →  t2  →  t3   ▷   Σ1 
 Δ  ,  E  ,  El   ⊢  exp1  :  t1   ▷   Σ2 
 Δ  ,  E  ,  El   ⊢  exp2  :  t2   ▷   Σ3 
Δ  ,  E  ,  El   ⊢  exp1   ‵  x  ‵  l   exp2  :  t3   ▷   Σ1   ⋃   Σ2   ⋃   Σ3
  check_exp_aux_infix_app2
 El   ⊢  id1   not   shadowed    ...    El   ⊢  idn   not   shadowed 
 Δ  ,  E  ⊢   field   id1  :  t_args   p  →  t1   ▷   (  x1   of   names  )    ...    Δ  ,  E  ⊢   field   idn  :  t_args   p  →  tn   ▷   (  xn   of   names  ) 
 Δ  ,  E  ,  El   ⊢  exp1  :  t1   ▷   Σ1    ...    Δ  ,  E  ,  El   ⊢  expn  :  tn   ▷   Σn 
 duplicates   (  x1  ,   ...   ,  xn  )  =   ∅ 
 names  =  {  x1  ,   ...   ,  xn  } 
Δ  ,  E  ,  El   ⊢  ⟨|  id1  =  exp1   l1  ;   ...   ;  idn  =  expn   ln   ;?   l  |⟩  :  t_args   p   ▷   Σ1   ⋃   ...   ⋃   Σn
  check_exp_aux_record
 El   ⊢  id1   not   shadowed    ...    El   ⊢  idn   not   shadowed 
 Δ  ,  E  ⊢   field   id1  :  t_args   p  →  t1   ▷   (  x1   of   names  )    ...    Δ  ,  E  ⊢   field   idn  :  t_args   p  →  tn   ▷   (  xn   of   names  ) 
 Δ  ,  E  ,  El   ⊢  exp1  :  t1   ▷   Σ1    ...    Δ  ,  E  ,  El   ⊢  expn  :  tn   ▷   Σn 
 duplicates   (  x1  ,   ...   ,  xn  )  =   ∅ 
 Δ  ,  E  ,  El   ⊢  exp  :  t_args   p   ▷   Σ′ 
Δ  ,  E  ,  El   ⊢  ⟨|  exp   with   id1  =  exp1   l1  ;   ...   ;  idn  =  expn   ln   ;?   l  |⟩  :  t_args   p   ▷   Σ′   ⋃   Σ1   ⋃   ...   ⋃   Σn
  check_exp_aux_recup
 El   ⊢  id   not   shadowed 
 Δ  ,  E  ⊢   field   id  :  t_args   p  →  t   ▷   (  x   of   names  ) 
 Δ  ,  E  ,  El   ⊢  exp  :  t_args   p   ▷   Σ 
Δ  ,  E  ,  El   ⊢  exp  .  id  :  t   ▷   Σ
  check_exp_aux_field
 Δ  ,  E  ,  El   ⊢  pat1  :  t   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  t   ▷   Enl  
 Δ  ,  E  ,  El   ⊎  E1l   ⊢  exp1  :  u   ▷   Σ1    ...    Δ  ,  E  ,  El   ⊎  Enl   ⊢  expn  :  u   ▷   Σn 
 Δ  ,  E  ,  El   ⊢  exp  :  t   ▷   Σ′ 
Δ  ,  E  ,  El   ⊢  match   exp   with   |?   pat1  →  exp1   l1  ∣   ...   ∣  patn  →  expn   ln   l   end  :  u   ▷   Σ′   ⋃   Σ1   ⋃   ...   ⋃   Σn
  check_exp_aux_case
 Δ  ,  E  ,  El   ⊢  exp  :  t   ▷   Σ 
 Δ  ,  E  ⊢  typ  ↝  t 
Δ  ,  E  ,  El   ⊢  (  exp  :  typ  )  :  t   ▷   Σ
  check_exp_aux_typed
 Δ  ,  E  ,  E1l   ⊢  letbind   ▷   E2l   ,  Σ1 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp  :  t   ▷   Σ2 
Δ  ,  E  ,  El   ⊢  let   letbind   in   exp  :  t   ▷   Σ1   ⋃   Σ2
  check_exp_aux_let
 Δ  ,  E  ,  El   ⊢  exp1  :  t1   ▷   Σ1    ....    Δ  ,  E  ,  El   ⊢  expn  :  tn   ▷   Σn 
Δ  ,  E  ,  El   ⊢  (  exp1  ,   ....   ,  expn  )  :  t1  *   ....   *  tn   ▷   Σ1   ⋃   ....   ⋃   Σn
  check_exp_aux_tup
 Δ  ⊢  t   ok 
 Δ  ,  E  ,  El   ⊢  exp1  :  t   ▷   Σ1    ..    Δ  ,  E  ,  El   ⊢  expn  :  t   ▷   Σn 
Δ  ,  E  ,  El   ⊢  [  exp1  ;   ..   ;  expn   ;?  ]  :  (  t  )    __list    ▷   Σ1   ⋃   ..   ⋃   Σn
  check_exp_aux_list
 Δ  ,  E  ,  El   ⊢  exp  :  t   ▷   Σ 
Δ  ,  E  ,  El   ⊢  (  exp  )  :  t   ▷   Σ
  check_exp_aux_paren
 Δ  ,  E  ,  El   ⊢  exp  :  t   ▷   Σ 
Δ  ,  E  ,  El   ⊢  begin   exp   end  :  t   ▷   Σ
  check_exp_aux_begin
 Δ  ,  E  ,  El   ⊢  exp1  :  (     )    __bool    ▷   Σ1 
 Δ  ,  E  ,  El   ⊢  exp2  :  t   ▷   Σ2 
 Δ  ,  E  ,  El   ⊢  exp3  :  t   ▷   Σ3 
Δ  ,  E  ,  El   ⊢  if   exp1   then   exp2   else   exp3  :  t   ▷   Σ1   ⋃   Σ2   ⋃   Σ3
  check_exp_aux_if
 Δ  ,  E  ,  El   ⊢  exp1  :  t   ▷   Σ1 
 Δ  ,  E  ,  El   ⊢  exp2  :  (  t  )    __list    ▷   Σ2 
Δ  ,  E  ,  El   ⊢  exp1  ::  exp2  :  (  t  )    __list    ▷   Σ1   ⋃   Σ2
  check_exp_aux_cons
 ⊢  lit  :  t 
Δ  ,  E  ,  El   ⊢  lit  :  t   ▷   {     }
  check_exp_aux_lit
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
 Δ  ,  E  ,  El   ⊎  {  x1  ↦  t1  ,   ..   ,  xn  ↦  tn  }  ⊢  exp1  :  t   ▷   Σ1 
 Δ  ,  E  ,  El   ⊎  {  x1  ↦  t1  ,   ..   ,  xn  ↦  tn  }  ⊢  exp2  :  (     )    __bool    ▷   Σ2 
 disjoint   doms   (  El   ,  {  x1  ↦  t1  ,   ..   ,  xn  ↦  tn  }  ) 
 E  =  ⟨  Em   ,  Ep   ,  Ex   ⟩ 
 x1   ∉   dom   (  Ex   )    ..    xn   ∉   dom   (  Ex   ) 
Δ  ,  E  ,  El   ⊢  {  exp1  ∣  exp2  }  :  (  t  )    __set    ▷   Σ1   ⋃   Σ2
  check_exp_aux_set_comp
 Δ  ,  E  ,  E1l   ⊢  qbind1   ..   qbindn   ▷   E2l   ,  Σ1 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp1  :  t   ▷   Σ2 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp2  :  (     )    __bool    ▷   Σ3 
Δ  ,  E  ,  E1l   ⊢  {  exp1  ∣   forall   qbind1   ..   qbindn  ∣  exp2  }  :  (  t  )    __set    ▷   Σ1   ⋃   Σ2   ⋃   Σ3
  check_exp_aux_set_comp_binding
 Δ  ⊢  t   ok 
 Δ  ,  E  ,  El   ⊢  exp1  :  t   ▷   Σ1    ..    Δ  ,  E  ,  El   ⊢  expn  :  t   ▷   Σn 
Δ  ,  E  ,  El   ⊢  {  exp1  ;   ..   ;  expn   ;?  }  :  (  t  )    __set    ▷   Σ1   ⋃   ..   ⋃   Σn
  check_exp_aux_set
 Δ  ,  E  ,  E1l   ⊢  qbind1   ...   qbindn   ▷   E2l   ,  Σ1 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp  :  (     )    __bool    ▷   Σ2 
Δ  ,  E  ,  E1l   ⊢  q   qbind1   ...   qbindn  .  exp  :  (     )    __bool    ▷   Σ1   ⋃   Σ2
  check_exp_aux_quant
 Δ  ,  E  ,  E1l   ⊢   list   qbind1   ..   qbindn   ▷   E2l   ,  Σ1 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp1  :  t   ▷   Σ2 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp2  :  (     )    __bool    ▷   Σ3 
Δ  ,  E  ,  E1l   ⊢  [  exp1  ∣   forall   qbind1   ..   qbindn  ∣  exp2  ]  :  (  t  )    __list    ▷   Σ1   ⋃   Σ2   ⋃   Σ3
  check_exp_aux_list_comp_binding

Δ , E , E1l qbind1   ..   qbindn   ▷   E2l , Σ   Build the environment for quantifier bindings, collecting typeclass constraints

Δ  ,  E  ,  El   ⊢     ▷   {     }  ,  {     }
  check_listquant_binding_empty
 Δ  ⊢  t   ok 
 Δ  ,  E  ,  E1l   ⊎  {  x  ↦  t  }  ⊢  qbind1   ..   qbindn   ▷   E2l   ,  Σ1 
 disjoint   doms   (  {  x  ↦  t  }  ,  E2l   ) 
Δ  ,  E  ,  E1l   ⊢  x   l   qbind1   ..   qbindn   ▷   {  x  ↦  t  }  ⊎  E2l   ,  Σ1
  check_listquant_binding_var
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E3l  
 Δ  ,  E  ,  E1l   ⊢  exp  :  (  t  )    __set    ▷   Σ1 
 Δ  ,  E  ,  E1l   ⊎  E3l   ⊢  qbind1   ..   qbindn   ▷   E2l   ,  Σ2 
 disjoint   doms   (  E3l   ,  E2l   ) 
Δ  ,  E  ,  E1l   ⊢  (  pat   IN   exp  )   qbind1   ..   qbindn   ▷   E2l   ⊎  E3l   ,  Σ1   ⋃   Σ2
  check_listquant_binding_restr
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E3l  
 Δ  ,  E  ,  E1l   ⊢  exp  :  (  t  )    __list    ▷   Σ1 
 Δ  ,  E  ,  E1l   ⊎  E3l   ⊢  qbind1   ..   qbindn   ▷   E2l   ,  Σ2 
 disjoint   doms   (  E3l   ,  E2l   ) 
Δ  ,  E  ,  E1l   ⊢  (  pat   MEM   exp  )   qbind1   ..   qbindn   ▷   E2l   ⊎  E3l   ,  Σ1   ⋃   Σ2
  check_listquant_binding_list_restr

Δ , E , E1l ⊢   list   qbind1   ..   qbindn   ▷   E2l , Σ   Build the environment for quantifier bindings, collecting typeclass constraints

Δ  ,  E  ,  El   ⊢   list     ▷   {     }  ,  {     }
  check_quant_binding_empty
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E3l  
 Δ  ,  E  ,  E1l   ⊢  exp  :  (  t  )    __list    ▷   Σ1 
 Δ  ,  E  ,  E1l   ⊎  E3l   ⊢  qbind1   ..   qbindn   ▷   E2l   ,  Σ2 
 disjoint   doms   (  E3l   ,  E2l   ) 
Δ  ,  E  ,  E1l   ⊢   list   (  pat   MEM   exp  )   qbind1   ..   qbindn   ▷   E2l   ⊎  E3l   ,  Σ1   ⋃   Σ2
  check_quant_binding_restr

Δ , E , El funcl   ▷   { xt } , Σ   Build the environment for a function definition clause, collecting typeclass constraints

 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 Δ  ,  E  ,  El   ⊎  E1l   ⊎   ...   ⊎  Enl   ⊢  exp  :  u   ▷   Σ 
 disjoint   doms   (  E1l   ,   ...   ,  Enl   ) 
 Δ  ,  E  ⊢  typ  ↝  u 
Δ  ,  E  ,  El   ⊢  x   l1   pat1   ...   patn   :  typ  =  exp   l2   ▷   {  x  ↦  curry   (  (  t1  *   ...   *  tn  )  ,  u  )  }  ,  Σ
  check_funcl_annot
 Δ  ,  E  ,  El   ⊢  pat1  :  t1   ▷   E1l     ...    Δ  ,  E  ,  El   ⊢  patn  :  tn   ▷   Enl  
 Δ  ,  E  ,  El   ⊎  E1l   ⊎   ...   ⊎  Enl   ⊢  exp  :  u   ▷   Σ 
 disjoint   doms   (  E1l   ,   ...   ,  Enl   ) 
Δ  ,  E  ,  El   ⊢  x   l1   pat1   ...   patn     =  exp   l2   ▷   {  x  ↦  curry   (  (  t1  *   ...   *  tn  )  ,  u  )  }  ,  Σ
  check_funcl_noannot

Δ , E , E1l letbind   ▷   E2l , Σ   Build the environment for a let binding, collecting typeclass constraints

 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E2l  
 Δ  ,  E  ,  E1l   ⊢  exp  :  t   ▷   Σ 
 Δ  ,  E  ⊢  typ  ↝  t 
Δ  ,  E  ,  E1l   ⊢  pat   :  typ  =  exp   l   ▷   E2l   ,  Σ
  check_letbind_val_annot
 Δ  ,  E  ,  E1l   ⊢  pat  :  t   ▷   E2l  
 Δ  ,  E  ,  E1l   ⊢  exp  :  t   ▷   Σ 
Δ  ,  E  ,  E1l   ⊢  pat     =  exp   l   ▷   E2l   ,  Σ
  check_letbind_val_noannot
 Δ  ,  E  ,  E1l   ⊢  funcl_aux   l   ▷   {  x  ↦  t  }  ,  Σ 
Δ  ,  E  ,  E1l   ⊢  funcl_aux   l   ▷   {  x  ↦  t  }  ,  Σ
  check_letbind_fn

Δ , E , El rule   ▷   { xt } , Σ   Build the environment for an inductive relation clause, collecting typeclass constraints

 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
 E2l   =  {  y1  ↦  t1  ,   ..   ,  yn  ↦  tn  } 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp  :  (     )    __bool    ▷   Σ′ 
 Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  exp1  :  u1   ▷   Σ1    ..    Δ  ,  E  ,  E1l   ⊎  E2l   ⊢  expi  :  ui   ▷   Σi 
Δ  ,  E  ,  E1l   ⊢  forall   y1   l1   ..   yn   ln  .  exp  =⇒  x   l   exp1   ..   expi   l   ▷   {  x  ↦  curry   (  (  u1  *   ..   *  ui  )  ,  (     )    __bool   )  }  ,  Σ′   ⋃   Σ1   ⋃   ..   ⋃   Σi
  check_rule_rule

xs , Δ1 , E ⊢   tc   td   ▷   Δ2 , Ep   Extract the type constructor information

 tyvars  ↝  tvs 
 Δ  ,  E  ⊢  typ  ↝  t 
 duplicates   (  tvs  )  =   ∅ 
 FV   (  t  )   ⊂   tvs 
 y1  .   ..   yn  .  x   ∉   dom   (  Δ  ) 
y1   ..   yn  ,  Δ  ,  E  ⊢   tc   tyvars   x   l  =  typ   ▷   {  y1  .   ..   yn  .  x  ↦  tvs   .  t  }  ,  {  x  ↦  y1  .   ..   yn  .  x  }
  check_texp_tc_abbrev
 tyvars  ↝  tvs 
 duplicates   (  tvs  )  =   ∅ 
 y1  .   ..   yn  .  x   ∉   dom   (  Δ  ) 
y1   ..   yn  ,  Δ  ,  E1  ⊢   tc   tyvars   x   l   ▷   {  y1  .   ..   yn  .  x  ↦  tvs     }  ,  {  x  ↦  y1  .   ..   yn  .  x  }
  check_texp_tc_abstract
 tyvars  ↝  tvs 
 duplicates   (  tvs  )  =   ∅ 
 y1  .   ..   yn  .  x   ∉   dom   (  Δ  ) 
y1   ..   yn  ,  Δ1  ,  E  ⊢   tc   tyvars   x   l  =  ⟨|  x1l  :  typ1  ;   ...   ;  xjl  :  typj   ;?  |⟩   ▷   {  y1  .   ..   yn  .  x  ↦  tvs     }  ,  {  x  ↦  y1  .   ..   yn  .  x  }
  check_texp_tc_rec
 tyvars  ↝  tvs 
 duplicates   (  tvs  )  =   ∅ 
 y1  .   ..   yn  .  x   ∉   dom   (  Δ  ) 
y1   ..   yn  ,  Δ1  ,  E  ⊢   tc   tyvars   x   l  =  |?   ctor_def1  ∣   ...   ∣  ctor_defj   ▷   {  y1  .   ..   yn  .  x  ↦  tvs     }  ,  {  x  ↦  y1  .   ..   yn  .  x  }
  check_texp_tc_var

xs , Δ1 , E ⊢   tc   td1   ..   tdi   ▷   Δ2 , Ep   Extract the type constructor information

xs  ,  Δ  ,  E  ⊢   tc     ▷   {     }  ,  {     }
  check_texps_tc_empty
 xs  ,  Δ1  ,  E  ⊢   tc   td   ▷   Δ2  ,  E2p  
 xs  ,  Δ1  ⊎  Δ2  ,  E  ⊎  ⟨  {     }  ,  E2p   ,  {     }  ⟩  ⊢   tc   td1   ..   tdi   ▷   Δ3  ,  E3p  
 dom   (  E2p   )   ⋂   dom   (  E3p   )  =   ∅ 
xs  ,  Δ1  ,  E  ⊢   tc   td   td1   ..   tdi   ▷   Δ2  ⊎  Δ3  ,  E2p   ⊎  E3p 
  check_texps_tc_abbrev

Δ , Etvs   p = texp   ▷   Ex   Check a type definition, with its path already resolved

Δ  ,  E  ⊢  tvs   p  =  typ   ▷   {     }
  check_texp_abbrev
 Δ  ,  E  ⊢  typ1  ↝  t1    ...    Δ  ,  E  ⊢  typn  ↝  tn 
 names  =  {  x1  ,   ...   ,  xn  } 
 duplicates   (  x1  ,   ...   ,  xn  )  =   ∅ 
 FV   (  t1  )   ⊂   tvs    ...    FV   (  tn  )   ⊂   tvs 
 Ex   =  {  x1  ↦  {  field  }   ⟨   forall   tvs  .  p  →  t1  ,  (  x1   of   names  )  ⟩  ,   ...   ,  xn  ↦  {  field  }   ⟨   forall   tvs  .  p  →  tn  ,  (  xn   of   names  )  ⟩  } 
Δ  ,  E  ⊢  tvs   p  =  ⟨|  x1l  :  typ1  ;   ...   ;  xnl  :  typn   ;?  |⟩   ▷   Ex 
  check_texp_rec
 Δ  ,  E  ⊢  typs1  ↝  t_multi1    ...    Δ  ,  E  ⊢  typsn  ↝  t_multin 
 names  =  {  x1  ,   ...   ,  xn  } 
 duplicates   (  x1  ,   ...   ,  xn  )  =   ∅ 
 FV   (  t_multi1  )   ⊂   tvs    ...    FV   (  t_multin  )   ⊂   tvs 
 Ex   =  {  x1  ↦  {  ctor  }   ⟨   forall   tvs  .  t_multi1  →  p  ,  (  x1   of   names  )  ⟩  ,   ...   ,  xn  ↦  {  ctor  }   ⟨   forall   tvs  .  t_multin  →  p  ,  (  xn   of   names  )  ⟩  } 
Δ  ,  E  ⊢  tvs   p  =  |?   x1l   of   typs1  ∣   ...   ∣  xnl   of   typsn   ▷   Ex 
  check_texp_var

xs , Δ , Etd1   ..   tdn   ▷   Ex   

xs  ,  Δ  ,  E  ⊢     ▷   {     }
  check_texps_empty
 tyvars  ↝  tvs 
 Δ  ,  E1  ⊢  tvs   y1  .   ..   yn  .  x  =  texp   ▷   E1x  
 y1   ..   yn  ,  Δ  ,  E  ⊢  td1   ..   tdi   ▷   E2x  
 dom   (  E1x   )   ⋂   dom   (  E2x   )  =   ∅ 
y1   ..   yn  ,  Δ  ,  E  ⊢  tyvars   x   l  =  texp   td1   ..   tdi   ▷   E1x   ⊎  E2x 
  check_texps_cons_concrete
 xs  ,  Δ  ,  E  ⊢  td1   ..   tdn   ▷   Ex  
xs  ,  Δ  ,  E  ⊢  tyvars   x   l   td1   ..   tdn   ▷   Ex 
  check_texps_cons_abstract

δ , Eidp   Lookup a type class

 E  (  id  )   ▷   p 
 δ  (  p  )   ▷   xs 
δ  ,  E  ⊢  id  ↝  p
  convert_class_all

I ⊢ ( p   t )   IN   C   Solve class constraint

I  ⊢  (  p   α  )   IN   (  p1   α1  )   ..   (  pi   αi  )  (  p   α  )  (  p1   α′1  )   ..   (  pj   α′j  )
  solve_class_constraint_immediate
 (  p1   α1  )   ..   (  pn   αn  )  ⇒  (  p   t  )   IN   I 
 I  ⊢  (  p1   σ  (  α1  )  )   IN   C     ..    I  ⊢  (  pn   σ  (  αn  )  )   IN   C  
I  ⊢  (  p   σ  (  t  )  )   IN   C 
  solve_class_constraint_chain

I ⊢ Σ   ▷   C   Solve class constraints

 I  ⊢  (  p1   t1  )   IN   C     ..    I  ⊢  (  pn   tn  )   IN   C  
I  ⊢  {  (  p1   t1  )  ,   ..   ,  (  pn   tn  )  }   ▷   C 
  solve_class_constraints_all

targets? ↝ κ   Get the binding type for an optional target

↝  {  let  }
  targets_opts_to_kinds_none
{  target1  ;   ..   ;  targetn  }  ↝  {  target1  ;   ..   ;  targetn  }
  targets_opts_to_kinds_some

Δ , I , Eval_def   ▷   Ex   Check a value definition

 Δ  ,  E  ,  {     }  ⊢  letbind   ▷   {  x1  ↦  t1  ,   ..   ,  xn  ↦  tn  }  ,  Σ 
 I  ⊢  Σ   ▷   C  
 FV   (  t1  )   ⊂   tvs    ..    FV   (  tn  )   ⊂   tvs 
 FV   (  C   )   ⊂   tvs 
 targets?  ↝  κ 
Δ  ,  I  ,  E1  ⊢  let   targets?   letbind   ▷   {  x1  ↦  κ   forall   tvs  .  C   ⇒  t1  ,   ..   ,  xn  ↦  κ   forall   tvs  .  C   ⇒  tn  }
  check_val_def_val
 Δ  ,  E  ,  El   ⊢  funcl1   ▷   {  x1  ↦  t1  }  ,  Σ1    ...    Δ  ,  E  ,  El   ⊢  funcln   ▷   {  xn  ↦  tn  }  ,  Σn 
 I  ⊢  Σ   ▷   C  
 FV   (  t1  )   ⊂   tvs    ...    FV   (  tn  )   ⊂   tvs 
 FV   (  C   )   ⊂   tvs 
 compatible   overlap   (  {  x1  ↦  t1  }  ,   ...   ,  {  xn  ↦  tn  }  ) 
 El   =  {  x1  ↦  t1  ,   ...   ,  xn  ↦  tn  } 
 targets?  ↝  κ 
Δ  ,  I  ,  E  ⊢  let   rec   targets?   funcl1   and   ...   and   funcln   ▷   {  x1  ↦  κ   forall   tvs  .  C   ⇒  t1  ,   ...   ,  xn  ↦  κ   forall   tvs  .  C   ⇒  tn  }
  check_val_def_recfun

Δ , ( α1 ,   ..   , αn ) ⊢ t   instance   Check that t be a typeclass instance

Δ  ,  (  α  )  ⊢  α   instance
  check_t_instance_var
Δ  ,  (  α1  ,   ....   ,  αn  )  ⊢  α1  *   ....   *  αn   instance
  check_t_instance_tup
Δ  ,  (  α1  ,  α2  )  ⊢  α1  →  αn   instance
  check_t_instance_fn
 Δ  (  p  )   ▷   α′1   ..   α′n    
Δ  ,  (  α1  ,   ..   ,  αn  )  ⊢  (  α1  ,   ..   ,  αn  )   p   instance
  check_t_instance_tc

E1x E2x E3x   Check that new definitions are compatible with existing ones

E1x   ⊢  {     }  ↝  {     }
  convert_v_env_empty
 x   ∉   dom   (  E1x   ) 
 E1x   ⊢  E2x   ↝  E3x  
E1x   ⊢  E2x   ⊎  {  x  ↦  κ   v_desc  }  ↝  E3x   ⊎  {  x  ↦  κ   v_desc  }
  convert_v_env_first
 E1x   (  x  )   ▷   κ′   v_desc 
 κ   ⋂   κ′  =   ∅ 
 κ   ⋂   {  mthd  ;  ctor  ;  field  }  =   ∅ 
 κ′   ⋂   {  mthd  ;  ctor  ;  field  }  =   ∅ 
  spec  ∈  κ  
 E1x   ⊢  E2x   ↝  E3x  
E1x   ⊢  E2x   ⊎  {  x  ↦  κ   v_desc  }  ↝  E3x   ⊎  {  x  ↦  κ   ⋃   κ′   v_desc  }
  convert_v_env_duplicate

xs , D1 , E1def   ▷   D2 , E2   Check a definition

 xs  ,  Δ1  ,  E  ⊢   tc   td1   ...   tdn   ▷   Δ2  ,  Ep  
 xs  ,  Δ1  ⊎  Δ2  ,  E  ⊎  ⟨  {     }  ,  Ep   ,  {     }  ⟩  ⊢  td1   ...   tdn   ▷   Ex  
xs  ,  ⟨  Δ1  ,  δ  ,  I  ⟩  ,  E  ⊢  type   td1   and   ...   and   tdn   l   ▷   ⟨  Δ2  ,  {     }  ,  {     }  ⟩  ,  ⟨  {     }  ,  Ep   ,  Ex   ⟩
  check_def_type
 Δ  ,  I  ,  E  ⊢  val_def   ▷   Ex  
xs  ,  ⟨  Δ  ,  δ  ,  I  ⟩  ,  E  ⊢  val_def   l   ▷   є  ,  ⟨  {     }  ,  {     }  ,  Ex   ⟩
  check_def_val_def
 Δ  ,  E1  ,  El   ⊢  rule1   ▷   {  x1  ↦  t1  }  ,  Σ1    ...    Δ  ,  E1  ,  El   ⊢  rulen   ▷   {  xn  ↦  tn  }  ,  Σn 
 I  ⊢  Σ1   ⋃   ...   ⋃   Σn   ▷   C  
 FV   (  t1  )   ⊂   tvs    ...    FV   (  tn  )   ⊂   tvs 
 FV   (  C   )   ⊂   tvs 
 compatible   overlap   (  {  x1  ↦  t1  }  ,   ...   ,  {  xn  ↦  tn  }  ) 
 El   =  {  x1  ↦  t1  ,   ...   ,  xn  ↦  tn  } 
 targets?  ↝  κ 
 E2  =  ⟨  {     }  ,  {     }  ,  {  x1  ↦  κ   forall   tvs  .  C   ⇒  t1  ,   ...   ,  xn  ↦  κ   forall   tvs  .  C   ⇒  tn  }  ⟩ 
xs  ,  ⟨  Δ  ,  δ  ,  I  ⟩  ,  E1  ⊢  indreln   targets?   rule1   and   ...   and   rulen   l   ▷   є  ,  E2
  check_def_indreln
 x1   ..   xn   x  ,  D1  ,  E1  ,  {     }  ⊢  defs   ▷   D2  ,  E2 
x1   ..   xn  ,  D1  ,  E1  ⊢  module   x   l1  =   struct   defs   end   l2   ▷   D2  ,  ⟨  {  x  ↦  E2  }  ,  {     }  ,  {     }  ⟩
  check_def_module
 E1  (  id  )   ▷   E2 
xs  ,  D  ,  E1  ⊢  module   x   l1  =  id   l2   ▷   є  ,  ⟨  {  x  ↦  E2  }  ,  {     }  ,  {     }  ⟩
  check_def_module_rename
 Δ  ,  E  ⊢  typ  ↝  t 
 FV   (  t  )   ⊂   α1   ..   αi 
 FV   (  α′1  *   ..   *  α′j  )   ⊂   α1   ..   αi 
 δ  ,  E  ⊢  id1  ↝  p1    ..    δ  ,  E  ⊢  idj  ↝  pj 
 E  =  ⟨  {     }  ,  {     }  ,  {  x  ↦  {  spec  }   forall   α1   ..   αi  .  (  p1   α′1  )   ..   (  pj   α′j  )  ⇒  t  }  ⟩ 
xs  ,  ⟨  Δ  ,  δ  ,  I  ⟩  ,  E  ⊢  val   x   l1  :  forall   α1   l1   ..   αi   li  .  (  id1   α′1   l1  )   ..   (  idj   α′j   lj  )  ⇒   typ   l2   ▷   є  ,  E
  check_def_spec
 Δ  ⊢  t1   ok    ..    Δ  ⊢  tn   ok 
 disjoint   doms   (  {  y1  ↦  t1  }  ,   ..   ,  {  yn  ↦  tn  }  ) 
 Δ  ,  E1  ,  {  y1  ↦  t1  ,   ..   ,  yn  ↦  tn  }  ⊢  exp  :  t   ▷   {     } 
 t  =  curry   (  (  t1  *   ..   *  tn  )  ,  t  ) 
 FV   (  t  )   ⊂   tvs 
 E2  =  ⟨  {     }  ,  {     }  ,  {  x  ↦  {  target  }   forall   tvs  .     ⇒  t  }  ⟩ 
xs  ,  ⟨  Δ  ,  δ  ,  I  ⟩  ,  E1  ⊢  sub   [  target  ]  x   l   y1   l1   ..   yn   ln  =  exp   l   ▷   є  ,  E2
  check_def_sub
 Δ  ,  E1  ⊢  typ1  ↝  t1    ...    Δ  ,  E1  ⊢  typn  ↝  tn 
 FV   (  t1  )   ⊂   α    ...    FV   (  tn  )   ⊂   α 
 p  =  z1  .   ..   zi  .  x 
 E2  =  ⟨  {     }  ,  {  x  ↦  p  }  ,  {  y1  ↦  {  mthd  }   forall   α  .  (  p   α  )  ⇒  t1  ,   ...   ,  yn  ↦  {  mthd  }   forall   α  .  (  p   α  )  ⇒  tn  }  ⟩ 
 δ2  =  {  p  ↦  y1   ...   yn  } 
 p   ∉   dom   (  δ1  ) 
z1   ..   zi  ,  ⟨  Δ  ,  δ1  ,  I  ⟩  ,  E1  ⊢  class   (  x   l   α   l  )   val   y1   l1  :  typ1   l1   ...   val   yn   ln  :  typn   ln   end   l   ▷   ⟨  {     }  ,  δ2  ,  {     }  ⟩  ,  E2
  check_def_class
 E  =  ⟨  Em   ,  Ep   ,  Ex   ⟩ 
 Δ  ,  E  ⊢  typ  ↝  t 
 Δ  ,  (  α1  ,   ..   ,  αi  )  ⊢  t   instance 
 tvs  =  α1   ..   αi 
 duplicates   (  tvs  )  =   ∅ 
 δ  ,  E  ⊢  id1  ↝  p1    ..    δ  ,  E  ⊢  idj  ↝  pj 
 FV   (  α′1  *   ..   *  α′j  )   ⊂   tvs 
 E  (  id  )   ▷   p 
 δ  (  p  )   ▷   xs 
 I2  =  {     ⇒  (  p1   α′1  )  ,   ..   ,     ⇒  (  pj   α′j  )  } 
 Δ  ,  I   ⋃   I2  ,  E  ⊢  val_def1   ▷   E1x     ...    Δ  ,  I   ⋃   I2  ,  E  ⊢  val_defn   ▷   Enx  
 disjoint   doms   (  E1x   ,   ...   ,  Enx   ) 
 Ex   (  x1  )   ▷   {  mthd  }   forall   α″  .  (  p   α″  )  ⇒  t1    ..    Ex   (  xk  )   ▷   {  mthd  }   forall   α″  .  (  p   α″  )  ⇒  tk 
 {  x1  ↦  {  let  }   forall   tvs  .     ⇒  {  α″  ↦  t  }  (  t1  )  ,   ..   ,  xk  ↦  {  let  }   forall   tvs  .     ⇒  {  α″  ↦  t  }  (  tk  )  }  =  E1x   ⊎   ...   ⊎  Enx  
 x1   ..   xk  =  xs 
 I3  =  {  (  p1   α′1  )   ..   (  pj   α′j  )  ⇒  (  p   t  )  } 
 (  p   {  α1  ↦  α‴1   ..   αi  ↦  α‴i  }  (  t  )  )   ∉   I 
xs  ,  ⟨  Δ  ,  δ  ,  I  ⟩  ,  E  ⊢  instance   forall   α1   l1   ..   αi   li  .  (  id1   α′1   l1  )   ..   (  idj   α′j   lj  )  ⇒  (  id   typ  )   val_def1   l1   ...   val_defn   ln   end   l   ▷   ⟨  {     }  ,  {     }  ,  I3  ⟩  ,  є
  check_def_instance_tc

xs , D1 , E1 , Ex defs   ▷   D2 , E2   Check definitions

xs  ,  D  ,  E  ,  Ex   ⊢      ▷   є  ,  є
  check_defs_empty
 xs  ,  D1  ,  E1  ⊢  def   ▷   D2  ,  E2 
 E2  =  ⟨  E2m   ,  E2p   ,  E2x   ⟩ 
 E1x   ⊢  E2x   ↝  E4x  
 xs  ,  D1  ⊎  D2  ,  E1  ⊎  ⟨  E2m   ,  E2p   ,  E4x   ⟩  ,  E1x   ⊎  E4x   ⊢  def1   ;;1?   ..   defn   ;;n?   ▷   D3  ,  E3 
 E3  =  ⟨  E3m   ,  E3p   ,  E3x   ⟩ 
 dom   (  E2m   )   ⋂   dom   (  E3m   )  =   ∅ 
 dom   (  E2p   )   ⋂   dom   (  E3p   )  =   ∅ 
xs  ,  D1  ,  E1  ,  E1x   ⊢  def   ;;?   def1   ;;1?   ..   defn   ;;n?   ▷   D2  ⊎  D3  ,  E2  ⊎  E3
  check_defs_def
 E1  (  id  )   ▷   E3 
 xs  ,  D1  ,  E1  ⊎  E3  ,  Ex   ⊢  def1   ;;1?   ..   defn   ;;n?   ▷   D2  ,  E2 
xs  ,  D1  ,  E1  ,  Ex   ⊢  open   id   l   ;;?   def1   ;;1?   ..   defn   ;;n?   ▷   D2  ,  E2
  check_defs_open

This document was translated from LATEX by HEVEA.