indexvar n , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} metavar num , zero ::= {{ phantom }} {{ lex numeric }} {{ ocaml int }} {{ hol num }} {{ lem num }} {{ com Numeric literals }} 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 text = string type l = Parse_ast.l type 'a annot = l * 'a }} embed {{ lem 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 }} metavar x , y , z ::= {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com identifier }} {{ ocamlvar "[[x]]" }} {{ lemvar "[[x]]" }} metavar ix ::= {{ lex alphanum }} {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com infix identifier }} {{ ocamlvar "[[ix]]" }} {{ lemvar "[[ix]]" }} grammar l :: '' ::= {{ phantom }} {{ ocaml l }} {{ lem l }} {{ hol unit }} {{ com Source location }} | :: :: Unknown {{ ocaml Unknown }} {{ lem Unknown }} {{ hol () }} annot :: '' ::= {{ phantom }} {{ ocaml 'a annot }} {{ lem annot }} {{ hol unit }} id :: '' ::= {{ com Identifier }} {{ aux _ l }} | x :: :: id | ( x ) :: :: deIid {{ com remove infix status }} % 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. | bool :: M :: bool {{ com Built in type identifiers }} {{ ichlo bool_id }} | bit :: M :: bit {{ ichlo bit_id }} | unit :: M :: unit {{ ichlo unit_id }} | nat :: M :: nat {{ ichlo nat_id }} | string :: M :: string {{ ichlo string_id }} | enum :: M :: enum {{ ichlo enum_id }} | vector :: M :: vector {{ ichlo vector_id }} | list :: M :: list {{ ichlo list_id }} | set :: M :: set {{ ichlo set_id }} | reg :: M :: reg {{ ichlo reg_id }} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kinds and Types % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar % a :: 'A_' ::= % {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} % {{ com Type variables }} % | ' x :: :: A % {{ ichlo [[x]] }} % % N :: 'N_' ::= % {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} % {{ com numeric variables }} % | ' ' x :: :: N % {{ ichlo [[x]] }} % % EN :: 'EN_' ::= % {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} % {{ com endianness variables }} % | ' ' ' x :: :: EN % {{ ichlo [[x]] }} % % EFF :: 'EFF_' ::= % {{ aux _ l }} % {{ ocaml terminal * text }} % {{ lem terminal * string }} % {{ hol string }} % {{ com effect set variables }} % | ' ' ' ' x :: :: EFF % {{ ichlo [[x]] }} % % TODO: better concrete syntax!!!! % % % tnvar :: '' ::= % {{ com variables of the base kinds }} % | a :: :: Av % | N :: :: Nv % | EN :: :: ENv % | EFF :: :: EFFv % % tnvars :: '' ::= {{ phantom }} % {{ hol tnvar list }} % {{ ocaml tnvar list }} % {{ lem list tnvar }} % {{ com Type variable lists }} % | tnvar1 .. tnvarn :: :: Tvars % {{ hol [[tnvar1..tnvarn]] }} % {{ ocaml [[tnvar1..tnvarn]] }} % {{ lem [[tnvar1..tnvarn]] }} % % % ids :: '' ::= {{ phantom }} % {{ hol id list }} % {{ ocaml id list }} % {{ lem list id }} % {{ com Type variable lists }} % | id1 .. idn :: :: Tvars % {{ hol [[id1..idn]] }} % {{ ocaml [[id1..idn]] }} % {{ lem [[id1..idn]] }} 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 }} | Effects :: :: effects {{ com kind of effect sets }} kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} {{ aux _ l }} | id :: :: id {{ com identifier }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} %{{ com must be linear after normalisation... except for the type of *, ahem }} | nexp1 + nexp2 :: :: sum {{ com sum }} | 2 ** nexp :: :: exp {{ com exponential }} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} | id :: :: id {{ com identifier }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ ichlo [[order]] }} efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} | wmem :: :: wmem {{ com write memory }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} | effect id :: :: var | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }} % 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 :: :: var {{ com Type variable }} | typ1 -> typ2 effects :: :: fn {{ com Function type (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 type }} % 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]] }} typ_arg :: 'Typ_arg_' ::= {{ com Type constructor arguments of all kinds }} {{ aux _ l }} | nexp :: :: nexp | typ :: :: typ | order :: :: order | effects :: :: effects % 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 | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} | [ nexp : nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % 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 ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }} | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} % ...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 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 nexp_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le | id '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 }} | id :: :: none {{ com identifier }} | kind id :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} {{ aux _ l }} | kinded_id :: :: id {{ com An optionally kinded identifier }} | nexp_constraint :: :: const {{ com A constraint for this type }} 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 sugar, omitting quantifier and constraints }} 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 }} %% naming_scheme_opt :: 'Name_sect_' ::= {{ com Optional variable-naming-scheme specification for variables of defined type }} {{ 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 naming_scheme_opt = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} | typedef id naming_scheme_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 naming_scheme_opt = const union typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: variant {{ com union type definition}} {{ texlong }} | typedef id naming_scheme_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 }} % also sugar [ nexp ] 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? | undefined :: :: undef {{ com constant representing undefined values }} | string :: :: string {{ com string 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 % XXX < > are necessary to make the grammar non ambiguous | ( < 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 }} % | id '+' num :: :: num_add % {{ com constant addition 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar exp :: 'E_' ::= {{ com Expression }} {{ aux _ annot }} {{ auxparam 'a }} | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) | id :: :: id {{ com identifier }} | lit :: :: lit {{ com literal constant }} | ( typ ) exp :: :: cast {{ com cast }} | exp exp1 ... expn :: :: app {{ com function application }} % Note: fully applied function application only % We might restrict exp to be an identifier % We might require expn to have outermost parentheses (but not two sets if it's a tuple) | 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 exp4 :: :: for {{ com loop }} | foreach id from exp1 to exp2 exp3 :: S :: forbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }} | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 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 ] :: :: 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? % 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 }} | ( exp ) :: S :: paren {{ ichlo [[exp]] }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} | id exp :: :: memory {{ com memory write via function call }} | 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 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 _ annot }} {{ auxparam 'a }} % | :: :: 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 }} effects_opt :: 'Effects_opt_' ::= {{ com Optional effect annotation for functions }} {{ aux _ annot }} {{ auxparam 'a }} | :: :: pure {{ com sugar for empty effect set }} | effects :: :: effects 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 effects_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 }} | typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} | let pat = exp :: :: val_implicit {{ com value binding, implicit type ([[pat]] must be total)}} val_spec :: 'VS_' ::= {{ com Value type specification }} {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ annot }} {{ auxparam 'a }} | default base_kind id :: :: 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] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% def :: 'DEF_' ::= {{ com Top-level definition }} {{ aux _ annot }} {{ auxparam 'a }} | 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_typing_spec :: :: default {{ com default kind and type assumptions }} | register typ id :: :: reg_dec {{ com register declaration }} | scattered function rec_opt tannot_opt effects_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} | function clause funcl :: :: scattered_funcl {{ com scattered function definition clause }} | scattered typedef id naming_scheme_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} | union id member typ id' :: :: scattered_unioncl {{ com scattered union definition member }} | end id :: :: scattered_end {{ com scattered definition end }} defs :: '' ::= {{ com Definition sequence }} {{ auxparam 'a }} | def1 .. defn :: :: Defs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Machinery for typing rules % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grammar %% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }} %% %% {{ hol (a # t) list }} %% %% {{ lem list (tnvar * t) }} %% %% {{ com Type variable substitutions }} %% %% | { tnvar1 |-> t1 .. tnvarn |-> tn } :: :: T_subst %% %% {{ ocaml (assert false) }} %% %% {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }} %% %% {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }} %% %% k :: 'Ki_' ::= {{ com Internal kinds }} | K_Typ :: :: typ | K_Nat :: :: nat | K_Ord :: :: ord | K_Efct :: :: efct | K_Val :: :: val {{ com Representing values, for use in identifier checks }} | K_Lam ( k0 .. kn -> k' ) :: :: ctor | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} t , u :: 'T_' ::= {{ phantom }} {{ com Internal types }} | id :: :: var | t1 -> t2 effects :: :: fn | t1 * .... * tn :: :: tup | id t_args :: :: app %% %% | t_subst ( t ) :: M :: subst_app %% %% {{ com Multiple substitutions }} %% %% {{ ocaml (assert false) }} %% %% {{ hol (t_subst_t [[t_subst]] [[t]]) }} %% %% {{ lem (t_subst_t [[t_subst]] [[t]]) }} %% %% | t_subst ( tnv ) :: M :: var_subst_app %% %% {{ com Single variable substitution }} %% %% {{ ocaml (assert false) }} %% %% {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }} %% %% {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }} %% %% | curry ( t_multi , t ) :: M :: multifn %% %% {{ com Curried, multiple argument functions }} %% %% {{ ocaml (assert false) }} %% %% {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }} %% %% {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }} %% %% ne :: 'Ne_' ::= {{ com internal numeric expressions }} | id :: :: var | num :: :: const | ne1 * ne2 :: :: mult | ne1 + ne2 :: :: add | 2 ** ne :: :: exp | ( - ne ) :: :: unary %% %% | ne1 + ... + nen :: M :: addmany %% %% {{ ocaml (assert false) }} %% %% {{ hol ARB }} %% %% {{ lem (sumation_nes [[ne1...nen]]) }} | bitlength ( bin ) :: M :: cbin {{ ocaml (asssert false) }} {{ hol ARB }} {{ lem (blength [[bin]]) }} | bitlength ( hex ) :: M :: chex {{ ocaml (assert false) }} {{ hol ARB }} {{ lem (hlength [[hex]]) }} %% %% | 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 :: '' ::= {{ phantom }} {{ com Argument to type constructors }} | t :: :: typ | ne :: :: nexp | effects :: :: effect | order :: :: order t_args :: '' ::= {{ phantom }} {{ com Arguments to type constructors }} | t_arg1 ... t_argn :: :: T_args %% %% nec :: '' ::= %% %% {{ com Numeric expression constraints }} %% %% | ne < nec :: :: lessthan %% %% | ne = nec :: :: eq %% %% | ne <= nec :: :: lteq %% %% | ne :: :: base %% %% %% %% parsing %% %% T_fn right T_fn %% %% T_tup <= T_multi %% %% %% %% embed %% %% {{ lem %% %% %% %% val t_subst_t : list (tnv * t) -> t -> t %% %% val t_subst_tnv : list (tnv * t) -> tnv -> t %% %% val ftv_t : t -> list tnv %% %% val ftv_tm : list t -> list tnv %% %% val ftv_s : list (p*tnv) -> list tnv %% %% val compatible_overlap : list (x*t) -> bool %% %% %% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*) %% %% let normalize n = n %% %% %% %% let blength (_,bit) = Ne_const 8 %% %% let hlength (_,bit) = Ne_const 8 %% %% %% %% let rec sumation_nes nes = match nes with %% %% | [ a; b] -> Ne_add a b %% %% | x :: y -> Ne_add x (sumation_nes y) %% %% end %% %% %% %% }} %% %% %% %% grammar %% %% %% %% %% %% names :: '' ::= {{ phantom }} %% %% {{ hol x set }} %% %% {{ lem set x }} %% %% {{ ocaml Set.Make(String).t }} %% %% {{ com Sets of names }} %% %% | { x1 , .. , xn } :: :: Names %% %% {{ hol (LIST_TO_SET [[x1..xn]]) }} %% %% {{ lem (set_from_list [[x1..xn]]) }} %% %% %% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::= %% %% {{ hol (p#tnv) list }} %% %% {{ lem list (p*tnv) }} %% %% % {{ com Typeclass constraint lists }} %% %% % | ( p1 tnv1 ) .. ( pn tnvn ) :: :: SemC_concrete %% %% % {{ hol ([[p1 tnv1..pn tnvn]]) }} %% %% % {{ lem ([[p1 tnv1..pn tnvn]]) }} %% %% %% %% env_tag :: '' ::= %% %% {{ com Tags for the (non-constructor) value descriptions }} %% %% % | method :: :: method %% %% % {{ com Bound to a method }} %% %% | val :: :: spec %% %% {{ com Specified with val }} %% %% | let :: :: def %% %% {{ com Defined with let or indreln }} %% %% %% %% v_desc :: 'V_' ::= %% %% {{ com Value descriptions }} %% %% | < forall tnvs . t_multi -> p , ( x of names ) > :: :: constr %% %% {{ com Constructors }} %% %% | < forall tnvs . semC => t , env_tag > :: :: val %% %% {{ com Values }} %% %% %% %% f_desc :: 'F_' ::= %% %% | < forall tnvs . p -> t , ( x of names ) > :: :: field %% %% {{ com Fields }} %% %% %% %% embed %% %% {{ hol %% %% load "fmaptreeTheory"; %% %% val _ = %% %% Hol_datatype %% %% `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`; %% %% %% %% val _ = Define ` %% %% env_union e1 e2 = %% %% let i1 = item e1 in %% %% let m1 = map e1 in %% %% let i2 = item e2 in %% %% let m2 = map e2 in %% %% FTNode <| env_p:=FUNION i1.env_p i2.env_p; %% %% env_f:=FUNION i1.env_f i2.env_f; %% %% env_v:=FUNION i1.env_v i2.env_v |> %% %% (FUNION m1 m2)`; %% %% }} %% %% {{ lem %% %% type env = %% %% | EnvEmp %% %% | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc) %% %% %% %% val env_union : env -> env -> env %% %% let env_union e1 e2 = %% %% match (e1,e2) with %% %% | (EnvEmp,e2) -> e2 %% %% | (e1,EnvEmp) -> e1 %% %% | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) -> %% %% Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2) %% %% end %% %% %% %% }} %% %% %% %% grammar %% %% %% %% xs :: '' ::= {{ phantom }} %% %% {{ hol string list }} %% %% {{ lem list string }} %% %% | x1 .. xn :: :: Xs %% %% {{ hol [[x1..xn]] }} %% %% {{ lem [[x1..xn]] }} %% %% %% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }} %% %% {{ hol nec list }} %% %% {{ lem list nec }} %% %% {{ com nexp constraint lists }} %% %% | { nec1 , .. , necn } :: :: Sn_concrete %% %% {{ hol [[nec1 .. necn]] }} %% %% {{ lem [[nec1 .. necn]] }} %% %% | S_N1 union .. union S_Nn :: M :: SN_union %% %% {{ hol (FLAT [[S_N1..S_Nn]]) }} %% %% {{ lem (List.flatten [[S_N1..S_Nn]]) }} %% %% {{ ocaml assert false }} %% %% %% %% E :: '' ::= {{ phantom }} {{ hol ((string,env_body) fmaptree) }} {{ lem env }} {{ com Environments }} | < E_t , E_k > :: :: E {{ hol arb }} {{ lem (Env [[E_k]] [[E_t]]) }} | E1 u+ E2 :: M :: E_union {{ hol (env_union [[E1]] [[E2]]) }} {{ lem (env_union [[E1]] [[E2]]) }} {{ ocaml assert false }} | empty :: M :: E_empty {{ hol arb }} {{ lem EnvEmp }} {{ ocaml assert false }} E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::= {{ phantom }} {{ hol (id-> k) }} {{ lem map id k }} {{ com Kind environments }} | { id1 |-> k1 , .. , idn |-> kn } :: :: concrete {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 k1 .. idn kn]]) }} {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 k1 .. idn kn]] Pmap.empty) }} | E_k1 u+ .. u+ E_kn :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }} {{ ocaml (assert false) }} E_t {{ tex \ottnt{E}^{\textsc{t} } }} :: 'E_t_' ::= {{ phantom }} {{ hol (id |-> t) }} {{ lem map x f_desc }} {{ com Type environments }} | { id1 |-> t1 , .. , idn |-> tn } :: :: concrete {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 t1 .. idn tn]]) }} {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 t1 .. idn tn]] Pmap.empty) }} | E_t1 u+ .. u+ E_tn :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_t1..E_tn]]) }} {{ lem (List.fold_right union_map [[E_t1..E_tn]] Pmap.empty) }} {{ ocaml (assert false) }} %% %% tc_abbrev :: 'Tc_abbrev_' ::= {{ phantom }} %% %% {{ hol t option }} %% %% {{ lem option t }} %% %% {{ ocaml t option }} %% %% {{ com Type abbreviations }} %% %% | . t :: :: some %% %% {{ hol (SOME [[t]]) }} %% %% {{ lem (Some [[t]]) }} %% %% | :: :: none %% %% {{ hol NONE }} %% %% {{ lem None }} %% %% %% %% tc_def :: '' ::= %% %% {{ com Type and class constructor definitions }} %% %% | tnvs tc_abbrev :: :: Tc_def %% %% {{ com Type constructors }} %% %% %% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::= {{ phantom }} %% %% {{ hol p |-> tc_def }} %% %% {{ lem map p tc_def }} %% %% {{ com Type constructor definitions }} %% %% | { p1 |-> tc_def1 , .. , pn |-> tc_defn } :: :: concrete %% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }} %% %% {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} %% %% {{ ocaml (assert false) }} %% %% | TD1 u+ TD2 :: M :: union %% %% {{ hol (FUNION [[TD1]] [[TD2]]) }} %% %% {{ lem (union_map [[TD1]] [[TD2]]) }} %% %% {{ ocaml (assert false) }} %% %% %% %% %% %% %% %% D :: 'D_' ::= {{ phantom }} %% %% {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }} %% %% {{ lem tdefs}} %% %% {{ com Global type definition store }} %% %% | < TD , TC , I > :: :: concrete %% %% {{ hol ([[TD]], [[TC]], [[I]]) }} %% %% {{ lem (D [[TD]] [[TC]] [[I]]) }} %% %% | D1 u+ D2 :: M :: union %% %% {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }} %% %% {{ lem (union_tcdefs [[D1]] [[D2]]) }} %% %% {{ ocaml (assert false) }} %% %% | empty :: M :: empty %% %% {{ hol (FEMPTY, FEMPTY, []) }} %% %% {{ lem DEmp }} %% %% {{ ocaml assert false }} %% %% %% %% parsing %% %% E_union left E_union %% %% %% %% embed %% %% {{ lem %% %% type tdefs = %% %% | DEmp %% %% | D of (map p tc_def) * (map p (list x)) * (set inst) %% %% %% %% val union_tcdefs : tdefs -> tdefs -> tdefs %% %% %% %% }} grammar terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} | >= :: :: geq {{ tex \ensuremath{\geq} }} {{ com \texttt{>=} }} | '<=' :: :: leq {{ tex \ensuremath{\leq} }} {{ com \texttt{<=} }} | -> :: :: arrow {{ tex \ensuremath{\rightarrow} }} {{ 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} }} % | union :: :: union % {{ tex \ensuremath{\cup} }} | u+ :: :: uplus {{ tex \ensuremath{\uplus} }} | 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} }} | > :: :: gt {{ tex \ensuremath{\rangle} }} | |- :: :: 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} }} | ' :: :: quote {{ tex \mbox{'} }} | |-> :: :: mapsto {{ tex \ensuremath{\mapsto} }} | gives :: :: gives {{ tex \ensuremath{\triangleright} }} | ~> :: :: leadsto {{ tex \ensuremath{\leadsto} }} | => :: :: Rightarrow {{ tex \ensuremath{\Rightarrow} }} | -- :: :: dashdash {{ tex \mbox{--} }} | empty :: :: empty {{ tex \ensuremath{\epsilon} }} formula :: formula_ ::= | judgement :: :: judgement | formula1 .. formulan :: :: dots | E_k ( id ) gives k :: :: lookup_k {{ com Kind lookup }} {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }} {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }} | E_t ( id ) gives t :: :: lookup_t {{ com Type lookup }} {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }} {{ lem Pmap.find [[id]] [[E_t]] = [[t]] }} | E_k ( id ) <-| k :: :: update_k {{ com Update the kind associated with id to k }} %% %% % | TD ( p ) gives tc_def :: :: lookup_tc %% %% % {{ com Type constructor lookup }} %% %% % {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }} %% %% % {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} %% %% %% %% | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset :: :: E_m_disjoint %% %% {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }} %% %% {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]]) }} | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }} {{ lem disjoint_all (List.map Pmap.domain [[E_t1 .... E_tn]]) }} {{ com Pairwise disjoint domains }} %% %% %% %% | compatible overlap ( x1 |-> t1 , .. , xn |-> tn ) :: :: E_l_compat %% %% {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m = FST __n) ==> (SND __m = SND __n)) }} %% %% {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} %% %% {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }} %% %% %% %% | duplicates ( tnvs ) = emptyset :: :: no_dups_tnvs %% %% {{ hol (ALL_DISTINCT [[tnvs]]) }} %% %% {{ lem (duplicates [[tnvs]]) = [ ] }} %% %% %% %% | duplicates ( x1 , .. , xn ) = emptyset :: :: no_dups %% %% {{ hol (ALL_DISTINCT [[x1..xn]]) }} %% %% {{ lem (duplicates [[x1..xn]]) = [ ] }} | id NOTIN dom ( E_k ) :: :: notin_dom_k {{ hol ([[id]] NOTIN FDOM [[E_k]]) }} {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }} | id NOTIN dom ( E_t ) :: :: notin_dom_t {{ hol ([[id]] NOTIN FDOM [[E_t]]) }} {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }} %% %% %% %% %% %% | FV ( t ) SUBSET tnvs :: :: FV_t %% %% {{ com Free type variables }} %% %% {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }} %% %% {{ lem subst (ftv_t [[t]]) [[tnvs]] }} %% %% %% %% | FV ( t_multi ) SUBSET tnvs :: :: FV_t_multi %% %% {{ com Free type variables }} %% %% {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }} %% %% {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]] }} %% %% %% %% | FV ( semC ) SUBSET tnvs :: :: FV_semC %% %% {{ com Free type variables }} %% %% {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }} %% %% {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} %% %% %% %% | inst 'IN' I :: :: inst_in %% %% {{ hol (MEM [[inst]] [[I]]) }} %% %% {{ lem ([[inst]] IN [[I]]) }} %% %% %% %% | ( p t ) NOTIN I :: :: notin_I %% %% {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }} %% %% {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }} %% %% | E_k1 = E_k2 :: :: E_k_eqn {{ ichl ([[E_k1]] = [[E_k2]]) }} | E_t1 = E_t2 :: :: E_f_eqn {{ ichl ([[E_t1]] = [[E_t2]]) }} | E1 = E2 :: :: E_eqn {{ ichl ([[E1]] = [[E2]]) }} %% %% | TD1 = TD2 :: :: TD_eqn %% %% {{ ichl ([[TD1]] = [[TD2]]) }} %% %% %% %% | TC1 = TC2 :: :: TC_eqn %% %% {{ ichl ([[TC1]] = [[TC2]]) }} %% %% %% %% | I1 = I2 :: :: I_eqn %% %% {{ ichl ([[I1]] = [[I2]]) }} %% %% %% %% | names1 = names2 :: :: names_eq %% %% {{ ichl ([[names1]] = [[names2]]) }} %% %% | t1 = t2 :: :: t_eq {{ ichl ([[t1]] = [[t2]]) }} | ne1 = ne2 :: :: ne_eq {{ ichl ([[ne1]] = [[ne2]]) }} %% %% %% %% | t_subst1 = t_subst2 :: :: t_subst_eq %% %% {{ ichl ([[t_subst1]] = [[t_subst2]]) }} %% %% %% %% | p1 = p2 :: :: p_eq %% %% {{ ichl ([[p1]] = [[p2]]) }} %% %% %% %% | xs1 = xs2 :: :: xs_eq %% %% {{ ichl ([[xs1]] = [[xs2]]) }} %% %% %% %% | tnvs1 = tnvs2 :: :: tnvs_eq %% %% {{ ichl ([[tnvs1]] = [[tnvs2]]) }} % Substitutions and freevars are not correctly generated for the OCaml ast.ml %substitutions %multiple t a :: t_subst % %freevars %t a :: ftv