path: root/src/lem_interp/interp_ast.lem

(*========================================================================*)
(*     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_typ.ott l2.ott *)
open import Pervasives

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 base_kind = 
 | BK_aux of base_kind_aux * l


type kid_aux =  (* variables 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 list base_kind


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

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_rmemt (* read memory and tag *)
 | BE_wmem (* write memory *)
 | BE_eamem (* signal effective address for writing memory *)
 | 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 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 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 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 $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 = 
 | 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 list quant_item
 | TypQ_no_forall (* sugar, omitting quantifier and constraints *)


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_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 $Type$ *)
 | 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 list typ (* Tuple type *)
 | 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 = 
 | L_aux of lit_aux * l


type typschm_aux =  (* type scheme *)
 | TypSchm_ts of typquant * typ


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 typschm = 
 | TypSchm_aux of typschm_aux * l


type reg_id_aux 'a = 
 | RI_id of id


type exp_aux 'a =  (* Expression *)
 | E_block of list (exp 'a) (* block *)
 | E_nondet of list (exp 'a) (* 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 * (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 (* Expression to return the value of the nexp variable or expression at run time *)
 | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
 | E_return of (exp 'a) (* 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 (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
 | 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 *)

and exp 'a = 
 | E_aux of (exp_aux 'a) * annot 'a

and lexp_aux 'a =  (* lvalue expression *)
 | LEXP_id of id (* identifier *)
 | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
 | LEXP_cast of typ * id
 | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *)
 | 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 vectors, to define a defualt value for any unspecified positions in a sparse map *)
 | 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) (* value binding, explicit type ((pat 'a) must be total) *)
 | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)

and letbind 'a = 
 | LB_aux of (letbind_aux 'a) * annot 'a


type reg_id 'a = 
 | RI_aux of (reg_id_aux 'a) * annot 'a


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 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 alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
 | 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)


type type_union = 
 | Tu_aux of type_union_aux * l


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 name_scm_opt = 
 | Name_sect_aux of name_scm_opt_aux * l


type effect_opt = 
 | Effect_opt_aux of effect_opt_aux * l


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 alias_spec 'a = 
 | AL_aux of (alias_spec_aux 'a) * annot 'a


type default_spec_aux 'a =  (* Default kinding or typing assumption *)
 | DT_kind of base_kind * kid
 | DT_order of order
 | DT_typ of typschm * id


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 (* 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 val_spec_aux 'a =  (* 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 kind_def_aux 'a =  (* 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 * 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 scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
         a file. Each one must end in $id$ *)
 | 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 fundef_aux 'a =  (* Function definition *)
 | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)


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 default_spec 'a = 
 | DT_aux of (default_spec_aux 'a) * l


type type_def 'a = 
 | TD_aux of (type_def_aux 'a) * annot 'a


type val_spec 'a = 
 | VS_aux of (val_spec_aux 'a) * annot 'a


type kind_def 'a = 
 | KD_aux of (kind_def_aux 'a) * annot 'a


type scattered_def 'a = 
 | SD_aux of (scattered_def_aux 'a) * annot 'a


type fundef 'a = 
 | FD_aux of (fundef_aux 'a) * annot 'a


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)


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 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 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 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 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 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 widenvec = 
 | Widenvec_widen
 | Widenvec_dont
 | Widenvec_dontcare


type widennum = 
 | Widennum_widen
 | Widennum_dont
 | Widennum_dontcare


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 widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
 | Widening_w of widennum * widenvec

 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 E = env


type I = inf