1 files changed, 304 insertions, 0 deletions
diff --git a/language/l2.lem b/language/l2.lem
new file mode 100644
index 00000000..51831898
--- /dev/null
+++ b/language/l2.lem
@@ -0,0 +1,304 @@
+(* 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 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 id =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type kind =  (* kinds *)
+ | K_kind of list base_kind
+
+
+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 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 kinded_id =  (* optionally kind-annotated identifier *)
+ | KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
+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 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 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 typquant =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+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_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
+type typschm =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
+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 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 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) *)
+
+and 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
+
+
+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 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 effects_opt =  (* Optional effect annotation for functions *)
+ | Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
+
+
+type funcl =  (* Function clause *)
+ | FCL_Funcl of id * pat * exp
+
+
+type tannot_opt =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type default_typing_spec =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * id
+ | DT_typ of typschm * id
+
+
+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 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 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 ctor_def =  (* Datatype constructor definition clause *)
+ | CT_ct of id * typschm
+
+
+type defs =  (* Definition sequence *)
+ | Defs of list def
+
+
+