grammar

mut :: 'mut_' ::=
  |  immutable :: :: immutable
  |  mutable :: :: mutable

lvar :: 'lvar_' ::=
  | register typ :: :: register
  | enum typ     :: :: enum
  | local mut typ :: :: local
  | union typquant typ :: :: union
  | unbound :: :: unbound
  


G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::=  {{ com Type environment }} 
   | empty                              :: :: empty {{ tex \epsilon }} {{ com Empty context }}
   | G , x1 : typ1 , .. , xn : typn     :: :: type_list  {{ com List of variables and their types }}
%   | G , x1 : k1 , .. , xn : kn         :: :: kind_list  {{ com List of variables and their kinds }}
   | G , kid1 , .. , kidn               :: :: kid_list
%   | G , quant_item1 , .. , quant_itemn :: :: quant_list
%   | G , { nec1 , .. , necn }           :: :: constraint_list {{ com Constraints }}
   | G , G1 .. Gn                       :: :: merge {{ com Merge or disjoint union }}
   | G , id : lvar                       :: :: add_local


formula :: formula_ ::=
  | judgement                                                   :: :: judgement
  | formula1 .. formulan                                        :: :: dots
  | G ( id ) = lvar                                             :: :: lookup_id
  | G ( typ1 , id ) = typ2                                      :: :: lookup_record_field
  | G ( typ1 ) = typ2                                           :: :: lookup_typ
  |  nexp = length [|| exp , exp1 , .. , expn ||]               :: :: vector_length
  | order_inc                                                   :: :: default_order_inc
  | order_dec                                                   :: :: default_order_dec
  |  G |= nexp1 <= nexp2  :: :: prove_lteq

defns
  declarative :: '' ::=

defn
 G |- typ1  ~< typ2   :: :: subtype :: subtype_
 {{ com $[[typ1]]$ is a subtype of $[[typ2]]$  }}
 {{ tex [[G]] \vdash [[typ1]]  \preccurlyeq [[typ2]] }}
by


----------------- :: refl
G |- typ ~< typ

--------------------- :: wild
G |- _ ~< _



------------- :: id
G |- id ~< id

G |- typ1 ~< typ'1 .. G |- typn ~< typ'n
--------------------------------------------------- :: tuple
G |- (typ1 , .. , typn ) ~< (typ'1, .. , typ'n)


defn
G |-l lit => typ  :: :: infer_lit :: infer_lit_
{{ com Infer that type of $[[lit]]$ is $[[typ]]$ }}
{{ tex [[G]] \vdash_l [[lit]] \Rightarrow [[typ]] }}
by


----------------------------- :: unit
G |-l () => unit

-------------------- :: zero
G |-l bitzero => bit

-------------------- :: one
G |-l bitone => bit


---------------------- :: num
G |-l num => atom < num >


---------------------- :: true
G |-l true => bool


---------------------- :: false
G |-l false => bool

defn
G |- lexp := exp => typ -| D :: :: bind_assignment :: bind_assignment_
{{ com Bind assignment returning updated environment  }}
{{ tex [[G]] \vdash [[lexp]] := [[exp]] \Rightarrow [[typ]] \dashv [[D]] }}
by


G |- exp => typ
G |- id <= typ -| D
------------------------------- :: id
G |- id := exp => unit -| D

defn
G |- pat <= typ -| D :: :: bind_pat :: bind_pat_
{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }}
by

G |- lit <= typ
-------------------     :: lit
G |- lit <= typ -| G

%% FIXME do add_local
G(id) = local mutable typ'
---------------------- :: local
G |- id <= typ -| G

G(id) = unbound
---------------------- :: unbound
G |- id <= typ -| G


G(id) = enum typ'
G |- typ' ~< typ
---------------------- :: enum
G |- id <= typ -| G


---------------------- :: wild
G |- _ <= typ -| G


%% FIXME Should be fold?
G |- pat1 <= typ1 -| G1 .. G |- patn <= typn -| Gn
------------------------------------------------------- :: tup
G |- (pat1 , .. , patn ) <= (typ1 , .. , typn ) -| G , G1 .. Gn



