Fixes to grammar omissions (i.e. naming_scheme_opt and type_def vs tdef), more token addition, and start of parsing

3 files changed, 121 insertions, 117 deletions

diff --git a/src/ast.ml b/src/ast.ml
index f7454253..0195a73b 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -49,12 +49,6 @@ type x = terminal * text (* identifier *)
 type ix = terminal * text (* infix identifier *)
 
 type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of terminal * x * terminal (* remove infix status *)
-
-
-type 
 base_kind_aux =  (* base kind *)
    BK_type of terminal (* kind of types *)
  | BK_nat of terminal (* kind of natural number size expressions *)
@@ -63,8 +57,9 @@ base_kind_aux =  (* base kind *)
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of terminal * x * terminal (* remove infix status *)
 
 
 type 
@@ -73,14 +68,13 @@ base_kind =
 
 
 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 *)
+id = 
+   Id_aux of id_aux * l
+
+
+type 
+kind_aux =  (* kinds *)
+   K_kind of (base_kind * terminal) list
 
 
 type 
@@ -96,13 +90,19 @@ and nexp =
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind * terminal) list
+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 
-effect = 
-   Effect_aux of effect_aux * l
+kind = 
+   K_aux of kind_aux * l
 
 
 type 
@@ -114,14 +114,19 @@ nexp_constraint_aux =  (* constraint over kind $_$ *)
 
 
 type 
-kind = 
-   K_aux of kind_aux * l
+effect = 
+   Effect_aux of effect_aux * l
 
 
 type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *)
+kinded_id =  (* optionally kind-annotated identifier *)
+   KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
+type 
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
 
 
 type 
@@ -132,31 +137,31 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
+effects_aux =  (* effect set, of kind $_$ *)
+   Effects_var of id
+ | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *)
 
 
 type 
-kinded_id =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of terminal * (kinded_id) list * terminal * (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 
-effects = 
-   Effects_aux of effects_aux * l
+order = 
+   Ord_aux of order_aux * l
 
 
 type 
-order = 
-   Ord_aux of order_aux * l
+effects = 
+   Effects_aux of effects_aux * l
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of terminal * (kinded_id) list * terminal * (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 *)
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -175,11 +180,6 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 typschm_aux =  (* type scheme *)
    TypSchm_ts of typquant * typ
 
@@ -288,20 +288,30 @@ and letbind =
 
 
 type 
+effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
+
+
+type 
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * terminal * exp
+
+
+type 
 rec_opt_aux =  (* Optional recursive annotation for functions *)
    Rec_nonrec (* non-recursive *)
  | Rec_rec of terminal (* recursive *)
 
 
 type 
-effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * terminal * exp
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
@@ -316,23 +326,26 @@ rec_opt =
 
 
 type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
+fundef_aux =  (* Function definition *)
+   FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list
 
 
 type 
-funcl = 
-   FCL_aux of funcl_aux * l
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of terminal * typschm * id
 
 
 type 
-fundef_aux =  (* Function definition *)
-   FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list
+naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of terminal * typschm * id
+index_range =  (* 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 *)
 
 
 type 
@@ -352,13 +365,22 @@ val_spec =
 
 
 type 
+type_def =  (* Type definition body *)
+   TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *)
+ | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
+ | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * 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 * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
+
+
+type 
 default_typing_spec = 
    DT_aux of default_typing_spec_aux * l
 
 
 type 
 def_aux =  (* Top-level definition *)
-   DEF_type of terminal (* type definition *)
+   DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
  | DEF_val of letbind (* value definition *)
  | DEF_spec of val_spec (* top-level type constraint *)
@@ -366,7 +388,7 @@ def_aux =  (* Top-level definition *)
  | DEF_reg_dec of terminal * typ * id (* register declaration *)
  | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
  | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *)
- | DEF_scattered_variant of terminal * terminal * id * terminal * terminal * terminal * terminal * typquant (* scattered union definition header *)
+ | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *)
  | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *)
  | DEF_scattered_end of terminal * id (* scattered definition end *)
 
@@ -395,39 +417,18 @@ typ_lib_aux =  (* library types and syntactic sugar for them *)
 
 
 type 
-index_range =  (* 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 *)
-
-
-type 
-defs_aux =  (* Definition sequence *)
+defs =  (* Definition sequence *)
    Defs of (def) list
 
 
 type 
-typ_lib = 
-   Typ_lib_aux of typ_lib_aux * l
-
-
-type 
 ctor_def =  (* Datatype constructor definition clause *)
    CT_ct of id * terminal * typschm
 
 
 type 
-tdef =  (* Type definition body *)
-   TD_abbrev of terminal * id * terminal * terminal * typschm (* type abbreviation *)
- | TD_record of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
- | TD_variant of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *)
- | TD_enum of terminal * id * terminal * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
- | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
-
-
-type 
-defs = 
-   Defs_aux of defs_aux * l
+typ_lib = 
+   Typ_lib_aux of typ_lib_aux * l
 
 
 
diff --git a/src/lexer.mll b/src/lexer.mll
index 1ab7fa26..d6a47d5e 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -62,8 +62,10 @@ let kw_table =
      ("and",                     (fun x -> And(x)));
      ("as",                      (fun x -> As(x)));
      ("case",			 (fun x -> Case(x)));
