path: root/language/l2.lem

(* 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 list 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 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 nec =  (* Numeric expression constraints *)
 | Nec_lteq of ne * ne
 | Nec_eq of ne * ne
 | Nec_gteq of ne * ne


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 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_memory of id * exp (* memory write via function call *)
 | 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 effects_opt =  (* Optional effect annotation for functions *)
 | Effects_opt_pure (* sugar for empty effect set *)
 | Effects_opt_effects of effects


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 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 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 defs =  (* Definition sequence *)
 | Defs of list def


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 *)