defn
G |- pat => typ -| D :: :: infer_pat :: infer_pat_
{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }}
by

G(id) = enum typ 
-------------------- ::  id
G |- id => typ -| G


G |- pat <= typ -| D
------------------------------- :: typ
G |- (typ) pat => typ -| D


G |-l lit => typ
-----------------------  :: lit
G |- lit => typ -| G


defn
G |-i id => typ :: :: infer_id :: infer_id_
{{ com Infer type of indentifier }}
{{ tex [[G]] \vdash_i [[id]] \Rightarrow [[typ]] }}
by


G(id) = local mut typ
---------------------- :: local
G |-i id => typ


G(id) = enum typ
---------------------- :: enum
G |-i id => typ


G(id) = register typ
---------------------- :: register
G |-i id => typ


G(id) = union typquant typ
------------------------------------- :: union
G |-i id => typ

defn
G |-f exp . id => typ :: :: infer_field :: infer_field_
{{ tex [[G]] \vdash_f [[exp]] . [[id]] \Rightarrow [[typ]] }}
by


G |- exp => typ1
G ( typ1 ) = register [ id2 ]
G ( id2 ) = (base,top,ranges)
ranges ( id ) = vec_typ
---------------------------- :: register
G |-f exp . id => vec_typ



G |- exp => typ1
G ( typ1 , id ) = typ
---------------------------- :: record
G |-f exp . id => typ


defn
G |- exp1 => n_constraint :: :: infer_flow :: infer_flow_
by


G |- x => atom < nexp1 >
G |- y => atom < nexp2 >
---------------------------- :: lteq
G |- :E_app: lteq_atom_atom ( x , y ) =>  nexp1 <= nexp2


G |- x => atom < nexp1 >
G |- y => atom < nexp2 >
---------------------------- :: gteq
G |- :E_app: gteq_atom_atom ( x , y ) =>  nexp1 >= nexp2

G |- x => atom < nexp1 >
G |- y => atom < nexp2 >
---------------------------- :: lt
G |- :E_app: lt_atom_atom ( x , y ) =>  nexp1 + numOne <= nexp2

G |- x => atom < nexp1 >
G |- y => atom < nexp2 >
---------------------------- :: gt
G |- :E_app: lteq_atom_atom ( x , y ) =>  nexp1 >= nexp2 + numOne


G |- id => range <nexp1 , nexp2 >
G |- y => atom < nexp >
------------------------------------------------------------------------------- :: lt_range_atom
G |- :E_app: lt_range_atom ( id , y ) => range < nexp1 , min (nexp - 1 , nexp2 ) >




defn
 G |- exp => typ :: :: infer_exp :: infer_exp_
{{ com Infer that type of $[[exp]]$ is $[[typ]]$ }}
{{ tex [[G]] \vdash [[exp]] \Rightarrow [[typ]]  }}
by


G |- exp1 <= unit ... G |- expn <= unit
------------------------------------------ :: nondet
G |- nondet { exp1 ; ... ; expn } => unit


G |-i id => typ
---------------- :: id
G |- id => typ


G |-l lit => typ
---------------- :: lit
G |- lit => typ


----------------------------------- :: sizeof
G |- sizeof nexp => atom < nexp >


-------------------------------------------- :: constraint
G |- constraint n_constraint => bool

G |-f exp . id => typ
------------------------ :: field
G |- exp . id => typ


G |- exp1 => typ1 .... G |- expn => typn
---------------------------------------------------------- :: tuple
G |- ( exp1 , .... , expn ) => (typ1 , .... , typn )




G |- lexp := exp => typ -| D
-------------------- :: assign
G |- lexp := exp => typ



---------------------------- :: record_update
G |- lexp . id := exp => typ


G |- exp <= typ
----------------------- :: cast
G |- ( typ ) exp => typ



G |- :E_app: id ( exp1 , exp2 ) => typ
-------------------------------- :: app_infix
G |- exp1 id exp2 => typ


--------------------------------------- :: app
G |- :E_app: id (exp1 , .. , expn ) => typ



