Source file ast.ml

(*Generated by Lem from ast.lem.*)
(* generated by Ott 0.34 from: ../../language/sail.ott *)
open Lem_pervasives


type l = Parse_ast.l

open Value

type loop = While | Until

type 'a annot = l * 'a

type extern = { pure : bool; bindings : (string * string) list }


type x = string (* identifier *)
type ix = string (* infix identifier *)

type kid_aux =  (* kinded IDs: Type, Int, and Order variables *)
 | Var of x


type kind_aux =  (* base kind *)
 | K_type (* kind of types *)
 | K_int (* kind of natural number size expressions *)
 | K_order (* kind of vector order specifications *)
 | K_bool (* kind of constraints *)


type id_aux =  (* Identifier *)
 | Id of x
 | Operator of x (* remove infix status *)


type kid = 
 | Kid_aux of kid_aux * l


type kind = 
 | K_aux of kind_aux * l


type id = 
 | Id_aux of id_aux * l


type order_aux =  (* vector order specifications, of kind Order *)
 | Ord_var of kid (* variable *)
 | Ord_inc (* increasing *)
 | Ord_dec (* decreasing *)


type kinded_id_aux =  (* optionally kind-annotated identifier *)
 | KOpt_kind of kind * kid (* kind-annotated variable *)


type nexp_aux =  (* numeric expression, of kind Int *)
 | Nexp_id of id (* abbreviation identifier *)
 | Nexp_var of kid (* variable *)
 | Nexp_constant of Nat_big_num.num (* constant *)
 | Nexp_app of id * nexp list (* app *)
 | 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 (* unary negation *)

and nexp = 
 | Nexp_aux of nexp_aux * l


type order = 
 | Ord_aux of order_aux * l


type kinded_id = 
 | KOpt_aux of kinded_id_aux * l


