diff options
Diffstat (limited to 'language/l2_rules.ott')
| -rw-r--r-- | language/l2_rules.ott | 113 |
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_ ::= |