G |- exp1 => bool
G |- exp2 => unit
------------------------------- :: while_loop
G |- while exp1 do exp2 => unit

G |- exp1 => unit
G |- exp2 => bool
------------------------------- :: until_loop
G |- repeat exp1 until exp2 => unit

G |- exp1 => range <nexp1,nexp1'>
G |- exp2 => range <nexp2,nexp2'>
G |= nexp1' <= nexp2
G |- exp3 <= int
G |- exp4 => unit
----------------------------------------------------------------------- :: for_inc
G |-  foreach ( id from exp1 to exp2 by exp3 in inc ) exp4 => unit

G |- exp1 => range <nexp1,nexp1'>
G |- exp2 => range <nexp2,nexp2'>
G |= nexp2' <= nexp1
G |- exp3 <= int
G |- exp4 => unit
----------------------------------------------------------------------- :: for_dec
G |-  foreach ( id from exp1 to exp2 by exp3 in dec ) exp4 => unit


G |- foreach ( id from exp1 to exp2 by exp3 in inc) exp4 => typ
----------------------------------------------------------------------- :: forup
G |- foreach ( id from exp1 to exp2 by exp3 ) exp4 => typ


G |- foreach ( id from exp1 to exp2 by numOne in inc) exp3 => typ
----------------------------------------------------------------------- :: forupbyone
G |- foreach ( id from exp1 to exp2 ) exp3 => typ


G |- foreach ( id from exp1 to exp2 by exp3 in dec) exp4   => typ
--------------------------------------------------------------------------- :: fordown
G |- foreach ( id from exp1 downto exp2 by exp3 ) exp4   => typ

G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3  => typ
------------------------------------------------------------------------- :: fordownbyone
G |- foreach ( id from exp1 downto exp2 ) exp3  => typ


G |- exp1 => n_constraint
%G , flows , constrs |- exp2 => typ
%G , flows , negate constrs |- exp3 <= typ
-------------------------------------------- :: if
G |- if exp1 then exp2 else exp3 => typ

G |- :E_app: vector_access ( exp , exp' ) => typ
------------------------------ :: vector_access
G |- exp [ exp' ] => typ


G |- :E_app: vector_subrange ( exp , exp1 , exp2 ) => typ
--------------------------- :: vector_subrange
G |- exp [ exp1 .. exp2 ] => typ


G |- :E_app: vector_update ( exp , exp1 , exp2 ) => typ
---------------------------------- :: vector_update
G |- :E_vector_update: [ exp with exp1 = exp2] => typ


G |- :E_app: vector_update_subrange ( exp , exp1 , exp2 , exp3 ) => typ
------------------------------------------ ::  vector_update_subrange
G |- :E_vector_update_subrange: [  exp with exp1 : exp2 = exp3 ] => typ


G |- :E_app: vector_append ( exp1 , exp2 ) => typ
----------------------------------- ::   vector_append
G |- exp1 : exp2  => typ


order_inc
G |- exp => typ
G |- exp1 <= typ .. G |- expn <= typ
nexp = length [|| exp , exp1 , .. , expn ||]
-------------------------------------------- :: vector_inc
G |- [|| exp , exp1 , .. , expn ||] => typ [ numZero <: nexp ]

order_dec
G |- exp => typ
G |- exp1 <= typ .. G |- expn <= typ
nexp = length [|| exp , exp1 , .. , expn ||]
-------------------------------------------- :: vector_dec
G |- [|| exp , exp1 , .. , expn ||] => typ [ nexp :> numZero ]


G |- exp1 <= bool
G |- exp2 <= string
----------------------------------- :: assert
G |- assert (exp1, exp2 ) => unit


defn
 G |- exp <= typ :: :: check_exp :: check_exp_
{{ com Check that type of $[[exp]]$ is $[[typ]]$ }}
{{ tex [[G]] \vdash [[exp]] \Leftarrow [[typ]]  }}
by


G |- exp1 <= unit ... G |- expn <= unit
G |- exp <= typ
----------------------------------- :: block
G |- { exp1; ... ; expn ; exp } <= typ