Merge branch 'interp_typed'

Conflicts:
	src/lem_interp/interp.lem
	src/lem_interp/run_interp.ml

1 files changed, 0 insertions, 318 deletions

diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 7e3efcb7..3bade9d4 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -1,323 +1,5 @@
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules                                   %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-embed
-{{ lem
-
-let rec remove_one i l =
-  match l with
-  | [] -> []
-  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
-end
-
-let rec remove_from l l2 =
-  match l2 with 
-  | [] -> l
-  | i::l2' -> remove_from (remove_one i l) l2'
-end
-
-let disjoint s1 s2 = Set.null (s1 inter s2)
-
-let rec disjoint_all sets =
-  match sets with
-  | [] -> true
-  | s1::[] -> true
-  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
-end
-}}
-
- 
-grammar 
-
-k :: 'Ki_' ::=
-{{ com Internal kinds }}
-   | K_Typ                                             :: :: typ
-   | K_Nat                                             :: :: nat
-   | K_Ord                                             :: :: ord
-   | K_Efct                                            :: :: efct
-   | K_Lam ( k0 .. kn -> k' )                          :: :: ctor
-   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
-   | K_Abbrev t                                        :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}
-
-t , u :: 'T_' ::=                                
-{{ com Internal types }}
-   | id                                           :: :: id
-   | kid                                          :: :: var
-   | t1 -> t2 effect tag S_N                      :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
-   | ( t1 * .... * tn )                           :: :: tup
-   | id t_args                                    :: :: app 
-   | register t_args                              :: :: reg_app
-   | t [ t1 / id1 ... tn / idn ]		  :: :: subst
-
-tag :: 'Tag_' ::=                                 
-{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
-   | None                                 :: :: empty 
-   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
-   | Extern                               :: :: extern {{ com External function, specied only with a val statement }}
-   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
-   | _                                    :: :: dontcare 
-
-ne :: 'Ne_' ::=
- {{ com internal numeric expressions }}
-   | kid                                 :: :: var
-   | num                                 :: :: const
-   | ne1 * ne2                           :: :: mult
-   | ne1 + ... + nen                     :: :: add
-   | 2 ** ne				 :: :: exp
-   | ( - ne )                            :: :: unary
-   | zero   				 :: M :: zero
-     {{ lem (Ne_const 0) }}
-   | bitlength ( bin )                   :: M :: cbin
-     {{ ocaml (asssert false) }}
-     {{ hol ARB }}
-     {{ lem (blength [[bin]]) }}
-   | bitlength ( hex )                   :: M :: chex
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (hlength [[hex]]) }}
-   | length ( pat1 ... patn )            :: M :: cpat
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-   | length ( exp1 ... expn )            :: M :: cexp
-     {{ hol ARB }}
-     {{ ocaml (assert false) }}
-     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
- 
- t_arg :: 't_arg_' ::=  
- {{ com Argument to type constructors }}
- | t :: :: typ
- | ne :: :: nexp
- | effect :: :: effect
- | order :: :: order
-
- t_args :: '' ::=   {{ lem list t_arg }}
-  {{ com Arguments to type constructors }}
-   | t_arg1 ... t_argn                            :: :: T_args
-
- nec :: 'Nec_' ::=
-   {{ com Numeric expression constraints }}
-   | ne <= ne'            :: :: lteq
-   | ne = ne'            :: :: eq
-   | ne >= ne'           :: :: gteq
-   | kid 'IN' { num1 , ... , numn } :: :: in
-
-S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
-                                                                    {{ hol nec list }}
-                                                                    {{ lem list nec }}
-    {{ com nexp constraint lists }}
-    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-      {{ hol [[nec1 .. necn]] }}
-      {{ lem [[nec1 .. necn]] }}
-   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
-     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
-     {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }}
-     {{ ocaml (assert false) }}
-   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
-     {{ ocaml (assert false) }}
-     {{ ichl todo }}
-   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
-     {{ ocaml assert false }}
-     {{ ichl todo }}
-   | resolve ( S_N )                                                :: :: resolution
-     {{ lem [[S_N]] (* Write constraint solver *) }}
- 
-
- E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=  {{ phantom }}
-                                                         {{ lem definition_env }}
- {{ com Environments storing top level information, such as defined records, enumerations, and kinds }}
- | < E_k , E_r , E_e >	     	       		    	 :: :: base
-   {{ hol arb }}
-   {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }}
- | empty       	     					 :: :: empty
-   {{ hol arb }}
-   {{ lem DenvEmp }}
- | E_d u+ E_d'						 :: :: union
-   {{ hol arb }}
-   {{ lem (denv_union [[E_d]] [[E_d']]) }}
- 
- kinf :: 'kinf_' ::=
-   {{ com Whether a kind is default or from a local binding }}
-   | k                                        :: :: k
-   | k default                                :: :: def
-
- tid :: 'tid_' ::=
-   {{ com A type identifier or type variable }}
-   | id                                      :: :: id
-   | kid                                     :: :: var
-
- E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
-                                                                 {{ hol (tid-> kinf) }}
-                                                                 {{ lem (map tid kinf) }}
-   {{ com Kind environments }}
-   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
-     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
-     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
-   | E_k1 u+ .. u+ E_kn                                          :: M :: union
-     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
-     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }}
-     {{ ocaml (assert false) }}
-   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
-     {{ ocaml assert false }}
-
- 
- tinf :: 'tinf_' ::=                                                 
-    {{ com Type variables, type, and constraints, bound to an identifier }}
-    | t                                                 :: :: typ
-    | E_k , S_N , tag , t         :: :: quant_typ                                                             
-
- field_typs :: 'FT_' ::=     {{ phantom }}
-                             {{ lem list (id * t) }}
- {{ com Record fields }}
- | id1 : t1 , .. , idn : tn :: :: fields
-   {{ lem [[id1 t1..idn tn]] }}
-
- E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
-                                                                 {{ hol (id*t) |-> tinf) }}
-                                                                 {{ lem map (list (id*t)) tinf }}
-   {{ com Record environments }}
-   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} 
-   | E_r1 u+ .. u+ E_rn                                          :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }}
-     {{ ocaml (assert false) }}
-
-  enumerate_map :: '' ::=                                        {{ phantom }}
-                                                                 {{ lem (list (nat*id)) }}
-   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
-    {{ lem [[num1 id1...numn idn]] }}
-
-  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
-                                                                 {{ lem (map t (list (nat*id))) }}
-   {{ com Enumeration environments }}
-   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
-   | E_e1 u+ .. u+ E_en                                         :: :: union
-     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}
-
-    
-embed
-{{ lem
- type definition_env =
-   | DenvEmp
-   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
-
-}}
-
 grammar
 