type lit_aux =  (* literal constant *)
 | L_unit
 | L_zero
 | L_one
 | L_true
 | L_false
 | L_num of Nat_big_num.num (* 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 typ_aux =  (* type expressions, of kind Type *)
 | Typ_internal_unknown
 | Typ_id of id (* defined type *)
 | Typ_var of kid (* type variable *)
 | Typ_fn of typ list * typ (* Function (first-order only) *)
 | Typ_bidir of typ * typ (* Mapping *)
 | Typ_tup of typ list (* Tuple *)
 | Typ_app of id * typ_arg list (* type constructor application *)
 | Typ_exist of kinded_id list * n_constraint * typ

and typ = 
 | Typ_aux of typ_aux * l

and typ_arg_aux =  (* type constructor arguments of all kinds *)
 | A_nexp of nexp
 | A_typ of typ
 | A_order of order
 | A_bool of n_constraint

and typ_arg = 
 | A_aux of typ_arg_aux * l

and n_constraint_aux =  (* constraint over kind Int *)
 | NC_equal of nexp * nexp
 | NC_bounded_ge of nexp * nexp
 | NC_bounded_gt of nexp * nexp
 | NC_bounded_le of nexp * nexp
 | NC_bounded_lt of nexp * nexp
 | NC_not_equal of nexp * nexp
 | NC_set of kid * Nat_big_num.num list
 | NC_or of n_constraint * n_constraint
 | NC_and of n_constraint * n_constraint
 | NC_app of id * typ_arg list
 | NC_var of kid
 | NC_true
 | NC_false

and n_constraint = 
 | NC_aux of n_constraint_aux * l


type lit = 
 | L_aux of lit_aux * l


type typ_pat_aux =  (* type pattern *)
 | TP_wild
 | TP_var of kid
 | TP_app of id * typ_pat list

and typ_pat = 
 | TP_aux of typ_pat_aux * l


type quant_item_aux =  (* kinded identifier or Int constraint *)
 | QI_id of kinded_id (* optionally kinded identifier *)
 | QI_constraint of n_constraint (* constraint *)


type 'a pat_aux =  (* pattern *)
 | P_lit of lit (* literal constant pattern *)
 | P_wild (* wildcard *)
 | P_or of ( 'a pat) * ( 'a pat) (* pattern disjunction *)
 | P_not of ( 'a pat) (* pattern negation *)
 | 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) * typ_pat (* bind pattern to type variable *)
 | P_app of id * ( 'a pat) list (* union constructor pattern *)
 | P_vector of ( 'a pat) list (* vector pattern *)
 | 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 *)
 | P_string_append of ( 'a pat) list (* string append pattern, x ^^ y *)

and 'a pat = 
 | P_aux of ( 'a pat_aux) * 'a annot


type quant_item = 
 | QI_aux of quant_item_aux * l


type 'a internal_loop_measure_aux =  (* internal syntax for an optional termination measure for a loop *)
 | Measure_none
 | Measure_some of ( 'a exp)

and 'a internal_loop_measure = 
 | Measure_aux of ( 'a internal_loop_measure_aux) * l

and 'a exp_aux =  (* expression *)
 | E_block of ( 'a exp) list (* sequential block *)
 | E_id of id (* identifier *)
 | E_lit of lit (* literal constant *)
 | E_cast of typ * ( 'a exp) (* cast *)
 | E_app of id * ( 'a exp) list (* function application *)
 | 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 internal_loop_measure) * ( 'a exp) * ( 'a exp)
 | E_for of id * ( 'a exp) * ( 'a exp) * ( 'a exp) * order * ( 'a exp) (* for loop *)
 | E_vector of ( 'a exp) list (* vector (indexed from 0) *)
 | E_vector_access of ( 'a exp) * ( 'a exp) (* vector access *)
 | E_vector_subrange of ( 'a exp) * ( 'a exp) * ( 'a exp) (* subvector extraction *)
 | E_vector_update of ( 'a exp) * ( 'a exp) * ( 'a exp) (* vector functional update *)
 | E_vector_update_subrange of ( 'a exp) * ( 'a exp) * ( 'a exp) * ( 'a exp) (* vector subrange update, with vector *)
 | E_vector_append of ( 'a exp) * ( 'a exp) (* vector concatenation *)
 | E_list of ( 'a exp) list (* list *)
 | E_cons of ( 'a exp) * ( 'a exp) (* cons *)
 | E_record of ( 'a fexp) list (* struct *)
 | E_record_update of ( 'a exp) * ( 'a fexp) list (* functional update of struct *)
 | E_field of ( 'a exp) * id (* field projection from struct *)
 | 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 $(exp 'a)$ from current function *)
 | E_exit of ( 'a exp) (* halt all current execution *)
 | E_ref of id
 | E_throw of ( 'a exp)
 | E_try of ( 'a exp) * ( 'a pexp) list
 | E_assert of ( 'a exp) * ( 'a exp) (* halt with error message $(exp 'a)$ when not $(exp 'a)$. exp' is optional. *)
 | E_var 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_internal_assume of n_constraint * ( 'a exp) (* Internal node for additional type checker assumptions *)
 | E_constraint of n_constraint

and 'a exp = 
 | E_aux of ( 'a exp_aux) * 'a annot

and 'a lexp_aux =  (* lvalue expression *)
 | LEXP_id of id (* identifier *)
 | LEXP_deref of ( 'a exp)
 | LEXP_memory of id * ( 'a exp) list (* memory or register write via function call *)
 | LEXP_cast of typ * id
 | LEXP_tup of ( 'a lexp) list (* multiple (non-memory) assignment *)
 | LEXP_vector_concat of ( 'a lexp) list (* vector concatenation L-exp *)
 | LEXP_vector of ( 'a lexp) * ( 'a exp) (* vector element *)
 | LEXP_vector_range of ( 'a lexp) * ( 'a exp) * ( 'a exp) (* subvector *)
 | LEXP_field of ( 'a lexp) * id (* struct field *)

and 'a lexp = 
 | LEXP_aux of ( 'a lexp_aux) * 'a annot

and 'a fexp_aux =  (* field expression *)
 | FE_Fexp of id * ( 'a exp)

and 'a fexp = 
 | FE_aux of ( 'a fexp_aux) * 'a annot

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 of ( 'a pat) * ( 'a exp) (* let, implicit type ($(pat 'a)$ must be total) *)

and 'a letbind = 
 | LB_aux of ( 'a letbind_aux) * 'a annot


type 'a mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *)
 | MP_lit of lit
 | MP_id of id
 | MP_app of id * ( 'a mpat) list
 | MP_vector of ( 'a mpat) list
 | MP_vector_concat of ( 'a mpat) list
 | MP_tup of ( 'a mpat) list
 | MP_list of ( 'a mpat) list
 | MP_cons of ( 'a mpat) * ( 'a mpat)
 | MP_string_append of ( 'a mpat) list
 | MP_typ of ( 'a mpat) * typ
 | MP_as of ( 'a mpat) * id

and 'a mpat = 
 | MP_aux of ( 'a mpat_aux) * 'a annot


type typquant_aux =  (* type quantifiers and constraints *)
 | TypQ_tq of quant_item list
 | TypQ_no_forall (* empty *)


type 'a mpexp_aux = 
 | MPat_pat of ( 'a mpat)
 | MPat_when of ( 'a mpat) * ( 'a exp)


type typquant = 
 | TypQ_aux of typquant_aux * l


type 'a pexp_funcl = ( 'a pexp)


type 'a mpexp = 
 | MPat_aux of ( 'a mpexp_aux) * 'a annot


type type_union_aux =  (* type union constructors *)
 | Tu_ty_id of typ * id


type tannot_opt_aux =  (* optional type annotation for functions *)
 | Typ_annot_opt_none
 | Typ_annot_opt_some of typquant * typ


type 'a rec_opt_aux =  (* optional recursive annotation for functions *)
 | Rec_nonrec (* non-recursive *)
 | Rec_rec (* recursive without termination measure *)
 | Rec_measure of ( 'a pat) * ( 'a exp) (* recursive with termination measure *)


type 'a funcl_aux =  (* function clause *)
 | FCL_Funcl of id * ( 'a pexp_funcl)


type 'a mapcl_aux =  (* mapping clause (bidirectional pattern-match) *)
 | MCL_bidir of ( 'a mpexp) * ( 'a mpexp)
 | MCL_forwards of ( 'a mpexp) * ( 'a exp)
 | MCL_backwards of ( 'a mpexp) * ( 'a exp)


type typschm_aux =  (* type scheme *)
 | TypSchm_ts of typquant * typ


type index_range_aux =  (* index specification, for bitfields in register types *)
 | BF_single of nexp (* single index *)
 | BF_range of nexp * nexp (* index range *)
 | BF_concat of index_range * index_range (* concatenation of index ranges *)

and index_range = 
 | BF_aux of index_range_aux * l


type type_union = 
 | Tu_aux of type_union_aux * l


type tannot_opt = 
 | Typ_annot_opt_aux of tannot_opt_aux * l


type 'a rec_opt = 
 | Rec_aux of ( 'a rec_opt_aux) * l


type 'a funcl = 
 | FCL_aux of ( 'a funcl_aux) * 'a annot


type 'a mapcl = 
 | MCL_aux of ( 'a mapcl_aux) * 'a annot


type typschm = 
 | TypSchm_aux of typschm_aux * l


type type_def_aux =  (* type definition body *)
 | TD_abbrev of id * typquant * typ_arg (* type abbreviation *)
 | TD_record of id * typquant * (typ * id) list * bool (* struct type definition *)
 | TD_variant of id * typquant * type_union list * bool (* tagged union type definition *)
 | TD_enum of id * id list * bool (* enumeration type definition *)
 | TD_bitfield of id * typ * (id * index_range) list (* register mutable bitfield type definition *)


type 'a fundef_aux =  (* function definition *)
 | FD_function of ( 'a rec_opt) * tannot_opt * ( 'a funcl) list


type 'a mapdef_aux =  (* mapping definition (bidirectional pattern-match function) *)
 | MD_mapping of id * tannot_opt * ( 'a mapcl) list


type subst_aux =  (* instantiation substitution *)
 | IS_typ of kid * typ (* instantiate a type variable with a type *)
 | IS_id of id * id (* instantiate an identifier with another identifier *)


type outcome_spec_aux =  (* outcome declaration *)
 | OV_outcome of id * typschm * kinded_id list


type 'a instantiation_spec_aux = 
 | IN_id of id


type val_spec_aux = VS_val_spec of typschm * id *  extern option * bool


type default_spec_aux =  (* default kinding or typing assumption *)
 | DT_order of order


type 'a scattered_def_aux =  (* scattered function and union type definitions *)
 | SD_function of ( 'a rec_opt) * tannot_opt * id (* scattered function definition header *)
 | SD_funcl of ( 'a funcl) (* scattered function definition clause *)
 | SD_variant of id * typquant (* scattered union definition header *)
 | SD_unioncl of id * type_union (* scattered union definition member *)
 | SD_mapping of id * tannot_opt
 | SD_mapcl of id * ( 'a mapcl)
 | SD_end of id (* scattered definition end *)


type 'a dec_spec_aux =  (* register declarations *)
 | DEC_reg of typ * id *  ( 'a exp)option


type 'a opt_default_aux =  (* optional default value for indexed vector expressions *)
 | Def_val_empty
 | Def_val_dec of ( 'a exp)


type 'a impldef_aux =  (* impl for target *)
 | Impl_impl of ( 'a funcl)


type 'a type_def = TD_aux of type_def_aux * 'a annot


type 'a fundef = 
 | FD_aux of ( 'a fundef_aux) * 'a annot


type 'a mapdef = 
 | MD_aux of ( 'a mapdef_aux) * 'a annot


type subst = 
 | IS_aux of subst_aux * l


type outcome_spec = 
 | OV_aux of outcome_spec_aux * l


type 'a instantiation_spec = 
 | IN_aux of ( 'a instantiation_spec_aux) * 'a annot


type 'a val_spec = VS_aux of val_spec_aux * 'a annot


type default_spec = 
 | DT_aux of default_spec_aux * l


type 'a scattered_def = 
 | SD_aux of ( 'a scattered_def_aux) * 'a annot


type 'a dec_spec = 
 | DEC_aux of ( 'a dec_spec_aux) * 'a annot


type prec = 
 | Infix
 | InfixL
 | InfixR


type 'a loop_measure = 
 | Loop of loop * ( 'a exp)


type 'a opt_default = 
 | Def_val_aux of ( 'a opt_default_aux) * 'a annot


type 'a impldef = 
 | Impl_aux of ( 'a impldef_aux) * l


type cast_opt = bool


type 'a def =  (* top-level definition *)
 | DEF_type of 'a type_def (* type definition *)
 | DEF_fundef of ( 'a fundef) (* function definition *)
 | DEF_mapdef of ( 'a mapdef) (* mapping definition *)
 | DEF_impl of ( 'a funcl) (* impl definition *)
 | DEF_val of ( 'a letbind) (* value definition *)
 | DEF_spec of 'a val_spec (* top-level type constraint *)
 | DEF_outcome of outcome_spec * ( 'a def) list (* top-level outcome definition *)
 | DEF_instantiation of ( 'a instantiation_spec) * subst list (* instantiation *)
 | DEF_fixity of prec * Nat_big_num.num * id (* fixity declaration *)
 | DEF_overload of id * id list (* operator overload specification *)
 | DEF_default of default_spec (* default kind and type assumptions *)
 | DEF_scattered of ( 'a scattered_def) (* scattered function and type definition *)
 | DEF_measure of id * ( 'a pat) * ( 'a exp) (* separate termination measure declaration *)
 | DEF_loop_measures of id * ( 'a loop_measure) list (* separate termination measure declaration *)
 | DEF_reg_dec of ( 'a dec_spec) (* register declaration *)
 | DEF_internal_mutrec of ( 'a fundef) list (* internal representation of mutually recursive functions *)
 | DEF_pragma of string * string * l (* compiler directive *)