diff options
| author | Kathy Gray | 2013-10-25 14:48:25 +0100 |
|---|---|---|
| committer | Kathy Gray | 2013-10-25 14:48:25 +0100 |
| commit | 694d99ddd473fc44060add438011c1f2873ae58c (patch) | |
| tree | f475f9b0b9f434633523c3399b16925a10c65680 /language | |
| parent | caf7734e5540300856bf8fe2bbcbf3f1faed5c39 (diff) | |
More type rules
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 6 | ||||
| -rw-r--r-- | language/l2_rules.ott | 10 |
2 files changed, 10 insertions, 6 deletions
diff --git a/language/l2.ott b/language/l2.ott index 50f9a353..bc2f0c8d 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1115,7 +1115,7 @@ S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }} {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }} {{ ocaml (assert false) }} - E_t {{ tex \ottnt{E}^{\textsc{t} } }} :: 'E_t_' ::= {{ phantom }} + E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} {{ hol (id |-> t) }} {{ lem map x f_desc }} {{ com Type environments }} @@ -1130,6 +1130,8 @@ S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }} {{ hol arb }} {{ lem arb }} {{ ocaml assert false }} + | E_t u- E_t1 .. E_tn :: M :: multi_set_minus + {{ hol arb }} {{ lem arb }} {{ ocaml assert false }} | ( E_t1 inter .... inter E_tn ) :: M :: intersect {{ hol arb }} {{ lem syntax error }} @@ -1182,6 +1184,8 @@ terminals :: '' ::= {{ tex \ensuremath{\cap} }} | u+ :: :: uplus {{ tex \ensuremath{\uplus} }} + | u- :: :: uminus + {{ tex \ensuremath{\setminus} }} | NOTIN :: :: notin {{ tex \ensuremath{\not\in} }} | SUBSET :: :: subset diff --git a/language/l2_rules.ott b/language/l2_rules.ott index c07f41a0..b1bc3466 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -525,11 +525,11 @@ E_r (id t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/> ------------------------------------------------------------ :: field <E_t,E_r,E_k> |- exp.id : t gives I,E_t -%% % </TD,E,E_l |- pati : t gives E_li//i/> -%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci,S_Ni//i/> -%% % TD,E,E_l |- exp : t gives S_c',S_N' -%% % ------------------------------------------------------------ :: case -%% % TD,E,E_l |- match exp with bar_opt </pati -> expi li//i/> l end : u gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/> +</<E_t,E_r,E_k> |- pati : t gives E_ti,S_Ni//i/> +</<(E_t u+ E_ti),E_r,E_k> |- expi : u gives Ii,E_t'i//i/> +<E_t,E_r,E_k> |- exp : t gives I,E_t +------------------------------------------------------------ :: case +<E_t,E_r,E_k> |- switch exp { </case pati -> expi//i/> }: u gives I u+ </Ii u+ <S_Ni,pure>//i/>, inter </E_t'i//i/> u- </E_ti//i/> <E_t,E_r,E_k> |- exp : t gives I,E_t E_k |- typ ~> t |