diff options
Diffstat (limited to 'language/l2_parse2.ott')
| -rw-r--r-- | language/l2_parse2.ott | 1424 |
1 files changed, 1424 insertions, 0 deletions
diff --git a/language/l2_parse2.ott b/language/l2_parse2.ott new file mode 100644 index 00000000..0f8dc8e7 --- /dev/null +++ b/language/l2_parse2.ott @@ -0,0 +1,1424 @@ +indexvar n , i , j , k ::= + {{ phantom }} + {{ com Index variables for meta-lists }} + +metavar num ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml int }} + {{ hol num }} + {{ lem integer }} + {{ com Numeric literals }} + {{ ocamllex ['0'-'9']+ }} + +metavar hex ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} +{{ ocamllex '0''x'['0'-'9' 'A' - 'F' 'a'-'f' '_']+ }} + {{ com Bit vector literal, specified by C-style hex number }} + +metavar bin ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} +{{ ocamllex '\'' ['0' '1' ' ']* '\'' }} + {{ com Bit vector literal, specified by C-style binary number }} + +metavar string ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ ocamllex "a" }} {{ phantom }} + {{ com String literals }} + +metavar regexp ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ ocamllex "a" }} {{ phantom }} + {{ com Regular expresions, as a string literal }} + +embed +{{ ocaml + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +}} + +embed +{{ lem +open import Map +open import Maybe +open import Pervasives + +type l = + | Unknown + | Trans of string * maybe l + | Range of nat * nat + +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 string }} + {{ lem string }} + {{ hol string }} + {{ com identifier }} + {{ ocamlvar "[[x]]" }} + {{ lemvar "[[x]]" }} + {{ ocamllex "a" }} {{ phantom }} + +metavar ix ::= + {{ lex alphanum }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com infix identifier }} + {{ ocamlvar "[[ix]]" }} + {{ lemvar "[[ix]]" }} + {{ ocamllex "a" }} {{ phantom }} + + +grammar + +l :: '' ::= {{ phantom }} + {{ ocaml l }} + {{ lem l }} + {{ hol unit }} + {{ com Source location }} + | :: :: Unknown + {{ ocaml Unknown }} + {{ lem Unknown }} + {{ hol () }} + + +id :: '' ::= + {{ com Identifier }} + {{ aux _ l }} + | x :: :: id + | op x :: :: deIid {{ com remove infix status }} + + +kid :: '' ::= + {{ com identifiers with kind, ticked to differntiate from program variables }} + {{ aux _ l }} + | ' x :: :: var + +% 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. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% 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 + +base_effect :: 'BE_' ::= + {{ com effect }} + {{ aux _ l }} + | rreg :: :: rreg {{ com read register }} + | wreg :: :: wreg {{ com write register }} + | rmem :: :: rmem {{ com read memory }} + | wmem :: :: wmem {{ com write memory }} + | wmv :: :: wmv {{ com write memory value }} + | eamem :: :: eamem {{ com address for write signaled }} + | barr :: :: barr {{ com memory barrier }} + | depend :: :: depend {{ com dynmically dependent footprint }} + | undef :: :: undef {{ com undefined-instruction exception }} + | unspec :: :: unspec {{ com unspecified values }} + | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} + | escape :: :: escape + + + +atomic_typ :: 'ATyp_' ::= + {{ quotient-with atyp }} + | id :: :: id + | kid :: :: var + | num :: :: constant + | dec :: :: dec + | inc :: :: inc + | id ( atyp1 , ... , atypn ) :: :: app + | ( atyp ) :: S :: paren {{ ocaml [[atyp]] }} + | ( atyp1 , .... , atypn ) :: :: tup + | {| num_list |} :: S :: existential_set {{ ocaml + { let v = mk_kid "n" $startpos $endpos in + let atom_id = mk_id (Id "atom") $startpos $endpos in + let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in + mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, [[num_list]]), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } }} + | { kid_list . atyp } :: S :: existential_true {{ ocaml + { mk_typ (ATyp_exist ([[kid_list]], NC_aux (NC_true, loc $startpos $endpos), [[atyp]])) $startpos $endpos } }} + | { kid_list , nc . atyp } :: :: exist + | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} + | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} + + +atyp :: 'ATyp_' ::= + {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }} + {{ aux _ l }} + | atomic_typ :: S :: atomic {{ ocaml [[atomic_typ]] }} {{ quotient-remove }} + | atyp1 * atyp2 :: :: times {{ com product }} + | atyp1 + atyp2 :: :: sum {{ com sum }} + | atyp1 - atyp2 :: :: minus {{ com subtraction }} + | 2** atyp :: :: exp {{ com exponential }} + | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} + | atyp1 -> atyp2 effect atyp3 :: :: fn + {{ com Function type (first-order only in user code), last atyp is an 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 +% | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-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 atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }} +% probably some sugar for vector types, using [ ] similarly to enums: +% (but with .. not : in the former, to avoid confusion...) +% | atyp [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }} +% | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }} +% ...so bit [ nexp ] etc is just an instance of that +% | list atyp :: :: list {{ com list of [[atyp]] }} +% | set atyp :: :: set {{ com finite set of [[atyp]] }} +% | reg atyp :: :: reg {{ com mutable register components holding [[atyp]] }} +% "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 +% +% ATyp_tup <= ATyp_tup +% ATyp_fn right ATyp_fn +% ATyp_fn <= ATyp_tup + +grammar + +n_constraint :: 'NC_' ::= + {{ com constraint over kind $[[Nat]]$ }} + {{ aux _ l }} + | atyp = atyp' :: :: fixed + | atyp >= atyp' :: :: bounded_ge + | atyp '<=' atyp' :: :: 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 Either a kinded identifier or a nexp constraint for a typquant }} + {{ aux _ l }} + | kinded_id :: :: id {{ com An optionally kinded identifier }} + | n_constraint :: :: const {{ com A constraint for this type }} + +typquant :: 'TypQ_' ::= + {{ com type quantifiers and constraints}} + {{ aux _ l }} + | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }} + | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} + +typschm :: 'TypSchm_' ::= + {{ com type scheme }} + {{ aux _ l }} + | typquant atyp :: :: ts + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Type definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +grammar +%ctor_def :: 'CT_' ::= +% {{ com Datatype constructor definition clause }} +% {{ aux _ l }} +% | id : typschm :: :: ct +% but we could get away with disallowing constraints in typschm, we +% think - if it's useful to do that + + name_scm_opt :: 'Name_sect_' ::= + {{ com Optional variable-naming-scheme specification for variables of defined type }} + {{ aux _ l }} + | :: :: none + | [ name = regexp ] :: :: some + +type_union :: 'Tu_' ::= + {{ com Type union constructors }} + {{ aux _ l }} + | id :: :: id + | atyp id :: :: ty_id + +type_def :: 'TD_' ::= + {{ com Type definition body }} + {{ aux _ l }} + | typedef id name_scm_opt = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | typedef id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record + {{ com struct type definition }} {{ texlong }} + | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + {{ com union type definition}} {{ texlong }} + | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + + | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +:: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + +kind_def :: 'KD_' ::= + {{ com Definition body for elements of kind; many are shorthands for type\_defs }} + {{ aux _ l }} + | Def kind id name_scm_opt = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | Def kind id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record + {{ com struct type definition }} {{ texlong }} + | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + {{ com union type definition}} {{ texlong }} + | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + + | Def kind id = register bits [ atyp : atyp' ] { 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 }} + | undefined :: :: undef {{ com undefined value }} + | 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 _ l }} + | lit :: :: lit + {{ com literal constant pattern }} + | _ :: :: wild + {{ com wildcard }} + | ( pat as id ) :: :: as + {{ com named pattern }} + | ( atyp ) pat :: :: typ + {{ com typed pattern }} + + | id :: :: id + {{ com identifier }} + + | id ( pat1 , .. , patn ) :: :: app + {{ com union constructor pattern }} + + | { fpat1 ; ... ; fpatn semi_opt } :: :: record + {{ com struct pattern }} + + | [ pat1 , .. , patn ] :: :: vector + {{ com vector pattern }} + + | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed + {{ com vector pattern (with explicit indices) }} + + | 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]] }} + +fpat :: 'FP_' ::= + {{ com Field pattern }} + {{ aux _ l }} + | id = pat :: :: Fpat + +parsing +P_app <= P_app +P_app <= P_as + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Expressions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +grammar + +exp :: 'E_' ::= + {{ com Expression }} + {{ aux _ l }} + + | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} +% maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) + + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com block that can evaluate the contained expressions in any ordering }} + + | id :: :: id + {{ com identifier }} + + | lit :: :: lit + {{ com literal constant }} + + | ( atyp ) exp :: :: cast + {{ com cast }} + + + | id exp :: S :: tup_app {{ ichlo [[id]] ( [[exp]] ) }} {{ com No extra parens needed when exp is a tuple }} + | id ( exp1 , .. , expn ) :: :: app + {{ com function application }} +% 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 {{ icho [[ if exp1 then exp2 else unit ]] }} + + | foreach id from exp1 to exp2 by exp3 in atyp 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 {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} + | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }} + | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ icho [[ 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 + + | [ exp1 , ... , 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 exp1 ; .. ; expn } :: :: 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 }} + | letbind in exp :: :: let + {{ com let expression }} + + | exp := exp' :: :: assign + {{ com imperative assignment }} + + | sizeof atyp :: :: sizeof + | exit exp :: :: exit + | return exp :: :: return + | assert ( exp , exp' ) :: :: assert + + | ( exp ) :: S :: paren {{ ichlo [[exp]] }} + + +lexp :: 'LEXP_' ::= {{ com lvalue expression, can't occur out of the parser }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + {{ com identifier }} + | id ( exp1 , .. , expn ) :: :: mem + | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} + | 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 _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id = exp :: :: Fexp + +fexps :: 'FES_' ::= + {{ com Field-expression list }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | fexp1 ; ... ; fexpn semi_opt :: :: Fexps + +opt_default :: 'Def_val_' ::= + {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ aux _ l }} + | :: :: empty + | ; default = exp :: :: dec + +pexp :: 'Pat_' ::= + {{ com Pattern match }} + {{ aux _ l }} +% {{ 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 }} +% {{ aux _ annot }} {{ auxparam 'a }} + | :: :: none + | typquant atyp :: :: 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 }} +% {{ aux _ annot }} {{ auxparam 'a }} + | :: :: pure {{ com sugar for empty effect set }} + | effectkw atyp :: :: effect + +funcl :: 'FCL_' ::= + {{ com Function clause }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id pat = exp :: :: Funcl + + +fundef :: 'FD_' ::= + {{ com Function definition}} + {{ aux _ l }} +% {{ 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 _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | let 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 _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | val typschm id :: :: val_spec + | val extern typschm id :: :: extern_no_rename + | val extern typschm id = string :: :: extern_spec + +default_typing_spec :: 'DT_' ::= + {{ com Default kinding or typing assumption, and default order for literal vectors and vector shorthands }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | default base_kind kid :: :: kind + | default base_kind atyp :: :: order + | 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 Function and type union definitions that can be spread across + a file. Each one must end in $[[end id]]$ }} + {{ aux _ l }} + | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} + + | function clause funcl :: :: scattered_funcl +{{ 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 {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ com scattered definition end }} + +dec_spec :: 'DEC_' ::= + {{ com Register declarations }} + {{ aux _ l }} + | register atyp id :: :: reg + | register alias id = exp :: :: alias + | register alias atyp id = exp :: :: typ_alias + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Top-level definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +def :: 'DEF_' ::= + {{ com Top-level definition }} + | 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_typing_spec :: :: default + {{ com default kind and type assumptions }} + | scattered_def :: :: scattered + {{ com scattered definition }} + | dec_spec :: :: reg_dec + {{ com register declaration }} + +defs :: '' ::= + {{ com Definition sequence }} + | def1 .. defn :: :: Defs + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Machinery for typing rules % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%% %% +%% %% +%% %% grammar +%% %% +%% %% +%% %% p :: 'Path_' ::= +%% %% {{ com Unique paths }} +%% %% | x1 . .. xn . x :: :: def +%% %% | __list :: :: list +%% %% {{ tex \ottkw{\_\_list} }} +%% %% | __bool :: :: bool +%% %% {{ tex \ottkw{\_\_bool} }} +%% %% | __num :: :: num +%% %% {{ tex \ottkw{\_\_num} }} +%% %% | __set :: :: set +%% %% {{ tex \ottkw{\_\_set} }} +%% %% | __string :: :: string +%% %% {{ tex \ottkw{\_\_string} }} +%% %% | __unit :: :: unit +%% %% {{ tex \ottkw{\_\_unit} }} +%% %% | __bit :: :: bit +%% %% {{ tex \ottkw{\_\_bit} }} +%% %% | __vector :: :: vector +%% %% {{ tex \ottkw{\_\_vector} }} +%% %% %TODO morally, delete the above - but what are the __ things for? +%% %% % cleaner to declare early in the library? +%% %% +%% %% 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]]) }} +%% %% +%% %% t , u :: 'T_' ::= +%% %% {{ com Internal types }} +%% %% | a :: :: var +%% %% | t1 -> t2 :: :: fn +%% %% | t1 * .... * tn :: :: tup +%% %% | p t_args :: :: app +%% %% | ne :: :: len +%% %% | 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 }} +%% %% | N :: :: var +%% %% | nat :: :: const +%% %% | ne1 * ne2 :: :: mult +%% %% | ne1 + ne2 :: :: add +%% %% | ( - ne ) :: :: unary +%% %% | normalize ( ne ) :: M :: normalize +%% %% {{ ocaml (assert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (normalize [[ne]] ) }} +%% %% | 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_args :: '' ::= +%% %% {{ com Lists of types }} +%% %% | t1 .. tn :: :: T_args +%% %% | t_subst ( t_args ) :: M :: T_args_subst_app +%% %% {{ com Multiple substitutions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }} +%% %% {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }} +%% %% +%% %% t_multi :: '' ::= {{ phantom }} +%% %% {{ hol t list }} +%% %% {{ ocaml t list }} +%% %% {{ lem list t }} +%% %% {{ com Lists of types }} +%% %% | ( t1 * .. * tn ) :: :: T_multi +%% %% {{ hol [[t1..tn]] }} +%% %% {{ lem [[t1..tn]] }} +%% %% | t_subst ( t_multi ) :: M :: T_multi_subst_app +%% %% {{ com Multiple substitutions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }} +%% %% {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }} +%% %% +%% %% 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]] }} +%% %% +%% %% %TODO: no clue what the following are: +%% %% S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::= {{ phantom }} +%% %% {{ hol (p#t) list }} +%% %% {{ lem list (p*t) }} +%% %% {{ com Typeclass constraints }} +%% %% | { ( p1 t1 ) , .. , ( pn tn ) } :: :: S_concrete +%% %% {{ hol [[p1 t1 .. pn tn]] }} +%% %% {{ lem [[p1 t1 .. pn tn]] }} +%% %% | S_c1 union .. union S_cn :: M :: S_union +%% %% {{ hol (FLAT [[S_c1..S_cn]]) }} +%% %% {{ lem (List.flatten [[S_c1..S_cn]]) }} +%% %% {{ ocaml assert false }} +%% %% +%% %% 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) }} +%% %% +%% %% +%% %% %TODO: simplify by removing E_m throughout? And E_p?? +%% %% {{ lem env }} +%% %% {{ com Environments }} +%% %% | < E_m , E_p , E_f , E_x > :: :: E +%% %% {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }} +%% %% {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }} +%% %% | E1 u+ E2 :: M :: E_union +%% %% {{ hol (env_union [[E1]] [[E2]]) }} +%% %% {{ lem (env_union [[E1]] [[E2]]) }} +%% %% {{ ocaml assert false }} +%% %% | empty :: M :: E_empty +%% %% {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }} +%% %% {{ lem EnvEmp }} +%% %% {{ ocaml assert false }} +%% %% +%% %% E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::= {{ phantom }} +%% %% {{ hol (x|-> v_desc) }} +%% %% {{ lem map x v_desc }} +%% %% {{ com Value environments }} +%% %% | { x1 |-> v_desc1 , .. , xn |-> v_descn } :: :: concrete +%% %% {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }} +%% %% {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} +%% %% | E_x1 u+ .. u+ E_xn :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }} +%% %% {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::= {{ phantom }} +%% %% {{ hol (x |-> f_desc) }} +%% %% {{ lem map x f_desc }} +%% %% {{ com Field environments }} +%% %% | { x1 |-> f_desc1 , .. , xn |-> f_descn } :: :: concrete +%% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }} +%% %% {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} +%% %% | E_f1 u+ .. u+ E_fn :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }} +%% %% {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::= {{ phantom }} +%% %% {{ hol (string |-> (string,env_body) fmaptree) }} +%% %% {{ lem map x env }} +%% %% % {{ com Module environments }} +%% %% % | { x1 |-> E1 , .. , xn |-> En } :: :: concrete +%% %% % {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }} +%% %% % {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} +%% %% % +%% %% % _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::= {{ phantom }} +%% %% % {{ hol (x |-> p) }} +%% %% % {{ lem map x p }} +%% %% % {{ com Path environments }} +%% %% % | { x1 |-> p1 , .. , xn |-> pn } :: :: concrete +%% %% % {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }} +%% %% % {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} +%% %% % | E_p1 u+ .. u+ E_pn :: M :: union +%% %% % {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }} +%% %% % {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }} +%% %% % +%% %% % {{ ocaml (assert false) }} +%% %% E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::= {{ phantom }} +%% %% {{ hol (x |-> t) }} +%% %% {{ lem map x t }} +%% %% {{ com Lexical bindings }} +%% %% | { x1 |-> t1 , .. , xn |-> tn } :: :: concrete +%% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }} +%% %% {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} +%% %% | E_l1 u+ .. u+ E_ln :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }} +%% %% {{ lem (List.fold_right union_map [[E_l1..E_ln]] 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} }} + | ' :: :: 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} }} + | effectkw :: :: effectkw + {{ tex \ottkw{effect} }} + + +formula :: formula_ ::= + | judgement :: :: judgement + + | formula1 .. formulan :: :: dots + +% | E_m ( x ) gives E :: :: lookup_m +% {{ com Module lookup }} +% {{ hol (FLOOKUP [[E_m]] [[x]] = SOME [[E]]) }} +% {{ lem (Pmap.find [[x]] [[E_m]]) = [[E]] }} +% +% | E_p ( x ) gives p :: :: lookup_p +% {{ com Path lookup }} +% {{ hol (FLOOKUP [[E_p]] [[x]] = SOME [[p]]) }} +% {{ lem Pmap.find [[x]] [[E_p]] = [[p]] }} + +%% %% | E_f ( x ) gives f_desc :: :: lookup_f +%% %% {{ com Field lookup }} +%% %% {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} +%% %% +%% %% | E_x ( x ) gives v_desc :: :: lookup_v +%% %% {{ com Value lookup }} +%% %% {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} +%% %% +%% %% | E_l ( x ) gives t :: :: lookup_l +%% %% {{ com Lexical binding lookup }} +%% %% {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} +%% %% +%% %% % | 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]] }} +%% %% % +%% %% % | TC ( p ) gives xs :: :: lookup_class +%% %% % {{ com Type constructor lookup }} +%% %% % {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }} +%% %% % {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} +%% %% +%% %% | 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_x1 ) inter dom ( E_x2 ) = emptyset :: :: E_x_disjoint +%% %% {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }} +%% %% {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]]) }} +%% %% +%% %% | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset :: :: E_f_disjoint +%% %% {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} +%% %% {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} +%% %% +%% %% % | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset :: :: E_p_disjoint +%% %% % {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }} +%% %% % {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} +%% %% % +%% %% | disjoint doms ( E_l1 , .... , E_ln ) :: :: E_l_disjoint +%% %% {{ 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_l1....E_ln]] <> NONE) }} +%% %% {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }} +%% %% {{ com Pairwise disjoint domains }} +%% %% +%% %% | disjoint doms ( E_x1 , .... , E_xn ) :: :: 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_x1....E_xn]] <> NONE) }} +%% %% {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }} +%% %% {{ 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]]) = [ ] }} +%% %% +%% %% | x NOTIN dom ( E_l ) :: :: notin_dom_l +%% %% {{ hol ([[x]] NOTIN FDOM [[E_l]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} +%% %% +%% %% | x NOTIN dom ( E_x ) :: :: notin_dom_v +%% %% {{ hol ([[x]] NOTIN FDOM [[E_x]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} +%% %% +%% %% | x NOTIN dom ( E_f ) :: :: notin_dom_f +%% %% {{ hol ([[x]] NOTIN FDOM [[E_f]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} +%% %% +%% %% % | p NOTIN dom ( TC ) :: :: notin_dom_tc +%% %% % {{ hol ([[p]] NOTIN FDOM [[TC]]) }} +%% %% % {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} +%% %% +%% %% | p NOTIN dom ( TD ) :: :: notin_dom_td +%% %% {{ hol ([[p]] NOTIN FDOM [[TD]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} +%% %% +%% %% | 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_l1 = E_l2 :: :: E_l_eqn +%% %% {{ ichl ([[E_l1]] = [[E_l2]]) }} +%% %% +%% %% | E_x1 = E_x2 :: :: E_x_eqn +%% %% {{ ichl ([[E_x1]] = [[E_x2]]) }} +%% %% +%% %% | E_f1 = E_f2 :: :: E_f_eqn +%% %% {{ ichl ([[E_f1]] = [[E_f2]]) }} +%% %% +%% %% | 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]]) }} +%% %% +%% %% | 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]]) }} + |