A parser without any conflicts.

The ott files have been adjusted to reflect some syntax changes in typquant specifications, and the type annotations are not optional for function definitions; we need additional syntax to help the parser if we want to allow functions without type annotations.

3 files changed, 169 insertions, 153 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 8a0c6022..9a394767 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -80,17 +80,6 @@ id =
 
 
 type 
-efct_aux =  (* effect *)
-   Effect_rreg (* read register *)
- | Effect_wreg (* write register *)
- | Effect_rmem (* read memory *)
- | Effect_wmem (* write memory *)
- | Effect_undef (* undefined-instruction exception *)
- | Effect_unspec (* unspecified values *)
- | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
-
-
-type 
 kind = 
    K_aux of kind_aux * l
 
@@ -108,8 +97,14 @@ and nexp =
 
 
 type 
-efct = 
-   Effect_aux of efct_aux * l
+efct_aux =  (* effect *)
+   Effect_rreg (* read register *)
+ | Effect_wreg (* write register *)
+ | Effect_rmem (* read memory *)
+ | Effect_wmem (* write memory *)
+ | Effect_undef (* undefined-instruction exception *)
+ | Effect_unspec (* unspecified values *)
+ | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
 type 
@@ -127,6 +122,21 @@ type
 
 
 type 
+efct = 
+   Effect_aux of efct_aux * l
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+'a nexp_constraint = 
+   NC_aux of 'a nexp_constraint_aux * 'a annot
+
+
+type 
 effects_aux =  (* effect set, of kind $_$ *)
    Effects_var of id
  | Effects_set of (efct) list (* effect set *)
@@ -140,13 +150,9 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
-'a nexp_constraint = 
-   NC_aux of 'a nexp_constraint_aux * 'a annot
+quant_item =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of 'a nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -161,8 +167,7 @@ order =
 
 type 
 'a typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (kinded_id) list * ('a nexp_constraint) list
- | TypQ_no_constraint of (kinded_id) list (* sugar, omitting constraints *)
+   TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
@@ -246,7 +251,11 @@ type
 
 
 type 
-'a letbind = 
+'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of 'a typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+and 'a letbind = 
    LB_aux of 'a letbind_aux * 'a annot
 
 and 'a exp_aux =  (* Expression *)
@@ -303,15 +312,17 @@ and 'a pexp_aux =  (* Pattern match *)
 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 * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+type 
+'a effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
+'a tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of 'a typquant * typ
 
 
 type 
@@ -326,30 +337,19 @@ type
 
 
 type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of 'a typquant * typ
-
-
-type 
-'a effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of int (* single index *)
- | BF_range of int * int (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
 
 
 type 
@@ -363,22 +363,18 @@ type
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
-
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
- | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* union type definition *)
- | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+and index_range = 
+   BF_aux of index_range_aux * l
 
 
 type 
@@ -387,24 +383,33 @@ type
 
 
 type 
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+
+
+type 
 'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * id
  | DT_typ of 'a typschm * id
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * naming_scheme_opt * 'a typschm (* type abbreviation *)
+ | TD_record of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * naming_scheme_opt * 'a typquant * ((typ * id)) list * bool (* union type definition *)
+ | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
@@ -413,8 +418,8 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
@@ -433,6 +438,16 @@ type
 
 
 type 
