From fb8ca50af3bb9392b66505b28ba718c90f8ab0ab Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Fri, 3 Feb 2017 14:54:22 +0000 Subject: fix headers --- src/ast.ml | 582 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 581 insertions(+), 1 deletion(-) mode change 120000 => 100644 src/ast.ml (limited to 'src/ast.ml') diff --git a/src/ast.ml b/src/ast.ml deleted file mode 120000 index 8bf3b60c..00000000 --- a/src/ast.ml +++ /dev/null @@ -1 +0,0 @@ -../language/l2.ml \ No newline at end of file diff --git a/src/ast.ml b/src/ast.ml new file mode 100644 index 00000000..5eb45554 --- /dev/null +++ b/src/ast.ml @@ -0,0 +1,581 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +(* generated by Ott 0.25 from: l2.ott *) + + +type text = string + +type l = Parse_ast.l + +type 'a annot = l * 'a + + +type x = text (* identifier *) +type ix = text (* infix identifier *) + +type +base_kind_aux = (* base kind *) + BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effect (* kind of effect sets *) + + +type +base_kind = + BK_aux of base_kind_aux * l + + +type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type +kid_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x + + +type +kind_aux = (* kinds *) + K_kind of (base_kind) list + + +type +id = + Id_aux of id_aux * l + + +type +kid = + Kid_aux of kid_aux * l + + +type +kind = + K_aux of kind_aux * l + + +type +nexp_aux = (* expression of kind Nat, for vector sizes and origins *) + Nexp_id of id (* identifier, bound by def Nat x = nexp *) + | 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 *) + +and nexp = + Nexp_aux of nexp_aux * l + + +type +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) + | BE_barr (* memory barrier *) + | BE_depend (* dynamic footprint *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) + | BE_escape (* Tracking of expressions and functions that might call exit *) + | BE_lset (* Local mutation happend; not user-writable *) + | BE_lret (* Local return happened; 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 (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) + + +type +order = + Ord_aux of order_aux * l + + +type +effect = + Effect_aux of effect_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 nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_nat_set_bounded of kid * (int) list + + +type +kinded_id = + 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 +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 (* constant representing undefined values *) + | L_string of string (* string constant *) + + +type +typquant = + TypQ_aux of typquant_aux * 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 type (first-order only in user code) *) + | Typ_tup of (typ) list (* Tuple type *) + | Typ_app of id * (typ_arg) list (* 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 = + L_aux of lit_aux * l + + +type +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ + + +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_app of id * ('a pat) list (* union constructor pattern *) + | P_record of ('a fpat) list * bool (* struct pattern *) + | P_vector of ('a pat) list (* vector pattern *) + | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *) + | P_vector_concat of ('a pat) list (* concatenated vector pattern *) + | P_tup of ('a pat) list (* tuple pattern *) + | P_list of ('a pat) list (* list pattern *) + +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 +typschm = + TypSchm_aux of typschm_aux * l + + +type +'a reg_id_aux = + RI_id of id + + +type +'a exp_aux = (* Expression *) + E_block of ('a exp) list (* block *) + | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) + | 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_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 (* Expression to return the value of the nexp variable or expression at run time *) + | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) + | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) + | 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 *) + +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 write via function call *) + | LEXP_cast of typ * id + | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *) + | 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 vectors, to define a defualt value for any unspecified positions in a sparse map *) + 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 + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) + LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) + | LB_val_implicit of 'a pat * 'a exp (* value binding, 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 +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of typ * 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 +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp + + +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 +'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) + 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 +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 +effect_opt = + Effect_opt_aux of effect_opt_aux * l + + +type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot + + +type +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l + + +type +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot + + +type +'a default_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid + | DT_order of order + | DT_typ of typschm * id + + +type +'a 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 (* 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 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 (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) + + +type +'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) + KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) + | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +'a 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 '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 fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list + + +type +'a dec_spec_aux = (* Register declarations *) + DEC_reg of typ * id + | DEC_alias of id * 'a alias_spec + | DEC_typ_alias of typ * id * 'a alias_spec + + +type +'a default_spec = + DT_aux of 'a default_spec_aux * l + + +type +'a type_def = + TD_aux of 'a type_def_aux * 'a annot + + +type +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot + + +type +'a kind_def = + KD_aux of 'a kind_def_aux * 'a annot + + +type +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot + + +type +'a fundef = + FD_aux of 'a fundef_aux * 'a annot + + +type +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot + + +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_default of 'a default_spec (* default kind and type assumptions *) + | DEF_scattered of 'a scattered_def (* scattered function and type definition *) + | DEF_reg_dec of 'a dec_spec (* register declaration *) + | DEF_comm of 'a dec_comm (* generated comments *) + + +type +'a defs = (* Definition sequence *) + Defs of ('a def) list + + + -- cgit v1.2.3