- E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
-                                                                 {{ hol (id |-> tinf) }}
-                                                                 {{ lem map id tinf }}
-   {{ com Type environments }}
-   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
-   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}
-     {{ ocaml (assert false) }}
-   | u+ E_t1 .. E_tn                                            :: M :: multi_union
-     {{ hol arb }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-   | E_t u- E_t1 .. E_tn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} 
-     {{ ocaml assert false }}
-   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b)))))  Map.empty [[E_t1....E_tn]]) }} 
-     {{ ocaml (assert false) }}
-   | inter E_t1 .. E_tn                                            :: M :: multi_inter
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-
-
-ts :: ts_ ::=                                     {{ phantom }}
-                                                  {{ lem list t }}
-  | t1 , .. , tn :: :: lst 
-
-embed
-{{ lem
-let blength (bit) = Ne_const 8
-let hlength (bit) = Ne_const 8
-
- type env =
-   | EnvEmp 
-   | Env of (map id tinf) * definition_env
-
- type inf = 
-   | Iemp
-   | Inf of (list nec) * effect
-
- val denv_union : definition_env -> definition_env -> definition_env
- let denv_union de1 de2 = 
-  match (de1,de2) with
-   | (DenvEmp,de2) -> de2
-   | (de1,DenvEmp) -> de1
-   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
-      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
-   end
-
- val env_union : env -> env -> env
- let env_union e1 e2 =
-   match (e1,e2) with
-    | (EnvEmp,e2) -> e2
-    | (e1,EnvEmp) -> e1
-    | ((Env te1 de1),(Env te2 de2)) ->
-      Env (te1 union te2) (denv_union de1 de2)
- end
-
-let inf_union i1 i2 =
-  match (i1,i2) with 
- | (Iemp,i2) -> i2
- | (i1,Iemp) -> i1
- | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
- end
-
-let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
-
-}}
-
-grammar
-
- E :: '' ::=                                                     
-                                                                 {{ hol ((string,env_body) fmaptree) }}
-                                                                 {{ lem env }}
- {{ com Definition environment and lexical environment }}
- | < E_t , E_d >                                           :: :: E
-  {{ hol arb }}
-  {{ lem (Env [[E_t]] [[E_d]])  }}
- | empty                                                       :: M :: E_empty
-   {{ hol arb }}
-   {{ lem EnvEmp }}
-   {{ ocaml assert false }}
- | E u+ E'                                                      :: :: E_union
-   {{ lem (env_union [[E]] [[E']]) }}
-
- I :: '' ::=                                                     {{ lem inf }}
-  {{ com Information given by type checking an expression }}
-  | < S_N , effect >                                      :: :: I
-    {{ lem (Inf [[S_N]] [[effect]]) }}
-  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
-    {{ lem Iemp }}
-  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
-    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
-
-
 formula :: formula_ ::=
   | judgement                                                   :: :: judgement