+'a ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * 'a typschm
+
+
+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 (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -451,13 +466,13 @@ type
 
 
 type 
-'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * 'a typschm
+'a ctor_def = 
+   CT_aux of 'a ctor_def_aux * 'a annot
 
 
 type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
+'a defs =  (* Definition sequence *)
+   Defs of ('a def) list
 
 
 type 
@@ -465,14 +480,4 @@ type
    Typ_lib_aux of 'a typ_lib_aux * l
 
 
-type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
-
-
-type 
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
-
-
 
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 74ec4c68..7e65b40f 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -145,9 +145,19 @@ kinded_id =
 
 
 type 
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of nexp_constraint (* A constraint for this type *)
+
+
+type 
+quant_item = 
+   QI_aux of quant_item_aux * l
+
+
+type 
 typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (kinded_id) list * (nexp_constraint) list
- | TypQ_no_constraint of (kinded_id) list (* sugar, omitting constraints *)
+   TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
@@ -270,29 +280,29 @@ naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for va
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type 
 tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_none
  | Typ_annot_opt_some of typquant * atyp
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
-
-
-type 
 effects_opt_aux =  (* Optional effect annotation for functions *)
    Effects_opt_pure (* sugar for empty effect set *)
  | Effects_opt_effects of atyp
 
 
 type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type 
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
+
+
+type 
 index_range_aux =  (* index specification, for bitfields in register types *)
    BF_single of int (* single index *)
  | BF_range of int * int (* index range *)
@@ -308,29 +318,28 @@ naming_scheme_opt =
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-funcl = 
-   FCL_aux of funcl_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
@@ -343,8 +352,9 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -353,8 +363,8 @@ fundef_aux =  (* Function definition *)
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
@@ -363,8 +373,8 @@ type_def =
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
@@ -393,6 +403,11 @@ def =
 
 
 type 
+ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * typschm
+
+
+type 
 typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -411,11 +426,6 @@ typ_lib_aux =  (* library types and syntactic sugar for them *)
 
 
 type 
-ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
-type 
 lexp_aux =  (* lvalue expression *)
    LEXP_id of id (* identifier *)
  | LEXP_vector of lexp * exp (* vector element *)
@@ -432,13 +442,13 @@ defs =  (* Definition sequence *)
 
 
 type 
-typ_lib = 
-   Typ_lib_aux of typ_lib_aux * l
+ctor_def = 
+   CT_aux of ctor_def_aux * l
 
 
 type 
-ctor_def = 
-   CT_aux of ctor_def_aux * l
+typ_lib = 
+   Typ_lib_aux of typ_lib_aux * l
 
 
 
diff --git a/src/parser.mly b/src/parser.mly
index 67a22a18..5efd0537 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -128,7 +128,7 @@ let star = "*"
 
 %token Bar Colon Comma Dot Eof Minus Semi Under
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar
+%token BarBar BarGt BarSquare DotDot MinusGt LtBar LparenColon SquareBar
 
 /*Terminals with content*/
 
@@ -169,21 +169,21 @@ let star = "*"
 id:
   | Id
     { idl (Id($1)) }
-  | Lparen At Rparen
+  | LparenColon At Rparen
     { Id_aux(DeIid($2),loc ()) }
- | Lparen Eq Rparen
+ | LparenColon Eq Rparen
     { Id_aux(DeIid($2),loc ()) }
-  | Lparen IN Rparen
+  | LparenColon IN Rparen
     { Id_aux(DeIid("In"),loc ()) }
-  | Lparen BarBar Rparen
+  | LparenColon BarBar Rparen
     { Id_aux(DeIid("||"),loc ()) }
-  | Lparen ColonColon Rparen
+  | LparenColon ColonColon Rparen
     { Id_aux(DeIid($2),loc ()) }
-  | Lparen Star Rparen
+  | LparenColon Star Rparen
     { Id_aux(DeIid($2),loc ()) }
-  | Lparen Plus Rparen
+  | LparenColon Plus Rparen
     { Id_aux(DeIid($2),loc ()) }
-  | Lparen GtEq Rparen
+  | LparenColon GtEq Rparen
     { Id_aux(DeIid($2),loc ()) }
 
 atomic_kind:
@@ -252,13 +252,14 @@ atomic_typ:
   | Lsquare nexp_typ Colon nexp_typ Rsquare
       { assert false }
 
-vtyp_typ:
+/*Inherently ambiguous with type application, but type checking should be able to sort it out */
+/*vtyp_typ:
    | atomic_typ
        { $1 }
    | atomic_typ Lsquare nexp_typ Rsquare
      { assert false }
    | atomic_typ Lsquare nexp_typ Colon nexp_typ Rsquare
-     { assert false }
+     { assert false }*/
 
 atomic_typs:
   | atomic_typ
@@ -267,7 +268,7 @@ atomic_typs:
     { $1::$2 }
 
 app_typ:
-  | vtyp_typ
+  | atomic_typ
     { $1 }
   | id atomic_typs
     { tloc (ATyp_app($1,$2)) }
@@ -557,7 +558,6 @@ exp:
   | or_right_atomic_exp
     { $1 }
 
-
 comma_exps:
   | exp Comma exp
     { [$1;$3] }
@@ -625,9 +625,9 @@ fun_def:
         funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4))
       | _ ->
         funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-  | Function_ Rec funcl_ands
+/*  | Function_ Rec funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
-  | Function_ typquant atomic_typ effect_typ funcl_ands
+*/  | Function_ typquant atomic_typ effect_typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
   | Function_ typquant atomic_typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
@@ -637,9 +637,9 @@ fun_def:
         funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
       | _ ->
         funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-  | Function_ funcl_ands
+/*  | Function_ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-
+*/
 
 val_spec:
   | Val typquant atomic_typ id
@@ -652,14 +652,12 @@ kinded_id:
     { kiloc (KOpt_none $1) }
   | kind id
     { kiloc (KOpt_kind($1,$2))}
-  | Lparen kinded_id Rparen
-    { $2 }
 
-kinded_ids:
+/*kinded_ids:
   | kinded_id
     { [$1] }
   | kinded_id kinded_ids
-    { $1::$2 }
+    { $1::$2 }*/
 
 nums:
   | Num
@@ -677,29 +675,32 @@ nexp_constraint:
   | id IN Lcurly nums Rcurly
     { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
 
-nexp_constraints:
+id_constraint:
   | nexp_constraint
-    { [$1] }
-  | nexp_constraint Comma nexp_constraints
-    { $1::$3 }
+      { QI_aux((QI_const $1), loc())}
+  | kinded_id
+      { QI_aux((QI_id $1), loc()) }
+
+id_constraints:
+  | id_constraint
+      { [$1] }
+  | id_constraint Comma id_constraints
+      { $1::$3 }
 
 typquant:
-  /* This is a syntactic change to avoid 6 significant shift/reduce conflicts instead of the Dot */
-  | Forall kinded_ids Amp nexp_constraints Dot
-    { typql(TypQ_tq($2,$4)) }
-  | Forall kinded_ids Dot
-    { typql(TypQ_no_constraint($2)) }
+  | Forall id_constraints Dot
+    { typql(TypQ_tq($2)) }
 
 name_sect:
   | Lsquare Id Eq String Rsquare
     { Name_sect_aux(Name_sect_some($4), loc ()) }
 
 c_def_body:
-  | typ id
+  | atomic_typ id
     { [($1,$2)],false }
-  | typ id Semi
+  | atomic_typ id Semi
     { [($1,$2)],true }
-  | typ id Semi c_def_body
+  | atomic_typ id Semi c_def_body
     { ($1,$2)::(fst $4), snd $4 }
 
 index_range_atomic: