Improvements to menhir pretty printer and ocaml backend

Menhir pretty printer can now print enough sail to be useful with ASL parser

Fixity declarations are now preserved in the AST

Menhir parser now runs without the Pre-lexer

Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag

1 files changed, 54 insertions, 7 deletions

diff --git a/src/parser2.mly b/src/parser2.mly
index 59db84a1..a2fb3bfb 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -127,7 +127,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone Bits By Match Clause Dec Def Default Effect EFFECT End Op
 %token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch
+%token Undefined Union With Val Constraint Throw Try Catch Exit
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 %nonassoc Then
@@ -152,6 +152,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
+%token <Parse_ast.fixity_token> Fixity
+
 %start file
 %start typschm_eof
 %type <Parse_ast.typschm> typschm_eof
@@ -198,6 +200,14 @@ id:
   | Op Plus { mk_id (DeIid "+") $startpos $endpos }
   | Op Minus { mk_id (DeIid "-") $startpos $endpos }
   | Op Star { mk_id (DeIid "*") $startpos $endpos }
+  | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
+  | Op Lt { mk_id (DeIid "<") $startpos $endpos }
+  | Op Gt { mk_id (DeIid ">") $startpos $endpos }
+  | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
+  | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
+  | Op Amp { mk_id (DeIid "&") $startpos $endpos }
+  | Op Bar { mk_id (DeIid "|") $startpos $endpos }
+  | Op Caret { mk_id (DeIid "^") $startpos $endpos }
 
 op0: Op0 { mk_id (Id $1) $startpos $endpos }
 op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -585,12 +595,24 @@ typschm_eof:
   | typschm Eof
     { $1 }
 
-pat:
+pat1:
   | atomic_pat
     { $1 }
-  | atomic_pat As id
+  | atomic_pat At pat_concat
+    { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+
+pat_concat:
+  | atomic_pat
+    { [$1] }
+  | atomic_pat At pat_concat
+    { $1 :: $3 }
+
+pat:
+  | pat1
+    { $1 }
+  | pat1 As id
     { mk_pat (P_as ($1, $3)) $startpos $endpos }
-  | atomic_pat As kid
+  | pat1 As kid
     { mk_pat (P_var ($1, $3)) $startpos $endpos }
 
 pat_list:
@@ -610,12 +632,14 @@ atomic_pat:
     { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $startpos $endpos }
-  | pat Colon typ
+  | atomic_pat Colon typ
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
   | Lparen pat Rparen
     { $2 }
   | Lparen pat Comma pat_list Rparen
     { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+  | Lsquare pat_list Rsquare
+    { mk_pat (P_vector $2) $startpos $endpos }
 
 lit:
   | True
@@ -695,6 +719,7 @@ exp2:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp3 { $1 }
 exp2l:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -703,12 +728,14 @@ exp2l:
 exp2r:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp3 { $1 }
 
 exp3:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4 { $1 }
 exp3l:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -717,10 +744,16 @@ exp3l:
 exp3r:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4 { $1 }
 
 exp4:
   | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 { $1 }
@@ -845,6 +878,8 @@ atomic_exp:
     { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
+  | atomic_exp Dot id
+    { mk_exp (E_field ($1, $3)) $startpos $endpos }
   | id
     { mk_exp (E_id $1) $startpos $endpos }
   | kid
@@ -853,6 +888,8 @@ atomic_exp:
     { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
   | id Lparen exp_list Rparen
     { mk_exp (E_app ($1, $3)) $startpos $endpos }
+  | Exit Lparen exp Rparen
+    { mk_exp (E_exit $3) $startpos $endpos }
   | Sizeof Lparen typ Rparen
     { mk_exp (E_sizeof $3) $startpos $endpos }
   | Constraint Lparen nc Rparen
@@ -886,11 +923,19 @@ funcl:
   | id pat Eq exp
     { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
 
+funcls:
+  | id pat Eq exp
+    { [mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos] }
+  | id pat Eq exp And funcls
+    { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos :: $6 }
+
 type_def:
   | Typedef id typquant Eq typ
     { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
   | Typedef id Eq typ
     { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
+  | Struct id Eq Lcurly struct_fields Rcurly
+    { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Struct id typquant Eq Lcurly struct_fields Rcurly
     { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
   | Enum id Eq enum_bar
@@ -939,8 +984,8 @@ type_unions:
     { $1 :: $3 }
 
 fun_def:
-  | Function_ funcl
-    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
+  | Function_ funcls
+    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
 
 let_def:
   | Let_ letbind
@@ -977,6 +1022,8 @@ scattered_def:
 def:
   | fun_def
     { DEF_fundef $1 }
+  | Fixity
+    { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) }
   | val_spec_def
     { DEF_spec $1 }
   | type_def