Aligning Ott generated AST with actual ast.ml. Almost a drop-in replacement but problem with aux introduced 'a type variables

1 files changed, 164 insertions, 307 deletions

diff --git a/language/l2.ml b/language/l2.ml
index 13cb2567..8f041dc7 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -1,18 +1,33 @@
-(* generated by Ott 0.25 from: l2.ott *)
+(* generated by Ott 0.26 from: l2.ott *)
 
 
+type text = string
+
+type l = Parse_ast.l
+
 type 'a annot = l * 'a
 
+type loop = While | Until
+
 
-type x = string (* identifier *)
-type ix = string (* infix identifier *)
+type x = text (* identifier *)
+type ix = text (* infix identifier *)
 
 type 
 base_kind_aux =  (* base kind *)
    BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
  | BK_order (* kind of vector order specifications *)
- | BK_effect (* kind of effect sets *)
+
+
+type 
+base_kind = 
+   BK_aux of base_kind_aux * Parse_ast.l
+
+
+type 
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
@@ -21,14 +36,14 @@ kid_aux =  (* kinded IDs: $_$, $_$, $_$, and $_$ variables *)
 
 
 type 
-id_aux =  (* identifier *)
+id_aux =  (* Identifier *)
    Id of x
  | DeIid of x (* remove infix status *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * Parse_ast.l
+kind = 
+   K_aux of kind_aux * Parse_ast.l
 
 
 type 
@@ -42,31 +57,6 @@ id =
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
-
-
-type 
-nexp_aux =  (* numeric expression, of kind $_$ *)
-   Nexp_id of id (* abbreviation identifier *)
- | Nexp_var of kid (* variable *)
- | Nexp_constant of int (* constant *)
- | Nexp_times of nexp * nexp (* product *)
- | Nexp_sum of nexp * nexp (* sum *)
- | Nexp_minus of nexp * nexp (* subtraction *)
- | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* for internal use only *)
-
-and nexp = 
-   Nexp_aux of nexp_aux * Parse_ast.l
-
-
-type 
-kind = 
-   K_aux of kind_aux * Parse_ast.l
-
-
-type 
 base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
@@ -88,6 +78,21 @@ base_effect_aux =  (* effect *)
 
 
 type 
+nexp_aux =  (* numeric expression, of kind $_$ *)
+   Nexp_id of id (* abbreviation identifier *)
+ | Nexp_var of kid (* variable *)
+ | Nexp_constant of int (* constant *)
+ | Nexp_times of nexp * nexp (* product *)
+ | Nexp_sum of nexp * nexp (* sum *)
+ | Nexp_minus of nexp * nexp (* subtraction *)
+ | Nexp_exp of nexp (* exponential *)
+ | Nexp_neg of nexp (* for internal use only *)
+
+and nexp = 
+   Nexp_aux of nexp_aux * Parse_ast.l
+
+
+type 
 base_effect = 
    BE_aux of base_effect_aux * Parse_ast.l
 
@@ -116,27 +121,30 @@ effect =
 
 
 type 
-n_constraint_aux =  (* constraint over kind $_$ *)
-   NC_fixed of nexp * nexp
- | NC_bounded_ge of nexp * nexp
- | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of kid * (int) list
-
-
-type 
 kinded_id_aux =  (* optionally kind-annotated identifier *)
    KOpt_none of kid (* identifier *)
  | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
 type 
-n_constraint = 
-   NC_aux of n_constraint_aux * Parse_ast.l
+kinded_id = 
+   KOpt_aux of kinded_id_aux * Parse_ast.l
 
 
 type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * Parse_ast.l
+n_constraint_aux =  (* constraint over kind $_$ *)
+   NC_equal of nexp * nexp
+ | NC_bounded_ge of nexp * nexp
+ | NC_bounded_le of nexp * nexp
+ | NC_not_equal of nexp * nexp
+ | NC_set of kid * (int) list
+ | NC_or of n_constraint * n_constraint
+ | NC_and of n_constraint * n_constraint
+ | NC_true
+ | NC_false
+
+and n_constraint = 
+   NC_aux of n_constraint_aux * Parse_ast.l
 
 
 type 
