More lem homs

1 files changed, 68 insertions, 45 deletions

diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index d865d0ed..71a9b368 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -1,8 +1,47 @@
-grammar
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Machinery for typing rules                                   %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+embed
+{{ lem
+
+let blength (bit) = Ne_const 8
+let hlength (bit) = Ne_const 8
+
+%% %% let rec sumation_nes nes = match nes with
+%% %%   | [ a; b] -> Ne_add a b 
+%% %%   | x :: y -> Ne_add x (sumation_nes y)
+%% %% end
+%% %% 
+
+ type definition_type =
+   | DenvEmp
+   | Denv of (map tid kinf)  (map ... ...) (map ... ...)
+
+ type env =
+   | EnvEmp 
+   | Env of (map x v_desc) * definition_type
+
+ val denv_union : definition_type -> definition_type -> definition_type
+ let denv_union de1 de2 = 
+  match (de1,de2) with
+   | (DenvEmp,de2) -> de2
+   | (de1,DenvEmp) -> de1
+   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
+      Denv (union_map ke1 ke2) (union_map re1 re2) (union_map ee1 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 (union_map te1 te2) (denv_union de1 de2)
+ end
+}}
+
  
 grammar 
 
@@ -77,37 +116,6 @@ ne :: 'Ne_' ::=
    | ne >= ne'           :: :: gteq
    | kid 'IN' { num1 , ... , numn } :: :: in
 
-%%embed
-%%{{ lem
-%%
-%%let blength (bit) = Ne_const 8
-%%let hlength (bit) = Ne_const 8
-
-%% %% let rec sumation_nes nes = match nes with
-%% %%   | [ a; b] -> Ne_add a b 
-%% %%   | x :: y -> Ne_add x (sumation_nes y)
-%% %% end
-%% %% 
-
-%% type definition_type =
-%%   | DenvEmp
-%%   | Denv of (map tid k_inf)  
-%%
-%% type env =
-%%   | EnvEmp 
-%%   | Env of (map x v_desc) * definition_type
-
-%% %% 
-%% %% val env_union : env -> env -> env
-%% %% let env_union e1 e2 =
-%% %%   match (e1,e2) with
-%% %%    | (EnvEmp,e2) -> e2
-%% %%    | (e1,EnvEmp) -> e1
-%% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
-%% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
-%% %% end
-%%}}
-
 S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
                                                                     {{ hol nec list }}
                                                                     {{ lem list nec }}
@@ -147,12 +155,19 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
    {{ lem EnvEmp }}
    {{ ocaml assert false }}
  | E u+ E'                                                      :: :: E_union
+   {{ lem (env_union [[E]] [[E']]) }}
 
  E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=
  {{ 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 }}
@@ -165,8 +180,8 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
    | kid                                     :: :: var
 
  E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::=             {{ phantom }}
-                                                                 {{ hol (tid-> k) }}
-                                                                 {{ lem map tid k }}
+                                                                 {{ 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]]) }}
@@ -177,7 +192,9 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
      {{ lem (List.fold_right union_map [[E_k1..E_kn]] Map.empty) }}
      {{ ocaml (assert false) }}
    | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
-     {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
+     {{ hol arb }} 
+     {{ lem (remove_from [[E_k]] (List.fold_right union_map [[E_k1..E_kn]] Map.empty)) }} 
+     {{ ocaml assert false }}
 
  
  tinf :: 'tinf_' ::=                                                 
@@ -185,7 +202,7 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
     | t                                                 :: :: typ
     | E_k , S_N , tag , t         :: :: quant_typ                                                                 
 
- E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=             {{ phantom }}
+ E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
                                                                  {{ hol (id |-> tinf) }}
                                                                  {{ lem map x f_desc }}
    {{ com Type environments }}
@@ -198,45 +215,51 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
      {{ ocaml (assert false) }}
    | u+ E_t1 .. E_tn                                            :: M :: multi_union
      {{ hol arb }}
-     {{ lem arb }}
+     {{ lem (List.fold_right union_map [[E_t1..E_tn]] Map.empty) }}
      {{ ocaml assert false }}
    | E_t u- E_t1 .. E_tn                                            :: M :: multi_set_minus
-     {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
+     {{ hol arb }} {{ lem (remove_from [[E_t]] (List.fold_right union_map [[E_t1..E_tn]] Map.empty)) }} {{ ocaml assert false }}
    | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
      {{ hol arb }}
-     {{ lem syntax error }}
+     {{ lem (List.fold_right intersect_map [[E_t1....E_tn]] Map.empty) }} 
      {{ ocaml (assert false) }}
    | inter E_t1 .. E_tn                                            :: M :: multi_inter
      {{ hol arb }}
-     {{ lem arb }}
+     {{ lem (List.fold_right intersect_map [[E_t1..E_tn]] Map.empty) }}
      {{ ocaml assert false }}
 
 
  field_typs :: 'FT_' ::=     {{ phantom }}
+                             {{ lem list (id * t) }}
  {{ com Record fields }}
  | id1 : t1 , .. , idn : tn :: :: fields
 
  E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
-                                                                 {{ hol (id |-> t) }}
-                                                                 {{ lem map x f_desc }}
+                                                                 {{ 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.fold_right (fun (x,f) m -> Map.insert x f m)  Map.empty) }} 
+     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m) [[field_typs1 tinf1..field_typsn tinfn]] Map.empty) }} 
    | E_r1 u+ .. u+ E_rn                                          :: M :: union
      {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
      {{ lem (List.fold_right union_map [[E_r1..E_rn]] Map.empty) }}
      {{ ocaml (assert false) }}
 
-  enumerate_map :: '' ::=
+  enumerate_map :: '' ::=                                        {{ phantom }}
+                                                                 {{ lem (list (num*id)) }}
    | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
 
-  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=
+  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
+                                                                 {{ lem (map t (list (num*id))) }}
    {{ com Enumeration environments }}
    | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
+     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m) [[t1 enumerate_map1..tn enumerate_mapn]] Map.empty) }} 
    | E_e1 u+ .. u+ E_en                                         :: :: union
+     {{ lem (List.fold_right union_map [[E_e1..E_en]] Map.empty) }}
 
 ts :: ts_ ::=                                     {{ phantom }}
+                                                  {{ lem list t }}
   | t1 , .. , tn :: :: lst 
 
 formula :: formula_ ::=