diff options
| -rw-r--r-- | language/l2_rules.ott | 54 |
1 files changed, 43 insertions, 11 deletions
diff --git a/language/l2_rules.ott b/language/l2_rules.ott index fdd81c96..7d05457e 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -524,17 +524,42 @@ length(exp1 ... expn) = num ------------------------------------------------------------ :: vector E |- [ exp1 , ... , expn ] : vector zero num inc t gives I1 u+ ... u+ In -%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N -%% % |- nexp ~> ne -%% % ------------------------------------------------------------- :: vectorget -%% % TD,E,E_l |- exp .( nexp ) : t gives S_c,S_N union {ne<ne'} -%% % -%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N -%% % |- nexp1 ~> ne1 -%% % |- nexp2 ~> ne2 -%% % ne = :Ne_add: ne2 + (- ne1) -%% % ------------------------------------------------------------- :: vectorsub -%% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'} +E |- exp1 : vector ne ne' inc t gives I1 +E |- exp2 : enum ne2 ne2' inc gives I2 +------------------------------------------------------------- :: vectorgetInc +E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne<=ne2,ne2+ne2'<=ne+ne'},pure,None> + +E |- exp1 : vector ne ne' dec t gives I1 +E |- exp2 : enum ne2 ne'2 dec gives I2 +------------------------------------------------------------- :: vectorgetDec +E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne>=ne2,ne2+(-ne2')<=ne+(-ne')},pure,None> + +E |- exp1 : vector ne ne' order t gives I1 +E |- exp2 : enum ne2 ne'2 order gives I2 +E |- exp3 : enum ne3 ne'3 order gives I3 +------------------------------------------------------------- :: vectorsub +E |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector :t_arg_nexp: id :t_arg_nexp: id' order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, id >= ne2 , id <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, id' <=ne3 + ne'3},pure,None> + +E |- exp : vector ne1 ne2 order t gives I +E |- exp1 : enum ne3 ne4 order gives I1 +E |- exp2 : t gives I2 +------------------------------------------------------------ :: vectorup +E |- [ exp with exp1 = exp2 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne1 + ne2 >= ne3 + ne4},pure,None> + +E |- exp : vector ne1 ne2 order t gives I +E |- exp1 : enum ne3 ne4 order gives I1 +E |- exp2 : enum ne5 ne6 order gives I2 +E |- exp3 : vector ne7 ne8 order t gives I3 +------------------------------------------------------------ :: 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,None> + +E |- exp : vector ne1 ne2 order t gives I +E |- exp1 : enum ne3 ne4 order gives I1 +E |- exp2 : enum ne5 ne6 order gives I2 +E |- exp3 : t gives I3 +------------------------------------------------------------ :: 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,None> + E_r (id t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/> <E_t,E_r,E_k> |- exp : id t_args gives I @@ -572,6 +597,13 @@ E |- exp3 : t gives I3 ------------------------------------------------------------ :: if E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3 +<E_t,E_r,E_k> |- exp1 : enum ne1 ne2 order gives I1 +<E_t,E_r,E_k> |- exp2 : enum ne3 ne4 order gives I2 +<E_t,E_r,E_k> |- exp3 : enum ne5 ne6 order gives I3 +<E_t u+ {id |-> enum ne1 ne3+ne4 order},E_r,E_k> |- exp4 : t gives I4 +----------------------------------------------------------- :: for +<E_t,E_r,E_k> |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure,None> + E |- exp1 : t gives I1 E |- exp2 : list t gives I2 ------------------------------------------------------------ :: cons |