@@ -146,19 +154,23 @@ quant_item_aux =  (* kinded identifier or $_$ constraint *)
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * Parse_ast.l
-
-
-type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* empty *)
+lit_aux =  (* literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_string of string (* string constant *)
+ | L_undef (* undefined-value constant *)
+ | L_real of string
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * Parse_ast.l
+quant_item = 
+   QI_aux of quant_item_aux * Parse_ast.l
 
 
 type 
@@ -168,6 +180,7 @@ typ_aux =  (* type expressions, of kind $_$ *)
  | Typ_var of kid (* type variable *)
  | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *)
  | Typ_tup of (typ) list (* Tuple *)
+ | Typ_exist of (kid) list * n_constraint * typ
  | Typ_app of id * (typ_arg) list (* type constructor application *)
 
 and typ = 
@@ -177,49 +190,20 @@ and typ_arg_aux =  (* type constructor arguments of all kinds *)
    Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
- | Typ_arg_effect of effect
 
 and typ_arg = 
    Typ_arg_aux of typ_arg_aux * Parse_ast.l
 
 
 type 
-lit_aux =  (* literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_string of string (* string constant *)
- | L_undef (* undefined-value constant *)
-
-
-type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
-
-
-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 * Parse_ast.l
-
-
-type 
 lit = 
    L_aux of lit_aux * Parse_ast.l
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * Parse_ast.l
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* empty *)
 
 
 type 
@@ -229,13 +213,14 @@ type
  | P_as of 'a pat * id (* named pattern *)
  | P_typ of typ * 'a pat (* typed pattern *)
  | P_id of id (* identifier *)
