indexvar n , m , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} metavar num,numZero,numOne ::= {{ phantom }} {{ lex numeric }} {{ ocaml int }} {{ hol num }} {{ lem integer }} {{ com Numeric literals }} metavar nat ::= {{ phantom }} {{ lex numeric }} {{ lem nat }} metavar hex ::= {{ phantom }} {{ lex numeric }} {{ ocaml string }} {{ lem string }} {{ com Bit vector literal, specified by C-style hex number }} metavar bin ::= {{ phantom }} {{ lex numeric }} {{ ocaml string }} {{ lem string }} {{ com Bit vector literal, specified by C-style binary number }} metavar string ::= {{ phantom }} {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com String literals }} metavar regexp ::= {{ phantom }} {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com Regular expresions, as a string literal }} embed {{ ocaml type 'a annot = l * 'a }} embed {{ lem open import Pervasives open import Pervasives_extra 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 }} metavar x , y , z ::= {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com identifier }} {{ ocamlvar "[[x]]" }} {{ lemvar "[[x]]" }} metavar ix ::= {{ lex alphanum }} {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com infix identifier }} {{ ocamlvar "[[ix]]" }} {{ lemvar "[[ix]]" }} grammar l :: '' ::= {{ phantom }} {{ ocaml Parse_ast.l }} {{ lem l }} {{ hol unit }} {{ com source location }} | :: :: Unknown {{ ocaml Unknown }} {{ lem Unknown }} {{ hol () }} annot :: '' ::= {{ phantom }} {{ ocaml 'a annot }} {{ lem annot 'a }} {{ hol unit }} id :: '' ::= {{ com identifier }} {{ aux _ l }} | x :: :: id | ( deinfix x ) :: D :: deIid {{ com remove infix status }} | bool :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }} | bit :: M :: bit {{ ichlo (Id "bit") }} | unit :: M :: unit {{ ichlo (Id "unit") }} | nat :: M :: nat {{ ichlo (Id "nat") }} | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} | range :: M :: range {{ ichlo (Id "range") }} | atom :: M :: atom {{ ichlo (Id "atom") }} | vector :: M :: vector {{ ichlo (Id "vector") }} | list :: M :: list {{ ichlo (Id "list") }} % | set :: M :: set {{ ichlo (Id "set") }} | reg :: M :: reg {{ ichlo (Id "reg") }} | to_num :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }} | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} | msb :: M :: msb {{ ichlo (Id "msb") }} % Note: we have just a single namespace. We don't want the same % identifier to be reused as a type name or variable, expression % variable, and field name. We don't enforce any lexical convention % on type variables (or variables of other kinds) % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. kid :: '' ::= {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} {{ aux _ l }} | ' x :: :: var %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kinds and Types % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar base_kind :: 'BK_' ::= {{ com base kind}} {{ aux _ l }} | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} | Effect :: :: effect {{ com kind of effect sets }} kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat , .. Order , .. or Effects nexp :: 'Nexp_' ::= {{ com numeric expression, of kind $[[Nat]]$ }} {{ aux _ l }} | id :: :: id {{ com abbreviation identifier }} | kid :: :: var {{ com variable }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} | nexp1 + nexp2 :: :: sum {{ com sum }} | nexp1 - nexp2 :: :: minus {{ com subtraction }} | 2** nexp :: :: exp {{ com exponential }} | neg nexp :: I :: neg {{ com for internal use only}} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} | kid :: :: var {{ com variable }} | inc :: :: inc {{ com increasing }} | dec :: :: dec {{ com decreasing }} | ( order ) :: S :: paren {{ ichlo [[order]] }} base_effect :: 'BE_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | rmemt :: :: rmemt {{ com read memory and tag }} | wmem :: :: wmem {{ com write memory }} | wmea :: :: eamem {{ com signal effective address for writing memory }} | exmem :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }} | wmv :: :: wmv {{ com write memory, sending only value }} | wmvt :: :: wmvt {{ com write memory, sending only value and tag }} | barr :: :: barr {{ com memory barrier }} | depend :: :: depend {{ com dynamic footprint }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} | escape :: :: escape {{ com potential call of $[[exit]]$ }} | lset :: :: lset {{ com local mutation; not user-writable }} | lret :: :: lret {{ com local return; not user-writable }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} {{ aux _ l }} | kid :: :: var | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ lem (Effect_set []) }} {{icho [[{}]] }} | effect1 u+ .. u+ effectn :: M :: union {{ com union of sets of effects }} {{ icho [] }} {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} embed {{ lem 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 }} grammar % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. typ :: 'Typ_' ::= {{ com type expressions, of kind $[[Type]]$ }} {{ aux _ l }} | _ :: :: wild {{ com unspecified type }} | id :: :: id {{ com defined type }} | kid :: :: var {{ com type variable }} | typ1 -> typ2 effectkw effect :: :: fn {{ com Function (first-order only in user code) }} % TODO: build first-order restriction into AST or just into type rules? neither - see note % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }} % TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker | id < typ_arg1 , .. , typ_argn > :: :: app {{ com type constructor application }} | ( typ ) :: S :: paren {{ ichlo [[typ]] }} % | range < nexp1, nexp2> :: :: range {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }} | [| nexp |] :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }} | [| nexp : nexp' |] :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }} % | atom < nexp > :: :: atom {{ com equivalent to range }} | [: nexp :] :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom}=\texttt{range} }} % use .. not - to avoid ambiguity with nexp - % total maps and vectors indexed by finite subranges of nat % | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} % probably some sugar for vector types, using [ ] similarly to enums: % (but with .. not : in the former, to avoid confusion...) | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} {{ com sugar for vector indexed by \texttt{[|} [[nexp]] \texttt{|]} }} | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for vector indexed by \texttt{[|} [[nexp]]..[[nexp']] \texttt{|]} }} | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} % ...so bit [ nexp ] etc is just an instance of that % | List < typ > :: :: list {{ com list of [[typ]] }} % | Set < typ > :: :: set {{ com finite set of [[typ]] }} % | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }} % "reg t" is basically the ML "t ref" % not sure how first-class it should be, though % use "reg word32" etc for the types of vanilla registers typ_arg :: 'Typ_arg_' ::= {{ com type constructor arguments of all kinds }} {{ aux _ l }} | nexp :: :: nexp | typ :: :: typ | order :: :: order | effect :: :: effect % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ %typ_lib :: 'Typ_lib_' ::= % {{ com library types and syntactic sugar for them }} % {{ aux _ l }} {{ auxparam 'a }} % boring base types: %% | unit :: :: unit {{ com unit type with value $()$ }} % | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} % | bit :: :: bit {{ com pure bit values (not mutable bits) }} % experimentally trying with two distinct types of bool and bit ... % | nat :: :: nat {{ com natural numbers 0,1,2,... }} % | string :: :: string {{ com UTF8 strings }} % finite subranges of nat parsing Typ_tup <= Typ_tup Typ_fn right Typ_fn Typ_fn <= Typ_tup %Typ_fn right Typ_app1 %Typ_tup right Typ_app1 grammar n_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded % Note only id on the left and constants on the right in a % finite-set-bound, as we don't think we need anything more kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} | kid :: :: none {{ com identifier }} | kind kid :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com kinded identifier or $[[Nat]]$ constraint }} {{ aux _ l }} | kinded_id :: :: id {{ com optionally kinded identifier }} | n_constraint :: :: const {{ com $[[Nat]]$ constraint }} typquant :: 'TypQ_' ::= {{ com type quantifiers and constraints}} {{ aux _ l }} | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE | :: :: no_forall {{ com empty }} typschm :: 'TypSchm_' ::= {{ com type scheme }} {{ aux _ l }} | typquant typ :: :: ts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Type definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar %ctor_def :: 'CT_' ::= % {{ com Datatype constructor definition clause }} % {{ aux _ annot }} {{ auxparam 'a }} % | id : typschm :: :: ct % but we could get away with disallowing constraints in typschm, we % think - if it's useful to do that %enum_opt :: 'EnumOpt_' ::= % | :: :: empty % | enum :: :: enum %% tdefbody :: 'TD_' ::= %% {{ com Type definition bodies }} %% | typschm :: :: abbrev %% {{ com Type abbreviations }} %% | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |> :: :: record %% {{ com Record types }} %% | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant %% {{ com Variant types }} %% name_scm_opt :: 'Name_sect_' ::= {{ com optional variable naming-scheme constraint}} {{ aux _ l }} | :: :: none | [ name = regexp ] :: :: some %% %% type_def :: '' ::= %% {{ com Type definitions }} %% | type id : kind naming_scheme_opt = tdefbody :: :: Td %% % | enumeration id naming_scheme_opt = tdefbody :: :: Td2 %% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum... %% % TODO: do we need mutually recursive type definitions? %%% OR, IN C STYLE type_def :: 'TD_' ::= {{ com type definition body }} {{ aux _ annot }} {{ auxparam 'a }} | typedef id name_scm_opt = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record {{ com struct type definition }} {{ texlong }} % for specifying constructor result types of nat-indexed GADTs, we can % let the typi be function types (as constructors are not allowed to % take parameters of function types) % concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant {{ com tagged union type definition}} {{ texlong }} | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} % the D(eprecated) forms here should be removed; they add complexity for no purpose. The nexp abbreviation form should have better syntax. % ; many are shorthands for type\_defs kind_def :: 'KD_' ::= {{ com Definition body for elements of kind }} {{ aux _ annot }} {{ auxparam 'a }} | Def kind id name_scm_opt = nexp :: :: nabbrev {{ com $[[Nat]]$-expression abbreviation }} | Def kind id name_scm_opt = typschm :: D :: abbrev {{ com type abbreviation }} {{ texlong }} | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record {{ com struct type definition }} {{ texlong }} | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant {{ com union type definition}} {{ texlong }} | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum {{ com enumeration type definition}} {{ texlong }} | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } :: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} % also sugar [ nexp ] type_union :: 'Tu_' ::= {{ com type union constructors }} {{ aux _ l }} | id :: :: id | typ id :: :: ty_id index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} {{ aux _ l }} | num :: :: 'single' {{ com single index }} | num1 '..' num2 :: :: range {{ com index range }} | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Literals % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar lit :: 'L_' ::= {{ com literal constant }} {{ aux _ l }} | ( ) :: :: unit {{ com $() : [[unit]]$ }} %Presumably we want to remove bitzero and bitone ? | bitzero :: :: zero {{ com $[[bitzero]] : [[bit]]$ }} | bitone :: :: one {{ com $[[bitone]] : [[bit]]$ }} | true :: :: true {{ com $[[true]] : [[bool]]$ }} | false :: :: false {{ com $[[false]] : [[bool]]$ }} | num :: :: num {{ com natural number constant }} | hex :: :: hex {{ com bit vector constant, C-style }} {{ com hex and bin are constant bit vectors, C-style }} | bin :: :: bin {{ com bit vector constant, C-style }} % Should undefined be of type bit[alpha] or alpha[beta] or just alpha? | string :: :: string {{ com string constant }} | undefined :: :: undef {{ com undefined-value constant }} semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} {{ ocaml bool }} {{ lem bool }} {{ hol bool }} {{ com optional semi-colon }} | :: :: no {{ hol F }} {{ ocaml false }} {{ lem false }} | ';' :: :: yes {{ hol T }} {{ ocaml true }} {{ lem true }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Patterns % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% pat :: 'P_' ::= {{ com pattern }} {{ aux _ annot }} {{ auxparam 'a }} | lit :: :: lit {{ com literal constant pattern }} | _ :: :: wild {{ com wildcard }} | ( pat as id ) :: :: as {{ com named pattern }} % ML-style % | ( pat : typ ) :: :: typ % {{ com Typed patterns }} % C-style | ( typ ) pat :: :: typ {{ com typed pattern }} | id :: :: id {{ com identifier }} % | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} % OR? do we invent something ghastly including a union keyword? Perhaps not... % | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record % {{ com Record patterns }} % OR | { fpat1 ; ... ; fpatn semi_opt } :: :: record {{ com struct pattern }} %Patterns for vectors %Should these be the same since vector syntax has changed, and lists have also changed? | [ pat1 , .. , patn ] :: :: vector {{ com vector pattern }} | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed {{ com vector pattern (with explicit indices) }} % cf ntoes for this | pat1 : .... : patn :: :: vector_concat {{ com concatenated vector pattern }} | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren {{ ichlo [[pat]] }} % | pat1 '::' pat2 :: :: cons % {{ com Cons patterns }} % XXX Is this still useful? fpat :: 'FP_' ::= {{ com field pattern }} {{ aux _ annot }} {{ auxparam 'a }} | id = pat :: :: Fpat parsing P_app <= P_app P_app <= P_as %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Machinery for typing rules % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% embed {{ lem 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 }} grammar k :: 'Ki_' ::= {{ com Internal kinds }} | K_Typ :: :: typ | K_Nat :: :: nat | K_Ord :: :: ord | K_Efct :: :: efct | K_Lam ( k0 .. kn -> k' ) :: :: ctor | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} t , u :: 'T_' ::= {{ com Internal types }} | x :: :: id | ' x :: :: var | t1 -> t2 effect :: :: fn | ( t1 , .... , tn ) :: :: tup | x < t_args > :: :: app | t |-> t1 :: :: abbrev | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} | atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }} | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }} | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }} | bit :: S :: bit_typ {{ ichlo T_id "bit" }} | string :: S :: string_typ {{ ichlo T_id "string" }} | unit :: S :: unit_typ {{ ichlo T_id "unit" }} | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} | x :: :: optx_x {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} | :: :: optx_none {{ lem Nothing }} {{ ocaml None }} tag :: 'Tag_' ::= {{ com Data indicating where the identifier arises and thus information necessary in compilation }} | None :: :: empty | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} | Set :: :: set {{ com Denotes an expression that mutates a local variable }} | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} | Ctor :: :: ctor {{ com Data constructor from a type union }} | Extern optx :: :: extern {{ com External function, specied only with a val statement }} | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} | Spec :: :: spec | Enum num :: :: enum | Alias :: :: alias | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} ne :: 'Ne_' ::= {{ com internal numeric expressions }} | x :: :: id | ' x :: :: var | num :: :: const | infinity :: :: inf | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add | ne1 - ne2 :: :: minus | 2 ** ne :: :: exp | ( - ne ) :: :: unary | zero :: S :: zero {{ ichlo (Ne_const 0) }} | one :: S :: one {{ ichlo (Ne_const 1) }} | bitlength ( bin ) :: M :: cbin {{ ocaml (asssert false) }} {{ hol ARB }} {{ lem (blength [[bin]]) }} | bitlength ( hex ) :: M :: chex {{ ocaml (assert false) }} {{ hol ARB }} {{ lem (hlength [[hex]]) }} | count ( num0 ... numi ) :: M :: length {{ichlo "todo" }} | length ( pat1 ... patn ) :: M :: cpat {{ ocaml (assert false) }} {{ hol ARB }} {{ lem (Ne_const (List.length [[pat1...patn]])) }} | length ( exp1 ... expn ) :: M :: cexp {{ hol ARB }} {{ ocaml (assert false) }} {{ lem (Ne_const (List.length [[exp1...expn]])) }} t_arg :: 't_arg_' ::= {{ com Argument to type constructors }} | t :: :: typ | ne :: :: nexp | effect :: :: effect | order :: :: order | fresh :: M :: freshvar {{ ichlo T_arg (T_var "fresh") }} t_args :: '' ::= {{ lem list t_arg }} {{ com Arguments to type constructors }} | t_arg1 ... t_argn :: :: T_args nec :: 'Nec_' ::= {{ com Numeric expression constraints }} | ne <= ne' :: :: lteq | ne = ne' :: :: eq | ne >= ne' :: :: gteq | ' x 'IN' { num1 , ... , numn } :: :: in | nec0 .. necn -> nec'0 ... nec'm :: :: cond | nec0 ... necn :: :: branch S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} {{ hol nec list }} {{ lem list nec }} {{ com nexp constraint lists }} | { nec1 , .. , necn } :: :: Sn_concrete {{ hol [[nec1 .. necn]] }} {{ lem [[nec1 .. necn]] }} | S_N1 u+ .. u+ S_Nn :: M :: SN_union {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }} {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }} {{ ocaml (assert false) }} | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }} {{ ocaml (assert false) }} {{ ichl todo }} | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }} {{ ocaml assert false }} {{ ichl todo }} | resolve ( S_N ) :: :: resolution {{ lem [[S_N]] (* Write constraint solver *) }} E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} {{ lem definition_env }} {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }} | < E_k , E_a , E_r , E_e > :: :: base {{ hol arb }} {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} | empty :: :: empty {{ hol arb }} {{ lem DenvEmp }} | E_d u+ E_d' :: :: union {{ hol arb }} {{ lem (denv_union [[E_d]] [[E_d']]) }} kinf :: 'kinf_' ::= {{ com Whether a kind is default or from a local binding }} | k :: :: k | k default :: :: def tid :: 'tid_' ::= {{ com A type identifier or type variable }} | id :: :: id | kid :: :: var E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} {{ hol (tid-> kinf) }} {{ lem (map tid kinf) }} {{ com Kind environments }} | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} | E_k1 u+ .. u+ E_kn :: M :: union {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }} {{ ocaml (assert false) }} | E_k u- E_k1 .. E_kn :: M :: multi_set_minus {{ hol arb }} {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} {{ ocaml assert false }} tinf :: 'tinf_' ::= {{ com Type variables, type, and constraints, bound to an identifier }} | t :: :: typ | E_k , S_N , tag , t :: :: quant_typ tinflist :: 'tinfs_' ::= {{ com In place so that a list of tinfs can be referred to without the dot form }} | empty :: :: empty | tinf1 ... tinfn :: :: ls conformsto :: 'conformsto_' ::= {{ com how much conformance does overloading need }} | full :: :: full | parm :: :: parm widenvec :: 'widenvec_' ::= | vectors :: :: widen | none :: :: dont | _ :: :: dontcare widennum :: 'widennum_' ::= | nums :: :: widen | none :: :: dont | _ :: :: dontcare widening :: 'widening_' ::= {{ com Should we widen vector start locations, should we widen atoms and ranges }} | ( widennum , widenvec ) :: :: w E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::= {{ phantom }} {{ hol tid |-> tinf}} {{ lem map tid tinf }} | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete | E_a1 u+ .. u+ E_an :: :: union field_typs :: 'FT_' ::= {{ phantom }} {{ lem list (id * t) }} {{ com Record fields }} | id1 : t1 , .. , idn : tn :: :: fields {{ lem [[id1 t1..idn tn]] }} E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} {{ hol (id*t) |-> tinf) }} {{ lem map (list (id*t)) tinf }} {{ com Record environments }} | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} | E_r1 u+ .. u+ E_rn :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} {{ ocaml (assert false) }} enumerate_map :: '' ::= {{ phantom }} {{ lem (list (nat*id)) }} | { num1 |-> id1 ... numn |-> idn } :: :: enum_map {{ lem [[num1 id1...numn idn]] }} E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} {{ lem (map t (list (nat*id))) }} {{ com Enumeration environments }} | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} | E_e1 u+ .. u+ E_en :: :: union {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} embed {{ lem type definition_env = | DenvEmp | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) }} grammar E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} {{ hol (id |-> tinf) }} {{ lem map id tinf }} {{ com Type environments }} | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} | { id |-> overload tinf conformsto : tinf1 , ... , tinfn } :: :: overload | ( E_t1 u+ .... u+ E_tn ) :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} {{ ocaml (assert false) }} | u+ E_t1 .. E_tn :: M :: multi_union {{ hol arb }} {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} {{ ocaml assert false }} | E_t u- id1 .. idn :: M :: multi_set_minus {{ hol arb }} {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} {{ ocaml assert false }} | ( E_t1 inter .... inter E_tn ) :: M :: intersect {{ hol arb }} {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} {{ ocaml (assert false) }} | inter E_t1 .. E_tn :: M :: multi_inter {{ hol arb }} {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} {{ ocaml assert false }} ts :: ts_ ::= {{ phantom }} {{ lem list t }} | t1 , .. , tn :: :: lst embed {{ lem 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*) }} grammar E :: '' ::= {{ hol ((string,env_body) fmaptree) }} {{ lem env }} {{ com Definition environment and lexical environment }} | < E_t , E_d > :: :: E {{ hol arb }} {{ lem (Env [[E_t]] [[E_d]]) }} | empty :: M :: E_empty {{ hol arb }} {{ lem EnvEmp }} {{ ocaml assert false }} | E u+ E' :: :: E_union {{ lem (env_union [[E]] [[E']]) }} I :: '' ::= {{ lem inf }} {{ com Information given by type checking an expression }} | < S_N , effect > :: :: I {{ lem (Inf [[S_N]] [[effect]]) }} | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} {{ lem Iemp }} | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }} | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% embed {{ lem type tannot = maybe (t * tag * list nec * effect * effect) }} grammar tannot :: '' ::= {{ phantom }} {{ ocaml tannot }} {{ lem tannot }} exp :: 'E_' ::= {{ com expression }} {{ aux _ annot }} {{ auxparam 'a }} | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} | id :: :: id {{ com identifier }} | lit :: :: lit {{ com literal constant }} | ( typ ) exp :: :: cast {{ com cast }} | id ( exp1 , .. , expn ) :: :: app {{ com function application }} | id exp :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} {{ com funtion application to tuple }} % Note: fully applied function application only | exp1 id exp2 :: :: app_infix {{ com infix function application }} | ( exp1 , .... , expn ) :: :: tuple {{ com tuple }} | if exp1 then exp2 else exp3 :: :: if {{ com conditional }} | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} | foreach ( id from exp1 downto exp2 by exp3 ) exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }} | foreach ( id from exp1 downto exp2 ) exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }} % vectors | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} % order comes from global command-line option??? % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn % the expi and the result are both of type vector of 'a | [ num1 = exp1 , ... , numn = expn opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }} % num1 .. numn must be a consecutive list of naturals % we pick [ ] not { } for vector literals for consistency with their % array-like access syntax, in contrast to the C which has funny % syntax for array literals. We don't have to preserve [ ] for lists % as we don't expect to use lists very much. | exp [ exp' ] :: :: vector_access {{ com vector access }} | exp [ exp1 '..' exp2 ] :: :: vector_subrange {{ com subvector extraction }} % do we want to allow a comma-separated list of such thingies? | [ exp with exp1 = exp2 ] :: :: vector_update {{ com vector functional update }} | [ exp with exp1 : exp2 = exp3 ] :: :: vector_update_subrange {{ com vector subrange update, with vector}} % do we want a functional update form with a comma-separated list of such? | exp : exp2 :: :: vector_append {{ com vector concatenation }} % lists | [|| exp1 , .. , expn ||] :: :: list {{ com list }} | exp1 '::' exp2 :: :: cons {{ com cons }} % const unions % const structs % TODO | { fexps } :: :: record {{ com struct }} | { exp with fexps } :: :: record_update {{ com functional update of struct }} | exp . id :: :: field {{ com field projection from struct }} %Expressions for creating and accessing vectors % map : forall 'x 'y ''N. ('x -> 'y) -> vector ''N 'x -> vector ''N 'y % zip : forall 'x 'y ''N. vector ''N 'x -> vector ''N 'y -> vector ''N ('x*'y) % foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y % foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y % foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z %(or unzip) % and maybe with nice syntax | switch exp { case pexp1 ... case pexpn } :: :: case {{ com pattern matching }} % | ( typ ) exp :: :: Typed % {{ com Type-annotated expressions }} | letbind in exp :: :: let {{ com let expression }} | lexp := exp :: :: assign {{ com imperative assignment }} | sizeof nexp :: :: sizeof {{ com the value of [[nexp]] at run time }} | return exp :: :: return {{ com return [[exp]] from current function }} % this can be used to break out of for loops | exit exp :: :: exit {{ com halt all current execution }} %, potentially calling a system, trap, or interrupt handler with exp | assert ( exp , exp' ) :: :: assert {{ com halt with error [[exp']] when not [[exp]] }} % exp' is optional? | ( exp ) :: S :: paren {{ ichlo [[exp]] }} | ( annot ) exp :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} | annot :: I :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} | sizeof annot :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}} | annot , annot' :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} | comment string :: I :: comment {{ com For generated unstructured comments }} | comment exp :: I :: comment_struc {{ com For generated structured comments }} | let lexp = exp in exp' :: I :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} | return_int ( exp ) :: I :: internal_return {{ com For internal use to embed into monad definition }} | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} i_direction :: 'I' ::= | IInc :: :: Inc | IDec :: :: Dec ctor_kind :: 'C_' ::= | C_Enum nat :: :: Enum | C_Union :: :: Union reg_form :: 'Form_' ::= | Reg id tannot i_direction :: :: Reg | SubReg id reg_form index_range :: :: SubReg reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} value :: 'V_' ::= {{ com interpreter evaluated value }} | Boxref nat t :: :: boxref | Lit lit :: :: lit | Tuple ( value1 , ... , valuen ) :: :: tuple | List ( value1 , ... , valuen ) :: :: list | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse | Record t ( id1 value1 , ... , idn valuen ) :: :: record | V_ctor id t ctor_kind value1 :: :: ctor | Unknown :: :: unknown | Register reg_form :: :: register | Register_alias alias_spec_tannot tannot :: :: register_alias | Track value reg_form_set :: :: track lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} {{ com sugared form of above for explicit tuple [[exp]] }} | ( typ ) id :: :: cast {{ com cast }} | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too | lexp . id :: :: field {{ com struct field }} fexp :: 'FE_' ::= {{ com field expression }} {{ aux _ annot }} {{ auxparam 'a }} | id = exp :: :: Fexp fexps :: 'FES_' ::= {{ com field expression list }} {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps opt_default :: 'Def_val_' ::= {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map {{ aux _ annot }} {{ auxparam 'a }} | :: :: empty | ; default = exp :: :: dec pexp :: 'Pat_' ::= {{ com pattern match }} {{ aux _ annot }} {{ auxparam 'a }} | pat -> exp :: :: exp % apparently could use -> or => for this. %% % psexp :: 'Pats' ::= %% % {{ com Multi-pattern matches }} %% % {{ aux _ l }} %% % | pat1 ... patn -> exp :: :: exp parsing %P_app right LB_Let_val %%P_app <= Fun %%Fun right App %%Function right App E_case right E_app E_let right E_app %%Fun <= Field %%Function <= Field E_app <= E_field E_case <= E_field E_let <= E_field E_app left E_app %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Function definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% old Lem style %%%%%% grammar %% % lem_tannot_opt_aux :: 'LEM_Typ_annot_' ::= %% % {{ com Optional type annotations }} %% % | :: :: none %% % | : typ :: :: some %% % %% % lem_tannot_opt {{ tex \ottnt{tannot}^? }} :: 'LEM_Typ_annot_' ::= %% % {{ com location-annotated optional type annotations }} %% % | tannot_opt_aux l :: :: aux %% % %% % lem_funcl :: 'LEM_FCL' ::= %% % {{ com Function clauses }} %% % {{ aux _ l }} %% % | id pat1 ... patn tannot_opt = exp :: :: Funcl %% % %% % lem_letbind :: 'LEM_LB_' ::= %% % {{ com Let bindings }} %% % {{ aux _ l }} %% % | pat tannot_opt = exp :: :: Let_val %% % {{ com Value bindings }} %% % | lem_funcl :: :: Let_fun %% % {{ com Function bindings }} %% % %% % %% % grammar %% % lem_val_def :: 'LEM_VD' ::= %% % {{ com Value definitions }} %% % {{ aux _ l }} %% % | let lem_letbind :: :: Let_def %% % {{ com Non-recursive value definitions }} %% % | let rec lem_funcl1 and ... and lem_funcln :: :: Let_rec %% % {{ com Recursive function definitions }} %% % %% % lem_val_spec :: 'LEM_VS' ::= %% % {{ com Value type specifications }} %% % {{ aux _ l }} %% % | val x_l : typschm :: :: Val_spec %%%%% C-ish style %%%%%%%%%% tannot_opt :: 'Typ_annot_opt_' ::= {{ com optional type annotation for functions}} {{ aux _ l }} % | :: :: none % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return | typquant typ :: :: some rec_opt :: 'Rec_' ::= {{ com optional recursive annotation for functions }} {{ aux _ l }} | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} effect_opt :: 'Effect_opt_' ::= {{ com optional effect annotation for functions }} {{ aux _ l }} | :: :: pure {{ com sugar for empty effect set }} | effectkw effect :: :: effect funcl :: 'FCL_' ::= {{ com function clause }} {{ aux _ annot }} {{ auxparam 'a }} | id pat = exp :: :: Funcl fundef :: 'FD_' ::= {{ com function definition}} {{ aux _ annot }} {{ auxparam 'a }} | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} % {{ com function definition }} % TODO note that the typ in the tannot_opt is the *result* type, not % the type of the whole function. The argument type comes from the % pattern in the funcl % TODO the above is ok for single functions, but not for mutually % recursive functions - the tannot_opt scopes over all the funcli, % which is ok for the typ_quant part but not for the typ part letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} | let typschm pat = exp :: :: val_explicit {{ com let, explicit type ([[pat]] must be total)}} % at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here | let pat = exp :: :: val_implicit {{ com let, implicit type ([[pat]] must be total)}} val_spec :: 'VS_' ::= {{ com value type specification }} {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec {{ com specify the type of an upcoming definition }} | val extern typschm id :: :: extern_no_rename {{ com specify the type of an external function }} | val extern typschm id = string :: :: extern_spec {{ com specify the type of a function from Lem }} %where the string must provide an explicit path to the required function but will not be checked default_spec :: 'DT_' ::= {{ com default kinding or typing assumption }} {{ aux _ l }} {{ auxparam 'a }} | default Order order :: :: order | default base_kind kid :: :: kind | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position % doesn't have a kind or type annotation, then we look through the % default regexps (in order from the beginning) and pick the first % assumption for which id matches the regexp, if there is one. % Otherwise we try to infer. Perhaps warn if there are multiple matches. % For example, we might often have default Type ['alphanum] scattered_def :: 'SD_' ::= {{ com scattered function and union type definitions }} {{ aux _ annot }} {{ auxparam 'a }} | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} | function clause funcl :: :: scattered_funcl {{ texlong }} {{ com scattered function definition clause }} | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} | union id member type_union :: :: scattered_unioncl {{ texlong }} {{ com scattered union definition member }} | end id :: :: scattered_end {{ texlong }} {{ com scattered definition end }} reg_id :: 'RI_' ::= {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id alias_spec :: 'AL_' ::= {{ com register alias expression forms }} %. Other than where noted, each id must refer to an unaliased register of type vector {{ aux _ annot }} {{ auxparam 'a }} | reg_id . id :: :: subreg | reg_id [ exp ] :: :: bit | reg_id [ exp '..' exp' ] :: :: slice | reg_id : reg_id' :: :: concat dec_spec :: 'DEC_' ::= {{ com register declarations }} {{ aux _ annot }} {{ auxparam 'a }} | register typ id :: :: reg | register alias id = alias_spec :: :: alias | register alias typ id = alias_spec :: :: typ_alias dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} | comment string :: :: comm {{ com generated unstructured comment }} | comment def :: :: comm_struct {{ com generated structured comment }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% def :: 'DEF_' ::= {{ com top-level definition }} {{ auxparam 'a }} | kind_def :: :: kind {{ com definition of named kind identifiers }} | type_def :: :: type {{ com type definition }} | fundef :: :: fundef {{ com function definition }} | letbind :: :: val {{ com value definition }} | val_spec :: :: spec {{ com top-level type constraint }} | default_spec :: :: default {{ com default kind and type assumptions }} | scattered_def :: :: scattered {{ com scattered function and type definition }} | dec_spec :: :: reg_dec {{ com register declaration }} | dec_comm :: I :: comm {{ com generated comments }} defs :: '' ::= {{ com definition sequence }} {{ auxparam 'a }} | def1 .. defn :: :: Defs terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} % | >= :: :: geq % % {{ tex \ensuremath{\geq} }} % {{ tex \ottsym{\textgreater=} }} % {{ com \texttt{>=} }} % | '<=' :: :: leq % % {{ tex \ensuremath{\leq} }} % {{ tex \ottsym{\textless=} }} % {{ com \texttt{<=} }} % | -> :: :: arrow % % {{ tex \ensuremath{\rightarrow} }} % {{ tex \ottsym{-\textgreater} }} % {{ com \texttt{->} }} | ==> :: :: Longrightarrow {{ tex \ensuremath{\Longrightarrow} }} {{ com \texttt{==>} }} % | <| :: :: startrec % {{ tex \ensuremath{\langle|} }} % {{ com \texttt{<|} }} % | |> :: :: endrec % {{ tex \ensuremath{|\rangle} }} % {{ com \texttt{|>} }} | inter :: :: inter {{ tex \ensuremath{\cap} }} | u+ :: :: uplus {{ tex \ensuremath{\uplus} }} | u- :: :: uminus {{ tex \ensuremath{\setminus} }} | NOTIN :: :: notin {{ tex \ensuremath{\not\in} }} | SUBSET :: :: subset {{ tex \ensuremath{\subset} }} | NOTEQ :: :: noteq {{ tex \ensuremath{\not=} }} | emptyset :: :: emptyset {{ tex \ensuremath{\emptyset} }} % | < :: :: lt % % {{ tex \ensuremath{\langle} }} % {{ tex \ottsym{<} }} % | > :: :: gt % % {{ tex \ensuremath{\rangle} }} % {{ tex \ottsym{>} }} | lt :: :: mathlt {{ tex < }} | gt :: :: mathgt {{ tex > }} | ~= :: :: alphaeq {{ tex \ensuremath{\approx} }} | ~< :: :: consist {{ tex \ensuremath{\precapprox} }} | |- :: :: vdash {{ tex \ensuremath{\vdash} }} | |-t :: :: vdashT {{ tex \ensuremath{\vdash_t} }} | |-n :: :: vdashN {{ tex \ensuremath{\vdash_n} }} | |-e :: :: vdashE {{ tex \ensuremath{\vdash_e} }} | |-o :: :: vdashO {{ tex \ensuremath{\vdash_o} }} | |-c :: :: vdashC {{ tex \ensuremath{\vdash_c} }} | ' :: :: quote {{ tex \ottsym{'} }} | |-> :: :: mapsto {{ tex \ensuremath{\mapsto} }} | gives :: :: gives {{ tex \ensuremath{\triangleright} }} | ~> :: :: leadsto {{ tex \ensuremath{\leadsto} }} | select :: :: select {{ tex \ensuremath{\sigma} }} | => :: :: Rightarrow {{ tex \ensuremath{\Rightarrow} }} | -- :: :: dashdash {{ tex \mbox{--} }} | effectkw :: :: effectkw {{ tex \ottkw{effect} }} | empty :: :: empty {{ tex \ensuremath{\epsilon} }} | consistent_increase :: :: ci {{ tex \ottkw{consistent\_increase}~ }} | consistent_decrease :: :: cd {{ tex \ottkw{consistent\_decrease}~ }} | == :: :: equiv {{ tex \equiv }} % | [| :: :: range_start % {{ tex \mbox{$\ottsym{[\textbar}$} }} % | |] :: :: range_end % {{ tex \mbox{$\ottsym{\textbar]}$} }} % | [|| :: :: list_start % {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} % | ||] :: :: list_end % {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }}