From 09fca718c6e850a3a94db399fd1744dc537bbe41 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 4 Apr 2018 15:14:39 +0100 Subject: Cleanup repository by removing old and generated files Rename l2.ott to sail.ott --- language/l2.lem | 705 ----------------------------- language/l2.ml | 552 ----------------------- language/l2.ott | 1211 -------------------------------------------------- language/l2_parse.ml | 466 ------------------- language/sail.ott | 1211 ++++++++++++++++++++++++++++++++++++++++++++++++++ language/sil.ott | 451 ------------------- 6 files changed, 1211 insertions(+), 3385 deletions(-) delete mode 100644 language/l2.lem delete mode 100644 language/l2.ml delete mode 100644 language/l2.ott delete mode 100644 language/l2_parse.ml create mode 100644 language/sail.ott delete mode 100644 language/sil.ott (limited to 'language') 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.ott b/language/l2.ott deleted file mode 100644 index a437f915..00000000 --- a/language/l2.ott +++ /dev/null @@ -1,1211 +0,0 @@ -%% -%% Grammar for user language. Generates ./src/ast.ml -%% - -indexvar n , m , i , j ::= - {{ phantom }} - {{ com Index variables for meta-lists }} - -metavar num,numZero,numOne ::= - {{ phantom }} - {{ lex numeric }} - {{ ocaml big_int }} - {{ hol num }} - {{ lem integer }} - {{ com Numeric literals }} - -metavar nat ::= - {{ phantom }} - {{ ocaml int }} - {{ lex numeric }} - {{ lem nat }} - -metavar hex ::= - {{ phantom }} - {{ lex numeric }} - {{ ocaml string }} - {{ lem string }} - {{ com Bit vector literal, specified by C-style hex number }} - -metavar bin ::= - {{ phantom }} - {{ lex numeric }} - {{ ocaml string }} - {{ lem string }} - {{ com Bit vector literal, specified by C-style binary number }} - -metavar string ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - {{ hol string }} - {{ com String literals }} - -metavar regexp ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - {{ hol string }} - {{ com Regular expresions, as a string literal }} - -metavar real ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - {{ hol string }} - {{ com Real number literal }} - -metavar value ::= - {{ phantom }} - {{ ocaml value }} - {{ lem value }} - -embed -{{ ocaml - -open Big_int -open Value - -type text = string - -type l = Parse_ast.l - -type 'a annot = l * 'a - -type loop = While | Until - -}} - -embed -{{ lem - -type l = | Unknown - -type value = | Val - -type loop = While | Until - -type annot 'a = l * 'a - -}} - -metavar x , y , z ::= - {{ ocaml text }} - {{ lem string }} - {{ hol string }} - {{ com identifier }} - {{ ocamlvar "[[x]]" }} - {{ lemvar "[[x]]" }} - -metavar ix ::= - {{ lex alphanum }} - {{ ocaml text }} - {{ lem string }} - {{ hol string }} - {{ com infix identifier }} - {{ ocamlvar "[[ix]]" }} - {{ lemvar "[[ix]]" }} - -grammar - -l :: '' ::= {{ phantom }} - {{ ocaml Parse_ast.l }} - {{ lem l }} - {{ hol unit }} - {{ com source location }} - | :: :: Unknown - {{ ocaml Unknown }} - {{ lem Unknown }} - {{ hol () }} - -annot :: '' ::= - {{ phantom }} - {{ ocaml 'a annot }} - {{ lem annot 'a }} - {{ hol unit }} - -id :: '' ::= - {{ com Identifier }} - {{ aux _ l }} - | x :: :: id - | ( deinfix x ) :: D :: deIid {{ com remove infix status }} - | bool :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }} - | bit :: M :: bit {{ ichlo (Id "bit") }} - | unit :: M :: unit {{ ichlo (Id "unit") }} - | nat :: M :: nat {{ ichlo (Id "nat") }} - | int :: M :: int {{ ichlo (Id "int") }} - | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} - | range :: M :: range {{ ichlo (Id "range") }} - | atom :: M :: atom {{ ichlo (Id "atom") }} - | vector :: M :: vector {{ ichlo (Id "vector") }} - | list :: M :: list {{ ichlo (Id "list") }} -% | set :: M :: set {{ ichlo (Id "set") }} - | reg :: M :: reg {{ ichlo (Id "reg") }} - | to_num :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }} - | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} - | msb :: M :: msb {{ ichlo (Id "msb") }} -% Note: we have just a single namespace. We don't want the same -% identifier to be reused as a type name or variable, expression -% variable, and field name. We don't enforce any lexical convention -% on type variables (or variables of other kinds) -% We don't enforce a lexical convention on infix operators, as some of the -% targets use alphabetical infix operators. - -% Vector builtins - | vector_access :: M :: vector_access {{ ichlo (Id "vector_access") }} - | vector_update :: M :: vector_update {{ ichlo (Id "vector_update") }} - | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }} - | vector_subrange :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }} - | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} - -% Comparison builtins - | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }} - | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }} - | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }} - | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }} - -kid :: '' ::= - {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} - {{ aux _ l }} - | ' x :: :: var - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Kinds and Types % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -grammar - -base_kind :: 'BK_' ::= - {{ com base kind}} - {{ aux _ l }} - | Type :: :: type {{ com kind of types }} - | Nat :: :: nat {{ com kind of natural number size expressions }} - | Order :: :: order {{ com kind of vector order specifications }} - - -kind :: 'K_' ::= - {{ com kinds}} - {{ aux _ l }} - | base_kind1 -> ... -> base_kindn :: :: kind -% we'll never use ...-> Nat , .. Order , .. or Effects - -nexp :: 'Nexp_' ::= - {{ com numeric expression, of kind $[[Nat]]$ }} - {{ aux _ l }} - | id :: :: id {{ com abbreviation identifier }} - | kid :: :: var {{ com variable }} - | num :: :: constant {{ com constant }} - | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} - | nexp1 * nexp2 :: :: times {{ com product }} - | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} - | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: I :: neg {{ com for internal use only}} - | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} - -order :: 'Ord_' ::= - {{ com vector order specifications, of kind $[[Order]]$}} - {{ aux _ l }} - | kid :: :: var {{ com variable }} - | inc :: :: inc {{ com increasing }} - | dec :: :: dec {{ com decreasing }} - | ( order ) :: S :: paren {{ ichlo [[order]] }} - -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 exception }} - -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]]) }} - -% TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. - -typ :: 'Typ_' ::= - {{ com type expressions, of kind $[[Type]]$ }} - {{ aux _ l }} - | id :: :: id - {{ com defined type }} - | kid :: :: var - {{ com type variable }} - | typ1 -> typ2 effectkw effect :: :: fn - {{ com Function (first-order only in user code) }} -% TODO: build first-order restriction into AST or just into type rules? neither - see note -% TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. - | ( typ1 , .... , typn ) :: :: tup - {{ com Tuple }} - | exist kid1 , .. , kidn , n_constraint . typ :: :: exist -% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker - | id < typ_arg1 , .. , typ_argn > :: :: app - {{ com type constructor application }} - | ( typ ) :: S :: paren {{ ichlo [[typ]] }} -% | range < nexp1, nexp2> :: :: range {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }} - | [| nexp |] :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }} - | [| nexp : nexp' |] :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }} -% | atom < nexp > :: :: atom {{ com equivalent to range }} - | [: nexp :] :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom}=\texttt{range} }} -% use .. not - to avoid ambiguity with nexp - -% total maps and vectors indexed by finite subranges of nat -% | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} -% probably some sugar for vector types, using [ ] similarly to enums: -% (but with .. not : in the former, to avoid confusion...) - | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} -{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$ \texttt{|]} }} - | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} -{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }} - | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} - | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} -% | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }} -% ...so bit [ nexp ] etc is just an instance of that -% | List < typ > :: :: list {{ com list of [[typ]] }} -% | Set < typ > :: :: set {{ com finite set of [[typ]] }} -% | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }} -% "reg t" is basically the ML "t ref" -% not sure how first-class it should be, though -% use "reg word32" etc for the types of vanilla registers - - -typ_arg :: 'Typ_arg_' ::= - {{ com type constructor arguments of all kinds }} - {{ aux _ l }} - | nexp :: :: nexp - | typ :: :: typ - | order :: :: order - -% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ - -%typ_lib :: 'Typ_lib_' ::= -% {{ com library types and syntactic sugar for them }} -% {{ aux _ l }} {{ auxparam 'a }} -% boring base types: -%% | unit :: :: unit {{ com unit type with value $()$ }} -% | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} -% | bit :: :: bit {{ com pure bit values (not mutable bits) }} -% experimentally trying with two distinct types of bool and bit ... -% | nat :: :: nat {{ com natural numbers 0,1,2,... }} -% | string :: :: string {{ com UTF8 strings }} -% finite subranges of nat - -parsing - -Typ_tup <= Typ_tup -Typ_fn right Typ_fn -Typ_fn <= Typ_tup -%Typ_fn right Typ_app1 -%Typ_tup right Typ_app1 - -grammar - -n_constraint :: 'NC_' ::= - {{ com constraint over kind $[[Nat]]$ }} - {{ aux _ l }} - | nexp = nexp' :: :: equal - | nexp >= nexp' :: :: bounded_ge - | nexp '<=' nexp' :: :: bounded_le - | nexp != nexp' :: :: not_equal - | kid 'IN' { num1 , ... , numn } :: :: set - | n_constraint \/ n_constraint' :: :: or - | n_constraint /\ n_constraint' :: :: and - | true :: :: true - | false :: :: false - -% Note only id on the left and constants on the right in a -% finite-set-bound, as we don't think we need anything more - -kinded_id :: 'KOpt_' ::= - {{ com optionally kind-annotated identifier }} - {{ aux _ l }} - | kid :: :: none {{ com identifier }} - | kind kid :: :: kind {{ com kind-annotated variable }} - -quant_item :: 'QI_' ::= - {{ com kinded identifier or $[[Nat]]$ constraint }} - {{ aux _ l }} - | kinded_id :: :: id {{ com optionally kinded identifier }} - | n_constraint :: :: const {{ com $[[Nat]]$ constraint }} - -typquant :: 'TypQ_' ::= - {{ com type quantifiers and constraints}} - {{ aux _ l }} - | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }} -% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE - | :: :: no_forall {{ com empty }} - -typschm :: 'TypSchm_' ::= - {{ com type scheme }} - {{ aux _ l }} - | typquant typ :: :: ts - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Type definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -grammar -%ctor_def :: 'CT_' ::= -% {{ com Datatype constructor definition clause }} -% {{ aux _ annot }} {{ auxparam 'a }} -% | id : typschm :: :: ct -% but we could get away with disallowing constraints in typschm, we -% think - if it's useful to do that - -%enum_opt :: 'EnumOpt_' ::= -% | :: :: empty -% | enum :: :: enum - -%% tdefbody :: 'TD_' ::= -%% {{ com Type definition bodies }} -%% | typschm :: :: abbrev -%% {{ com Type abbreviations }} -%% | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |> :: :: record -%% {{ com Record types }} -%% | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant -%% {{ com Variant types }} -%% - name_scm_opt :: 'Name_sect_' ::= - {{ com optional variable naming-scheme constraint}} - {{ aux _ l }} - | :: :: none - | [ name = regexp ] :: :: some -%% -%% type_def :: '' ::= -%% {{ com Type definitions }} -%% | type id : kind naming_scheme_opt = tdefbody :: :: Td -%% % | enumeration id naming_scheme_opt = tdefbody :: :: Td2 -%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum... -%% - -% TODO: do we need mutually recursive type definitions? - - -%%% OR, IN C STYLE - -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 name_scm_opt = typschm :: :: abbrev - {{ com type abbreviation }} {{ texlong }} - | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record - {{ com struct type definition }} {{ texlong }} -% for specifying constructor result types of nat-indexed GADTs, we can -% let the typi be function types (as constructors are not allowed to -% take parameters of function types) -% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = - | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant - {{ com tagged union type definition}} {{ texlong }} - - | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum - {{ com enumeration type definition}} {{ texlong }} - - | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield - {{ com register mutable bitfield type definition }} {{ texlong }} - -% | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -% :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} - - -% the D(eprecated) forms here should be removed; they add complexity for no purpose. The nexp abbreviation form should have better syntax. -% ; many are shorthands for type\_defs -kind_def :: 'KD_' ::= - {{ com Definition body for elements of kind }} - {{ aux _ annot }} {{ auxparam 'a }} - | Def kind id name_scm_opt = nexp :: :: nabbrev - {{ com $[[Nat]]$-expression abbreviation }} -% | Def kind id name_scm_opt = typschm :: D :: abbrev -% {{ com type abbreviation }} {{ texlong }} -% | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record -% {{ com struct type definition }} {{ texlong }} -% | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant -% {{ com union type definition}} {{ texlong }} -% | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum -% {{ com enumeration type definition}} {{ texlong }} -% -% | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} - - - -% also sugar [ nexp ] - -type_union :: 'Tu_' ::= - {{ com type union constructors }} - {{ aux _ l }} - | 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 % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -grammar - -lit :: 'L_' ::= - {{ com literal constant }} - {{ aux _ l }} - | ( ) :: :: unit {{ com $() : [[unit]]$ }} -%Presumably we want to remove bitzero and bitone ? - | 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 }} - | hex :: :: hex {{ com bit vector constant, C-style }} - {{ com hex and bin are constant bit vectors, C-style }} - | bin :: :: bin {{ com bit vector constant, C-style }} -% Should undefined be of type bit[alpha] or alpha[beta] or just alpha? - | string :: :: string {{ com string constant }} - | undefined :: :: undef {{ com undefined-value constant }} - | real :: :: real - -semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} - {{ ocaml bool }} - {{ lem bool }} - {{ hol bool }} - {{ com optional semi-colon }} - | :: :: no - {{ hol F }} - {{ ocaml false }} - {{ lem false }} - | ';' :: :: yes - {{ hol T }} - {{ ocaml true }} - {{ lem true }} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Patterns % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -typ_pat :: 'TP_' ::= - {{ com type pattern }} - {{ aux _ l }} - | _ :: :: wild - | kid :: :: var - | id ( typ_pat1 , .. , typ_patn ) :: :: app - -pat :: 'P_' ::= - {{ com pattern }} - {{ aux _ annot }} {{ auxparam 'a }} - | lit :: :: lit - {{ com literal constant pattern }} - | _ :: :: wild - {{ com wildcard }} - | ( pat as id ) :: :: as - {{ com named pattern }} -% ML-style -% | ( pat : typ ) :: :: typ -% {{ com Typed patterns }} -% C-style - | ( typ ) pat :: :: typ - {{ com typed pattern }} - | id :: :: id - {{ com identifier }} - | pat typ_pat :: :: var - {{ com bind pattern to type variable }} - | id ( pat1 , .. , patn ) :: :: app - {{ com union constructor pattern }} - -% OR? do we invent something ghastly including a union keyword? Perhaps not... - -% | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record -% {{ com Record patterns }} -% OR - | { fpat1 ; ... ; fpatn semi_opt } :: :: record - {{ com struct pattern }} - -%Patterns for vectors -%Should these be the same since vector syntax has changed, and lists have also changed? - - | [ pat1 , .. , patn ] :: :: vector - {{ com vector pattern }} - -% | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed -% {{ com vector pattern (with explicit indices) }} - -% cf ntoes for this - | pat1 : .... : patn :: :: vector_concat - {{ com concatenated vector pattern }} - - | ( pat1 , .... , patn ) :: :: tup - {{ com tuple pattern }} - | [|| pat1 , .. , patn ||] :: :: list - {{ com list pattern }} - | ( pat ) :: S :: paren - {{ ichlo [[pat]] }} - | pat1 '::' pat2 :: :: cons - {{ com Cons patterns }} - -% XXX Is this still useful? -fpat :: 'FP_' ::= - {{ com field pattern }} - {{ aux _ annot }} {{ auxparam 'a }} - | id = pat :: :: Fpat - -parsing -P_app <= P_app -P_app <= P_as - -grammar - -% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% % Interpreter specific things % -% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -% optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} -% | x :: :: optx_x -% {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} -% | :: :: optx_none -% {{ lem Nothing }} {{ ocaml None }} - -% tag :: 'Tag_' ::= -% {{ com Data indicating where the identifier arises and thus information necessary in compilation }} -% | None :: :: empty -% | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} -% | Set :: :: set {{ com Denotes an expression that mutates a local variable }} -% | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} -% | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} -% | Ctor :: :: ctor {{ com Data constructor from a type union }} -% | Extern optx :: :: extern {{ com External function, specied only with a val statement }} -% | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} -% | Spec :: :: spec -% | Enum num :: :: enum -% | Alias :: :: alias -% | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} - -% embed -% {{ lem - -% type tannot = maybe (typ * tag * list unit * effect * effect) - -% }} - -% embed -% {{ ocaml - -% (* Interpreter specific things are just set to unit here *) -% type tannot = unit - -% type reg_form_set = unit - -% }} - -% grammar -% tannot :: '' ::= -% {{ phantom }} -% {{ ocaml unit }} -% {{ lem tannot }} - -% i_direction :: 'I' ::= -% | IInc :: :: Inc -% | IDec :: :: Dec - -% ctor_kind :: 'C_' ::= -% | C_Enum nat :: :: Enum -% | C_Union :: :: Union - -% reg_form :: 'Form_' ::= -% | Reg id tannot i_direction :: :: Reg -% | SubReg id reg_form index_range :: :: SubReg - -% reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} - -% alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} - -% value :: 'V_' ::= {{ com interpreter evaluated value }} -% | Boxref nat typ :: :: boxref -% | Lit lit :: :: lit -% | Tuple ( value1 , ... , valuen ) :: :: tuple -% | List ( value1 , ... , valuen ) :: :: list -% | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector -% | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse -% | Record typ ( id1 value1 , ... , idn valuen ) :: :: record -% | V_ctor id typ ctor_kind value1 :: :: ctor -% | Unknown :: :: unknown -% | Register reg_form :: :: register -% | Register_alias alias_spec_tannot tannot :: :: register_alias -% | Track value reg_form_set :: :: track - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Expressions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -loop :: loop ::= {{ phantom }} - | while :: :: while - | until :: :: until - -exp :: 'E_' ::= - {{ com expression }} - {{ aux _ annot }} {{ auxparam 'a }} - - | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} -% maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) - - | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} - - | id :: :: id - {{ com identifier }} - - | lit :: :: lit - {{ com literal constant }} - - | ( typ ) exp :: :: cast - {{ com cast }} - - | id ( exp1 , .. , expn ) :: :: app - {{ com function application }} - | id exp :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} - {{ com funtion application to tuple }} - -% Note: fully applied function application only - - | exp1 id exp2 :: :: app_infix - {{ com infix function application }} - - | ( exp1 , .... , expn ) :: :: tuple - {{ com tuple }} - - | if exp1 then exp2 else exp3 :: :: if - {{ com conditional }} - - | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} - | loop exp1 exp2 :: :: loop - | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} - | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }} - | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} - | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} - | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} - | foreach ( id from exp1 downto exp2 by exp3 ) exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }} - | foreach ( id from exp1 downto exp2 ) exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }} - -% vectors - | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} -% order comes from global command-line option??? -% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn -% the expi and the result are both of type vector of 'a - -% we pick [ ] not { } for vector literals for consistency with their -% array-like access syntax, in contrast to the C which has funny -% syntax for array literals. We don't have to preserve [ ] for lists -% as we don't expect to use lists very much. - - | exp [ exp' ] :: :: vector_access - {{ com vector access }} - - | exp [ exp1 '..' exp2 ] :: :: vector_subrange - {{ com subvector extraction }} - % do we want to allow a comma-separated list of such thingies? - - | [ exp with exp1 = exp2 ] :: :: vector_update - {{ com vector functional update }} - - | [ exp with exp1 : exp2 = exp3 ] :: :: vector_update_subrange - {{ com vector subrange update, with vector}} - % do we want a functional update form with a comma-separated list of such? - - | exp : exp2 :: :: vector_append - {{ com vector concatenation }} - -% lists - | [|| exp1 , .. , expn ||] :: :: list - {{ com list }} - | exp1 '::' exp2 :: :: cons - {{ com cons }} - - -% const unions - -% const structs - -% TODO - - | { fexps } :: :: record - {{ com struct }} - | { exp with fexps } :: :: record_update - {{ com functional update of struct }} - | exp . id :: :: field - {{ com field projection from struct }} - -%Expressions for creating and accessing vectors - - - -% map : forall 'x 'y ''N. ('x -> 'y) -> vector ''N 'x -> vector ''N 'y -% zip : forall 'x 'y ''N. vector ''N 'x -> vector ''N 'y -> vector ''N ('x*'y) -% foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y -% foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y -% foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z -%(or unzip) - -% and maybe with nice syntax - - | switch exp { case pexp1 ... case pexpn } :: :: case - {{ com pattern matching }} -% | ( typ ) exp :: :: Typed -% {{ com Type-annotated expressions }} - | letbind in exp :: :: let - {{ com let expression }} - - | lexp := exp :: :: assign - {{ com imperative assignment }} - - | sizeof nexp :: :: sizeof - {{ com the value of $[[nexp]]$ at run time }} - - | return exp :: :: return {{ com return $[[exp]]$ from current function }} -% this can be used to break out of for loops - | exit exp :: :: exit - {{ com halt all current execution }} - | ref id :: :: ref - | throw exp :: :: throw - | try exp catch pexp1 .. pexpn :: :: try -%, potentially calling a system, trap, or interrupt handler with exp - | assert ( exp , exp' ) :: :: assert - {{ com halt with error $[[exp']]$ when not $[[exp]]$ }} -% exp' is optional? - | ( exp ) :: S :: paren {{ ichlo [[exp]] }} - | ( annot ) exp :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} - | annot :: I :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} - | sizeof annot :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}} - | annot , annot' :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} - | comment string :: I :: comment {{ com For generated unstructured comments }} - | comment exp :: I :: comment_struc {{ com For generated structured comments }} - | var lexp = exp in exp' :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} - | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} - | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} - | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} - | constraint n_constraint :: :: constraint - -%i_direction :: 'I' ::= -% | IInc :: :: Inc -% | IDec :: :: Dec - -%ctor_kind :: 'C_' ::= -% | C_Enum nat :: :: Enum -% | C_Union :: :: Union - -%reg_form :: 'Form_' ::= -% | Reg id tannot i_direction :: :: Reg -% | SubReg id reg_form index_range :: :: SubReg - -%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} - -%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} - - -lexp :: 'LEXP_' ::= {{ com lvalue expression }} - {{ aux _ annot }} {{ auxparam 'a }} - | id :: :: id -% | ref id :: :: ref - | deref exp :: :: deref - {{ com identifier }} - | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} - | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} -{{ com sugared form of above for explicit tuple $[[exp]]$ }} - | ( typ ) id :: :: cast -{{ com cast }} - | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} - | lexp [ exp ] :: :: vector {{ com vector element }} - | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} - % maybe comma-sep such lists too - | 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 semi_opt :: :: Fexps - -opt_default :: 'Def_val_' ::= - {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map - {{ aux _ annot }} {{ auxparam 'a }} - | :: :: empty - | ; default = exp :: :: dec - -pexp :: 'Pat_' ::= - {{ com pattern match }} - {{ aux _ annot }} {{ auxparam 'a }} - | pat -> exp :: :: exp - | pat when exp1 -> exp :: :: when -% apparently could use -> or => for this. - -%% % psexp :: 'Pats' ::= -%% % {{ com Multi-pattern matches }} -%% % {{ aux _ l }} -%% % | pat1 ... patn -> exp :: :: exp - - -parsing - -%P_app right LB_Let_val - -%%P_app <= Fun - -%%Fun right App -%%Function right App -E_case right E_app -E_let right E_app - -%%Fun <= Field -%%Function <= Field -E_app <= E_field -E_case <= E_field -E_let <= E_field - -E_app left E_app - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Function definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%% old Lem style %%%%%% -grammar -%% % lem_tannot_opt_aux :: 'LEM_Typ_annot_' ::= -%% % {{ com Optional type annotations }} -%% % | :: :: none -%% % | : typ :: :: some -%% % -%% % lem_tannot_opt {{ tex \ottnt{tannot}^? }} :: 'LEM_Typ_annot_' ::= -%% % {{ com location-annotated optional type annotations }} -%% % | tannot_opt_aux l :: :: aux -%% % -%% % lem_funcl :: 'LEM_FCL' ::= -%% % {{ com Function clauses }} -%% % {{ aux _ l }} -%% % | id pat1 ... patn tannot_opt = exp :: :: Funcl -%% % -%% % lem_letbind :: 'LEM_LB_' ::= -%% % {{ com Let bindings }} -%% % {{ aux _ l }} -%% % | pat tannot_opt = exp :: :: Let_val -%% % {{ com Value bindings }} -%% % | lem_funcl :: :: Let_fun -%% % {{ com Function bindings }} -%% % -%% % -%% % grammar -%% % lem_val_def :: 'LEM_VD' ::= -%% % {{ com Value definitions }} -%% % {{ aux _ l }} -%% % | let lem_letbind :: :: Let_def -%% % {{ com Non-recursive value definitions }} -%% % | let rec lem_funcl1 and ... and lem_funcln :: :: Let_rec -%% % {{ com Recursive function definitions }} -%% % -%% % lem_val_spec :: 'LEM_VS' ::= -%% % {{ com Value type specifications }} -%% % {{ aux _ l }} -%% % | val x_l : typschm :: :: Val_spec - -%%%%% C-ish style %%%%%%%%%% - -tannot_opt :: 'Typ_annot_opt_' ::= - {{ com optional type annotation for functions}} - {{ aux _ l }} - | :: :: none -% Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return - | 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 - -% Generate a pexp, but from slightly different syntax (= rather than ->) -pexp_funcl :: 'Pat_funcl_' ::= - {{ auxparam 'a }} - {{ icho ('a pexp) }} - {{ lem (pexp 'a) }} - | pat = exp :: :: exp {{ ichlo (Pat_aux (Pat_exp [[pat]] [[exp]],Unknown)) }} - | ( pat when exp1 ) = exp :: :: when {{ ichlo (Pat_aux (Pat_when [[pat]] [[exp1]] [[exp]],Unknown)) }} - -funcl :: 'FCL_' ::= - {{ com function clause }} - {{ aux _ annot }} {{ auxparam 'a }} - | id pexp_funcl :: :: Funcl - - -fundef :: 'FD_' ::= - {{ com function definition}} - {{ aux _ annot }} {{ auxparam 'a }} - | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} -% {{ com function definition }} -% TODO note that the typ in the tannot_opt is the *result* type, not -% the type of the whole function. The argument type comes from the -% pattern in the funcl -% TODO the above is ok for single functions, but not for mutually -% recursive functions - the tannot_opt scopes over all the funcli, -% which is ok for the typ_quant part but not for the typ part - -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 * (string -> 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 }} - | val cast typschm id :: S :: cast - {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }} - | val extern typschm id :: S :: extern_no_rename - {{ com specify the type of an external function }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] ([[Some id]]) false) }} {{ lem }} - | val extern typschm id = string :: S :: extern_spec - {{ com specify the type of a function from Lem }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] ([[Some string]]) false) }} {{ lem }} -%where the string must provide an explicit path to the required function but will not be checked - -default_spec :: 'DT_' ::= - {{ com default kinding or typing assumption }} - {{ aux _ l }} - | default Order order :: :: order - | default base_kind kid :: :: kind - | default typschm id :: :: typ -% The intended semantics of these is that if an id in binding position -% doesn't have a kind or type annotation, then we look through the -% default regexps (in order from the beginning) and pick the first -% assumption for which id matches the regexp, if there is one. -% Otherwise we try to infer. Perhaps warn if there are multiple matches. -% For example, we might often have default Type ['alphanum] - -scattered_def :: 'SD_' ::= - {{ com scattered function and union type definitions }} - {{ aux _ annot }} {{ auxparam 'a }} - | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function -{{ texlong }} {{ com scattered function definition header }} - - | function clause funcl :: :: scattered_funcl -{{ texlong }} {{ com scattered function definition clause }} - - | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant -{{ texlong }} {{ com scattered union definition header }} - - | union id member type_union :: :: scattered_unioncl -{{ texlong }} {{ com scattered union definition member }} - | end id :: :: scattered_end -{{ texlong }} {{ com scattered definition end }} - -reg_id :: 'RI_' ::= - {{ aux _ annot }} {{ auxparam 'a }} - | id :: :: id - -alias_spec :: 'AL_' ::= - {{ com register alias expression forms }} -%. Other than where noted, each id must refer to an unaliased register of type vector - {{ 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 - -dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} - | comment string :: :: comm {{ com generated unstructured comment }} - | comment def :: :: comm_struct {{ com generated structured comment }} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Top-level definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -prec :: '' ::= - | infix :: :: Infix - | infixl :: :: InfixL - | infixr :: :: InfixR - -def :: 'DEF_' ::= - {{ com top-level definition }} - {{ auxparam 'a }} - | kind_def :: :: kind - {{ com definition of named kind identifiers }} - | 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 }} - | scattered_def :: :: scattered - {{ com scattered function and type definition }} - | dec_spec :: :: reg_dec - {{ com register declaration }} - | dec_comm :: I :: comm - {{ com generated comments }} - | fundef1 .. fundefn :: I :: internal_mutrec - {{ com internal representation of mutually recursive functions }} - -defs :: '' ::= - {{ com definition sequence }} - {{ auxparam 'a }} - | def1 .. defn :: :: Defs - - - -terminals :: '' ::= - | ** :: :: starstar - {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} - {{ com \texttt{**} }} - | >= :: :: geq - {{ tex \ensuremath{\geq} }} -% {{ tex \ottsym{\textgreater=} }} -% {{ com \texttt{>=} }} - | '<=' :: :: leq - {{ tex \ensuremath{\leq} }} -% {{ tex \ottsym{\textless=} }} -% {{ com \texttt{<=} }} - | -> :: :: arrow - {{ tex \ensuremath{\rightarrow} }} -% {{ tex \ottsym{-\textgreater} }} -% {{ com \texttt{->} }} - | ==> :: :: Longrightarrow - {{ tex \ensuremath{\Longrightarrow} }} - {{ com \texttt{==>} }} -% | <| :: :: startrec -% {{ tex \ensuremath{\langle|} }} -% {{ com \texttt{<|} }} -% | |> :: :: endrec -% {{ tex \ensuremath{|\rangle} }} -% {{ com \texttt{|>} }} - | inter :: :: inter - {{ tex \ensuremath{\cap} }} - | u+ :: :: uplus - {{ tex \ensuremath{\uplus} }} - | u- :: :: uminus - {{ tex \ensuremath{\setminus} }} - | NOTIN :: :: notin - {{ tex \ensuremath{\not\in} }} - | SUBSET :: :: subset - {{ tex \ensuremath{\subset} }} - | NOTEQ :: :: noteq - {{ tex \ensuremath{\not=} }} - | emptyset :: :: emptyset - {{ tex \ensuremath{\emptyset} }} -% | < :: :: lt - {{ tex \ensuremath{\langle} }} -% {{ tex \ottsym{<} }} -% | > :: :: gt - {{ tex \ensuremath{\rangle} }} -% {{ tex \ottsym{>} }} - | lt :: :: mathlt - {{ tex < }} - | gt :: :: mathgt - {{ tex > }} - | ~= :: :: alphaeq - {{ tex \ensuremath{\approx} }} - | ~< :: :: consist - {{ tex \ensuremath{\precapprox} }} - | |- :: :: vdash - {{ tex \ensuremath{\vdash} }} - | |-t :: :: vdashT - {{ tex \ensuremath{\vdash_t} }} - | |-n :: :: vdashN - {{ tex \ensuremath{\vdash_n} }} - | |-e :: :: vdashE - {{ tex \ensuremath{\vdash_e} }} - | |-o :: :: vdashO - {{ tex \ensuremath{\vdash_o} }} - | |-c :: :: vdashC - {{ tex \ensuremath{\vdash_c} }} - | ' :: :: quote - {{ tex \ottsym{'} }} - | |-> :: :: mapsto - {{ tex \ensuremath{\mapsto} }} - | gives :: :: gives - {{ tex \ensuremath{\triangleright} }} - | ~> :: :: leadsto - {{ tex \ensuremath{\leadsto} }} - | select :: :: select - {{ tex \ensuremath{\sigma} }} - | => :: :: Rightarrow - {{ tex \ensuremath{\Rightarrow} }} - | -- :: :: dashdash - {{ tex \mbox{--} }} - | effectkw :: :: effectkw - {{ tex \ottkw{effect} }} - | empty :: :: empty - {{ tex \ensuremath{\epsilon} }} - | consistent_increase :: :: ci - {{ tex \ottkw{consistent\_increase}~ }} - | consistent_decrease :: :: cd - {{ tex \ottkw{consistent\_decrease}~ }} - | == :: :: equiv - {{ tex \equiv }} -% | [| :: :: range_start -% {{ tex \mbox{$\ottsym{[\textbar}$} }} -% | |] :: :: range_end -% {{ tex \mbox{$\ottsym{\textbar]}$} }} -% | [|| :: :: list_start -% {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} -% | ||] :: :: list_end -% {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} 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/sail.ott b/language/sail.ott new file mode 100644 index 00000000..a437f915 --- /dev/null +++ b/language/sail.ott @@ -0,0 +1,1211 @@ +%% +%% Grammar for user language. Generates ./src/ast.ml +%% + +indexvar n , m , i , j ::= + {{ phantom }} + {{ com Index variables for meta-lists }} + +metavar num,numZero,numOne ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml big_int }} + {{ hol num }} + {{ lem integer }} + {{ com Numeric literals }} + +metavar nat ::= + {{ phantom }} + {{ ocaml int }} + {{ lex numeric }} + {{ lem nat }} + +metavar hex ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} + {{ com Bit vector literal, specified by C-style hex number }} + +metavar bin ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} + {{ com Bit vector literal, specified by C-style binary number }} + +metavar string ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com String literals }} + +metavar regexp ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com Regular expresions, as a string literal }} + +metavar real ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com Real number literal }} + +metavar value ::= + {{ phantom }} + {{ ocaml value }} + {{ lem value }} + +embed +{{ ocaml + +open Big_int +open Value + +type text = string + +type l = Parse_ast.l + +type 'a annot = l * 'a + +type loop = While | Until + +}} + +embed +{{ lem + +type l = | Unknown + +type value = | Val + +type loop = While | Until + +type annot 'a = l * 'a + +}} + +metavar x , y , z ::= + {{ ocaml text }} + {{ lem string }} + {{ hol string }} + {{ com identifier }} + {{ ocamlvar "[[x]]" }} + {{ lemvar "[[x]]" }} + +metavar ix ::= + {{ lex alphanum }} + {{ ocaml text }} + {{ lem string }} + {{ hol string }} + {{ com infix identifier }} + {{ ocamlvar "[[ix]]" }} + {{ lemvar "[[ix]]" }} + +grammar + +l :: '' ::= {{ phantom }} + {{ ocaml Parse_ast.l }} + {{ lem l }} + {{ hol unit }} + {{ com source location }} + | :: :: Unknown + {{ ocaml Unknown }} + {{ lem Unknown }} + {{ hol () }} + +annot :: '' ::= + {{ phantom }} + {{ ocaml 'a annot }} + {{ lem annot 'a }} + {{ hol unit }} + +id :: '' ::= + {{ com Identifier }} + {{ aux _ l }} + | x :: :: id + | ( deinfix x ) :: D :: deIid {{ com remove infix status }} + | bool :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }} + | bit :: M :: bit {{ ichlo (Id "bit") }} + | unit :: M :: unit {{ ichlo (Id "unit") }} + | nat :: M :: nat {{ ichlo (Id "nat") }} + | int :: M :: int {{ ichlo (Id "int") }} + | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} + | range :: M :: range {{ ichlo (Id "range") }} + | atom :: M :: atom {{ ichlo (Id "atom") }} + | vector :: M :: vector {{ ichlo (Id "vector") }} + | list :: M :: list {{ ichlo (Id "list") }} +% | set :: M :: set {{ ichlo (Id "set") }} + | reg :: M :: reg {{ ichlo (Id "reg") }} + | to_num :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }} + | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} + | msb :: M :: msb {{ ichlo (Id "msb") }} +% Note: we have just a single namespace. We don't want the same +% identifier to be reused as a type name or variable, expression +% variable, and field name. We don't enforce any lexical convention +% on type variables (or variables of other kinds) +% We don't enforce a lexical convention on infix operators, as some of the +% targets use alphabetical infix operators. + +% Vector builtins + | vector_access :: M :: vector_access {{ ichlo (Id "vector_access") }} + | vector_update :: M :: vector_update {{ ichlo (Id "vector_update") }} + | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }} + | vector_subrange :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }} + | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} + +% Comparison builtins + | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }} + | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }} + | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }} + | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }} + +kid :: '' ::= + {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} + {{ aux _ l }} + | ' x :: :: var + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Kinds and Types % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +grammar + +base_kind :: 'BK_' ::= + {{ com base kind}} + {{ aux _ l }} + | Type :: :: type {{ com kind of types }} + | Nat :: :: nat {{ com kind of natural number size expressions }} + | Order :: :: order {{ com kind of vector order specifications }} + + +kind :: 'K_' ::= + {{ com kinds}} + {{ aux _ l }} + | base_kind1 -> ... -> base_kindn :: :: kind +% we'll never use ...-> Nat , .. Order , .. or Effects + +nexp :: 'Nexp_' ::= + {{ com numeric expression, of kind $[[Nat]]$ }} + {{ aux _ l }} + | id :: :: id {{ com abbreviation identifier }} + | kid :: :: var {{ com variable }} + | num :: :: constant {{ com constant }} + | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} + | nexp1 * nexp2 :: :: times {{ com product }} + | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction }} + | 2** nexp :: :: exp {{ com exponential }} + | neg nexp :: I :: neg {{ com for internal use only}} + | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} + +order :: 'Ord_' ::= + {{ com vector order specifications, of kind $[[Order]]$}} + {{ aux _ l }} + | kid :: :: var {{ com variable }} + | inc :: :: inc {{ com increasing }} + | dec :: :: dec {{ com decreasing }} + | ( order ) :: S :: paren {{ ichlo [[order]] }} + +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 exception }} + +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]]) }} + +% TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. + +typ :: 'Typ_' ::= + {{ com type expressions, of kind $[[Type]]$ }} + {{ aux _ l }} + | id :: :: id + {{ com defined type }} + | kid :: :: var + {{ com type variable }} + | typ1 -> typ2 effectkw effect :: :: fn + {{ com Function (first-order only in user code) }} +% TODO: build first-order restriction into AST or just into type rules? neither - see note +% TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. + | ( typ1 , .... , typn ) :: :: tup + {{ com Tuple }} + | exist kid1 , .. , kidn , n_constraint . typ :: :: exist +% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker + | id < typ_arg1 , .. , typ_argn > :: :: app + {{ com type constructor application }} + | ( typ ) :: S :: paren {{ ichlo [[typ]] }} +% | range < nexp1, nexp2> :: :: range {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }} + | [| nexp |] :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }} + | [| nexp : nexp' |] :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }} +% | atom < nexp > :: :: atom {{ com equivalent to range }} + | [: nexp :] :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom}=\texttt{range} }} +% use .. not - to avoid ambiguity with nexp - +% total maps and vectors indexed by finite subranges of nat +% | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} +% probably some sugar for vector types, using [ ] similarly to enums: +% (but with .. not : in the former, to avoid confusion...) + | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} +{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$ \texttt{|]} }} + | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} +{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }} + | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} + | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} +% | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }} +% ...so bit [ nexp ] etc is just an instance of that +% | List < typ > :: :: list {{ com list of [[typ]] }} +% | Set < typ > :: :: set {{ com finite set of [[typ]] }} +% | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }} +% "reg t" is basically the ML "t ref" +% not sure how first-class it should be, though +% use "reg word32" etc for the types of vanilla registers + + +typ_arg :: 'Typ_arg_' ::= + {{ com type constructor arguments of all kinds }} + {{ aux _ l }} + | nexp :: :: nexp + | typ :: :: typ + | order :: :: order + +% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ + +%typ_lib :: 'Typ_lib_' ::= +% {{ com library types and syntactic sugar for them }} +% {{ aux _ l }} {{ auxparam 'a }} +% boring base types: +%% | unit :: :: unit {{ com unit type with value $()$ }} +% | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} +% | bit :: :: bit {{ com pure bit values (not mutable bits) }} +% experimentally trying with two distinct types of bool and bit ... +% | nat :: :: nat {{ com natural numbers 0,1,2,... }} +% | string :: :: string {{ com UTF8 strings }} +% finite subranges of nat + +parsing + +Typ_tup <= Typ_tup +Typ_fn right Typ_fn +Typ_fn <= Typ_tup +%Typ_fn right Typ_app1 +%Typ_tup right Typ_app1 + +grammar + +n_constraint :: 'NC_' ::= + {{ com constraint over kind $[[Nat]]$ }} + {{ aux _ l }} + | nexp = nexp' :: :: equal + | nexp >= nexp' :: :: bounded_ge + | nexp '<=' nexp' :: :: bounded_le + | nexp != nexp' :: :: not_equal + | kid 'IN' { num1 , ... , numn } :: :: set + | n_constraint \/ n_constraint' :: :: or + | n_constraint /\ n_constraint' :: :: and + | true :: :: true + | false :: :: false + +% Note only id on the left and constants on the right in a +% finite-set-bound, as we don't think we need anything more + +kinded_id :: 'KOpt_' ::= + {{ com optionally kind-annotated identifier }} + {{ aux _ l }} + | kid :: :: none {{ com identifier }} + | kind kid :: :: kind {{ com kind-annotated variable }} + +quant_item :: 'QI_' ::= + {{ com kinded identifier or $[[Nat]]$ constraint }} + {{ aux _ l }} + | kinded_id :: :: id {{ com optionally kinded identifier }} + | n_constraint :: :: const {{ com $[[Nat]]$ constraint }} + +typquant :: 'TypQ_' ::= + {{ com type quantifiers and constraints}} + {{ aux _ l }} + | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }} +% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE + | :: :: no_forall {{ com empty }} + +typschm :: 'TypSchm_' ::= + {{ com type scheme }} + {{ aux _ l }} + | typquant typ :: :: ts + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Type definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +grammar +%ctor_def :: 'CT_' ::= +% {{ com Datatype constructor definition clause }} +% {{ aux _ annot }} {{ auxparam 'a }} +% | id : typschm :: :: ct +% but we could get away with disallowing constraints in typschm, we +% think - if it's useful to do that + +%enum_opt :: 'EnumOpt_' ::= +% | :: :: empty +% | enum :: :: enum + +%% tdefbody :: 'TD_' ::= +%% {{ com Type definition bodies }} +%% | typschm :: :: abbrev +%% {{ com Type abbreviations }} +%% | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |> :: :: record +%% {{ com Record types }} +%% | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant +%% {{ com Variant types }} +%% + name_scm_opt :: 'Name_sect_' ::= + {{ com optional variable naming-scheme constraint}} + {{ aux _ l }} + | :: :: none + | [ name = regexp ] :: :: some +%% +%% type_def :: '' ::= +%% {{ com Type definitions }} +%% | type id : kind naming_scheme_opt = tdefbody :: :: Td +%% % | enumeration id naming_scheme_opt = tdefbody :: :: Td2 +%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum... +%% + +% TODO: do we need mutually recursive type definitions? + + +%%% OR, IN C STYLE + +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 name_scm_opt = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record + {{ com struct type definition }} {{ texlong }} +% for specifying constructor result types of nat-indexed GADTs, we can +% let the typi be function types (as constructors are not allowed to +% take parameters of function types) +% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = + | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + {{ com tagged union type definition}} {{ texlong }} + + | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + + | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield + {{ com register mutable bitfield type definition }} {{ texlong }} + +% | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +% :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + + +% the D(eprecated) forms here should be removed; they add complexity for no purpose. The nexp abbreviation form should have better syntax. +% ; many are shorthands for type\_defs +kind_def :: 'KD_' ::= + {{ com Definition body for elements of kind }} + {{ aux _ annot }} {{ auxparam 'a }} + | Def kind id name_scm_opt = nexp :: :: nabbrev + {{ com $[[Nat]]$-expression abbreviation }} +% | Def kind id name_scm_opt = typschm :: D :: abbrev +% {{ com type abbreviation }} {{ texlong }} +% | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record +% {{ com struct type definition }} {{ texlong }} +% | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant +% {{ com union type definition}} {{ texlong }} +% | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum +% {{ com enumeration type definition}} {{ texlong }} +% +% | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} + + + +% also sugar [ nexp ] + +type_union :: 'Tu_' ::= + {{ com type union constructors }} + {{ aux _ l }} + | 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 % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +grammar + +lit :: 'L_' ::= + {{ com literal constant }} + {{ aux _ l }} + | ( ) :: :: unit {{ com $() : [[unit]]$ }} +%Presumably we want to remove bitzero and bitone ? + | 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 }} + | hex :: :: hex {{ com bit vector constant, C-style }} + {{ com hex and bin are constant bit vectors, C-style }} + | bin :: :: bin {{ com bit vector constant, C-style }} +% Should undefined be of type bit[alpha] or alpha[beta] or just alpha? + | string :: :: string {{ com string constant }} + | undefined :: :: undef {{ com undefined-value constant }} + | real :: :: real + +semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} + {{ ocaml bool }} + {{ lem bool }} + {{ hol bool }} + {{ com optional semi-colon }} + | :: :: no + {{ hol F }} + {{ ocaml false }} + {{ lem false }} + | ';' :: :: yes + {{ hol T }} + {{ ocaml true }} + {{ lem true }} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Patterns % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +typ_pat :: 'TP_' ::= + {{ com type pattern }} + {{ aux _ l }} + | _ :: :: wild + | kid :: :: var + | id ( typ_pat1 , .. , typ_patn ) :: :: app + +pat :: 'P_' ::= + {{ com pattern }} + {{ aux _ annot }} {{ auxparam 'a }} + | lit :: :: lit + {{ com literal constant pattern }} + | _ :: :: wild + {{ com wildcard }} + | ( pat as id ) :: :: as + {{ com named pattern }} +% ML-style +% | ( pat : typ ) :: :: typ +% {{ com Typed patterns }} +% C-style + | ( typ ) pat :: :: typ + {{ com typed pattern }} + | id :: :: id + {{ com identifier }} + | pat typ_pat :: :: var + {{ com bind pattern to type variable }} + | id ( pat1 , .. , patn ) :: :: app + {{ com union constructor pattern }} + +% OR? do we invent something ghastly including a union keyword? Perhaps not... + +% | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record +% {{ com Record patterns }} +% OR + | { fpat1 ; ... ; fpatn semi_opt } :: :: record + {{ com struct pattern }} + +%Patterns for vectors +%Should these be the same since vector syntax has changed, and lists have also changed? + + | [ pat1 , .. , patn ] :: :: vector + {{ com vector pattern }} + +% | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed +% {{ com vector pattern (with explicit indices) }} + +% cf ntoes for this + | pat1 : .... : patn :: :: vector_concat + {{ com concatenated vector pattern }} + + | ( pat1 , .... , patn ) :: :: tup + {{ com tuple pattern }} + | [|| pat1 , .. , patn ||] :: :: list + {{ com list pattern }} + | ( pat ) :: S :: paren + {{ ichlo [[pat]] }} + | pat1 '::' pat2 :: :: cons + {{ com Cons patterns }} + +% XXX Is this still useful? +fpat :: 'FP_' ::= + {{ com field pattern }} + {{ aux _ annot }} {{ auxparam 'a }} + | id = pat :: :: Fpat + +parsing +P_app <= P_app +P_app <= P_as + +grammar + +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Interpreter specific things % +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} +% | x :: :: optx_x +% {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} +% | :: :: optx_none +% {{ lem Nothing }} {{ ocaml None }} + +% tag :: 'Tag_' ::= +% {{ com Data indicating where the identifier arises and thus information necessary in compilation }} +% | None :: :: empty +% | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} +% | Set :: :: set {{ com Denotes an expression that mutates a local variable }} +% | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} +% | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} +% | Ctor :: :: ctor {{ com Data constructor from a type union }} +% | Extern optx :: :: extern {{ com External function, specied only with a val statement }} +% | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} +% | Spec :: :: spec +% | Enum num :: :: enum +% | Alias :: :: alias +% | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} + +% embed +% {{ lem + +% type tannot = maybe (typ * tag * list unit * effect * effect) + +% }} + +% embed +% {{ ocaml + +% (* Interpreter specific things are just set to unit here *) +% type tannot = unit + +% type reg_form_set = unit + +% }} + +% grammar +% tannot :: '' ::= +% {{ phantom }} +% {{ ocaml unit }} +% {{ lem tannot }} + +% i_direction :: 'I' ::= +% | IInc :: :: Inc +% | IDec :: :: Dec + +% ctor_kind :: 'C_' ::= +% | C_Enum nat :: :: Enum +% | C_Union :: :: Union + +% reg_form :: 'Form_' ::= +% | Reg id tannot i_direction :: :: Reg +% | SubReg id reg_form index_range :: :: SubReg + +% reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} + +% alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} + +% value :: 'V_' ::= {{ com interpreter evaluated value }} +% | Boxref nat typ :: :: boxref +% | Lit lit :: :: lit +% | Tuple ( value1 , ... , valuen ) :: :: tuple +% | List ( value1 , ... , valuen ) :: :: list +% | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector +% | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse +% | Record typ ( id1 value1 , ... , idn valuen ) :: :: record +% | V_ctor id typ ctor_kind value1 :: :: ctor +% | Unknown :: :: unknown +% | Register reg_form :: :: register +% | Register_alias alias_spec_tannot tannot :: :: register_alias +% | Track value reg_form_set :: :: track + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Expressions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +loop :: loop ::= {{ phantom }} + | while :: :: while + | until :: :: until + +exp :: 'E_' ::= + {{ com expression }} + {{ aux _ annot }} {{ auxparam 'a }} + + | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} +% maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) + + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} + + | id :: :: id + {{ com identifier }} + + | lit :: :: lit + {{ com literal constant }} + + | ( typ ) exp :: :: cast + {{ com cast }} + + | id ( exp1 , .. , expn ) :: :: app + {{ com function application }} + | id exp :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} + {{ com funtion application to tuple }} + +% Note: fully applied function application only + + | exp1 id exp2 :: :: app_infix + {{ com infix function application }} + + | ( exp1 , .... , expn ) :: :: tuple + {{ com tuple }} + + | if exp1 then exp2 else exp3 :: :: if + {{ com conditional }} + + | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} + | loop exp1 exp2 :: :: loop + | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} + | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }} + | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} + | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} + | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} + | foreach ( id from exp1 downto exp2 by exp3 ) exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }} + | foreach ( id from exp1 downto exp2 ) exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }} + +% vectors + | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} +% order comes from global command-line option??? +% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn +% the expi and the result are both of type vector of 'a + +% we pick [ ] not { } for vector literals for consistency with their +% array-like access syntax, in contrast to the C which has funny +% syntax for array literals. We don't have to preserve [ ] for lists +% as we don't expect to use lists very much. + + | exp [ exp' ] :: :: vector_access + {{ com vector access }} + + | exp [ exp1 '..' exp2 ] :: :: vector_subrange + {{ com subvector extraction }} + % do we want to allow a comma-separated list of such thingies? + + | [ exp with exp1 = exp2 ] :: :: vector_update + {{ com vector functional update }} + + | [ exp with exp1 : exp2 = exp3 ] :: :: vector_update_subrange + {{ com vector subrange update, with vector}} + % do we want a functional update form with a comma-separated list of such? + + | exp : exp2 :: :: vector_append + {{ com vector concatenation }} + +% lists + | [|| exp1 , .. , expn ||] :: :: list + {{ com list }} + | exp1 '::' exp2 :: :: cons + {{ com cons }} + + +% const unions + +% const structs + +% TODO + + | { fexps } :: :: record + {{ com struct }} + | { exp with fexps } :: :: record_update + {{ com functional update of struct }} + | exp . id :: :: field + {{ com field projection from struct }} + +%Expressions for creating and accessing vectors + + + +% map : forall 'x 'y ''N. ('x -> 'y) -> vector ''N 'x -> vector ''N 'y +% zip : forall 'x 'y ''N. vector ''N 'x -> vector ''N 'y -> vector ''N ('x*'y) +% foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y +% foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y +% foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z +%(or unzip) + +% and maybe with nice syntax + + | switch exp { case pexp1 ... case pexpn } :: :: case + {{ com pattern matching }} +% | ( typ ) exp :: :: Typed +% {{ com Type-annotated expressions }} + | letbind in exp :: :: let + {{ com let expression }} + + | lexp := exp :: :: assign + {{ com imperative assignment }} + + | sizeof nexp :: :: sizeof + {{ com the value of $[[nexp]]$ at run time }} + + | return exp :: :: return {{ com return $[[exp]]$ from current function }} +% this can be used to break out of for loops + | exit exp :: :: exit + {{ com halt all current execution }} + | ref id :: :: ref + | throw exp :: :: throw + | try exp catch pexp1 .. pexpn :: :: try +%, potentially calling a system, trap, or interrupt handler with exp + | assert ( exp , exp' ) :: :: assert + {{ com halt with error $[[exp']]$ when not $[[exp]]$ }} +% exp' is optional? + | ( exp ) :: S :: paren {{ ichlo [[exp]] }} + | ( annot ) exp :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} + | annot :: I :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} + | sizeof annot :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}} + | annot , annot' :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} + | comment string :: I :: comment {{ com For generated unstructured comments }} + | comment exp :: I :: comment_struc {{ com For generated structured comments }} + | var lexp = exp in exp' :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} + | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} + | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} + | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} + | constraint n_constraint :: :: constraint + +%i_direction :: 'I' ::= +% | IInc :: :: Inc +% | IDec :: :: Dec + +%ctor_kind :: 'C_' ::= +% | C_Enum nat :: :: Enum +% | C_Union :: :: Union + +%reg_form :: 'Form_' ::= +% | Reg id tannot i_direction :: :: Reg +% | SubReg id reg_form index_range :: :: SubReg + +%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} + +%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} + + +lexp :: 'LEXP_' ::= {{ com lvalue expression }} + {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id +% | ref id :: :: ref + | deref exp :: :: deref + {{ com identifier }} + | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} + | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} +{{ com sugared form of above for explicit tuple $[[exp]]$ }} + | ( typ ) id :: :: cast +{{ com cast }} + | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} + | lexp [ exp ] :: :: vector {{ com vector element }} + | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} + % maybe comma-sep such lists too + | 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 semi_opt :: :: Fexps + +opt_default :: 'Def_val_' ::= + {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map + {{ aux _ annot }} {{ auxparam 'a }} + | :: :: empty + | ; default = exp :: :: dec + +pexp :: 'Pat_' ::= + {{ com pattern match }} + {{ aux _ annot }} {{ auxparam 'a }} + | pat -> exp :: :: exp + | pat when exp1 -> exp :: :: when +% apparently could use -> or => for this. + +%% % psexp :: 'Pats' ::= +%% % {{ com Multi-pattern matches }} +%% % {{ aux _ l }} +%% % | pat1 ... patn -> exp :: :: exp + + +parsing + +%P_app right LB_Let_val + +%%P_app <= Fun + +%%Fun right App +%%Function right App +E_case right E_app +E_let right E_app + +%%Fun <= Field +%%Function <= Field +E_app <= E_field +E_case <= E_field +E_let <= E_field + +E_app left E_app + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Function definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%% old Lem style %%%%%% +grammar +%% % lem_tannot_opt_aux :: 'LEM_Typ_annot_' ::= +%% % {{ com Optional type annotations }} +%% % | :: :: none +%% % | : typ :: :: some +%% % +%% % lem_tannot_opt {{ tex \ottnt{tannot}^? }} :: 'LEM_Typ_annot_' ::= +%% % {{ com location-annotated optional type annotations }} +%% % | tannot_opt_aux l :: :: aux +%% % +%% % lem_funcl :: 'LEM_FCL' ::= +%% % {{ com Function clauses }} +%% % {{ aux _ l }} +%% % | id pat1 ... patn tannot_opt = exp :: :: Funcl +%% % +%% % lem_letbind :: 'LEM_LB_' ::= +%% % {{ com Let bindings }} +%% % {{ aux _ l }} +%% % | pat tannot_opt = exp :: :: Let_val +%% % {{ com Value bindings }} +%% % | lem_funcl :: :: Let_fun +%% % {{ com Function bindings }} +%% % +%% % +%% % grammar +%% % lem_val_def :: 'LEM_VD' ::= +%% % {{ com Value definitions }} +%% % {{ aux _ l }} +%% % | let lem_letbind :: :: Let_def +%% % {{ com Non-recursive value definitions }} +%% % | let rec lem_funcl1 and ... and lem_funcln :: :: Let_rec +%% % {{ com Recursive function definitions }} +%% % +%% % lem_val_spec :: 'LEM_VS' ::= +%% % {{ com Value type specifications }} +%% % {{ aux _ l }} +%% % | val x_l : typschm :: :: Val_spec + +%%%%% C-ish style %%%%%%%%%% + +tannot_opt :: 'Typ_annot_opt_' ::= + {{ com optional type annotation for functions}} + {{ aux _ l }} + | :: :: none +% Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return + | 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 + +% Generate a pexp, but from slightly different syntax (= rather than ->) +pexp_funcl :: 'Pat_funcl_' ::= + {{ auxparam 'a }} + {{ icho ('a pexp) }} + {{ lem (pexp 'a) }} + | pat = exp :: :: exp {{ ichlo (Pat_aux (Pat_exp [[pat]] [[exp]],Unknown)) }} + | ( pat when exp1 ) = exp :: :: when {{ ichlo (Pat_aux (Pat_when [[pat]] [[exp1]] [[exp]],Unknown)) }} + +funcl :: 'FCL_' ::= + {{ com function clause }} + {{ aux _ annot }} {{ auxparam 'a }} + | id pexp_funcl :: :: Funcl + + +fundef :: 'FD_' ::= + {{ com function definition}} + {{ aux _ annot }} {{ auxparam 'a }} + | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} +% {{ com function definition }} +% TODO note that the typ in the tannot_opt is the *result* type, not +% the type of the whole function. The argument type comes from the +% pattern in the funcl +% TODO the above is ok for single functions, but not for mutually +% recursive functions - the tannot_opt scopes over all the funcli, +% which is ok for the typ_quant part but not for the typ part + +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 * (string -> 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 }} + | val cast typschm id :: S :: cast + {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }} + | val extern typschm id :: S :: extern_no_rename + {{ com specify the type of an external function }} + {{ ocaml (VS_val_spec [[typschm]] [[id]] ([[Some id]]) false) }} {{ lem }} + | val extern typschm id = string :: S :: extern_spec + {{ com specify the type of a function from Lem }} + {{ ocaml (VS_val_spec [[typschm]] [[id]] ([[Some string]]) false) }} {{ lem }} +%where the string must provide an explicit path to the required function but will not be checked + +default_spec :: 'DT_' ::= + {{ com default kinding or typing assumption }} + {{ aux _ l }} + | default Order order :: :: order + | default base_kind kid :: :: kind + | default typschm id :: :: typ +% The intended semantics of these is that if an id in binding position +% doesn't have a kind or type annotation, then we look through the +% default regexps (in order from the beginning) and pick the first +% assumption for which id matches the regexp, if there is one. +% Otherwise we try to infer. Perhaps warn if there are multiple matches. +% For example, we might often have default Type ['alphanum] + +scattered_def :: 'SD_' ::= + {{ com scattered function and union type definitions }} + {{ aux _ annot }} {{ auxparam 'a }} + | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function +{{ texlong }} {{ com scattered function definition header }} + + | function clause funcl :: :: scattered_funcl +{{ texlong }} {{ com scattered function definition clause }} + + | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant +{{ texlong }} {{ com scattered union definition header }} + + | union id member type_union :: :: scattered_unioncl +{{ texlong }} {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ texlong }} {{ com scattered definition end }} + +reg_id :: 'RI_' ::= + {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + +alias_spec :: 'AL_' ::= + {{ com register alias expression forms }} +%. Other than where noted, each id must refer to an unaliased register of type vector + {{ 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 + +dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} + | comment string :: :: comm {{ com generated unstructured comment }} + | comment def :: :: comm_struct {{ com generated structured comment }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Top-level definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +prec :: '' ::= + | infix :: :: Infix + | infixl :: :: InfixL + | infixr :: :: InfixR + +def :: 'DEF_' ::= + {{ com top-level definition }} + {{ auxparam 'a }} + | kind_def :: :: kind + {{ com definition of named kind identifiers }} + | 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 }} + | scattered_def :: :: scattered + {{ com scattered function and type definition }} + | dec_spec :: :: reg_dec + {{ com register declaration }} + | dec_comm :: I :: comm + {{ com generated comments }} + | fundef1 .. fundefn :: I :: internal_mutrec + {{ com internal representation of mutually recursive functions }} + +defs :: '' ::= + {{ com definition sequence }} + {{ auxparam 'a }} + | def1 .. defn :: :: Defs + + + +terminals :: '' ::= + | ** :: :: starstar + {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} + {{ com \texttt{**} }} + | >= :: :: geq + {{ tex \ensuremath{\geq} }} +% {{ tex \ottsym{\textgreater=} }} +% {{ com \texttt{>=} }} + | '<=' :: :: leq + {{ tex \ensuremath{\leq} }} +% {{ tex \ottsym{\textless=} }} +% {{ com \texttt{<=} }} + | -> :: :: arrow + {{ tex \ensuremath{\rightarrow} }} +% {{ tex \ottsym{-\textgreater} }} +% {{ com \texttt{->} }} + | ==> :: :: Longrightarrow + {{ tex \ensuremath{\Longrightarrow} }} + {{ com \texttt{==>} }} +% | <| :: :: startrec +% {{ tex \ensuremath{\langle|} }} +% {{ com \texttt{<|} }} +% | |> :: :: endrec +% {{ tex \ensuremath{|\rangle} }} +% {{ com \texttt{|>} }} + | inter :: :: inter + {{ tex \ensuremath{\cap} }} + | u+ :: :: uplus + {{ tex \ensuremath{\uplus} }} + | u- :: :: uminus + {{ tex \ensuremath{\setminus} }} + | NOTIN :: :: notin + {{ tex \ensuremath{\not\in} }} + | SUBSET :: :: subset + {{ tex \ensuremath{\subset} }} + | NOTEQ :: :: noteq + {{ tex \ensuremath{\not=} }} + | emptyset :: :: emptyset + {{ tex \ensuremath{\emptyset} }} +% | < :: :: lt + {{ tex \ensuremath{\langle} }} +% {{ tex \ottsym{<} }} +% | > :: :: gt + {{ tex \ensuremath{\rangle} }} +% {{ tex \ottsym{>} }} + | lt :: :: mathlt + {{ tex < }} + | gt :: :: mathgt + {{ tex > }} + | ~= :: :: alphaeq + {{ tex \ensuremath{\approx} }} + | ~< :: :: consist + {{ tex \ensuremath{\precapprox} }} + | |- :: :: vdash + {{ tex \ensuremath{\vdash} }} + | |-t :: :: vdashT + {{ tex \ensuremath{\vdash_t} }} + | |-n :: :: vdashN + {{ tex \ensuremath{\vdash_n} }} + | |-e :: :: vdashE + {{ tex \ensuremath{\vdash_e} }} + | |-o :: :: vdashO + {{ tex \ensuremath{\vdash_o} }} + | |-c :: :: vdashC + {{ tex \ensuremath{\vdash_c} }} + | ' :: :: quote + {{ tex \ottsym{'} }} + | |-> :: :: mapsto + {{ tex \ensuremath{\mapsto} }} + | gives :: :: gives + {{ tex \ensuremath{\triangleright} }} + | ~> :: :: leadsto + {{ tex \ensuremath{\leadsto} }} + | select :: :: select + {{ tex \ensuremath{\sigma} }} + | => :: :: Rightarrow + {{ tex \ensuremath{\Rightarrow} }} + | -- :: :: dashdash + {{ tex \mbox{--} }} + | effectkw :: :: effectkw + {{ tex \ottkw{effect} }} + | empty :: :: empty + {{ tex \ensuremath{\epsilon} }} + | consistent_increase :: :: ci + {{ tex \ottkw{consistent\_increase}~ }} + | consistent_decrease :: :: cd + {{ tex \ottkw{consistent\_decrease}~ }} + | == :: :: equiv + {{ tex \equiv }} +% | [| :: :: range_start +% {{ tex \mbox{$\ottsym{[\textbar}$} }} +% | |] :: :: range_end +% {{ tex \mbox{$\ottsym{\textbar]}$} }} +% | [|| :: :: list_start +% {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} +% | ||] :: :: list_end +% {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} 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 -- cgit v1.2.3