Separated ott file for parsable AST and parser changes

2 files changed, 501 insertions, 74 deletions

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
new file mode 100644
index 00000000..b5f38aa4
--- /dev/null
+++ b/src/parse_ast.ml
@@ -0,0 +1,441 @@
+(* generated by Ott 0.22 from: l2_parse.ott *)
+
+
+type text = string
+
+type l =
+  | Unknown
+  | Trans of string * l option
+  | Range of Lexing.position * Lexing.position
+
+type 'a annot = l * 'a
+
+exception Parse_error_locn of l * string
+
+type ml_comment = 
+  | Chars of string
+  | Comment of ml_comment list
+
+type lex_skip =
+  | Com of ml_comment
+  | Ws of string
+  | Nl
+
+type lex_skips = lex_skip list option
+
+let pp_lex_skips ppf sk = 
+  match sk with
+    | None -> ()
+    | Some(sks) ->
+        List.iter
+          (fun sk ->
+             match sk with
+               | Com(ml_comment) ->
+                   (* TODO: fix? *)
+                   Format.fprintf ppf "(**)"
+               | Ws(r) ->
+                   Format.fprintf ppf "%s" r (*(Ulib.Text.to_string r)*)
+               | Nl -> Format.fprintf ppf "\\n")
+          sks
+
+let combine_lex_skips s1 s2 =
+  match (s1,s2) with
+    | (None,_) -> s2
+    | (_,None) -> s1
+    | (Some(s1),Some(s2)) -> Some(s2@s1)
+
+type terminal = lex_skips
+
+
+type x = terminal * text (* identifier *)
+type ix = terminal * text (* infix identifier *)
+
+type 
+base_kind_aux =  (* base kind *)
+   BK_type of terminal (* kind of types *)
+ | BK_nat of terminal (* kind of natural number size expressions *)
+ | BK_order of terminal (* kind of vector order specifications *)
+ | BK_effects of terminal (* kind of effect sets *)
+
+
+type 
+effect_aux =  (* effect *)
+   Effect_rreg of terminal (* read register *)
+ | Effect_wreg of terminal (* write register *)
+ | Effect_rmem of terminal (* read memory *)
+ | Effect_wmem of terminal (* write memory *)
+ | Effect_undef of terminal (* undefined-instruction exception *)
+ | Effect_unspec of terminal (* unspecified values *)
+ | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *)
+
+
+type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of terminal * x * terminal (* remove infix status *)
+
+
+type 
+base_kind = 
+   BK_aux of base_kind_aux * l
+
+
+type 
+effect = 
+   Effect_aux of effect_aux * l
+
+
+type 
+id = 
+   Id_aux of id_aux * l
+
+
+type 
+kind_aux =  (* kinds *)
+   K_kind of (base_kind * terminal) list
+
+
+type 
+atyp_aux =  (* expression of all kinds *)
+   ATyp_id of id (* identifier *)
+ | ATyp_constant of terminal * int (* constant *)
+ | ATyp_times of atyp * terminal * atyp (* product *)
+ | ATyp_sum of atyp * terminal * atyp (* sum *)
+ | ATyp_exp of terminal * terminal * atyp (* exponential *)
+ | ATyp_inc of terminal (* increasing (little-endian) *)
+ | ATyp_dec of terminal (* decreasing (big-endian) *)
+ | ATyp_set of terminal * (effect * terminal) list * terminal (* effect set *)
+ | ATyp_wild of terminal (* Unspecified type *)
+ | ATyp_fn of atyp * terminal * atyp * atyp (* Function type (first-order only in user code) *)
+ | ATyp_tup of (atyp * terminal) list (* Tuple type *)
+ | ATyp_app of id * (atyp) list (* type constructor application *)
+
+and atyp = 
+   ATyp_aux of atyp_aux * l
+
+
+type 
+kind = 
+   K_aux of kind_aux * l
+
+
+type 
+'a nexp_constraint_aux =  (* constraint over kind $_$ *)
+   NC_fixed of atyp * terminal * atyp
+ | NC_bounded_ge of atyp * terminal * atyp
+ | NC_bounded_le of atyp * terminal * atyp
+ | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal
+
+
+type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
+type 
+'a nexp_constraint = 
+   NC_aux of 'a nexp_constraint_aux * 'a annot
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+'a typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of terminal * (kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal
+ | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *)
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type 
+lit_aux =  (* Literal constant *)
+   L_unit of terminal * terminal (* $() : _$ *)
+ | L_zero of terminal (* $_ : _$ *)
+ | L_one of terminal (* $_ : _$ *)
+ | L_true of terminal (* $_ : _$ *)
+ | L_false of terminal (* $_ : _$ *)
+ | L_num of terminal * int (* natural number constant *)
+ | L_hex of terminal * string (* bit vector constant, C-style *)
+ | L_bin of terminal * string (* bit vector constant, C-style *)
+ | L_string of terminal * string (* string constant *)
+
+
+type 
+'a typquant = 
+   TypQ_aux of 'a typquant_aux * 'a annot
+
+
+type 
+lit = 
+   L_aux of lit_aux * l
+
+
+type 
+'a typschm_aux =  (* type scheme *)
+   TypSchm_ts of 'a typquant * atyp
+
+
+type 
+'a pat_aux =  (* Pattern *)
+   P_lit of lit (* literal constant pattern *)
+ | P_wild of terminal (* wildcard *)
+ | P_as of terminal * 'a pat * terminal * id * terminal (* named pattern *)
+ | P_typ of terminal * atyp * 'a pat * terminal (* typed pattern *)
+ | P_id of id (* identifier *)
+ | P_app of id * ('a pat) list (* union constructor pattern *)
+ | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
+ | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *)
+ | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
+ | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *)
+ | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *)
+ | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *)
+
+and 'a pat = 
+   P_aux of 'a pat_aux * 'a annot
+
+and 'a fpat_aux =  (* Field pattern *)
+   FP_Fpat of id * terminal * 'a pat
+
+and 'a fpat = 
+   FP_aux of 'a fpat_aux * 'a annot
+
+
+type 
+'a typschm = 
+   TypSchm_aux of 'a typschm_aux * 'a annot
+
+
+type 
+'a exp_aux =  (* Expression *)
+   E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of terminal * atyp * terminal * 'a exp (* cast *)
+ | E_app of 'a exp * ('a exp) list (* function application *)
+ | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
+ | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *)
+ | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *)
+ | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *)
+ | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *)
+ | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *)
+ | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *)
+ | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *)
+ | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *)
+ | E_list of terminal * ('a exp * terminal) list * terminal (* list *)
+ | E_cons of 'a exp * terminal * 'a exp (* cons *)
+ | E_record of terminal * 'a fexps * terminal (* struct *)
+ | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *)
+ | E_field of 'a exp * terminal * id (* field projection from struct *)
+ | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *)
+ | E_let of 'a letbind * terminal * 'a exp (* let expression *)
+ | E_assign of 'a lexp * terminal * 'a exp (* imperative assignment *)
+
+and 'a exp = 
+   E_aux of 'a exp_aux * 'a annot
+
+and 'a lexp_aux =  (* lvalue expression *)
+   LEXP_id of id (* identifier *)
+ | LEXP_vector of 'a lexp * terminal * 'a exp * terminal (* vector element *)
+ | LEXP_vector_range of 'a lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *)
+ | LEXP_field of 'a lexp * terminal * id (* struct field *)
+
+and 'a lexp = 
+   LEXP_aux of 'a lexp_aux * 'a annot
+
+and 'a fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * terminal * 'a exp
+
+and 'a fexp = 
+   FE_aux of 'a fexp_aux * 'a annot
+
+and 'a fexps_aux =  (* Field-expression list *)
+   FES_Fexps of ('a fexp * terminal) list * terminal * bool
+
+and 'a fexps = 
+   FES_aux of 'a fexps_aux * 'a annot
+
+and 'a pexp_aux =  (* Pattern match *)
+   Pat_exp of 'a pat * terminal * 'a exp
+
+and 'a pexp = 
+   Pat_aux of 'a pexp_aux * 'a annot
+
+and 'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+and 'a letbind = 
+   LB_aux of 'a letbind_aux * 'a annot
+
+
+type 
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * terminal * 'a exp
+
+
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec of terminal (* recursive *)
+
+
+type 
+'a effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of terminal
+
+
+type 
+'a tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of terminal * terminal
+
+
+type 
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal
+
+
+type 
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
+
+
+type 
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
+
+
+type 
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
+
+
+type 
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+
+
+type 
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of terminal * int (* single index *)
+ | BF_range of terminal * int * terminal * terminal * int (* index range *)
+ | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
+
+
+type 
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
+
+
+type 
+'a fundef_aux =  (* Function definition *)
+   FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list
+
+
+type 
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of terminal * id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *)
+ | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
+ | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* union type definition *)
+ | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
+ | TD_register of terminal * id * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
+
+
+type 
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of terminal * base_kind * id
+ | DT_typ of terminal * 'a typschm * id
+
+
+type 
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of terminal * 'a typschm * id
+
+
+type 
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
+
+
+type 
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
+
+
+type 
+'a default_typing_spec = 
+   DT_aux of 'a default_typing_spec_aux * 'a annot
+
+
+type 
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
+
+
+type 
+'a def_aux =  (* Top-level definition *)
+   DEF_type of 'a type_def (* type definition *)
+ | DEF_fundef of 'a fundef (* function definition *)
+ | DEF_val of 'a letbind (* value definition *)
+ | DEF_spec of 'a val_spec (* top-level type constraint *)
+ | DEF_default of 'a default_typing_spec (* default kind and type assumptions *)
+ | DEF_reg_dec of terminal * terminal * id (* register declaration *)
+ | DEF_scattered_function of terminal * terminal * rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
+ | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of terminal * id * terminal * terminal * id (* scattered union definition member *)
+ | DEF_scattered_end of terminal * id (* scattered definition end *)
+
+
+type 
+'a def = 
+   DEF_aux of 'a def_aux * 'a annot
+
+
+type 
+'a typ_lib_aux =  (* library types and syntactic sugar for them *)
+   Typ_lib_unit of terminal (* unit type with value $()$ *)
+ | Typ_lib_bool of terminal (* booleans $_$ and $_$ *)
+ | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *)
+ | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *)
+ | Typ_lib_string of terminal * string (* UTF8 strings *)
+ | Typ_lib_enum of terminal * terminal * terminal * terminal (* natural numbers _ .. _+_-1, ordered by _ *)
+ | Typ_lib_enum1 of terminal * terminal * terminal (* sugar for \texttt{enum nexp 0 inc} *)
+ | Typ_lib_enum2 of terminal * terminal * terminal * terminal * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
+ | Typ_lib_vector of terminal * terminal * terminal * terminal * terminal (* vector of _, indexed by natural range *)
+ | Typ_lib_vector2 of atyp * terminal * terminal * terminal (* sugar for vector indexed by [ _ ] *)
+ | Typ_lib_vector3 of atyp * terminal * terminal * terminal * terminal * terminal (* sugar for vector indexed by [ _.._ ] *)
+ | Typ_lib_list of terminal * atyp (* list of _ *)
+ | Typ_lib_set of terminal * atyp (* finite set of _ *)
+ | Typ_lib_reg of terminal * atyp (* mutable register components holding _ *)
+
+
+type 
+'a ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * terminal * 'a typschm
+
+
+type 
+'a defs =  (* Definition sequence *)
+   Defs of ('a def) list
+
+
+type 
+'a typ_lib = 
+   Typ_lib_aux of 'a typ_lib_aux * l
+
+
+type 
+'a ctor_def = 
+   CT_aux of 'a ctor_def_aux * 'a annot
+
+
+
diff --git a/src/parser.mly b/src/parser.mly
index dc024970..7f15b149 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -53,16 +53,15 @@ open Ast
 let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos())
 let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
 
