summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
Diffstat (limited to 'language')
-rw-r--r--language/l2_rules.ott194
-rw-r--r--language/l2_typ.ott3
2 files changed, 121 insertions, 76 deletions
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index e348e14a..a4624527 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -762,6 +762,15 @@ E_d |- u ~< t,S_N
E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u
u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect
+ui == ( implicit<ne>, t0 , .. , tm )
+<E_t,E_d>,(t0,..,tm) |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t'
+E_d,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect'
+------------------------------------------------------------ :: appImplicit
+<E_t,E_d>,t |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, E_t
+
+
+E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u
+u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect
<E_t,E_d>,ui |- exp : ui' gives exp',I,E_t'
E_d,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect'
------------------------------------------------------------ :: app
@@ -799,40 +808,42 @@ S_N' == u+ </S_N'i//i/>
------------------------------------------------------------ :: record
<E_t,<E_k,E_a,E_r,E_e>>,t |- { </idi = expi//i/> semi_opt} : x<t_args> gives{ </idi=exp'i//i/> semi_opt}, u+ <S_N u+ S_N', u+ </effecti//i/>>, {}
-<E_t,<E_k,E_r,E_e>>,t |- exp : id t_args gives exp', I,E_t
-E_r(id t_args) gives </ id'n:t'n//n/>
-</ <E_t,<E_k,E_r,E_e>>,ti |- expi : ui gives expi',Ii,E_t//i/>
+<E_t,<E_k,E_a,E_r,E_e>>,t |- exp : x<t_args> gives exp', I,E_t
+E_r(x<t_args>) gives </ id'n:t'n//n/>
+</ <E_t,<E_k,E_a,E_r,E_e>>,ti |- expi : ui gives expi',Ii,E_t//i/>
</idi:ti//i/> SUBSET </id'n : t'n//n/>
</<E_k,E_a,E_r,E_e> |- ui ~< ti,S_N'i//i/>
------------------------------------------------------------ :: recup
-<E_t,<E_k,E_r,E_e>> ,t |- { exp with </idi = expi//i/> semi_opt } : id t_args gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t
+<E_t,<E_k,E_a,E_r,E_e>> ,t |- { exp with </idi = expi//i/> semi_opt } : x<t_args> gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t
-E,t |- exp1 u1 t gives exp'1,I1,E_t ... E,t |- expn : un gives exp'n,In,E_t
-length(exp1 ... expn) = num
+<E_t,E_d>,t |- exp1 : u1 gives exp'1,I1,E_t' ... <E_t,E_d>,t |- expn : un gives exp'n,In,E_t'
+E_d |- u1 ~< t, S_N1 ... E_d |- un ~< t, S_Nn
+length(exp1 ... expn) == ne
+S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn
------------------------------------------------------------ :: vector
-E, vector<ne1,ne2,ord,t> |- [ exp1 , ... , expn ] : vector<ne3,num,ord,u> gives [exp'1,...,exp'n], I1 u+ ... u+ In, E_t
+E, vector<ne1 ne2 order t> |- [ exp1 , ... , expn ] : vector<ne1 num order t> gives [exp'1,...,exp'n], <S_N,pure> u+ I1 u+ ... u+ In , E_t
-E, vector<ne ne' ord t> |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t
+E, vector<ne ne' order t> |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t
E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t
------------------------------------------------------------- :: vectorgetInc
E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1<=ne3,ne3+ne3'<=ne1+ne1'},pure>,E_t
-E, vector<ne ne' ord t> |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t
+E, vector<ne ne' order t> |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t
E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t
------------------------------------------------------------- :: vectorgetDec
E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1>=ne3,ne3+(-ne3')<=ne1+(-ne1')},pure>,E_t
-E, vector<ne1 ne'1 inc t> |- exp1 : <vector ne2 ne'2 inc u> gives exp'1, I1,E_t
+E, vector<ne1 ne'1 inc t> |- exp1 : vector<ne2 ne'2 inc u> gives exp'1, I1,E_t
E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t
E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t
------------------------------------------------------------- :: vectorsubInc
-E, vector<ne ne' inc t> |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector<ne7 ne'7 inc u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t
+E, vector<ne ne' inc t> |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 inc u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t
-E, vector<ne1 ne'1 dec t> |- exp1 : <vector ne2 ne'2 dec u> gives exp'1, I1,E_t
+E, vector<ne1 ne'1 dec t> |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t
E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t
E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t
------------------------------------------------------------- :: vectorsubDec
-E, vector<ne ne' dec t> |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector<ne7 ne'7 dec u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t
+E, vector<ne ne' dec t> |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 dec u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t
E, vector<ne ne' inc t> |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t
E, range<ne'1 ne'2> |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t
@@ -846,26 +857,43 @@ E,t |- exp2 : u gives exp'2,I2,E_t
------------------------------------------------------------ :: vectorupDec
E, vector<ne ne' dec t> |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 dec u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 >= ne3, ne2 >= ne4},pure>,E_t
-E |- exp : vector ne1 ne2 order t gives I,E_t
-E |- exp1 : enum ne3 ne4 order gives I1,E_t
-E |- exp2 : enum ne5 ne6 order gives I2,E_t
-E |- exp3 : vector ne7 ne8 order t gives I3,E_t
------------------------------------------------------------- :: vecrangeup
-E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4), ne7 + ne8 = ne1 + ne2 + (- ne3) + (- ne4)},pure>,E_t
-
-E |- exp : vector ne1 ne2 order t gives I,E_t
-E |- exp1 : enum ne3 ne4 order gives I1,E_t
-E |- exp2 : enum ne5 ne6 order gives I2,E_t
-E |- exp3 : t gives I3,E_t
------------------------------------------------------------- :: vecrangeupvalue
-E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4)},pure>,E_t
-
-
-E_r (id t_args) gives </idi : ti//i/> id : u </id'j : t'j//j/>
-<E_t,<E_k,E_r,E_e>>,t'' |- exp : id t_args gives exp', I,E_t
+E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t
+E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
+E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
+E,vector<ne9 ne10 inc t> |- exp3 : vector <ne11 ne12 inc u> gives exp3',I3,E_t
+I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure>
+------------------------------------------------------------ :: vecrangeupInc
+E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t
+
+E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t
+E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
+E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
+E,u |- exp3 : u' gives exp3',I3,E_t
+I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure>
+------------------------------------------------------------ :: vecrangeupvalueInc
+E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t
+
+E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t
+E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
+E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
+E,vector<ne9 ne10 dec t> |- exp3 : vector <ne11 ne12 dec u> gives exp3',I3,E_t
+I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure>
+------------------------------------------------------------ :: vecrangeupDec
+E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t
+
+E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t
+E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
+E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
+E,u |- exp3 : u' gives exp3',I3,E_t
+I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure>
+------------------------------------------------------------ :: vecrangeupvalueDec
+E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t
+
+E_r (x<t_args>) gives </idi : ti//i/> id : u </id'j : t'j//j/>
+<E_t,<E_k,E_a,E_r,E_e>>,t'' |- exp : x< t_args> gives exp', I,E_t
E_d,t |- exp'.id : u gives t', exp1', S_N', effect
------------------------------------------------------------ :: field
-<E_t,<E_k,E_r,E_e>>,t |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t
+<E_t,<E_k,E_a,E_r,E_e>>,t |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t
<E_t,E_d>,t'' |- exp : u gives exp',I,E_t
</<E_t,E_d>,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/>
@@ -874,94 +902,108 @@ E_d,t |- exp'.id : u gives t', exp1', S_N', effect
<E_t,E_d>,t |- switch exp { </case pati -> expi//i/> }: u gives switch exp' { </case pat'i -> exp'i//i/> }, I u+ </Ii u+ <S_Ni,pure>//i/>, E_t
<E_t,E_d>,t'' |- exp : u gives exp',I,E_t
-E_d |- typ |-> t'
+E_d |- typ ~> t'
E_d,t' |- exp' : u gives u', exp'', S_N,effect
E_d,t |- exp'' : t' gives u'', exp''', S_N', effect'
------------------------------------------------------------ :: typed
-<E_t,E_d>,t |- (typ) exp : t gives exp''',Iu+<S_N u+ S_N',effect u+ effect'>,E_t
+<E_t,E_d>,t |- (typ) exp : t gives exp''',I u+ <S_N u+ S_N',effect u+ effect'>,E_t
<E_t,E_d> |- letbind gives E_t1, S_N, effect, {}
-<(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2
+<(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2
------------------------------------------------------------ :: let
-<E_t,E_d> |- letbind in exp : t gives <S_N,effect> u+ I2, E_t
+<E_t,E_d>,t |- letbind in exp : t gives exp', <S_N,effect> u+ I2, E_t
-E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t
+E,t1 |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn |- expn : un gives expn',In,E_tn
------------------------------------------------------------ :: tup
-E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In,E_t
+E,(t1, ...., tn) |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t
-E |- exp1 : t gives I1,E_t .. E |- expn : t gives In,E_t
+<E_t,E_d>,t |- exp1 : u1 gives exp1', I1,E_t1 .. <E_t,E_d>,t |- expn : un gives expn', In,E_tn
+E_d |- u1 ~< t,S_N1 .. E_d |- un ~< t,S_Nn
------------------------------------------------------------ :: list
-E |- [||exp1, .., expn ||] : list t gives I1 u+ .. u+ In,E_t
+<E_t,E_d>,list<t> |- [||exp1, .., expn ||] : list<u> gives [|| exp1', .., expn' ||], <S_N1 u+ .. u+ S_Nn,pure> u+ I1 u+ .. u+ In, E_t
-E |- exp1 : bool gives I1,E_t
-E |- exp2 : t gives I2,E_t2
-E |- exp3 : t gives I3,E_t3
+E,bit |- exp1 : bit gives exp1',I1,E_t'
+E,t |- exp2 : u1 gives exp2',I2,E_t2
+E,t |- exp3 : u2 gives exp3',I3,E_t3
+E_d |- u1 ~< t,S_N1
+E_d |- u2 ~< t,S_N2
------------------------------------------------------------ :: if
-E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3,(E_t2 inter E_t3)
+<E_t,E_d>,t |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', <S_N1 u+ S_N2,pure> u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3)
-<E_t,E_d> |- exp1 : enum ne1 ne2 order gives I1,E_t
-<E_t,E_d> |- exp2 : enum ne3 ne4 order gives I2,E_t
-<E_t,E_d> |- exp3 : enum ne5 ne6 order gives I3,E_t
-<(E_t u+ {id |-> enum ne1 ne3+ne4 order}),E_d> |- exp4 : t gives I4,(E_t u+ {id |-> enum ne1 ne3+ne4 order})
+<E_t,E_d>,range<ne1 ne2> |- exp1 : range< ne7 ne8> gives exp1', I1,E_t
+<E_t,E_d>,range<ne3 ne4> |- exp2 : range< ne9 ne10> gives exp2', I2,E_t
+<E_t,E_d>,range<ne5 ne6> |- exp3 : range< ne11 ne12> gives exp3',I3,E_t
+<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit |- exp4 : t gives exp4',I4,E_t'
----------------------------------------------------------- :: for
-<E_t,E_d> |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t
+<E_t,E_d>,unit |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t
-E |- exp1 : t gives I1,E_t
-E |- exp2 : list t gives I2,E_t
+E,t |- exp1 : u gives exp1',I1,E_t
+E,list<t> |- exp2 : list<u> gives exp2',I2,E_t
------------------------------------------------------------ :: cons
-E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t
+E,list<t> |- exp1 :: exp2 : list<u> gives exp1'::exp2', I1 u+ I2,E_t
-|- lit : t
+t |- lit : u => exp,S_N
------------------------------------------------------------ :: lit
-<E_t,E_d> |- lit : t gives Ie,E_t
+E,t |- lit : u gives exp,<S_N,pure>,E_t
-<E_t,E_d> |- exp : t gives I, E_t1
+<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1
------------------------------------------------------------ :: blockbase
-<E_t,E_d> |- { exp } : unit gives I, E_t
+<E_t,E_d>,unit |- { exp } : unit gives {exp'}, I, E_t
-<E_t,E_d> |- exp : u gives I1, E_t1
-<(E_t u+ E_t1),E_d> |- { </expi//i/> } : t gives I2, E_t2
+<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1
+<(E_t u+ E_t1),E_d>,unit |- { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2
------------------------------------------------------------ :: blockrec
-<E_t,E_d> |- { exp ; </expi//i/> } : t gives I1 u+ I2, E_t
+<E_t,E_d>,unit |- { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t
+<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1
+------------------------------------------------------------ :: nondetbase
+<E_t,E_d>,unit |- nondet { exp } : unit gives {exp'}, I, E_t
-<E_t,E_d> |- nondet { exp ; </expi//i/> } : unit
+<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1
+<(E_t u+ E_t1),E_d>,unit |- nondet { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2
+------------------------------------------------------------ :: nondetrec
+<E_t,E_d>,unit |- nondet { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t
-E |- exp:t gives I1, E_t1
-E |- lexp:t gives I2, E_t2
+E,t |- exp:u gives exp', I1, E_t1
+E |- lexp:t gives lexp', I2, E_t2
------------------------------------------------------------ :: assign
-E |- lexp := exp : unit gives I u+ I2, E_t2
+E,unit |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2
defn
-E |- lexp : t gives I , E_t :: :: check_lexp :: check_lexp_
+E |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_
{{ com Check the left hand side of an assignment }}
by
-E_t(id) gives register t
+E_t(id) gives register<t>
---------------------------------------------------------- :: wreg
-<E_t,E_d> |- id : t gives <{},{ wreg }>, E_t
+<E_t,E_d> |- id : t gives id,<{},{ wreg }>, E_t
-E_t(id) gives reg t
+E_t(id) gives reg<t>
---------------------------------------------------------- :: wlocl
-<E_t,E_d> |- id : t gives Ie, E_t
+<E_t,E_d> |- id : t gives id,Ie, E_t
E_t(id) gives t
---------------------------------------------------------- :: var
-<E_t,E_d> |- id : t gives Ie,E_t
+<E_t,E_d> |- id : t gives id,Ie,E_t
id NOTIN dom(E_t)
---------------------------------------------------------- :: wnew
-<E_t,E_d> |- id : t gives Ie, {id |-> reg t}
+<E_t,E_d> |- id : t gives id,Ie, {id |-> reg<t>}
-E_t(id) gives t1 -> t {</base_effecti//i/>, wmem, </base_effect'j//j/>} Extern {}
-<E_t,E_d> |- exp : t1 gives I,E_t1
+E_t(id) gives E_k, S_N, Extern, t1 -> t {</base_effecti//i/>, wmem, </base_effect'j//j/>}
+<E_t,E_d>,t1 |- exp : u1 gives exp',I,E_t1
---------------------------------------------------------- :: wmem
-<E_t,E_d> |- :LEXP_memory: id(exp) : t gives I u+ <{},{wmem}>,E_t
+<E_t,E_d> |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wmem}>,E_t
+
+E,atom<ne> |- exp : u gives exp',I1,E_t
+E |- lexp : vector<ne1 ne2 inc t> gives lexp',I2,E_t
+---------------------------------------------------------- :: wbitInc
+E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t
-E |- exp : enum ne1 ne2 order gives I1,E_t
-E |- lexp : vector ne3 ne4 order t gives I2,E_t
----------------------------------------------------------- :: wbit
-E |- lexp [exp] : t gives I1 u+ I2 u+ <{ne3 <= ne1, ne1 + ne2 <= ne3 + ne4},pure>,E_t
+E,atom<ne> |- exp : u gives exp',I1,E_t
+E |- lexp : vector<ne1 ne2 dec t> gives lexp',I2,E_t
+---------------------------------------------------------- :: wbitDec
+E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t
E |- exp1 : enum ne1 ne2 order gives I1,E_t
E |- exp2 : enum ne3 ne4 order gives I2,E_t
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
index 21002502..77b956c5 100644
--- a/language/l2_typ.ott
+++ b/language/l2_typ.ott
@@ -53,6 +53,8 @@ t , u :: 'T_' ::=
| atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }}
| vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }}
| list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }}
+ | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }}
+ | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }}
| bit :: S :: bit_typ {{ ichlo T_id "bit" }}
| string :: S :: string_typ {{ ichlo T_id "string" }}
| unit :: S :: unit_typ {{ ichlo T_id "unit" }}
@@ -348,6 +350,7 @@ grammar
{{ lem (Inf [[S_N]] [[effect]]) }}
| Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
{{ lem Iemp }}
+ | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }}
| I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }}
{{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 17:00:33 +0000