diff options
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2ff7b5e2..3147b7f4 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -109,7 +109,7 @@ kid_aux = (* identifiers with kind, ticked to differntiate from program variabl type id_aux = (* Identifier *) Id of x - | DeIid of x (* remove infix status *) + | Operator of x (* remove infix status *) type base_effect = @@ -172,8 +172,7 @@ and atyp = and kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) + KOpt_kind of string option * kid list * kind option (* kind-annotated variable *) and kinded_id = @@ -182,7 +181,7 @@ 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 atyp (* A constraint for this type *) + | QI_constraint of atyp (* A constraint for this type *) type @@ -219,7 +218,6 @@ pat_aux = (* Pattern *) | P_id of id (* identifier *) | P_var of pat * atyp (* bind pat to type variable *) | P_app of id * (pat) list (* union constructor pattern *) - | P_record of (fpat) list * bool (* struct pattern *) | P_vector of (pat) list (* vector pattern *) | P_vector_concat of (pat) list (* concatenated vector pattern *) | P_tup of (pat) list (* tuple pattern *) @@ -238,10 +236,16 @@ and fpat = type loop = While | Until -type +type measure_aux = (* optional termination measure for a loop *) + | Measure_none + | Measure_some of exp + +and measure = + | Measure_aux of measure_aux * l + +and exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) - | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) | E_id of id (* identifier *) | E_ref of id | E_deref of exp @@ -251,7 +255,7 @@ exp_aux = (* Expression *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of (exp) list (* tuple *) | E_if of exp * exp * exp (* conditional *) - | E_loop of loop * exp * exp + | E_loop of loop * measure * exp * exp | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) | E_vector_access of exp * exp (* vector access *) @@ -387,7 +391,6 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only | MP_lit of lit | MP_id of id | MP_app of id * ( mpat) list - | MP_record of ( mfpat) list * bool | MP_vector of ( mpat) list | MP_vector_concat of ( mpat) list | MP_tup of ( mpat) list @@ -400,12 +403,6 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only and mpat = | MP_aux of ( mpat_aux) * l -and mfpat_aux = (* Mapping field pattern, why does this have to exist *) - | MFP_mpat of id * mpat - -and mfpat = - | MFP_aux of mfpat_aux * l - type mpexp_aux = | MPat_pat of ( mpat) | MPat_when of ( mpat) * ( exp) @@ -443,7 +440,7 @@ type_def_aux = (* Type definition body *) type val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id * (string -> string option) * bool + VS_val_spec of typschm * id * (string * string) list * bool type dec_spec_aux = (* Register declarations *) @@ -489,6 +486,10 @@ dec_spec = DEC_aux of dec_spec_aux * l +type loop_measure = + | Loop of loop * exp + + type scattered_def = SD_aux of scattered_def_aux * l @@ -509,6 +510,7 @@ def = (* Top-level definition *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_measure of id * pat * exp (* separate termination measure declaration *) + | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list |