-let tloc t = Typ_l(t,loc ())
-let nloc n = Length_l(n,loc ())
-let lloc l = Lit_l(l,loc ())
 let ploc p = Pat_l(p,loc ())
 let eloc e = Expr_l(e,loc ())
 let lbloc lb = Letbind(lb,loc ())
 
 let bkloc k = BK_aux(k,loc ())
 let kloc k = K_aux(k,loc ())
-let nloc n = Nexp_aux(k,loc ())
+let tloc t = ATyp_aux(t,loc ())
+let lloc l = L_aux(l,loc ())
+
 
 let dloc d = DEF_aux(d,loc ())
 
@@ -165,10 +164,6 @@ id:
     { mk_pre_x_l $1 $2 $3 (loc ()) }
   | Lparen IN Rparen
     { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen MEM Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen MinusMinusGt Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
   | Lparen AmpAmp Rparen
     { mk_pre_x_l $1 $2 $3 (loc ()) }
   | Lparen BarBar Rparen
@@ -181,20 +176,8 @@ id:
     { mk_pre_x_l $1 $2 $3 (loc ()) }
   | Lparen GtEq Rparen
     { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen PlusX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen StarX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen GtEqX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen EqualX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen StarstarX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
   | Lparen At Rparen
     { mk_pre_x_l $1 $2 $3 (loc ()) }
-  | Lparen AtX Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
 
 atomic_kind:
   | TYPE
@@ -212,64 +195,54 @@ kind:
   | atomic_kind MinusGt kind
     { ($1,$2)::$3 }
 
-atomic_nexp_no_id:
-  | Num
-    { nloc (Nexp_constant(fst $1, snd$1)) }
-  | Lparen nexp Rparen
-    { $2 }
-
-atomic_nexp:
-   | id
-     { nloc (Nexp_var (fst $1, snd $1)) }
-   | atomic_nexp_no_id
-     { $1 }
-
-star_nexp:
-   | atomic_nexp
-     { $1 }
-   | atomic_nexp Star star_nexp
-     { nloc (Nexp_times($1, fst $2, $3)) }
-
-exp_nexp:
-   | star_nexp
-     { $1 }
-   | Num StarStar nexp
-     { if (2 = (fst $1))
-       then nloc (Nexp_exp((fst $1,snd $1),$2,$3))
-       else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") }
-
-nexp:
-   | exp_nexp
-     { $1 }
-   | exp_nexp Plus nexp
-     { nloc (Nexp_sum($1,fst $2,$3)) }
+effect:
+  | id
+    { (match id with
+       | Id_aux(Id(s,t),l) ->
+	 Effect_aux
+	   ((match s with
+	   | "rreg" -> (Effect_rreg t)
+	   | "wreg" -> (Effect_wreg t)
+	   | "rmem" -> (Effect_rmem t)
+	   | "wmem" -> (Effect_wmem t)
+	   | "undef" -> (Effect_undef t)
+	   | "unspec" -> (Effect_unspec t)
+	   | "nondet" -> (Effect_nondet t)
+	   | _ -> Parse_error_locn(l, "Invalid effect")),l)
+       | _ -> Parse_error_locn(loc () , "Invalid effect")) }
+
+effect_list:
+  | effect
+    { [($1,None)] }
+  | effect Comma effect_list
+    { ($1,Some($2))::$3 }
 
 atomic_typ:
-  | Under
-    { tloc (Typ_wild($1)) }
   | id
-    { tloc (Typ_var(A_l((fst $1, snd $1), loc()))) }
+    { tloc (Atyp_var (fst $1, snd $1)) }
+  | Num
+    { tloc (Atyp_constant(fst $1, snd$1)) }
+  | Pure
+    { tloc (Atyp_pure($1)) }
+  | Under
+    { tloc (ATyp_wild($1)) }
+  | Lcurly effect_list Rcurly
+    { tloc (ATyp_effects($1,$2,$3)) }
   | Lparen typ Rparen
-    { tloc (Typ_paren($1,$2,$3)) }
-
-appt_typ :
-  | atomic_typ
-    { $1 }
-  | atomic_nexp
-    { tloc (Typ_Nexps($1)) }
+    { $2 }
 
 atomic_typs:
-  | appt_typ
+  | atomic_typ
     { [$1] }
-  | appt_typ atomic_typs
+  | atomic_typ atomic_typs
     { $1::$2 }
 
 app_typ:
   | atomic_typ
     { $1 }
   | id atomic_typs
-    { tloc (Typ_app($1,$2)) }
-  
+    { tloc (ATyp_app($1,$2)) }
+
 star_typ_list:
   | app_typ
     { [($1,None)] }
@@ -282,14 +255,31 @@ star_typ:
         | [] -> assert false
         | [(t,None)] -> t
         | [(t,Some _)] -> assert false
-        | ts -> tloc (Typ_tup(ts)) }
+        | ts -> tloc (ATyp_tup(ts)) }
+
+exp_typ:
+   | star_typ
+     { $1 }
+   | Num StarStar nexp
+     { if (2 = (fst $1))
+       then tloc (ATyp_exp((fst $1,snd $1),$2,$3))
+       else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") }
+
+nexp_typ:
+   | exp_typ
+     { $1 }
+   | exp_typ Plus typ
+     { tloc (ATyp_sum($1,fst $2,$3)) }
 
 typ:
-  | star_typ
+  | nexp_typ
     { $1 }
-  | star_typ Arrow typ
-    { tloc (Typ_fn($1,$2,$3)) }
-
+  | star_typ MinusGt typ id
+    { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_id($4))))) }
+  | star_typ MinusGt typ Pure
+    { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_pure($4))))) }
+  | star_typ MinusGt typ Lcurly effect_list Rcurly
+    { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_effects($4,$5,$6))))) }
 
 lit:
   | True
@@ -302,10 +292,6 @@ lit:
     { lloc (L_string(fst $1, snd $1)) }
   | Lparen Rparen
     { lloc (L_unit($1,$2)) }
-  | HashZero
-    { lloc (L_zero($1)) }
-  | HashOne
-    { lloc (L_one($1)) }
   | Bin
     { lloc (L_bin(fst $1, snd $1)) }
   | Hex