diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 705 | ||||
| -rw-r--r-- | language/l2.ml | 552 | ||||
| -rw-r--r-- | language/l2_parse.ml | 466 | ||||
| -rw-r--r-- | language/sail.ott (renamed from language/l2.ott) | 0 | ||||
| -rw-r--r-- | language/sil.ott | 451 |
5 files changed, 0 insertions, 2174 deletions
diff --git a/language/l2.lem b/language/l2.lem deleted file mode 100644 index 2d99e304..00000000 --- a/language/l2.lem +++ /dev/null @@ -1,705 +0,0 @@ -(* generated by Ott 0.25 from: l2.ott *) -open import Pervasives - -open import Pervasives -open import Pervasives_extra -open import Map -open import Maybe -open import Set_extra - -type l = - | Unknown - | Int of string * maybe l (*internal types, functions*) - | Range of string * nat * nat * nat * nat - | Generated of l (*location for a generated node, where l is the location of the closest original source*) - -type annot 'a = l * 'a - -val duplicates : forall 'a. list 'a -> list 'a - -val set_from_list : forall 'a. list 'a -> set 'a - -val subst : forall 'a. list 'a -> list 'a -> bool - - -type x = string (* identifier *) -type ix = string (* 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 kid_aux = (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *) - | Var of x - - -type id_aux = (* identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - -type base_kind = - | BK_aux of base_kind_aux * l - - -type kid = - | Kid_aux of kid_aux * l - - -type id = - | Id_aux of id_aux * l - - -type kind_aux = (* kinds *) - | K_kind of list base_kind - - -type nexp_aux = (* numeric expression, of kind $Nat$ *) - | Nexp_id of id (* abbreviation identifier *) - | Nexp_var of kid (* variable *) - | Nexp_constant of integer (* 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 * l - - -type kind = - | K_aux of kind_aux * l - - -type base_effect_aux = (* effect *) - | BE_rreg (* read register *) - | BE_wreg (* write register *) - | BE_rmem (* read memory *) - | BE_rmemt (* read memory and tag *) - | BE_wmem (* write memory *) - | BE_eamem (* signal effective address for writing memory *) - | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *) - | BE_wmv (* write memory, sending only value *) - | BE_wmvt (* write memory, sending only value and tag *) - | BE_barr (* memory barrier *) - | BE_depend (* dynamic footprint *) - | BE_undef (* undefined-instruction exception *) - | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism, from $nondet$ *) - | BE_escape (* potential call of $exit$ *) - | BE_lset (* local mutation; not user-writable *) - | BE_lret (* local return; not user-writable *) - - -type base_effect = - | BE_aux of base_effect_aux * l - - -type order_aux = (* vector order specifications, of kind $Order$ *) - | Ord_var of kid (* variable *) - | Ord_inc (* increasing *) - | Ord_dec (* decreasing *) - - -type effect_aux = (* effect set, of kind $Effect$ *) - | Effect_var of kid - | Effect_set of list base_effect (* effect set *) - - -type order = - | Ord_aux of order_aux * l - - -type effect = - | Effect_aux of effect_aux * l - -let effect_union e1 e2 = - match (e1,e2) with - | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l - end - - -type n_constraint_aux = (* constraint over kind $Nat$ *) - | NC_fixed of nexp * nexp - | NC_bounded_ge of nexp * nexp - | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of kid * list integer - - -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 * l - - -type kinded_id = - | KOpt_aux of kinded_id_aux * l - - -type quant_item_aux = (* kinded identifier or $Nat$ constraint *) - | QI_id of kinded_id (* optionally kinded identifier *) - | QI_const of n_constraint (* $Nat$ constraint *) - - -type quant_item = - | QI_aux of quant_item_aux * l - - -type typquant_aux = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* empty *) - - -type typquant = - | TypQ_aux of typquant_aux * l - - -type typ_aux = (* type expressions, of kind $Type$ *) - | Typ_wild (* unspecified type *) - | Typ_id of id (* defined type *) - | Typ_var of kid (* type variable *) - | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) - | Typ_tup of list typ (* Tuple *) - | Typ_app of id * list typ_arg (* type constructor application *) - -and typ = - | Typ_aux of typ_aux * l - -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 * l - - -type lit_aux = (* literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* 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 index_range_aux = (* index specification, for bitfields in register types *) - | BF_single of integer (* single index *) - | BF_range of integer * integer (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - | BF_aux of index_range_aux * l - - -type typschm_aux = (* type scheme *) - | TypSchm_ts of typquant * typ - - -type lit = - | L_aux of lit_aux * l - - -type typschm = - | TypSchm_aux of typschm_aux * l - - -type pat_aux 'a = (* pattern *) - | P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | P_as of (pat 'a) * id (* named pattern *) - | P_typ of typ * (pat 'a) (* typed pattern *) - | P_id of id (* identifier *) - | P_app of id * list (pat 'a) (* union constructor pattern *) - | P_record of list (fpat 'a) * bool (* struct pattern *) - | P_vector of list (pat 'a) (* vector pattern *) - | P_vector_indexed of list (integer * (pat 'a)) (* vector pattern (with explicit indices) *) - | P_vector_concat of list (pat 'a) (* concatenated vector pattern *) - | P_tup of list (pat 'a) (* tuple pattern *) - | P_list of list (pat 'a) (* list pattern *) - -and pat 'a = - | P_aux of (pat_aux 'a) * annot 'a - -and fpat_aux 'a = (* field pattern *) - | FP_Fpat of id * (pat 'a) - -and fpat 'a = - | FP_aux of (fpat_aux 'a) * annot 'a - - -type name_scm_opt_aux = (* optional variable naming-scheme constraint *) - | Name_sect_none - | Name_sect_some of string - - -type type_union_aux = (* type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id - - -type name_scm_opt = - | Name_sect_aux of name_scm_opt_aux * l - - -type type_union = - | Tu_aux of type_union_aux * l - - -type kind_def_aux 'a = (* Definition body for elements of kind *) - | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression abbreviation *) - | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *) - | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type type_def_aux 'a = (* type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* tagged union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type kind_def 'a = - | KD_aux of (kind_def_aux 'a) * annot 'a - - -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a - - -let rec remove_one i l = - match l with - | [] -> [] - | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) -end - -let rec remove_from l l2 = - match l2 with - | [] -> l - | i::l2' -> remove_from (remove_one i l) l2' -end - -let disjoint s1 s2 = Set.null (s1 inter s2) - -let rec disjoint_all sets = - match sets with - | [] -> true - | s1::[] -> true - | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) -end - - -type ne = (* internal numeric expressions *) - | Ne_id of x - | Ne_var of x - | Ne_const of integer - | Ne_inf - | Ne_mult of ne * ne - | Ne_add of list ne - | 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 list t - | 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 list t_arg - - -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_ctor of list k * 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 * list integer - | Nec_cond of list nec * list nec - | Nec_branch of list nec - - -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 maybe string (* 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 integer - | Tag_alias - | Tag_unknown of maybe string (* 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 (map tid kinf) * list nec * 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 list tinf - - type definition_env = - | DenvEmp - | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) - - -let blength (bit) = Ne_const 8 -let hlength (bit) = Ne_const 8 - - type env = - | EnvEmp - | Env of (map id tinf) * definition_env - - type inf = - | Iemp - | Inf of (list nec) * effect - - val denv_union : definition_env -> definition_env -> definition_env - let denv_union de1 de2 = - match (de1,de2) with - | (DenvEmp,de2) -> de2 - | (de1,DenvEmp) -> de1 - | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> - Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) - end - - val env_union : env -> env -> env - let env_union e1 e2 = - match (e1,e2) with - | (EnvEmp,e2) -> e2 - | (e1,EnvEmp) -> e1 - | ((Env te1 de1),(Env te2 de2)) -> - Env (te1 union te2) (denv_union de1 de2) - end - -let inf_union i1 i2 = - match (i1,i2) with - | (Iemp,i2) -> i2 - | (i1,Iemp) -> i1 - | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) - end - -let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) - - - -type I = inf - - -type E = env - - -type tannot = maybe (t * tag * list nec * effect * effect) - - - -type i_direction = - | IInc - | IDec - - -type reg_id_aux 'a = - | RI_id of id - - -type reg_form = - | Form_Reg of id * tannot * i_direction - | Form_SubReg of id * reg_form * index_range - - -type ctor_kind = - | C_Enum of nat - | C_Union - - -type reg_id 'a = - | RI_aux of (reg_id_aux 'a) * annot 'a - - -type exp_aux 'a = (* expression *) - | E_block of list (exp 'a) (* sequential block *) - | E_nondet of list (exp 'a) (* nondeterministic block *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * (exp 'a) (* cast *) - | E_app of id * list (exp 'a) (* function application *) - | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) - | E_tuple of list (exp 'a) (* tuple *) - | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) - | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) - | E_vector of list (exp 'a) (* vector (indexed from 0) *) - | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) - | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) - | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) - | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) - | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *) - | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) - | E_list of list (exp 'a) (* list *) - | E_cons of (exp 'a) * (exp 'a) (* cons *) - | E_record of (fexps 'a) (* struct *) - | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) - | E_field of (exp 'a) * id (* field projection from struct *) - | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) - | E_let of (letbind 'a) * (exp 'a) (* let expression *) - | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) - | E_sizeof of nexp (* the value of nexp at run time *) - | E_return of (exp 'a) (* return (exp 'a) from current function *) - | E_exit of (exp 'a) (* halt all current execution *) - | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *) - | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) - | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) - | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) - | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) - | E_comment of string (* For generated unstructured comments *) - | E_comment_struc of (exp 'a) (* For generated structured comments *) - | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) - | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) - | E_internal_return of (exp 'a) (* 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 *) - -and exp 'a = - | E_aux of (exp_aux 'a) * annot 'a - -and value = (* interpreter evaluated value *) - | V_boxref of nat * t - | V_lit of lit - | V_tuple of list value - | V_list of list value - | V_vector of nat * i_direction * list value - | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value - | V_record of t * list (id * value) - | V_ctor of id * t * ctor_kind * value - | V_unknown - | V_register of reg_form - | V_register_alias of alias_spec tannot * tannot - | V_track of value * set reg_form - -and lexp_aux 'a = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *) - | LEXP_cast of typ * id (* cast *) - | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *) - | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) - | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) - | LEXP_field of (lexp 'a) * id (* struct field *) - -and lexp 'a = - | LEXP_aux of (lexp_aux 'a) * annot 'a - -and fexp_aux 'a = (* field expression *) - | FE_Fexp of id * (exp 'a) - -and fexp 'a = - | FE_aux of (fexp_aux 'a) * annot 'a - -and fexps_aux 'a = (* field expression list *) - | FES_Fexps of list (fexp 'a) * bool - -and fexps 'a = - | FES_aux of (fexps_aux 'a) * annot 'a - -and opt_default_aux 'a = (* optional default value for indexed vector expressions *) - | Def_val_empty - | Def_val_dec of (exp 'a) - -and opt_default 'a = - | Def_val_aux of (opt_default_aux 'a) * annot 'a - -and pexp_aux 'a = (* pattern match *) - | Pat_exp of (pat 'a) * (exp 'a) - -and pexp 'a = - | Pat_aux of (pexp_aux 'a) * annot 'a - -and letbind_aux 'a = (* let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *) - -and letbind 'a = - | LB_aux of (letbind_aux 'a) * annot 'a - -and alias_spec_aux 'a = (* register alias expression forms *) - | AL_subreg of (reg_id 'a) * id - | AL_bit of (reg_id 'a) * (exp 'a) - | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) - | AL_concat of (reg_id 'a) * (reg_id 'a) - -and alias_spec 'a = - | AL_aux of (alias_spec_aux 'a) * annot 'a - - -type funcl_aux 'a = (* function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) - - -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_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 - - -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * annot 'a - - -type rec_opt = - | Rec_aux of rec_opt_aux * l - - -type tannot_opt = - | Typ_annot_opt_aux of tannot_opt_aux * l - - -type effect_opt = - | Effect_opt_aux of effect_opt_aux * l - - -type val_spec_aux 'a = (* 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 *) - - -type fundef_aux 'a = (* function definition *) - | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) - - -type scattered_def_aux 'a = (* scattered function and union type definitions *) - | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) - - -type default_spec_aux 'a = (* default kinding or typing assumption *) - | DT_order of order - | DT_kind of base_kind * kid - | DT_typ of typschm * id - - -type dec_spec_aux 'a = (* register declarations *) - | DEC_reg of typ * id - | DEC_alias of id * (alias_spec 'a) - | DEC_typ_alias of typ * id * (alias_spec 'a) - - -type val_spec 'a = - | VS_aux of (val_spec_aux 'a) * annot 'a - - -type fundef 'a = - | FD_aux of (fundef_aux 'a) * annot 'a - - -type scattered_def 'a = - | SD_aux of (scattered_def_aux 'a) * annot 'a - - -type default_spec 'a = - | DT_aux of (default_spec_aux 'a) * l - - -type dec_spec 'a = - | DEC_aux of (dec_spec_aux 'a) * annot 'a - - -type dec_comm 'a = (* top-level generated comments *) - | DC_comm of string (* generated unstructured comment *) - | DC_comm_struct of (def 'a) (* generated structured comment *) - -and def 'a = (* top-level definition *) - | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) - | DEF_type of (type_def 'a) (* type definition *) - | DEF_fundef of (fundef 'a) (* function definition *) - | DEF_val of (letbind 'a) (* value definition *) - | DEF_spec of (val_spec 'a) (* top-level type constraint *) - | DEF_default of (default_spec 'a) (* default kind and type assumptions *) - | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) - | DEF_reg_dec of (dec_spec 'a) (* register declaration *) - | DEF_comm of (dec_comm 'a) (* generated comments *) - - -type defs 'a = (* definition sequence *) - | Defs of list (def 'a) - - - diff --git a/language/l2.ml b/language/l2.ml deleted file mode 100644 index c59ce838..00000000 --- a/language/l2.ml +++ /dev/null @@ -1,552 +0,0 @@ -(* 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 = 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 *) - - -type -base_kind = - BK_aux of base_kind_aux * Parse_ast.l - - -type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type -kid_aux = (* kinded IDs: $_$, $_$, $_$, and $_$ variables *) - Var of x - - -type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) - - -type -kind = - K_aux of kind_aux * Parse_ast.l - - -type -kid = - Kid_aux of kid_aux * Parse_ast.l - - -type -id = - Id_aux of id_aux * Parse_ast.l - - -type -base_effect_aux = (* effect *) - BE_rreg (* read register *) - | BE_wreg (* write register *) - | BE_rmem (* read memory *) - | BE_rmemt (* read memory and tag *) - | BE_wmem (* write memory *) - | BE_eamem (* signal effective address for writing memory *) - | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *) - | BE_wmv (* write memory, sending only value *) - | BE_wmvt (* write memory, sending only value and tag *) - | BE_barr (* memory barrier *) - | BE_depend (* dynamic footprint *) - | BE_undef (* undefined-instruction exception *) - | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism, from $_$ *) - | BE_escape (* potential call of $_$ *) - | BE_lset (* local mutation; not user-writable *) - | BE_lret (* local return; not user-writable *) - - -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 - - -type -order_aux = (* vector order specifications, of kind $_$ *) - Ord_var of kid (* variable *) - | Ord_inc (* increasing *) - | Ord_dec (* decreasing *) - - -type -effect_aux = (* effect set, of kind $_$ *) - Effect_var of kid - | Effect_set of (base_effect) list (* effect set *) - - -type -order = - Ord_aux of order_aux * Parse_ast.l - - -type -effect = - Effect_aux of effect_aux * Parse_ast.l - - -type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) - - -type -kinded_id = - KOpt_aux of kinded_id_aux * Parse_ast.l - - -type -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 -quant_item_aux = (* kinded identifier or $_$ constraint *) - QI_id of kinded_id (* optionally kinded identifier *) - | QI_const of n_constraint (* $_$ constraint *) - - -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 *) - | L_real of string - - -type -quant_item = - QI_aux of quant_item_aux * Parse_ast.l - - -type -typ_aux = (* type expressions, of kind $_$ *) - Typ_wild (* unspecified type *) - | Typ_id of id (* defined type *) - | 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 = - Typ_aux of typ_aux * Parse_ast.l - -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 - -and typ_arg = - Typ_arg_aux of typ_arg_aux * Parse_ast.l - - -type -lit = - L_aux of lit_aux * Parse_ast.l - - -type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* empty *) - - -type -'a pat_aux = (* pattern *) - P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | 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_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 - -and 'a fpat_aux = (* field pattern *) - FP_Fpat of id * 'a pat - -and 'a fpat = - FP_aux of 'a fpat_aux * 'a annot - - -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 - - -type -type_union_aux = (* type union constructors *) - Tu_id of id - | Tu_ty_id of typ * id - - -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 - - -type -type_union = - Tu_aux of type_union_aux * Parse_ast.l - - -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 *) - - -type -type_def_aux = (* type definition body *) - TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* tagged union type definition *) - | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) - - -type -'a kind_def = - KD_aux of 'a kind_def_aux * 'a annot - - -type -'a type_def = TD_aux of type_def_aux * 'a annot - - -type -'a reg_id_aux = - RI_id of id - - -type -'a exp_aux = (* expression *) - E_block of ('a exp) list (* sequential block *) - | E_nondet of ('a exp) list (* nondeterministic 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 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) *) - | 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 fexps (* struct *) - | E_record_update of 'a exp * 'a fexps (* 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 $'a exp$ from current function *) - | E_exit of 'a exp (* halt all current execution *) - | 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 *) - | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *) - | E_comment of string (* For generated unstructured comments *) - | E_comment_struc of 'a exp (* For generated structured comments *) - | 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_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_memory of id * ('a exp) list (* memory or register write via function call *) - | LEXP_cast of typ * id (* cast *) - | LEXP_tup of ('a lexp) list (* multiple (non-memory) assignment *) - | 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 fexps_aux = (* field expression list *) - FES_Fexps of ('a fexp) list * bool - -and 'a fexps = - FES_aux of 'a fexps_aux * 'a annot - -and 'a opt_default_aux = (* optional default value for indexed vector expressions *) - Def_val_empty - | Def_val_dec of 'a exp - -and 'a opt_default = - Def_val_aux of 'a opt_default_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 ($'a pat$ must be total) *) - -and 'a letbind = - LB_aux of 'a letbind_aux * 'a annot - - -type -'a reg_id = - RI_aux of 'a reg_id_aux * 'a annot - - -type -rec_opt_aux = (* optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) - - -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_none - | Typ_annot_opt_some of typquant * typ - - -type -'a funcl_aux = (* function clause *) - FCL_Funcl of id * 'a pat * 'a exp - - -type -'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 -rec_opt = - Rec_aux of rec_opt_aux * Parse_ast.l - - -type -effect_opt = - Effect_opt_aux of effect_opt_aux * Parse_ast.l - - -type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l - - -type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot - - -type -'a alias_spec = - AL_aux of 'a alias_spec_aux * 'a annot - - -type -'a scattered_def_aux = (* scattered function and union type definitions *) - SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) - - -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 -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 -default_spec_aux = (* default kinding or typing assumption *) - DT_order of order - | DT_kind of base_kind * kid - | DT_typ of typschm * id - - -type -prec = - Infix - | InfixL - | InfixR - - -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 -'a val_spec = VS_aux of val_spec_aux * 'a annot - - -type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot - - -type -default_spec = - DT_aux of default_spec_aux * Parse_ast.l - - -type -'a dec_comm = (* top-level generated comments *) - DC_comm of string (* generated unstructured comment *) - | DC_comm_struct of 'a def (* generated structured comment *) - -and 'a def = (* top-level definition *) - DEF_kind of 'a kind_def (* definition of named kind identifiers *) - | DEF_type of 'a type_def (* type 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 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 *) - | DEF_comm of 'a dec_comm (* generated comments *) - - -type -'a defs = (* definition sequence *) - Defs of ('a def) list - - - diff --git a/language/l2_parse.ml b/language/l2_parse.ml deleted file mode 100644 index 42ef8d44..00000000 --- a/language/l2_parse.ml +++ /dev/null @@ -1,466 +0,0 @@ -(* generated by Ott 0.25 from: l2_parse.ott *) - - -type l = - | Unknown - | Int of string * l option - | Generated of l - | Range of Lexing.position * Lexing.position - -type 'a annot = l * 'a - -exception Parse_error_locn of l * string - - -type x = string (* identifier *) -type ix = string (* 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 * l - - -type -base_effect_aux = (* effect *) - BE_rreg (* read register *) - | BE_wreg (* write register *) - | BE_rmem (* read memory *) - | BE_wmem (* write memory *) - | BE_wmv (* write memory value *) - | BE_eamem (* address for write signaled *) - | BE_barr (* memory barrier *) - | BE_depend (* dynmically dependent footprint *) - | BE_undef (* undefined-instruction exception *) - | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism from intra-instruction parallelism *) - | BE_escape - - -type -kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) - Var of x - - -type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) - - -type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type -base_effect = - BE_aux of base_effect_aux * l - - -type -kid = - Kid_aux of kid_aux * l - - -type -id = - Id_aux of id_aux * l - - -type -kind = - K_aux of kind_aux * l - - -type -atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) - ATyp_id of id (* identifier *) - | ATyp_var of kid (* ticked variable *) - | ATyp_constant of int (* constant *) - | ATyp_times of atyp * atyp (* product *) - | ATyp_sum of atyp * atyp (* sum *) - | ATyp_minus of atyp * atyp (* subtraction *) - | ATyp_exp of atyp (* exponential *) - | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) - | ATyp_inc (* increasing (little-endian) *) - | ATyp_dec (* decreasing (big-endian) *) - | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) - | ATyp_set of (base_effect) list (* effect set *) - | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) - | ATyp_tup of (atyp) list (* Tuple type *) - | ATyp_app of id * (atyp) list (* type constructor application *) - -and atyp = - ATyp_aux of atyp_aux * l - - -type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) - - -type -n_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of atyp * atyp - | NC_bounded_ge of atyp * atyp - | NC_bounded_le of atyp * atyp - | NC_nat_set_bounded of kid * (int) list - - -type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type -n_constraint = - NC_aux of n_constraint_aux * l - - -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 n_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 (quant_item) list - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type -typquant = - TypQ_aux of typquant_aux * 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_undef (* undefined value *) - | L_string of string (* string constant *) - - -type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * atyp - - -type -lit = - L_aux of lit_aux * l - - -type -typschm = - TypSchm_aux of typschm_aux * l - - -type -pat_aux = (* Pattern *) - P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) - | P_typ of atyp * pat (* typed pattern *) - | P_id of id (* identifier *) - | 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_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *) - | P_vector_concat of (pat) list (* concatenated vector pattern *) - | P_tup of (pat) list (* tuple pattern *) - | P_list of (pat) list (* list pattern *) - -and pat = - P_aux of pat_aux * l - -and fpat_aux = (* Field pattern *) - FP_Fpat of id * pat - -and fpat = - FP_aux of fpat_aux * l - - -type -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_lit of lit (* literal constant *) - | E_cast of atyp * exp (* cast *) - | E_app of id * (exp) list (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of (exp) list (* tuple *) - | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * atyp * exp (* loop *) - | E_vector of (exp) list (* vector (indexed from 0) *) - | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *) - | E_vector_access of exp * exp (* vector access *) - | E_vector_subrange of exp * exp * exp (* subvector extraction *) - | E_vector_update of exp * exp * exp (* vector functional update *) - | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) - | E_vector_append of exp * exp (* vector concatenation *) - | E_list of (exp) list (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) - | E_record_update of exp * (exp) list (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * (pexp) list (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of exp * exp (* imperative assignment *) - | E_sizeof of atyp - | E_exit of exp - | E_return of exp - | E_assert of exp * exp - -and exp = - E_aux of exp_aux * l - -and fexp_aux = (* Field-expression *) - FE_Fexp of id * exp - -and fexp = - FE_aux of fexp_aux * l - -and fexps_aux = (* Field-expression list *) - FES_Fexps of (fexp) list * bool - -and fexps = - FES_aux of fexps_aux * l - -and opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) - Def_val_empty - | Def_val_dec of exp - -and opt_default = - Def_val_aux of opt_default_aux * l - -and pexp_aux = (* Pattern match *) - Pat_exp of pat * exp - -and pexp = - Pat_aux of pexp_aux * l - -and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) - -and letbind = - LB_aux of letbind_aux * l - - -type -tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of typquant * atyp - - -type -effect_opt_aux = (* Optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect 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 -type_union_aux = (* Type union constructors *) - Tu_id of id - | Tu_ty_id of atyp * id - - -type -name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string - - -type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l - - -type -effect_opt = - Effect_opt_aux of effect_opt_aux * l - - -type -rec_opt = - Rec_aux of rec_opt_aux * l - - -type -funcl = - FCL_aux of funcl_aux * l - - -type -type_union = - Tu_aux of type_union_aux * 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 * l - - -type -name_scm_opt = - Name_sect_aux of name_scm_opt_aux * l - - -type -default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *) - DT_kind of base_kind * kid - | DT_order of base_kind * atyp - | DT_typ of typschm * id - - -type -fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list - - -type -type_def_aux = (* Type definition body *) - TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) - | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) - - -type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string - - -type -kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) - KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * ((atyp * 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 * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) - - -type -dec_spec_aux = (* Register declarations *) - DEC_reg of atyp * id - | DEC_alias of id * exp - | DEC_typ_alias of atyp * id * exp - - -type -scattered_def_aux = (* Function and type union definitions that can be spread across - a file. Each one must end in $_$ *) - SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of funcl (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) - - -type -default_typing_spec = - DT_aux of default_typing_spec_aux * l - - -type -fundef = - FD_aux of fundef_aux * l - - -type -type_def = - TD_aux of type_def_aux * l - - -type -val_spec = - VS_aux of val_spec_aux * l - - -type -kind_def = - KD_aux of kind_def_aux * l - - -type -dec_spec = - DEC_aux of dec_spec_aux * l - - -type -scattered_def = - SD_aux of scattered_def_aux * l - - -type -def = (* Top-level definition *) - DEF_kind of kind_def (* definition of named kind identifiers *) - | 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 *) - | DEF_default of default_typing_spec (* default kind and type assumptions *) - | DEF_scattered of scattered_def (* scattered definition *) - | DEF_reg_dec of dec_spec (* register declaration *) - - -type -lexp_aux = (* lvalue expression, can't occur out of the parser *) - LEXP_id of id (* identifier *) - | LEXP_mem of id * (exp) list - | LEXP_vector of lexp * exp (* vector element *) - | LEXP_vector_range of lexp * exp * exp (* subvector *) - | LEXP_field of lexp * id (* struct field *) - -and lexp = - LEXP_aux of lexp_aux * l - - -type -defs = (* Definition sequence *) - Defs of (def) list - - - diff --git a/language/l2.ott b/language/sail.ott index a437f915..a437f915 100644 --- a/language/l2.ott +++ b/language/sail.ott diff --git a/language/sil.ott b/language/sil.ott deleted file mode 100644 index 40adfc4d..00000000 --- a/language/sil.ott +++ /dev/null @@ -1,451 +0,0 @@ -%%% Sail Intermediate Language %%% - -% An attempt to precisely document the subset of sail that the -% rewriter is capable of re-writing sail into. It is intended to be a -% strict subset of the Sail AST, and be typecheckable with the full -% typechecker. -% -% Notably, it lacks: -% - Special (bit)vector syntax. -% - Complex l-values. -% - Existential types. -% - Polymorphism, of any kind. - -indexvar n , m , i , j ::= - {{ phantom }} - {{ com Index variables for meta-lists }} - -metavar num,numZero,numOne ::= - {{ phantom }} - {{ lex numeric }} - {{ ocaml int }} - {{ hol num }} - {{ lem integer }} - {{ com Numeric literals }} - -metavar nat ::= - {{ phantom }} - {{ ocaml int }} - {{ lex numeric }} - {{ lem nat }} - -metavar string ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - {{ hol string }} - {{ com String literals }} - -metavar real ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - {{ hol string }} - {{ com Real number literal }} - -embed -{{ ocaml - -type text = string - -type l = Parse_ast.l - -type 'a annot = l * 'a - -type loop = While | Until - -}} - -embed -{{ lem -open import Pervasives -open import Pervasives_extra -open import Map -open import Maybe -open import Set_extra - -type l = - | Unknown - | Int of string * maybe l (*internal types, functions*) - | Range of string * nat * nat * nat * nat - | Generated of l (*location for a generated node, where l is the location of the closest original source*) - -type annot 'a = l * 'a - -val duplicates : forall 'a. list 'a -> list 'a - -val set_from_list : forall 'a. list 'a -> set 'a - -val subst : forall 'a. list 'a -> list 'a -> bool - -type loop = While | Until - -}} - -metavar x , y , z ::= - {{ ocaml text }} - {{ lem string }} - {{ hol string }} - {{ com identifier }} - {{ ocamlvar "[[x]]" }} - {{ lemvar "[[x]]" }} - -grammar - -l :: '' ::= {{ phantom }} - {{ ocaml Parse_ast.l }} - {{ lem l }} - {{ hol unit }} - {{ com source location }} - | :: :: Unknown - {{ ocaml Unknown }} - {{ lem Unknown }} - {{ hol () }} - - -id :: '' ::= - {{ com Identifier }} - {{ aux _ l }} - | x :: :: id - | ( deinfix x ) :: D :: deIid {{ com remove infix status }} - -base_effect :: 'BE_' ::= - {{ com effect }} - {{ aux _ l }} - | rreg :: :: rreg {{ com read register }} - | wreg :: :: wreg {{ com write register }} - | rmem :: :: rmem {{ com read memory }} - | rmemt :: :: rmemt {{ com read memory and tag }} - | wmem :: :: wmem {{ com write memory }} - | wmea :: :: eamem {{ com signal effective address for writing memory }} - | exmem :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }} - | wmv :: :: wmv {{ com write memory, sending only value }} - | wmvt :: :: wmvt {{ com write memory, sending only value and tag }} - | barr :: :: barr {{ com memory barrier }} - | depend :: :: depend {{ com dynamic footprint }} - | undef :: :: undef {{ com undefined-instruction exception }} - | unspec :: :: unspec {{ com unspecified values }} - | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} - | escape :: :: escape {{ com potential call of $[[exit]]$ }} - | lset :: :: lset {{ com local mutation; not user-writable }} - | lret :: :: lret {{ com local return; not user-writable }} - -effect :: 'Effect_' ::= - {{ com effect set, of kind $[[Effect]]$ }} - {{ aux _ l }} - | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} - | pure :: M :: pure {{ com sugar for empty effect set }} - {{ lem (Effect_set []) }} {{icho [[{}]] }} - | effect1 u+ .. u+ effectn :: M :: union {{ com union of sets of effects }} {{ icho [] }} - {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Types % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -typ :: 'Typ_' ::= - {{ com type expressions, of kind $[[Type]]$ }} - {{ aux _ l }} - | id :: :: id - {{ com defined type }} - | typ1 -> typ2 effectkw effect :: :: fn - {{ com Function (first-order only in user code) }} - | ( typ1 , .... , typn ) :: :: tup - {{ com Tuple }} - | id < typ_arg1 , .. , typ_argn > :: :: app - {{ com type constructor application }} - -typ_arg :: 'Typ_arg_' ::= - {{ com type constructor arguments of all kinds }} - {{ aux _ l }} - | typ :: :: typ - -typquant :: 'TypQ_' ::= - {{ com type quantifiers and constraints}} - {{ aux _ l }} - | :: :: no_forall {{ com empty }} - -typschm :: 'TypSchm_' ::= - {{ com type scheme }} - {{ aux _ l }} - | typquant typ :: :: ts - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Type definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::= - {{ ocaml TD_aux of type_def_aux * 'a annot }} - {{ lem TD_aux of type_def_aux * annot 'a }} - | type_def_aux :: :: aux - -type_def_aux :: 'TD_' ::= - {{ com type definition body }} - | typedef id = typschm :: :: abbrev - {{ com type abbreviation }} {{ texlong }} - | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn } :: :: record - {{ com struct type definition }} {{ texlong }} - | typedef id = const union typquant { type_union1 ; ... ; type_unionn } :: :: variant - {{ com tagged union type definition}} {{ texlong }} - | typedef id = enumerate { id1 ; ... ; idn } :: :: enum - {{ com enumeration type definition}} {{ texlong }} - -% This one is a bit unusual - I think all nexps here must be constant, so replace with num. - | typedef id = register bits [ num : num' ] { index_range1 : id1 ; ... ; index_rangen : idn } - :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} - -type_union :: 'Tu_' ::= - {{ com type union constructors }} - {{ aux _ l }} - | id :: :: id - | typ id :: :: ty_id - -index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} - {{ aux _ l }} - | num :: :: 'single' {{ com single index }} - | num1 '..' num2 :: :: range {{ com index range }} - | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Literals % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -lit :: 'L_' ::= - {{ com literal constant }} - {{ aux _ l }} - | ( ) :: :: unit {{ com $() : [[unit]]$ }} - | bitzero :: :: zero {{ com $[[bitzero]] : [[bit]]$ }} - | bitone :: :: one {{ com $[[bitone]] : [[bit]]$ }} - | true :: :: true {{ com $[[true]] : [[bool]]$ }} - | false :: :: false {{ com $[[false]] : [[bool]]$ }} - | num :: :: num {{ com natural number constant }} -% Need to represent as a function call, e.g. sil#hex_string "0xFFFF". -% | hex :: :: hex {{ com bit vector constant, C-style }} -% | bin :: :: bin {{ com bit vector constant, C-style }} - | string :: :: string {{ com string constant }} - | undefined :: :: undef {{ com undefined-value constant }} - | real :: :: real {{ com real number }} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Patterns % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -pat :: 'P_' ::= - {{ com pattern }} - {{ aux _ annot }} {{ auxparam 'a }} - | _ :: :: wild - {{ com wildcard }} - | ( pat as id ) :: :: as - {{ com named pattern }} - | ( typ ) pat :: :: typ - {{ com typed pattern }} - | id :: :: id - {{ com identifier }} - | id ( pat1 , .. , patn ) :: :: app - {{ com union constructor pattern }} - | { fpat1 ; ... ; fpatn } :: :: record - {{ com struct pattern }} - | ( pat1 , .... , patn ) :: :: tup - {{ com tuple pattern }} - | [|| pat1 , .. , patn ||] :: :: list - {{ com list pattern }} - | ( pat ) :: S :: paren - {{ ichlo [[pat]] }} - | pat1 '::' pat2 :: :: cons - {{ com Cons patterns }} - -fpat :: 'FP_' ::= - {{ com field pattern }} - {{ aux _ annot }} {{ auxparam 'a }} - | id = pat :: :: Fpat - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Expressions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -loop :: loop ::= {{ phantom }} - | while :: :: while - | until :: :: until - -exp :: 'E_' ::= - {{ com expression }} - {{ aux _ annot }} {{ auxparam 'a }} - | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} - | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} - | id :: :: id - {{ com identifier }} - | lit :: :: lit - {{ com literal constant }} -% Purely an annotation as all casting is resolved by type checker, can -% be evaluated by simply dropping the type. - | ( typ ) exp :: :: cast - {{ com cast }} - | id ( exp1 , .. , expn ) :: :: app - {{ com function application }} - | ( exp1 , .... , expn ) :: :: tuple - {{ com tuple }} - | if exp1 then exp2 else exp3 :: :: if - {{ com conditional }} - | loop exp1 exp2 :: :: loop - {{ com while or until loop }} - | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for - {{ com for loop }} - | [|| exp1 , .. , expn ||] :: :: list - {{ com list }} - | exp1 '::' exp2 :: :: cons - {{ com cons }} - | { fexps } :: :: record - {{ com struct }} - | { exp with fexps } :: :: record_update - {{ com functional update of struct }} - | exp . id :: :: field - {{ com field projection from struct }} - | switch exp { case pexp1 ... case pexpn } :: :: case - {{ com pattern matching }} - | letbind in exp :: :: let - {{ com let expression }} - | lexp := exp :: :: assign - {{ com imperative assignment }} - | return exp :: :: return - {{ com return $[[exp]]$ from current function }} - | exit exp :: :: exit - {{ com halt all current execution }} - | value :: I :: value - {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} - -lexp :: 'LEXP_' ::= {{ com lvalue expression }} - {{ aux _ annot }} {{ auxparam 'a }} - | id :: :: id - {{ com identifier }} - | ( typ ) id :: :: cast - {{ com cast }} - | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} -% SIL: Not sure how much to rewrite L-expressions. -% | lexp [ exp ] :: :: vector {{ com vector element }} -% | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} -% | lexp . id :: :: field {{ com struct field }} - -fexp :: 'FE_' ::= - {{ com field expression }} - {{ aux _ annot }} {{ auxparam 'a }} - | id = exp :: :: Fexp - -fexps :: 'FES_' ::= - {{ com field expression list }} - {{ aux _ annot }} {{ auxparam 'a }} - | fexp1 ; ... ; fexpn :: :: Fexps - -pexp :: 'Pat_' ::= - {{ com pattern match }} - {{ aux _ annot }} {{ auxparam 'a }} - | pat -> exp :: :: exp - | pat when exp1 -> exp :: :: when - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Function definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -tannot_opt :: 'Typ_annot_opt_' ::= - {{ com optional type annotation for functions}} - {{ aux _ l }} - | :: :: none - | typquant typ :: :: some - -rec_opt :: 'Rec_' ::= - {{ com optional recursive annotation for functions }} - {{ aux _ l }} - | :: :: nonrec {{ com non-recursive }} - | rec :: :: rec {{ com recursive }} - -effect_opt :: 'Effect_opt_' ::= - {{ com optional effect annotation for functions }} - {{ aux _ l }} - | :: :: pure {{ com sugar for empty effect set }} - | effectkw effect :: :: effect - -funcl :: 'FCL_' ::= - {{ com function clause }} - {{ aux _ annot }} {{ auxparam 'a }} - | id pat = exp :: :: Funcl - -fundef :: 'FD_' ::= - {{ com function definition}} - {{ aux _ annot }} {{ auxparam 'a }} - | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} - -letbind :: 'LB_' ::= - {{ com let binding }} - {{ aux _ annot }} {{ auxparam 'a }} - | let pat = exp :: :: val - {{ com let, implicit type ($[[pat]]$ must be total)}} - -val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= - {{ ocaml VS_aux of val_spec_aux * 'a annot }} - {{ lem VS_aux of val_spec_aux * annot 'a }} - | val_spec_aux :: :: aux - -val_spec_aux :: 'VS_' ::= - {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} - {{ lem VS_val_spec of typschm * id * maybe string * bool }} - | val typschm id :: S :: val_spec - {{ com specify the type of an upcoming definition }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} - -default_spec :: 'DT_' ::= - {{ com default kinding or typing assumption }} - {{ aux _ l }} - | default Order order :: :: order - -reg_id :: 'RI_' ::= - {{ aux _ annot }} {{ auxparam 'a }} - | id :: :: id - -alias_spec :: 'AL_' ::= - {{ com register alias expression forms }} - {{ aux _ annot }} {{ auxparam 'a }} - | reg_id . id :: :: subreg - | reg_id [ exp ] :: :: bit - | reg_id [ exp '..' exp' ] :: :: slice - | reg_id : reg_id' :: :: concat - -dec_spec :: 'DEC_' ::= - {{ com register declarations }} - {{ aux _ annot }} {{ auxparam 'a }} - | register typ id :: :: reg - | register alias id = alias_spec :: :: alias - | register alias typ id = alias_spec :: :: typ_alias - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Top-level definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -prec :: '' ::= - | infix :: :: Infix - | infixl :: :: InfixL - | infixr :: :: InfixR - -def :: 'DEF_' ::= - {{ com top-level definition }} - {{ auxparam 'a }} - | type_def :: :: type - {{ com type definition }} - | fundef :: :: fundef - {{ com function definition }} - | letbind :: :: val - {{ com value definition }} - | val_spec :: :: spec - {{ com top-level type constraint }} - | fix prec num id :: :: fixity - {{ com fixity declaration }} - | overload id [ id1 ; ... ; idn ] :: :: overload - {{ com operator overload specification }} - | default_spec :: :: default - {{ com default kind and type assumptions }} - | dec_spec :: :: reg_dec - {{ com register declaration }} - -defs :: '' ::= - {{ com definition sequence }} - {{ auxparam 'a }} - | def1 .. defn :: :: Defs |