+     ("clause",                  (fun x -> Clause(x)));
      ("const",			 (fun x -> Const(x)));
      ("default",		 (fun x -> Default(x)));
+     ("end",                     (fun x -> End(x)));
      ("enum",			 (fun x -> Enum(x)));
      ("else",                    (fun x -> Else(x)));
      ("false",                   (fun x -> False(x)));
@@ -73,8 +75,10 @@ let kw_table =
      ("in",			 (fun x -> In(x)));
      ("IN",                      (fun x -> IN(x,r"IN")));     
      ("let",                     (fun x -> Let_(x)));
+     ("member",                  (fun x -> Member(x)));
      ("rec",			 (fun x -> Rec(x)));
      ("register",		 (fun x -> Register(x)));
+     ("scattered",               (fun x -> Scattered(x)));
      ("struct",                  (fun x -> Struct(x)));
      ("switch",			 (fun x -> Switch(x)));
      ("then",                    (fun x -> Then(x)));
diff --git a/src/parser.mly b/src/parser.mly
index 4dc413ba..497f55d9 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -54,15 +54,14 @@ 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 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 dloc d = Def_l(d,loc ())
-let irloc ir = Rule_l(ir,loc())
-let reclloc fcl = Rec_l(fcl,loc())*)
+
+let dloc d = DEF_aux(d,loc ())
 
 let pat_to_let p =
   match p with
@@ -126,9 +125,9 @@ let mk_pre_x_l sk1 (sk2,id) sk3 l =
 (*Terminals with no content*)
 }%
 
-%token <Ast.terminal> And As Case Const Default Enum Else False Forall Function_
-%token <Ast.terminal> If_ In IN Let_ Rec Register Struct Switch Then True 
-%token <Ast.terminal> Type Typedef Union With Val
+%token <Ast.terminal> And As Case Clause Const Default End Enum Else False Forall 
+%token <Ast.terminal> Function_ If_ In IN Let_ Member Rec Register Scattered  
+%token <Ast.terminal> Struct Switch Then True Type Typedef Union With Val
 
 %token <Ast.terminal> AND Div_ EOR Mod OR Quot Rem 
 
@@ -875,29 +874,7 @@ val_defs:
   | val_def val_defs
     { ($1,loc ())::$2 }
 
-def:
-  | Type tds
-    { dloc (Type_def($1,$2)) }
-  | val_def
-    { dloc (Val_def($1)) }
-  | Rename targets_opt id Eq x
-    { dloc (Ident_rename($1,$2,$3,fst $4,$5)) }
-  | Module_ x Eq Struct defs End
-    { mod_cap $2; dloc (Module($1,$2,fst $3,$4,$5,$6)) }
-  | Module_ x Eq id
-    { mod_cap $2; dloc (Rename($1,$2,fst $3,$4)) }
-  | Open_ id
-    { dloc (Open($1,$2)) }
-  | Indreln targets_opt and_indreln_clauses
-    { dloc (Indreln($1,$2,$3)) }
-  | val_spec
-    { dloc (Spec_def($1)) }
-  | Class_ Lparen x tnvar Rparen class_val_specs End
-    { dloc (Class($1,$2,$3,$4,$5,$6,$7)) }
-  | Inst instschm val_defs End
-    { dloc (Instance($1,$2,$3,$4)) }
-  | lemma
-    { dloc (Lemma $1) }
+
 
 xtyp:
   | x Colon typ
@@ -941,7 +918,7 @@ texp:
 
 name_sect:
   | Lsquare x Eq String Rsquare
-    { Name_sect_name($1,$2,fst $3,(fst $4),(snd $4),$5) }
+    { Name_sect_some($1,$2,fst $3,(fst $4),(snd $4),$5) }
  
 td:
   | x tnvs
@@ -959,15 +936,37 @@ tds:
   | td And tds
     { ($1,$2)::$3 }
 
+def:
+  | type_def
+    { dloc (DEF_type($1)) }
+  | fun_def
+    { dloc (DEF_fundef($1)) }
+  | letbind
+    { dloc (DEF_val($1)) }
+  | val_spec
+    { dloc (DEF_spec($1)) }
+  | default_typ 
+    { dloc (DEF_default($1)) }
+  | Register typ id
+    { dloc (DEF_reg_dec($1,$2,$3)) }
+  | Scattered Function_ rec_opt tannot_opt effects_opt id
+    { dloc (DEF_scattered_function($1,$2,$3,$4,$5,$6)) }
+  | Function_ Clause funcl
+    { dloc (DEF_funcl($1,$2,$3)) }
+  | Scattered Typedef id name_sect_opt Equal Const Union typquant
+    { dloc (DEF_scattered_variant($1,$2,$3,$4,$5,$6,$7,$8)) }
+  | Scattered Typedef id Equal Const Union typquant
+    { dloc (DEF_scattered_variant($1,$2,Name_sect_none,$3,$4,$5,$6,$7)) }
+  | Union id Member typ id
+    { dloc (DEF_scattered_unioncl($1,$2,$3,$4,$5)) }
+  | End id 
+    { dloc (DEF_scattered_end($1,$2)) }
+
 defs_help:
   | def
     { [($1,None,false)] }
-  | def SemiSemi
-    { [($1,$2,true)] }
   | def defs_help
     { ($1,None,false)::$2 }
-  | def SemiSemi defs_help
-    { ($1,$2,true)::$3 }
 
 defs:
   | defs_help