+ | P_var of 'a pat * kid (* bind pattern to type variable *)
  | P_app of id * ('a pat) list (* union constructor pattern *)
  | P_record of ('a fpat) list * bool (* struct pattern *)
  | P_vector of ('a pat) list (* vector pattern *)
- | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
  | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
  | P_tup of ('a pat) list (* tuple pattern *)
  | P_list of ('a pat) list (* list pattern *)
+ | P_cons of 'a pat * 'a pat (* Cons patterns *)
 
 and 'a pat = 
    P_aux of 'a pat_aux * 'a annot
@@ -248,6 +233,11 @@ and 'a fpat =
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * Parse_ast.l
+
+
+type 
 name_scm_opt_aux =  (* optional variable naming-scheme constraint *)
    Name_sect_none
  | Name_sect_some of string
@@ -260,6 +250,11 @@ type_union_aux =  (* type union constructors *)
 
 
 type 
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
+
+
+type 
 name_scm_opt = 
    Name_sect_aux of name_scm_opt_aux * Parse_ast.l
 
@@ -270,13 +265,23 @@ type_union =
 
 
 type 
+typschm = 
+   TypSchm_aux of typschm_aux * Parse_ast.l
+
+
+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 * Parse_ast.l
+
+
+type 
 'a kind_def_aux =  (* Definition body for elements of kind *)
    KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression abbreviation *)
- | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
- | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
 type 
@@ -299,165 +304,11 @@ type
 
 
 type 
-ne =  (* internal numeric expressions *)
-   Ne_id of x
- | Ne_var of x
- | Ne_const of int
- | Ne_inf
- | Ne_mult of ne * ne
- | Ne_add of (ne) list
- | Ne_minus of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
-type 
-t =  (* Internal types *)
-   T_id of x
- | T_var of x
- | T_fn of t * t * effect
- | T_tup of (t) list
- | T_app of x * t_args
- | T_abbrev of t * t
-
-and t_arg =  (* Argument to type constructors *)
-   T_arg_typ of t
- | T_arg_nexp of ne
- | T_arg_effect of effect
- | T_arg_order of order
-
-and t_args =  (* Arguments to type constructors *)
-   T_args of (t_arg) list
-
-
-type 
-k =  (* Internal kinds *)
-   Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_ctor of (k) list * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
-
-
-type 
-tid =  (* A type identifier or type variable *)
-   Tid_id of id
- | Tid_var of kid
-
-
-type 
-kinf =  (* Whether a kind is default or from a local binding *)
-   Kinf_k of k
- | Kinf_def of k
-
-
-type 
-nec =  (* Numeric expression constraints *)
-   Nec_lteq of ne * ne
- | Nec_eq of ne * ne
- | Nec_gteq of ne * ne
- | Nec_in of x * (int) list
- | Nec_cond of (nec) list * (nec) list
- | Nec_branch of (nec) list
-
-
-type 
-tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
-   Tag_empty
- | Tag_intro (* Denotes an assignment and lexp that introduces a binding *)
- | Tag_set (* Denotes an expression that mutates a local variable *)
- | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *)
- | Tag_global (* Globally let-bound or enumeration based value/variable *)
- | Tag_ctor (* Data constructor from a type union *)
- | Tag_extern of string option (* External function, specied only with a val statement *)
- | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
- | Tag_spec
- | Tag_enum of int
- | Tag_alias
- | Tag_unknown of string option (* Tag to distinguish an unknown path from a non-analysis non deterministic path *)
-
-
-type 
-tinf =  (* Type variables, type, and constraints, bound to an identifier *)
-   Tinf_typ of t
- | Tinf_quant_typ of e_k * s_N * tag * t
-
-
-type 
-conformsto =  (* how much conformance does overloading need *)
-   Conformsto_full
- | Conformsto_parm
-
-
-type 
-widennum = 
-   Widennum_widen
- | Widennum_dont
- | Widennum_dontcare
-
-
-type 
-widenvec = 
-   Widenvec_widen
- | Widenvec_dont
- | Widenvec_dontcare
-
-
-type 
-widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
-   Widening_w of widennum * widenvec
-
-
-type 
-tinflist =  (* In place so that a list of tinfs can be referred to without the dot form *)
-   Tinfs_empty
- | Tinfs_ls of (tinf) list
-
-
-type 
-i =  (* Information given by type checking an expression *)
-   I of s_N * effect
- | Iempty (* Empty constraints, effect *)
- | Singleunion of i * i
- | Iunion of (i) list (* Unions the constraints and effect *)
-
-
-type 
-e =  (* Definition environment and lexical environment *)
-   E of e_t * e_d
- | E_union of e * e
-
-
-type 
-i_direction = 
-   IInc
- | IDec
-
-
-type 
 'a reg_id_aux = 
    RI_id of id
 
 
 type 
-ctor_kind = 
-   C_Enum of nat
- | C_Union
-
-
-type 
-reg_form = 
-   Form_Reg of id * tannot * i_direction
- | Form_SubReg of id * reg_form * index_range
-
-
-type 
-'a reg_id = 
-   RI_aux of 'a reg_id_aux * 'a annot
-
-
-type 
 'a exp_aux =  (* expression *)
    E_block of ('a exp) list (* sequential block *)
  | E_nondet of ('a exp) list (* nondeterministic block *)
@@ -468,6 +319,8 @@ type
  | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
  | E_tuple of ('a exp) list (* tuple *)
  | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
+ | E_loop of loop * 'a exp * 'a exp
+ | E_until of 'a exp * 'a exp
  | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *)
  | E_vector of ('a exp) list (* vector (indexed from 0) *)
  | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *)
@@ -484,10 +337,12 @@ type
  | E_case of 'a exp * ('a pexp) list (* pattern matching *)
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
- | E_sizeof of nexp (* the value of nexp at run time *)
- | E_return of 'a exp (* return 'a exp from current function *)
+ | E_sizeof of nexp (* the value of $nexp$ at run time *)
+ | E_return of 'a exp (* return $'a exp$ from current function *)
  | E_exit of 'a exp (* halt all current execution *)
- | E_assert of 'a exp * 'a exp (* halt with error 'a exp when not 'a exp *)
+ | E_throw of 'a exp
+ | E_try of 'a exp * ('a pexp) list
+ | E_assert of 'a exp * 'a exp (* halt with error $'a exp$ when not $'a exp$ *)
  | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of 'a annot (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
  | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *)
@@ -497,25 +352,11 @@ type
  | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
  | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
  | E_internal_return of 'a exp (* For internal use to embed into monad definition *)
- | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *)
+ | E_constraint of n_constraint
 
 and 'a exp = 
    E_aux of 'a exp_aux * 'a annot
 
