diff options
Diffstat (limited to 'src/ast.lem')
| -rw-r--r-- | src/ast.lem | 602 |
1 files changed, 0 insertions, 602 deletions
diff --git a/src/ast.lem b/src/ast.lem deleted file mode 100644 index c3305c97..00000000 --- a/src/ast.lem +++ /dev/null @@ -1,602 +0,0 @@ -(* generated by Ott 0.22 from: l2.ott *) - -open Pmap -open Pervasives - -type l = - | Unknown - | Trans of string * option l - | Range of num * num - -val disjoint : forall 'a . set 'a -> set 'a -> bool -let disjoint s1 s2 = - let diff = s1 inter s2 in - diff = Pervasives.empty - -val disjoint_all : forall 'a. list (set 'a) -> bool -let rec disjoint_all ls = match ls with - | [] -> true - | [a] -> true - | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs)) -end - -val duplicates : forall 'a. list 'a -> list 'a - -val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b - -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 id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - -type base_kind = (* base kind *) - | BK_type (* kind of types *) - | BK_nat (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) - - -type nexp = (* expression of kind $Nat$, for vector sizes and origins *) - | Nexp_id of id (* identifier *) - | Nexp_constant of num (* constant *) - | Nexp_times of nexp * nexp (* product *) - | Nexp_sum of nexp * nexp (* sum *) - | Nexp_exp of nexp (* exponential *) - - -type kind = (* kinds *) - | K_kind of list base_kind - - -type efct = (* effect *) - | Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) - - -type nexp_constraint = (* 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 id * list num - - -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - -type order = (* vector order specifications, of kind $Order$ *) - | Ord_id of id (* identifier *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) - - -type effects = (* effect set, of kind $Effects$ *) - | Effects_var of id - | Effects_set of list efct (* effect set *) - - -type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) - - -type ne = (* internal numeric expressions *) - | Ne_var of id - | Ne_const of num - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type typ = (* Type expressions, of kind $Type$ *) - | Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) - | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) - | Typ_tup of list typ (* Tuple type *) - | Typ_app of id * list typ_arg (* type constructor application *) - -and typ_arg = (* Type constructor arguments of all kinds *) - | Typ_arg_nexp of nexp - | Typ_arg_typ of typ - | Typ_arg_order of order - | Typ_arg_effects of effects - - -type lit = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of num (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_string of string (* string constant *) - - -type typquant = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of list k * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type pat = (* Pattern *) - | P_lit of lit (* literal constant pattern *) - | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) - | P_typ of typ * pat (* typed pattern *) - | P_id of id (* identifier *) - | P_app of id * list pat (* union constructor pattern *) - | P_record of list fpat * bool (* struct pattern *) - | P_vector of list pat (* vector pattern *) - | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *) - | P_vector_concat of list pat (* concatenated vector pattern *) - | P_tup of list pat (* tuple pattern *) - | P_list of list pat (* list pattern *) - -and fpat = (* Field pattern *) - | FP_Fpat of id * pat - - -type typschm = (* type scheme *) - | TypSchm_ts of typquant * typ - - -type exp = (* Expression *) - | E_block of list exp (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) - | E_lit of lit (* literal constant *) - | E_cast of typ * exp (* cast *) - | E_app of exp * list exp (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of list exp (* tuple *) - | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * exp (* loop *) - | E_vector of list exp (* vector (indexed from 0) *) - | E_vector_indexed of list (num * exp) (* 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_list of list exp (* list *) - | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) - | E_record_update of exp * fexps (* functional update of struct *) - | E_field of exp * id (* field projection from struct *) - | E_case of exp * list pexp (* pattern matching *) - | E_let of letbind * exp (* let expression *) - | E_assign of lexp * exp (* imperative assignment *) - -and lexp = (* lvalue expression *) - | LEXP_id of id (* identifier *) - | LEXP_vector of lexp * exp (* vector element *) - | LEXP_vector_range of lexp * exp * exp (* subvector *) - | LEXP_field of lexp * id (* struct field *) - -and fexp = (* Field-expression *) - | FE_Fexp of id * exp - -and fexps = (* Field-expression list *) - | FES_Fexps of list fexp * bool - -and pexp = (* Pattern match *) - | Pat_exp of pat * exp - -and letbind = (* 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) *) - - -type index_range = (* index specification, for bitfields in register types *) - | BF_single of num (* single index *) - | BF_range of num * num (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - - -type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string - - -type rec_opt = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) - - -type tannot_opt = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ - - -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp - - -type effects_opt = (* Optional effect annotation for functions *) - | Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects - - -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id - - -type type_def = (* Type definition body *) - | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id - | DT_typ of typschm * id - - -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effects_opt * list funcl - - -type def = (* Top-level definition *) - | 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_reg_dec of typ * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) - - -type ctor_def = (* Datatype constructor definition clause *) - | CT_ct of id * typschm - - -type typ_lib = (* library types and syntactic sugar for them *) - | Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $true$ and $false$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of typ (* list of typ *) - | Typ_lib_set of typ (* finite set of typ *) - | Typ_lib_reg of typ (* mutable register components holding typ *) - - -type defs = (* Definition sequence *) - | Defs of list def - -(** definitions *) - (* defns translate_ast *) -indreln - -(** definitions *) - (* defns check_t *) -indreln -(* defn check_t *) - -check_t_var: forall E_k id . -( Pmap.find id E_k = Ki_typ ) - ==> -check_t E_k (T_var id) - -and -check_t_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_typ)) - ==> -check_t E_k (T_var id) - -and -check_t_fn: forall E_k t1 t2 effects . -(check_t E_k t1) && -(check_t E_k t2) && -(check_ef E_k effects) - ==> -check_t E_k (T_fn t1 t2 effects) - -and -check_t_tup: forall t_list E_k . -((List.for_all (fun b -> b) ((List.map (fun t_ -> check_t E_k t_) t_list)))) - ==> -check_t E_k (T_tup (t_list)) - -and -check_t_app: forall t_arg_k_list E_k id . -( Pmap.find id E_k = (Ki_ctor ((List.map (fun (t_arg_,k_) -> k_) t_arg_k_list)) Ki_typ) ) && -((List.for_all (fun b -> b) ((List.map (fun (t_arg_,k_) -> check_targs E_k k_ t_arg_) t_arg_k_list)))) - ==> -check_t E_k (T_app id (T_args ((List.map (fun (t_arg_,k_) -> t_arg_) t_arg_k_list)))) - - -and -(* defn check_ef *) - -check_ef_var: forall E_k id . -( Pmap.find id E_k = Ki_efct ) - ==> -check_ef E_k (Effects_var id) - -and -check_ef_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_efct)) - ==> -check_ef E_k (Effects_var id) - -and -check_ef_set: forall efct_list E_k . -true - ==> -check_ef E_k (Effects_set (efct_list)) - - -and -(* defn check_n *) - -check_n_var: forall E_k id . -( Pmap.find id E_k = Ki_nat ) - ==> -check_n E_k (Ne_var id) - -and -check_n_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_nat)) - ==> -check_n E_k (Ne_var id) - -and -check_n_num: forall E_k num . -true - ==> -check_n E_k (Ne_const num) - -and -check_n_sum: forall E_k ne1 ne2 . -(check_n E_k ne1) && -(check_n E_k ne2) - ==> -check_n E_k (Ne_add ne1 ne2) - -and -check_n_mult: forall E_k ne1 ne2 . -(check_n E_k ne1) && -(check_n E_k ne2) - ==> -check_n E_k (Ne_mult ne1 ne2) - -and -check_n_exp: forall E_k ne . -(check_n E_k ne) - ==> -check_n E_k (Ne_exp ne) - - -and -(* defn check_ord *) - -check_ord_var: forall E_k id . -( Pmap.find id E_k = Ki_ord ) - ==> -check_ord E_k (Ord_id id) - -and -check_ord_varInfer: forall E_k id . -( Pmap.find id E_k = Ki_infer ) && -((Formula_update_k E_k id Ki_ord)) - ==> -check_ord E_k (Ord_id id) - - -and -(* defn check_targs *) - -check_targs_typ: forall E_k t . -(check_t E_k t) - ==> -check_targs E_k Ki_typ (Typ t) - -and -check_targs_eff: forall E_k effects . -(check_ef E_k effects) - ==> -check_targs E_k Ki_efct (Effect effects) - -and -check_targs_nat: forall E_k ne . -(check_n E_k ne) - ==> -check_targs E_k Ki_nat (Nexp ne) - -and -check_targs_ord: forall E_k order . -(check_ord E_k order) - ==> -check_targs E_k Ki_ord (Order order) - - -(** definitions *) - (* defns convert_typ *) -indreln -(* defn convert_typ *) - -convert_typ_var: forall E_k id . -( Pmap.find id E_k = Ki_typ ) - ==> -convert_typ E_k (Typ_var id) (T_var id) - -and -convert_typ_fn: forall E_k typ1 typ2 effects t1 t2 . -(convert_typ E_k typ1 t1) && -(convert_typ E_k typ2 t2) && -(check_ef E_k effects) - ==> -convert_typ E_k (Typ_fn typ1 typ2 effects) (T_fn t1 t2 effects) - -and -convert_typ_tup: forall typ_t_list E_k . -((List.for_all (fun b -> b) ((List.map (fun (typ_,t_) -> convert_typ E_k typ_ t_) typ_t_list)))) - ==> -convert_typ E_k (Typ_tup ((List.map (fun (typ_,t_) -> typ_) typ_t_list))) (T_tup ((List.map (fun (typ_,t_) -> t_) typ_t_list))) - -and -convert_typ_app: forall typ_arg_t_arg_k_list E_k id . -( Pmap.find id E_k = (Ki_ctor ((List.map (fun (typ_arg_,t_arg_,k_) -> k_) typ_arg_t_arg_k_list)) Ki_typ) ) && -((List.for_all (fun b -> b) ((List.map (fun (typ_arg_,t_arg_,k_) -> convert_targ E_k k_ typ_arg_ t_arg_) typ_arg_t_arg_k_list)))) - ==> -convert_typ E_k (Typ_app id ((List.map (fun (typ_arg_,t_arg_,k_) -> typ_arg_) typ_arg_t_arg_k_list))) (T_app id (T_args ((List.map (fun (typ_arg_,t_arg_,k_) -> t_arg_) typ_arg_t_arg_k_list)))) - -and -convert_typ_eq: forall E_k typ t2 t1 . -(convert_typ E_k typ t1) - ==> -convert_typ E_k typ t2 - - -and -(* defn convert_targ *) - - -(** definitions *) - (* defns check_lit *) -indreln -(* defn check_lit *) - -check_lit_true: forall . -true - ==> -check_lit L_true (T_var bool_id ) - -and -check_lit_false: forall . -true - ==> -check_lit L_false (T_var bool_id ) - -and -check_lit_num: forall num . -true - ==> -check_lit (L_num num) (T_var nat_id ) - -and -check_lit_string: forall string . -true - ==> -check_lit (L_string string) (T_var string_id ) - -and -check_lit_hex: forall hex zero num . -( ( (Ne_const num) = (hlength hex ) ) ) - ==> -check_lit (L_hex hex) (T_app vector_id (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var bit_id )))]))) - -and -check_lit_bin: forall bin zero num . -( ( (Ne_const num) = (blength bin ) ) ) - ==> -check_lit (L_bin bin) (T_app vector_id (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var bit_id )))]))) - -and -check_lit_unit: forall . -true - ==> -check_lit L_unit (T_var unit_id ) - -and -check_lit_bitzero: forall . -true - ==> -check_lit L_zero (T_var bit_id ) - -and -check_lit_bitone: forall . -true - ==> -check_lit L_one (T_var bit_id ) - - -(** definitions *) - (* defns check_pat *) -indreln -(* defn check_pat *) - -check_pat_wild: forall E_k t . -(check_t E_k t) - ==> -(PARSE_ERROR "line 1762 - 1763" "no parses (char 16): <E_t,E_k> |- _ a***nnot : t gives {} ") - -and -check_pat_as: forall E_t E_k pat id t E_t1 . -(check_pat (Env E_k E_t ) pat t E_t1) && -( Pervasives.not (Pmap.mem id E_t1 ) ) - ==> -check_pat (Env E_k E_t ) (P_as pat id) t (List.fold_right union_map ([(E_t1)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m) ([(id,t)]) Pmap.empty) )]) Pmap.empty) - -and -check_pat_typ: forall E_t E_k typ pat t E_t1 . -(convert_typ E_k typ t) && -(check_pat (Env E_k E_t ) pat t E_t1) - ==> -check_pat (Env E_k E_t ) (P_typ typ pat) t E_t1 - -and -check_pat_ident_constr: forall pat_E_t_t_list E_t E_k id t_args . -((List.for_all (fun b -> b) ((List.map (fun (pat_,E_t_,t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_E_t_t_list)))) - ==> -check_pat (Env E_k E_t ) (P_app id ((List.map (fun (pat_,E_t_,t_) -> pat_) pat_E_t_t_list))) (T_app id t_args) (List.fold_right union_map ((List.map (fun (pat_,E_t_,t_) -> E_t_) pat_E_t_t_list)) Pmap.empty) - -and -check_pat_var: forall E_t E_k id t . -(check_t E_k t) - ==> -check_pat (Env E_k E_t ) (P_id id) t (List.fold_right union_map ([(E_t)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m) ([(id,t)]) Pmap.empty) )]) Pmap.empty) - -and -check_pat_tup: forall pat_t_E_t_list E_t E_k . -((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat (Env E_k E_t ) pat_ t_ E_t_) pat_t_E_t_list)))) && -( disjoint_all (List.map Pmap.domain ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) ) ) - ==> -check_pat (Env E_k E_t ) (P_tup ((List.map (fun (pat_,t_,E_t_) -> pat_) pat_t_E_t_list))) (T_tup ((List.map (fun (pat_,t_,E_t_) -> t_) pat_t_E_t_list))) (List.fold_right union_map ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) Pmap.empty) - - -(** definitions *) - (* defns check_exp *) -indreln - - - |