Remove base effects from Lexer and Parser

We're still a bit away from removing effect annotations entirely,
but this commit is one step closer

src/lib/lexer.mll

@@ -143,21 +143,6 @@ let kw_table =
      ("do",                      (fun _ -> Do));
      ("mutual",                  (fun _ -> Mutual));
      ("bitfield",                (fun _ -> Bitfield));
-     ("barr",                    (fun _ -> Barr));
-     ("depend",                  (fun _ -> Depend));
-     ("rreg",                    (fun _ -> Rreg));
-     ("wreg",                    (fun _ -> Wreg));
-     ("rmem",                    (fun _ -> Rmem));
-     ("rmemt",                   (fun _ -> Rmem));
-     ("wmem",                    (fun _ -> Wmem));
-     ("wmv",                     (fun _ -> Wmv));
-     ("wmvt",                    (fun _ -> Wmv));
-     ("eamem",                   (fun _ -> Eamem));
-     ("exmem",                   (fun _ -> Exmem));
-     ("undef",                   (fun _ -> Undef));
-     ("unspec",                  (fun _ -> Unspec));
-     ("nondet",                  (fun _ -> Nondet));
-     ("escape",                  (fun _ -> Escape));
      ("configuration",           (fun _ -> Configuration));
      ("termination_measure",     (fun _ -> TerminationMeasure));
      ("forwards",                (fun _ -> Forwards));

src/lib/parse_ast.ml

@@ -96,31 +96,12 @@ type kind_aux =
 
 type kind = K_aux of kind_aux * l
 
-type base_effect_aux =
-  | (* effect *)
-    BE_rreg (* read register *)
-  | BE_wreg (* write register *)
-  | BE_rmem (* read memory *)
-  | BE_wmem (* write memory *)
-  | BE_wmv (* write memory value *)
-  | BE_eamem (* address for write signaled *)
-  | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
-  | BE_barr (* memory barrier *)
-  | BE_depend (* dynamically dependent footprint *)
-  | BE_undef (* undefined-instruction exception *)
-  | BE_unspec (* unspecified values *)
-  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
-  | BE_escape
-  | BE_config
-
 type kid_aux = (* identifiers with kind, ticked to differentiate from program variables *)
   | Var of x
 
 type id_aux = (* Identifier *)
   | Id of x | Operator of x (* remove infix status *)
 
-type base_effect = BE_aux of base_effect_aux * l
-
 type kid = Kid_aux of kid_aux * l
 
 type id = Id_aux of id_aux * l
@@ -158,7 +139,7 @@ type atyp_aux =
   | ATyp_infix of (atyp infix_token * Lexing.position * Lexing.position) list
   | ATyp_inc (* increasing *)
   | ATyp_dec (* decreasing *)
-  | ATyp_set of base_effect list (* effect set *)
+  | ATyp_set of id list (* effect set *)
   | ATyp_fn of atyp * atyp * atyp (* Function type, last atyp is an effect *)
   | ATyp_bidir of atyp * atyp * atyp (* Mapping type, last atyp is an effect *)
   | ATyp_wild

src/lib/parser.mly

@@ -122,7 +122,6 @@ let rec same_pat_ops (Id_aux (_, l) as op) = function
                                 (string_of_id op')))
   | [] -> ()
 
-let mk_effect e n m = BE_aux (e, loc n m)
 let mk_typ t n m = ATyp_aux (t, loc n m)
 let mk_pat p n m = P_aux (p, loc n m)
 let mk_fpat fp n m = FP_aux (fp, loc n m)
@@ -254,7 +253,6 @@ let set_syntax_deprecated l =
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
-%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl
 %token InternalPLet InternalReturn InternalAssume
 %token Forwards Backwards
@@ -489,34 +487,10 @@ typquant:
     { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) }
 
 effect:
-  | Barr
-    { mk_effect BE_barr $startpos $endpos }
-  | Depend
-    { mk_effect BE_depend $startpos $endpos }
-  | Rreg
-    { mk_effect BE_rreg $startpos $endpos }
-  | Wreg
-    { mk_effect BE_wreg $startpos $endpos }
-  | Rmem
-    { mk_effect BE_rmem $startpos $endpos }
-  | Wmem
-    { mk_effect BE_wmem $startpos $endpos }
-  | Wmv
-    { mk_effect BE_wmv $startpos $endpos }
-  | Eamem
-    { mk_effect BE_eamem $startpos $endpos }
-  | Exmem
-    { mk_effect BE_exmem $startpos $endpos }
-  | Undef
-    { mk_effect BE_undef $startpos $endpos }
-  | Unspec
-    { mk_effect BE_unspec $startpos $endpos }
-  | Nondet
-    { mk_effect BE_nondet $startpos $endpos }
-  | Escape
-    { mk_effect BE_escape $startpos $endpos }
+  | id
+    { $1 }
   | Configuration
-    { mk_effect BE_config $startpos $endpos }
+    { mk_id (Id "configuration") $startpos $endpos }
 
 effect_list:
   | effect