-and value =  (* interpreter evaluated value *)
-   V_boxref of nat * t
- | V_lit of lit
- | V_tuple of (value) list
- | V_list of (value) list
- | V_vector of nat * i_direction * (value) list
- | V_vector_sparse of nat * nat * i_direction * ((nat * value)) list * value
- | V_record of t * ((id * value)) list
- | V_ctor of id * t * ctor_kind * value
- | V_unknown
- | V_register of reg_form
- | V_register_alias of tannot alias_spec * tannot
- | V_track of value * reg_form_set
-
 and 'a lexp_aux =  (* lvalue expression *)
    LEXP_id of id (* identifier *)
  | LEXP_memory of id * ('a exp) list (* memory or register write via function call *)
@@ -549,30 +390,21 @@ and 'a opt_default =
 
 and 'a pexp_aux =  (* pattern match *)
    Pat_exp of 'a pat * 'a exp
+ | Pat_when of 'a pat * 'a exp * 'a exp
 
 and 'a pexp = 
    Pat_aux of 'a pexp_aux * 'a annot
 
 and 'a letbind_aux =  (* let binding *)
-   LB_val_explicit of typschm * 'a pat * 'a exp (* let, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* let, implicit type ('a pat must be total) *)
+   LB_val of 'a pat * 'a exp (* let, implicit type ($'a pat$ must be total) *)
 
 and 'a letbind = 
    LB_aux of 'a letbind_aux * 'a annot
 
-and 'a alias_spec_aux =  (* register alias expression forms *)
-   AL_subreg of 'a reg_id * id
- | AL_bit of 'a reg_id * 'a exp
- | AL_slice of 'a reg_id * 'a exp * 'a exp
- | AL_concat of 'a reg_id * 'a reg_id
-
-and 'a alias_spec = 
-   AL_aux of 'a alias_spec_aux * 'a annot
-
 
 type 
-'a funcl_aux =  (* function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+'a reg_id = 
+   RI_aux of 'a reg_id_aux * 'a annot
 
 
 type 
@@ -582,19 +414,28 @@ rec_opt_aux =  (* optional recursive annotation for functions *)
 
 
 type 
+effect_opt_aux =  (* optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type 
 tannot_opt_aux =  (* optional type annotation for functions *)
-   Typ_annot_opt_some of typquant * typ
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * typ
 
 
 type 
-effect_opt_aux =  (* optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of effect
+'a funcl_aux =  (* function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+'a alias_spec_aux =  (* register alias expression forms *)
+   AL_subreg of 'a reg_id * id
+ | AL_bit of 'a reg_id * 'a exp
+ | AL_slice of 'a reg_id * 'a exp * 'a exp
+ | AL_concat of 'a reg_id * 'a reg_id
 
 
 type 
@@ -603,25 +444,23 @@ rec_opt =
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * Parse_ast.l
 
 
 type 
-effect_opt = 
-   Effect_opt_aux of effect_opt_aux * Parse_ast.l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l
 
 
 type 
-'a val_spec_aux =  (* value type specification *)
-   VS_val_spec of typschm * id (* specify the type of an upcoming definition *)
- | VS_extern_no_rename of typschm * id (* specify the type of an external function *)
- | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *)
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
 
 
 type 
-'a fundef_aux =  (* function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+'a alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
 
 
 type 
@@ -634,6 +473,22 @@ type
 
 
 type 
+'a dec_spec_aux =  (* register declarations *)
+   DEC_reg of typ * id
+ | DEC_alias of id * 'a alias_spec
+ | DEC_typ_alias of typ * id * 'a alias_spec
+
+
+type
+'a val_spec_aux = VS_val_spec of typschm * id * string option * bool
+
+
+type 
+'a fundef_aux =  (* function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+
+
+type 
 'a default_spec_aux =  (* default kinding or typing assumption *)
    DT_order of order
  | DT_kind of base_kind * kid
@@ -641,35 +496,35 @@ type
 
 
 type 
-'a dec_spec_aux =  (* register declarations *)
-   DEC_reg of typ * id
- | DEC_alias of id * 'a alias_spec
- | DEC_typ_alias of typ * id * 'a alias_spec
+prec = 
+   Infix
+ | InfixL
+ | InfixR
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a scattered_def = 
+   SD_aux of 'a scattered_def_aux * 'a annot
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a dec_spec = 
+   DEC_aux of 'a dec_spec_aux * 'a annot
 
 
 type 
-'a scattered_def = 
-   SD_aux of 'a scattered_def_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
-'a default_spec = 
-   DT_aux of 'a default_spec_aux * Parse_ast.l
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
-'a dec_spec = 
-   DEC_aux of 'a dec_spec_aux * 'a annot
+'a default_spec = 
+   DT_aux of 'a default_spec_aux * Parse_ast.l
 
 
 type 
@@ -683,6 +538,8 @@ and 'a def =  (* top-level 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_fixity of prec * int * id (* fixity declaration *)
+ | DEF_overload of id * (id) list (* operator overload specification *)
  | DEF_default of 'a default_spec (* default kind and type assumptions *)
  | DEF_scattered of 'a scattered_def (* scattered function and type definition *)
  | DEF_reg_dec of 'a dec_spec (* register declaration *)