diff options
| author | Kathy Gray | 2013-07-17 13:16:44 +0100 |
|---|---|---|
| committer | Kathy Gray | 2013-07-17 13:16:44 +0100 |
| commit | 80fd65368f2769a29ce657aaffef50f3c8f0455f (patch) | |
| tree | fd1d6c9d5040cbd9e55b445710db87c3ee6364f6 | |
| parent | ed9d7672cd04fbc60ef731996c51a748300dd8f6 (diff) | |
Separated ott file for parsable AST and parser changes
| -rw-r--r-- | language/Makefile | 8 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2597 | ||||
| -rw-r--r-- | src/parse_ast.ml | 441 | ||||
| -rw-r--r-- | src/parser.mly | 134 |
4 files changed, 3104 insertions, 76 deletions
diff --git a/language/Makefile b/language/Makefile index dcadaff2..2c3d2512 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,6 +1,6 @@ OTTLIB=$(dir $(shell which ott))../hol -all: l2.pdf +all: l2.pdf parse_ast.ml l2.pdf: l2.tex pdflatex l2.tex @@ -12,7 +12,11 @@ l2.tex ../src/ast.ml l2Script.sml: l2.ott ott -sort false -generate_aux_rules false -o l2.tex -picky_multiple_parses true l2.ott ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o ../src/ast.ml -o l2Script.sml -picky_multiple_parses true l2.ott - #rm -f ../src/ast.ml +parse_ast.ml ../src/parse_ast.ml: l2_parse.ott + ott -sort false -generate_aux_rules true -ocaml_include_terminals true -o ../src/parse_ast.ml -picky_multiple_parses true l2_parse.ott + + +# rm -f ../src/ast.ml # chmod a-w ../src/ast.ml l2.lem: l2.ott diff --git a/language/l2_parse.ott b/language/l2_parse.ott new file mode 100644 index 00000000..86f31122 --- /dev/null +++ b/language/l2_parse.ott @@ -0,0 +1,2597 @@ +indexvar n , i , j , k ::= + {{ phantom }} + {{ com Index variables for meta-lists }} + +metavar num ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml terminal * int }} + {{ hol num }} + {{ lem (terminal * num) }} + {{ com Numeric literals }} + +metavar hex ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml terminal * string }} + {{ lem (terminal * string) }} + {{ com Bit vector literal, specified by C-style hex number }} + +metavar bin ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml terminal * string }} + {{ lem (terminal * string) }} + {{ com Bit vector literal, specified by C-style binary number }} + +metavar string ::= + {{ phantom }} + {{ ocaml terminal * string }} + {{ lem (terminal * string) }} + {{ hol string }} + {{ com String literals }} + +metavar regexp ::= + {{ phantom }} + {{ ocaml terminal * string }} + {{ lem (terminal * string) }} + {{ hol string }} + {{ com Regular expresions, as a string literal }} + +embed +{{ ocaml + +type text = string + +type l = + | Unknown + | Trans of string * l option + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +type ml_comment = + | Chars of string + | Comment of ml_comment list + +type lex_skip = + | Com of ml_comment + | Ws of string + | Nl + +type lex_skips = lex_skip list option + +let pp_lex_skips ppf sk = + match sk with + | None -> () + | Some(sks) -> + List.iter + (fun sk -> + match sk with + | Com(ml_comment) -> + (* TODO: fix? *) + Format.fprintf ppf "(**)" + | Ws(r) -> + Format.fprintf ppf "%s" r (*(Ulib.Text.to_string r)*) + | Nl -> Format.fprintf ppf "\\n") + sks + +let combine_lex_skips s1 s2 = + match (s1,s2) with + | (None,_) -> s2 + | (_,None) -> s1 + | (Some(s1),Some(s2)) -> Some(s2@s1) + +type terminal = lex_skips + +}} + +embed +{{ lem +open Pmap +open Pervasives + +type l = + | Unknown + | Trans of string * option l + | Range of num * num + +type lex_skip = + | Com of string + | Ws of string + | Nl + +type lex_skips = option (list lex_skip) +type terminal = lex_skips + +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 terminal * text }} + {{ lem terminal * string }} + {{ hol string }} + {{ com identifier }} + {{ ocamlvar "[[x]]" }} + {{ lemvar "[[x]]" }} + +metavar ix ::= + {{ lex alphanum }} + {{ ocaml terminal * text }} + {{ lem terminal * 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. + + +%% +%% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::= +%% {{ com Location-annotated names }} +%% | x l :: :: X_l +%% | ( ix ) l :: :: PreX_l +%% {{ com Remove infix status }} +%% +%% ix_l {{ tex \ottnt{ix}^{l} }} :: '' ::= +%% {{ com Location-annotated infix names }} +%% | ix l :: :: SymX_l +%% | ` x ` l :: :: InX_l +%% {{ com Add infix status }} +%% +%% embed +%% {{ ocaml +%% let xl_to_l = function +%% | X_l(_,l) -> l +%% | PreX_l(_,_,_,l) -> l +%% +%% let ixl_to_l = function +%% | SymX_l(_,l) -> l +%% | InX_l(_,_,_,l) -> l +%% }} +%% {{ lem +%% +%% (*let xl_to_l = function +%% | X_l(_,l) -> l +%% | PreX_l(_,_,l) -> l +%% end +%% +%% let ixl_to_l = function +%% | SymX_l(_,l) -> l +%% | InX_l(_,_,_,l) -> l +%% end*) +%% +%% }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% 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 + +effect :: '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 }} + +atyp :: 'ATyp_' ::= + {{ com expression of all kinds }} + {{ aux _ l }} + | id :: :: id {{ com identifier }} + | num :: :: constant {{ com constant }} + | atyp1 * atyp2 :: :: times {{ com product }} +%{{ com must be linear after normalisation... except for the type of *, ahem }} + | atyp1 + atyp2 :: :: sum {{ com sum }} + | 2 ** atyp :: :: exp {{ com exponential }} + | ( atyp ) :: S :: paren {{ icho [[atyp]] }} + + | inc :: :: inc {{ com increasing (little-endian) }} + | dec :: :: dec {{ com decreasing (big-endian) }} + + | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} + +% 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}. + + | _ :: :: wild + {{ com Unspecified type }} + | atyp1 -> atyp2 atyp3 :: :: 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. + | atyp1 * .... * atypn :: :: 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 atyp1 .. atypn :: :: app + {{ com type constructor application }} + + +% 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...) + | atyp [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }} + | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} +% ...so bit [ nexp ] etc is just an instance of that + | list atyp :: :: list {{ com list of [[typ]] }} + | set atyp :: :: set {{ com finite set of [[typ]] }} + | reg atyp :: :: 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 + +ATyp_tup <= ATyp_tup +ATyp_fn right ATyp_fn +ATyp_fn <= ATyp_tup +%Typ_fn right Typ_app1 +%Typ_tup right Typ_app1 + +grammar + +nexp_constraint :: 'NC_' ::= + {{ com constraint over kind $[[Nat]]$ }} + {{ aux _ annot }} {{ auxparam 'a }} + | atyp = atyp' :: :: fixed + | atyp >= atyp' :: :: bounded_ge + | atyp '<=' atyp' :: :: 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 }} + | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} + +typquant :: 'TypQ_' ::= + {{ com type quantifiers and constraints}} + {{ aux _ annot }} {{ auxparam 'a }} + | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} + +% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE + + | forall kinded_id1 ... kinded_idn . :: :: no_constraint {{ com sugar, omitting constraints}} + | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} + +typschm :: 'TypSchm_' ::= + {{ com type scheme }} + {{ aux _ annot }} {{ auxparam 'a }} + | typquant atyp :: :: 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 : atyp1 ; ... ; idn : atypn 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 { atyp1 id1 ; ... ; atypn 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 { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: variant + {{ com union type definition}} {{ texlong }} + + | typedef id naming_scheme_opt = enum { 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 }} + | string :: :: string {{ com string constant }} + +semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} + {{ ocaml terminal * bool }} + {{ lem (terminal * 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 + | ( atyp 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 }} + +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 }} + + | ( atyp ) 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 }} + +% 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 }} + | 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 + | typ_quant 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 +%% %% +%% %% +%% %% 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} }} + + +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]]) }} + +% Substitutions and freevars are not correctly generated for the OCaml ast.ml +%substitutions +%multiple t a :: t_subst +% +%freevars +%t a :: ftv + +%% % +%% % +%% % defns +%% % convert_tnvars :: '' ::= +%% % +%% % defn +%% % tnvars ~> tnvs :: :: convert_tnvars :: convert_tnvars_ +%% % by +%% % +%% % :convert_tnvar: tnvar1 ~> tnv1 .. :convert_tnvar: tnvarn ~> tnvn +%% % ------------------------------------------------------------ :: none +%% % tnvar1 .. tnvarn ~> tnv1 .. tnvn +%% % +%% % defn +%% % tnvar ~> tnv :: :: convert_tnvar :: convert_tnvar_ +%% % by +%% % +%% % ----------------------------------------------------------- :: a +%% % a l ~> a +%% % +%% % ---------------------------------------------------------- :: N +%% % N l ~> N +%% % +%% % +%% % defns +%% % look_m :: '' ::= +%% % +%% % defn +%% % E1 ( x_l1 .. x_ln ) gives E2 :: :: look_m :: look_m_ +%% % {{ com Name path lookup }} +%% % by +%% % +%% % ------------------------------------------------------------ :: none +%% % E() gives E +%% % +%% % E_m(x) gives E1 +%% % E1(</y_li//i/>) gives E2 +%% % ------------------------------------------------------------ :: some +%% % <E_m,E_p,E_f,E_x>(x l </y_li//i/>) gives E2 +%% % +%% % defns +%% % look_m_id :: '' ::= +%% % +%% % defn +%% % E1 ( id ) gives E2 :: :: look_m_id :: look_m_id_ +%% % {{ com Module identifier lookup }} +%% % by +%% % +%% % E1(</y_li//i/> x l1) gives E2 +%% % ------------------------------------------------------------ :: all +%% % E1(</y_li.//i/> x l1 l2) gives E2 +%% % +%% % defns +%% % look_tc :: '' ::= +%% % +%% % defn +%% % E ( id ) gives p :: :: look_tc :: look_tc_ +%% % {{ com Path identifier lookup }} +%% % by +%% % +%% % E(</y_li//i/>) gives <E_m,E_p,E_f,E_x> +%% % E_p(x) gives p +%% % ------------------------------------------------------------ :: all +%% % E(</y_li.//i/> x l1 l2) gives p +%% % +%% % +%% % defns +%% % check_t :: '' ::= +%% % +%% % defn +%% % TD |- t ok :: :: check_t :: check_t_ +%% % {{ com Well-formed types }} +%% % by +%% % +%% % ------------------------------------------------------------ :: var +%% % TD |- a ok +%% % +%% % TD |- t1 ok +%% % TD |- t2 ok +%% % ------------------------------------------------------------ :: fn +%% % TD |- t1 -> t2 ok +%% % +%% % TD |- t1 ok .... TD |- tn ok +%% % ------------------------------------------------------------ :: tup +%% % TD |- t1 * .... * tn ok +%% % +%% % TD(p) gives tnv1..tnvn tc_abbrev +%% % TD,tnv1 |- t1 ok .. TD,tnvn |- tn ok +%% % ------------------------------------------------------------ :: app +%% % TD |- p t1 .. tn ok +%% % +%% % +%% % defn +%% % TD , tnv |- t ok :: :: check_tlen :: check_tlen_ +%% % {{ com Well-formed type/nexps matching the application type variable }} +%% % by +%% % +%% % TD |- t ok +%% % ------------------------------------------------------------ :: t +%% % TD,a |- t ok +%% % +%% % ------------------------------------------------------------ :: len +%% % TD,N |- ne ok +%% % +%% % %TODO type equality isn't right; neither is type conversion +%% % +%% % defns +%% % teq :: '' ::= +%% % +%% % defn +%% % TD |- t1 = t2 :: :: teq :: teq_ +%% % {{ com Type equality }} +%% % by +%% % +%% % TD |- t ok +%% % ------------------------------------------------------------ :: refl +%% % TD |- t = t +%% % +%% % TD |- t2 = t1 +%% % ------------------------------------------------------------ :: sym +%% % TD |- t1 = t2 +%% % +%% % TD |- t1 = t2 +%% % TD |- t2 = t3 +%% % ------------------------------------------------------------ :: trans +%% % TD |- t1 = t3 +%% % +%% % TD |- t1 = t3 +%% % TD |- t2 = t4 +%% % ------------------------------------------------------------ :: arrow +%% % TD |- t1 -> t2 = t3 -> t4 +%% % +%% % TD |- t1 = u1 .... TD |- tn = un +%% % ------------------------------------------------------------ :: tup +%% % TD |- t1*....*tn = u1*....*un +%% % +%% % TD(p) gives a1..an +%% % TD |- t1 = u1 .. TD |- tn = un +%% % ------------------------------------------------------------ :: app +%% % TD |- p t1 .. tn = p u1 .. un +%% % +%% % TD(p) gives a1..an . u +%% % ------------------------------------------------------------ :: expand +%% % TD |- p t1 .. tn = {a1|->t1..an|->tn}(u) +%% % +%% % ne = normalize (ne') +%% % ---------------------------------------------------------- :: nexp +%% % TD |- ne = ne' +%% % +%% % +%% % defns +%% % convert_typ :: '' ::= +%% % +%% % defn +%% % TD , E |- typ ~> t :: :: convert_typ :: convert_typ_ +%% % {{ com Convert source types to internal types }} +%% % by +%% % +%% % % TODO : Can't allow things like type t = _, but it's useful to have things +%% % % like f (x : (_, int)) = snd x +%% % %TD |- t ok +%% % %------------------------------------------------------------ :: wild +%% % %TD,E |- _ l ~> t +%% % +%% % ------------------------------------------------------------ :: var +%% % TD,E |- a l' l ~> a +%% % +%% % TD,E |- typ1 ~> t1 +%% % TD,E |- typ2 ~> t2 +%% % ------------------------------------------------------------ :: fn +%% % TD,E |- typ1->typ2 l ~> t1->t2 +%% % +%% % TD,E |- typ1 ~> t1 .... TD,E |- typn ~> tn +%% % ------------------------------------------------------------ :: tup +%% % TD,E |- typ1 * .... * typn l ~> t1 * .... * tn +%% % +%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn +%% % E(id) gives p +%% % TD(p) gives a1..an tc_abbrev +%% % ------------------------------------------------------------ :: app +%% % TD,E |- id typ1 .. typn l ~> p t1 .. tn +%% % +%% % |- nexp ~> ne +%% % ------------------------------------------------------------ :: nexp +%% % TD,E |- nexp ~> ne +%% % +%% % TD,E |- typ ~> t +%% % ------------------------------------------------------------ :: paren +%% % TD,E |- (typ) l ~> t +%% % +%% % +%% % TD,E |- typ ~> t1 +%% % TD |- t1 = t2 +%% % ------------------------------------------------------------ :: eq +%% % TD,E |- typ ~> t2 +%% % +%% % defn +%% % |- nexp ~> ne :: :: convert_nexp :: convert_nexp_ +%% % {{ com Convert and normalize numeric expressions }} +%% % by +%% % +%% % ------------------------------------------------------------ :: var +%% % |- N l ~> N +%% % +%% % ------------------------------------------------------------ :: num +%% % |- num l ~> nat +%% % +%% % |- nexp1 ~> ne1 +%% % |- nexp2 ~> ne2 +%% % ------------------------------------------------------------ :: mult +%% % |- nexp1 * nexp2 l ~> ne1 * ne2 +%% % +%% % |- nexp1 ~> ne1 +%% % |- nexp2 ~> ne2 +%% % ----------------------------------------------------------- :: add +%% % |- nexp1 + nexp2 l ~> :Ne_add: ne1 + ne2 +%% % +%% % defns +%% % convert_typs :: '' ::= +%% % +%% % defn +%% % TD , E |- typs ~> t_multi :: :: convert_typs :: convert_typs_ by +%% % +%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn +%% % ------------------------------------------------------------ :: all +%% % TD,E |- typ1 * .. * typn ~> (t1 * .. * tn) +%% % +%% % defns +%% % check_lit :: '' ::= +%% % +%% % defn +%% % |- lit : t :: :: check_lit :: check_lit_ +%% % {{ com Typing literal constants }} +%% % by +%% % +%% % ------------------------------------------------------------ :: true +%% % |- true l : __bool +%% % +%% % ------------------------------------------------------------ :: false +%% % |- false l : __bool +%% % +%% % ------------------------------------------------------------ :: num +%% % |- num l : __num +%% % +%% % nat = bitlength(hex) +%% % ------------------------------------------------------------ :: hex +%% % |- hex l : __vector nat __bit +%% % +%% % nat = bitlength(bin) +%% % ------------------------------------------------------------ :: bin +%% % |- bin l : __vector nat __bit +%% % +%% % ------------------------------------------------------------ :: string +%% % |- string l : __string +%% % +%% % ------------------------------------------------------------ :: unit +%% % |- () l : __unit +%% % +%% % ------------------------------------------------------------ :: bitzero +%% % |- bitzero l : __bit +%% % +%% % ------------------------------------------------------------ :: bitone +%% % |- bitone l : __bit +%% % +%% % +%% % defns +%% % inst_field :: '' ::= +%% % +%% % defn +%% % TD , E |- field id : p t_args -> t gives ( x of names ) :: :: inst_field :: inst_field_ +%% % {{ com Field typing (also returns canonical field names) }} +%% % by +%% % +%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> +%% % E_f(y) gives <forall tnv1..tnvn. p -> t, (z of names)> +%% % TD |- t1 ok .. TD |- tn ok +%% % ------------------------------------------------------------ :: all +%% % TD,E |- field </x_li.//i/> y l1 l2: p t1 .. tn -> {tnv1|->t1..tnvn|->tn}(t) gives (z of names) +%% % +%% % defns +%% % inst_ctor :: '' ::= +%% % +%% % defn +%% % TD , E |- ctor id : t_multi -> p t_args gives ( x of names ) :: :: inst_ctor :: inst_ctor_ +%% % {{ com Data constructor typing (also returns canonical constructor names) }} +%% % by +%% % +%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> +%% % E_x(y) gives <forall tnv1..tnvn. t_multi -> p, (z of names)> +%% % TD |- t1 ok .. TD |- tn ok +%% % ------------------------------------------------------------ :: all +%% % TD,E |- ctor </x_li.//i/> y l1 l2 : {tnv1|->t1..tnvn|->tn}(t_multi) -> p t1 .. tn gives (z of names) +%% % +%% % defns +%% % inst_val :: '' ::= +%% % +%% % defn +%% % TD , E |- val id : t gives S_c :: :: inst_val :: inst_val_ +%% % {{ com Typing top-level bindings, collecting typeclass constraints }} +%% % by +%% % +%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x> +%% % E_x(y) gives <forall tnv1..tnvn. (p1 tnv'1) .. (pi tnv'i) => t,env_tag> +%% % TD |- t1 ok .. TD |- tn ok +%% % t_subst = {tnv1|->t1..tnvn|->tn} +%% % ------------------------------------------------------------ :: all +%% % TD, E |- val </x_li.//i/> y l1 l2 : t_subst(t) gives {(p1 t_subst(tnv'1)), .. , (pi t_subst(tnv'i))} +%% % +%% % defns +%% % not_ctor :: '' ::= +%% % +%% % defn +%% % E , E_l |- x not ctor :: :: not_ctor :: not_ctor_ +%% % {{ com $\ottnt{v}$ is not bound to a data constructor }} +%% % by +%% % +%% % E_l(x) gives t +%% % ------------------------------------------------------------ :: val +%% % E,E_l |- x not ctor +%% % +%% % x NOTIN dom(E_x) +%% % ------------------------------------------------------------ :: unbound +%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor +%% % +%% % E_x(x) gives <forall tnv1..tnvn. (p1 tnv'1)..(pi tnv'i) => t,env_tag> +%% % ------------------------------------------------------------ :: bound +%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor +%% % +%% % defns +%% % not_shadowed :: '' ::= +%% % +%% % defn +%% % E_l |- id not shadowed :: :: not_shadowed :: not_shadowed_ +%% % {{ com $\ottnt{id}$ is not lexically shadowed }} +%% % by +%% % +%% % x NOTIN dom(E_l) +%% % ------------------------------------------------------------ :: sing +%% % E_l |- x l1 l2 not shadowed +%% % +%% % ------------------------------------------------------------ :: multi +%% % E_l |- x_l1. .. x_ln.y_l.z_l l not shadowed +%% % +%% % +%% % defns +%% % check_pat :: '' ::= +%% % +%% % defn +%% % TD , E , E_l1 |- pat : t gives E_l2 :: :: check_pat :: check_pat_ +%% % {{ com Typing patterns, building their binding environment }} +%% % by +%% % +%% % :check_pat_aux: TD,E,E_l1 |- pat_aux : t gives E_l2 +%% % ------------------------------------------------------------ :: all +%% % TD,E,E_l1 |- pat_aux l : t gives E_l2 +%% % +%% % defn +%% % TD , E , E_l1 |- pat_aux : t gives E_l2 :: :: check_pat_aux :: check_pat_aux_ +%% % {{ com Typing patterns, building their binding environment }} +%% % by +%% % +%% % TD |- t ok +%% % ------------------------------------------------------------ :: wild +%% % TD,E,E_l |- _ : t gives {} +%% % +%% % TD,E,E_l1 |- pat : t gives E_l2 +%% % x NOTIN dom(E_l2) +%% % ------------------------------------------------------------ :: as +%% % TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ {x|->t} +%% % +%% % TD,E,E_l1 |- pat : t gives E_l2 +%% % TD,E |- typ ~> t +%% % ------------------------------------------------------------ :: typ +%% % TD,E,E_l1 |- (pat : typ) : t gives E_l2 +%% % +%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names) +%% % E_l |- id not shadowed +%% % TD,E,E_l |- pat1 : t1 gives E_l1 .. TD,E,E_l |- patn : tn gives E_ln +%% % disjoint doms(E_l1,..,E_ln) +%% % ------------------------------------------------------------ :: ident_constr +%% % TD,E,E_l |- id pat1 .. patn : p t_args gives E_l1 u+ .. u+ E_ln +%% % +%% % TD |- t ok +%% % E,E_l |- x not ctor +%% % ------------------------------------------------------------ :: var +%% % TD,E,E_l |- x l1 l2 : t gives {x|->t} +%% % +%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i /> +%% % </TD,E,E_l |- pati : ti gives E_li//i/> +%% % disjoint doms(</E_li//i/>) +%% % duplicates(</xi//i/>) = emptyset +%% % ------------------------------------------------------------ :: record +%% % TD,E,E_l |- <| </idi = pati li//i/> semi_opt |> : p t_args gives u+ </E_li//i/> +%% % +%% % TD,E,E_l |- pat1 : t gives E_l1 ... TD,E,E_l |- patn : t gives E_ln +%% % disjoint doms(E_l1 , ... , E_ln) +%% % length(pat1 ... patn) = nat +%% % ----------------------------------------------------------- :: vector +%% % TD,E,E_l |- [| pat1 ; ... ; patn semi_opt |] : __vector nat t gives E_l1 u+ ... u+ E_ln +%% % +%% % TD,E,E_l |- pat1 : __vector ne1 t gives E_l1 ... TD,E,E_l |- patn : __vector nen t gives E_ln +%% % disjoint doms(E_l1 , ... , E_ln) +%% % ne' = ne1 + ... + nen +%% % ----------------------------------------------------------- :: vectorConcat +%% % TD,E,E_l |- [| pat1 ... patn |] : __vector ne' t gives E_l1 u+ ... u+ E_ln +%% % +%% % +%% % TD,E,E_l |- pat1 : t1 gives E_l1 .... TD,E,E_l |- patn : tn gives E_ln +%% % disjoint doms(E_l1,....,E_ln) +%% % ------------------------------------------------------------ :: tup +%% % TD,E,E_l |- (pat1, ...., patn) : t1 * .... * tn gives E_l1 u+ .... u+ E_ln +%% % +%% % TD |- t ok +%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln +%% % disjoint doms(E_l1,..,E_ln) +%% % ------------------------------------------------------------ :: list +%% % TD,E,E_l |- [pat1; ..; patn semi_opt] : __list t gives E_l1 u+ .. u+ E_ln +%% % +%% % TD,E,E_l1 |- pat : t gives E_l2 +%% % ------------------------------------------------------------ :: paren +%% % TD,E,E_l1 |- (pat) : t gives E_l2 +%% % +%% % TD,E,E_l1 |- pat1 : t gives E_l2 +%% % TD,E,E_l1 |- pat2 : __list t gives E_l3 +%% % disjoint doms(E_l2,E_l3) +%% % ------------------------------------------------------------ :: cons +%% % TD,E,E_l1 |- pat1 :: pat2 : __list t gives E_l2 u+ E_l3 +%% % +%% % |- lit : t +%% % ------------------------------------------------------------ :: lit +%% % TD,E,E_l |- lit : t gives {} +%% % +%% % E,E_l |- x not ctor +%% % ------------------------------------------------------------ :: num_add +%% % TD,E,E_l |- x l + num : __num gives {x|->__num} +%% % +%% % +%% % defns +%% % id_field :: '' ::= +%% % +%% % defn +%% % E |- id field :: :: id_field :: id_field_ +%% % {{ com Check that the identifier is a permissible field identifier }} +%% % by +%% % +%% % E_f(x) gives f_desc +%% % ------------------------------------------------------------ :: empty +%% % <E_m,E_p,E_f,E_x> |- x l1 l2 field +%% % +%% % +%% % E_m(x) gives E +%% % x NOTIN dom(E_f) +%% % E |- </y_li.//i/> z_l l2 field +%% % ------------------------------------------------------------ :: cons +%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 field +%% % +%% % defns +%% % id_value :: '' ::= +%% % +%% % defn +%% % E |- id value :: :: id_value :: id_value_ +%% % {{ com Check that the identifier is a permissible value identifier }} +%% % by +%% % +%% % E_x(x) gives v_desc +%% % ------------------------------------------------------------ :: empty +%% % <E_m,E_p,E_f,E_x> |- x l1 l2 value +%% % +%% % +%% % E_m(x) gives E +%% % x NOTIN dom(E_x) +%% % E |- </y_li.//i/> z_l l2 value +%% % ------------------------------------------------------------ :: cons +%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 value +%% % +%% % defns +%% % check_exp :: '' ::= +%% % +%% % defn +%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_ +%% % {{ com Typing expressions, collecting typeclass and index constraints }} +%% % by +%% % +%% % :check_exp_aux: TD,E,E_l |- exp_aux : t gives S_c,S_N +%% % ------------------------------------------------------------ :: all +%% % TD,E,E_l |- exp_aux l : t gives S_c,S_N +%% % +%% % defn +%% % TD , E , E_l |- exp_aux : t gives S_c , S_N :: :: check_exp_aux :: check_exp_aux_ +%% % {{ com Typing expressions, collecting typeclass and index constraints }} +%% % by +%% % +%% % E_l(x) gives t +%% % ------------------------------------------------------------ :: var +%% % TD,E,E_l |- x l1 l2 : t gives {},{} +%% % +%% % %TODO KG Add check that N is in scope +%% % ------------------------------------------------------------ :: nvar +%% % TD,E,E_l |- N : __num gives {},{} +%% % +%% % E_l |- id not shadowed +%% % E |- id value +%% % TD,E |- ctor id : t_multi -> p t_args gives (x of names) +%% % ------------------------------------------------------------ :: ctor +%% % TD,E,E_l |- id : curry(t_multi, p t_args) gives {},{} +%% % +%% % E_l |- id not shadowed +%% % E |- id value +%% % TD, E |- val id : t gives S_c +%% % ------------------------------------------------------------ :: val +%% % TD,E,E_l |- id : t gives S_c,{} +%% % +%% % +%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln +%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N +%% % disjoint doms(E_l1,...,E_ln) +%% % ------------------------------------------------------------ :: fn +%% % TD,E,E_l |- fun pat1 ... patn -> exp l : curry((t1*...*tn), u) gives S_c,S_N +%% % +%% % %TODO: the various patterns might want to use different specifications for vector length (i.e. 32 in one and 8+n+8 in another) +%% % % So should be pati : t gives E_li,S_Ni +%% % </TD,E,E_l |- pati : t gives E_li//i/> +%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci, S_Ni//i/> +%% % ------------------------------------------------------------ :: function +%% % TD,E,E_l |- function bar_opt </pati -> expi li//i/> end : t -> u gives </S_ci//i/> , </S_Ni//i/> +%% % +%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N +%% % TD,E,E_l |- exp1 : t1 -> t2 gives S_c1,S_N1 +%% % TD,E,E_l |- exp2 : t1 gives S_c2,S_N2 +%% % ------------------------------------------------------------ :: app +%% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2 +%% % +%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N +%% % % Same for t2 +%% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1 +%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2 +%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3 +%% % ------------------------------------------------------------ :: infix_app1 +%% % TD,E,E_l |- exp1 ix l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 +%% % +%% % %TODO, see above todo +%% % :check_exp_aux: TD,E,E_l |- x : t1 -> t2 -> t3 gives S_c1,S_N1 +%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2 +%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3 +%% % ------------------------------------------------------------ :: infix_app2 +%% % TD,E,E_l |- exp1 `x` l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 +%% % +%% % %TODO, see above todo, with regard to t_args +%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/> +%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/> +%% % duplicates(</xi//i/>) = emptyset +%% % names = {</xi//i/>} +%% % ------------------------------------------------------------ :: record +%% % TD,E,E_l |- <| </idi = expi li//i/> semi_opt l |> : p t_args gives </S_ci//i/>,</S_Ni//i/> +%% % +%% % %TODO, see above todo, with regard to t_args +%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/> +%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/> +%% % duplicates(</xi//i/>) = emptyset +%% % TD,E,E_l |- exp : p t_args gives S_c',S_N' +%% % ------------------------------------------------------------ :: recup +%% % TD,E,E_l |- <| exp with </idi = expi li//i/> semi_opt l |> : p t_args gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/> +%% % +%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 ... TD,E,E_l |- expn : t gives S_cn,S_Nn +%% % length(exp1 ... expn) = nat +%% % ------------------------------------------------------------ :: vector +%% % TD,E,E_l |- [| exp1 ; ... ; expn semi_opt |] : __vector nat t gives S_c1 union ... union S_cn, S_N1 union ... union S_Nn +%% % +%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N +%% % |- nexp ~> ne +%% % ------------------------------------------------------------- :: vectorget +%% % TD,E,E_l |- exp .( nexp ) : t gives S_c,S_N union {ne<ne'} +%% % +%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N +%% % |- nexp1 ~> ne1 +%% % |- nexp2 ~> ne2 +%% % ne = :Ne_add: ne2 + (- ne1) +%% % ------------------------------------------------------------- :: vectorsub +%% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'} +%% % +%% % E |- id field +%% % TD,E |- field id : p t_args -> t gives (x of names) +%% % TD,E,E_l |- exp : p t_args gives S_c,S_N +%% % ------------------------------------------------------------ :: field +%% % TD,E,E_l |- exp.id : t gives S_c,S_N +%% % +%% % </TD,E,E_l |- pati : t gives E_li//i/> +%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci,S_Ni//i/> +%% % TD,E,E_l |- exp : t gives S_c',S_N' +%% % ------------------------------------------------------------ :: case +%% % TD,E,E_l |- match exp with bar_opt </pati -> expi li//i/> l end : u gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/> +%% % +%% % TD,E,E_l |- exp : t gives S_c,S_N +%% % TD,E |- typ ~> t +%% % ------------------------------------------------------------ :: typed +%% % TD,E,E_l |- (exp : typ) : t gives S_c,S_N +%% % +%% % %KATHYCOMMENT: where does E_l1 come from? +%% % TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1 +%% % TD,E,E_l1 u+ E_l2 |- exp : t gives S_c2,S_N2 +%% % ------------------------------------------------------------ :: let +%% % TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2 +%% % +%% % TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn +%% % ------------------------------------------------------------ :: tup +%% % TD,E,E_l |- (exp1, ...., expn) : t1 * .... * tn gives S_c1 union .... union S_cn,S_N1 union .... union S_Nn +%% % +%% % TD |- t ok +%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn +%% % ------------------------------------------------------------ :: list +%% % TD,E,E_l |- [exp1; ..; expn semi_opt] : __list t gives S_c1 union .. union S_cn, S_N1 union .. union S_Nn +%% % +%% % TD,E,E_l |- exp : t gives S_c,S_N +%% % ------------------------------------------------------------ :: paren +%% % TD,E,E_l |- (exp) : t gives S_c,S_N +%% % +%% % TD,E,E_l |- exp : t gives S_c,S_N +%% % ------------------------------------------------------------ :: begin +%% % TD,E,E_l |- begin exp end : t gives S_c,S_N +%% % +%% % %TODO t might need different index constraints +%% % TD,E,E_l |- exp1 : __bool gives S_c1,S_N1 +%% % TD,E,E_l |- exp2 : t gives S_c2,S_N2 +%% % TD,E,E_l |- exp3 : t gives S_c3,S_N3 +%% % ------------------------------------------------------------ :: if +%% % TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3 +%% % +%% % %TODO t might need different index constraints +%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 +%% % TD,E,E_l |- exp2 : __list t gives S_c2,S_N2 +%% % ------------------------------------------------------------ :: cons +%% % TD,E,E_l |- exp1 :: exp2 : __list t gives S_c1 union S_c2,S_N1 union S_N2 +%% % +%% % |- lit : t +%% % ------------------------------------------------------------ :: lit +%% % TD,E,E_l |- lit : t gives {},{} +%% % +%% % % TODO: should require that each xi actually appears free in exp1 +%% % </TD |- ti ok//i/> +%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1 +%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2 +%% % disjoint doms(E_l, {</xi|->ti//i/>}) +%% % E = <E_m,E_p,E_f,E_x> +%% % </xi NOTIN dom(E_x)//i/> +%% % ------------------------------------------------------------ :: set_comp +%% % TD,E,E_l |- { exp1 | exp2 } : __set t gives S_c1 union S_c2,S_N1 union S_N2 +%% % +%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1 +%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2 +%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3 +%% % ------------------------------------------------------------ :: set_comp_binding +%% % TD,E,E_l1 |- { exp1 | forall </qbindi//i/> | exp2 } : __set t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3 +%% % +%% % TD |- t ok +%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn +%% % ------------------------------------------------------------ :: set +%% % TD,E,E_l |- { exp1; ..; expn semi_opt } : __set t gives S_c1 union .. union S_cn,S_N1 union .. union S_Nn +%% % +%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1 +%% % TD,E,E_l1 u+ E_l2 |- exp : __bool gives S_c2,S_N2 +%% % ------------------------------------------------------------ :: quant +%% % TD,E,E_l1 |- q </qbindi//i/> . exp : __bool gives S_c1 union S_c2,S_N2 +%% % +%% % TD,E,E_l1 |- list </qbindi//i/> gives E_l2,S_c1 +%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2 +%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3 +%% % ------------------------------------------------------------ :: list_comp_binding +%% % TD,E,E_l1 |- [ exp1 | forall </qbindi//i/> | exp2 ] : __list t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3 +%% % +%% % defn +%% % TD , E , E_l1 |- qbind1 .. qbindn gives E_l2 , S_c :: :: check_listquant_binding +%% % :: check_listquant_binding_ +%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }} +%% % by +%% % +%% % ------------------------------------------------------------ :: empty +%% % TD,E,E_l |- gives {},{} +%% % +%% % TD |- t ok +%% % TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1 +%% % disjoint doms({x |-> t}, E_l2) +%% % ------------------------------------------------------------ :: var +%% % TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1 +%% % +%% % TD,E,E_l1 |- pat : t gives E_l3 +%% % TD,E,E_l1 |- exp : __set t gives S_c1,S_N1 +%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: restr +%% % TD,E,E_l1 |- (pat IN exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 +%% % +%% % TD,E,E_l1 |- pat : t gives E_l3 +%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1 +%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: list_restr +%% % TD,E,E_l1 |- (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 +%% % +%% % defn +%% % TD , E , E_l1 |- list qbind1 .. qbindn gives E_l2 , S_c :: :: check_quant_binding :: check_quant_binding_ +%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }} +%% % by +%% % +%% % ------------------------------------------------------------ :: empty +%% % TD,E,E_l |- list gives {},{} +%% % +%% % TD,E,E_l1 |- pat : t gives E_l3 +%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1 +%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2 +%% % disjoint doms(E_l3, E_l2) +%% % ------------------------------------------------------------ :: restr +%% % TD,E,E_l1 |- list (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2 +%% % +%% % +%% % defn +%% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_ +%% % {{ com Build the environment for a function definition clause, collecting typeclass and index constraints }} +%% % by +%% % +%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln +%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N +%% % disjoint doms(E_l1,...,E_ln) +%% % TD,E |- typ ~> u +%% % ------------------------------------------------------------ :: annot +%% % TD,E,E_l |- x l1 pat1 ... patn : typ = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N +%% % +%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln +%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N +%% % disjoint doms(E_l1,...,E_ln) +%% % ------------------------------------------------------------ :: noannot +%% % TD,E,E_l |- x l1 pat1 ... patn = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N +%% % +%% % +%% % defn +%% % TD , E , E_l1 |- letbind gives E_l2 , S_c , S_N :: :: check_letbind :: check_letbind_ +%% % {{ com Build the environment for a let binding, collecting typeclass and index constraints }} +%% % by +%% % +%% % %TODO similar type equality issues to above ones +%% % TD,E,E_l1 |- pat : t gives E_l2 +%% % TD,E,E_l1 |- exp : t gives S_c,S_N +%% % TD,E |- typ ~> t +%% % ------------------------------------------------------------ :: val_annot +%% % TD,E,E_l1 |- pat : typ = exp l gives E_l2,S_c,S_N +%% % +%% % TD,E,E_l1 |- pat : t gives E_l2 +%% % TD,E,E_l1 |- exp : t gives S_c,S_N +%% % ------------------------------------------------------------ :: val_noannot +%% % TD,E,E_l1 |- pat = exp l gives E_l2,S_c,S_N +%% % +%% % :check_funcl:TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N +%% % ------------------------------------------------------------ :: fn +%% % TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N +%% % +%% % defns +%% % check_rule :: '' ::= +%% % +%% % defn +%% % TD , E , E_l |- rule gives { x |-> t } , S_c , S_N :: :: check_rule :: check_rule_ +%% % {{ com Build the environment for an inductive relation clause, collecting typeclass and index constraints }} +%% % by +%% % +%% % </TD |- ti ok//i/> +%% % E_l2 = {</yi|->ti//i/>} +%% % TD,E,E_l1 u+ E_l2 |- exp' : __bool gives S_c',S_N' +%% % TD,E,E_l1 u+ E_l2 |- exp1 : u1 gives S_c1,S_N1 .. TD,E,E_l1 u+ E_l2 |- expn : un gives S_cn,S_Nn +%% % ------------------------------------------------------------ :: rule +%% % TD,E,E_l1 |- x_l_opt forall </yi li//i/> . exp' ==> x l exp1 .. expn l' gives {x|->curry((u1 * .. * un) , __bool)}, S_c' union S_c1 union .. union S_cn,S_N' union S_N1 union .. union S_Nn +%% % +%% % defns +%% % check_texp_tc :: '' ::= +%% % +%% % defn +%% % xs , TD1 , E |- tc td gives TD2 , E_p :: :: check_texp_tc :: check_texp_tc_ +%% % {{ com Extract the type constructor information }} +%% % by +%% % +%% % tnvars ~> tnvs +%% % TD,E |- typ ~> t +%% % duplicates(tnvs) = emptyset +%% % FV(t) SUBSET tnvs +%% % </yi.//i/>x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: abbrev +%% % </yi//i/>,TD,E |- tc x l tnvars = typ gives {</yi.//i/>x|->tnvs.t},{x|-></yi.//i/>x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % </yi.//i/>x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: abstract +%% % </yi//i/>,TD,E1 |- tc x l tnvars gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % </yi.//i/>x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: rec +%% % </yi//i/>,TD1,E |- tc x l tnvars = <| x_l1 : typ1 ; ... ; x_lj : typj semi_opt |> gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x} +%% % +%% % tnvars ~> tnvs +%% % duplicates(tnvs) = emptyset +%% % </yi.//i/>x NOTIN dom(TD) +%% % ------------------------------------------------------------ :: var +%% % </yi//i/>,TD1,E |- tc x l tnvars = bar_opt ctor_def1 | ... | ctor_defj gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x} +%% % +%% % defns +%% % check_texps_tc :: '' ::= +%% % +%% % defn +%% % xs , TD1 , E |- tc td1 .. tdi gives TD2 , E_p :: :: check_texps_tc :: check_texps_tc_ +%% % {{ com Extract the type constructor information }} +%% % by +%% % +%% % ------------------------------------------------------------ :: empty +%% % xs,TD,E |- tc gives {},{} +%% % +%% % :check_texp_tc: xs,TD1,E |- tc td gives TD2,E_p2 +%% % xs,TD1 u+ TD2,E u+ <{},E_p2,{},{}> |- tc </tdi//i/> gives TD3,E_p3 +%% % dom(E_p2) inter dom(E_p3) = emptyset +%% % ------------------------------------------------------------ :: abbrev +%% % xs,TD1,E |- tc td </tdi//i/> gives TD2 u+ TD3,E_p2 u+ E_p3 +%% % +%% % defns +%% % check_texp :: '' ::= +%% % +%% % defn +%% % TD , E |- tnvs p = texp gives < E_f , E_x > :: :: check_texp :: check_texp_ +%% % {{ com Check a type definition, with its path already resolved }} +%% % by +%% % +%% % ------------------------------------------------------------ :: abbrev +%% % TD,E |- tnvs p = typ gives <{},{}> +%% % +%% % </TD,E |- typi ~> ti//i/> +%% % names = {</xi//i/>} +%% % duplicates(</xi//i/>) = emptyset +%% % </FV(ti) SUBSET tnvs//i/> +%% % E_f = {</xi|-> <forall tnvs. p -> ti, (xi of names)>//i/>} +%% % ------------------------------------------------------------ :: rec +%% % TD,E |- tnvs p = <| </x_li:typi//i/> semi_opt |> gives <E_f,{}> +%% % +%% % </TD,E |- typsi ~> t_multii//i/> +%% % names = {</xi//i/>} +%% % duplicates(</xi//i/>) = emptyset +%% % </FV(t_multii) SUBSET tnvs//i/> +%% % E_x = {</xi|-><forall tnvs. t_multii -> p, (xi of names)>//i/>} +%% % ------------------------------------------------------------ :: var +%% % TD,E |- tnvs p = bar_opt </x_li of typsi//i/> gives <{},E_x> +%% % +%% % defns +%% % check_texps :: '' ::= +%% % +%% % defn +%% % xs , TD , E |- td1 .. tdn gives < E_f , E_x > :: :: check_texps :: check_texps_ by +%% % +%% % ------------------------------------------------------------ :: empty +%% % </yi//i/>,TD,E |- gives <{},{}> +%% % +%% % tnvars ~> tnvs +%% % TD,E1 |- tnvs </yi.//i/>x = texp gives <E_f1,E_x1> +%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f2,E_x2> +%% % dom(E_x1) inter dom(E_x2) = emptyset +%% % dom(E_f1) inter dom(E_f2) = emptyset +%% % ------------------------------------------------------------ :: cons_concrete +%% % </yi//i/>,TD,E |- x l tnvars = texp </tdj//j/> gives <E_f1 u+ E_f2, E_x1 u+ E_x2> +%% % +%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f,E_x> +%% % ------------------------------------------------------------ :: cons_abstract +%% % </yi//i/>,TD,E |- x l tnvars </tdj//j/> gives <E_f,E_x> +%% % +%% % defns +%% % convert_class :: '' ::= +%% % +%% % defn +%% % TC , E |- id ~> p :: :: convert_class :: convert_class_ +%% % {{ com Lookup a type class }} +%% % by +%% % +%% % E(id) gives p +%% % TC(p) gives xs +%% % ------------------------------------------------------------ :: all +%% % TC,E |- id ~> p +%% % +%% % defns +%% % solve_class_constraint :: '' ::= +%% % +%% % defn +%% % I |- ( p t ) 'IN' semC :: :: solve_class_constraint :: solve_class_constraint_ +%% % {{ com Solve class constraint }} +%% % by +%% % +%% % ------------------------------------------------------------ :: immediate +%% % I |- (p a) IN (p1 tnv1) .. (pi tnvi) (p a) (p'1 tnv'1) .. (p'j tnv'j) +%% % +%% % (p1 tnv1)..(pn tnvn)=>(p t) IN I +%% % I |- (p1 t_subst(tnv1)) IN semC .. I |- (pn t_subst(tnvn)) IN semC +%% % ------------------------------------------------------------ :: chain +%% % I |- (p t_subst(t)) IN semC +%% % +%% % defns +%% % solve_class_constraints :: '' ::= +%% % +%% % defn +%% % I |- S_c gives semC :: :: solve_class_constraints :: solve_class_constraints_ +%% % {{ com Solve class constraints }} +%% % by +%% % +%% % I |- (p1 t1) IN semC .. I |- (pn tn) IN semC +%% % ------------------------------------------------------------ :: all +%% % I |- {(p1 t1), .., (pn tn)} gives semC +%% % +%% % defns +%% % check_val_def :: '' ::= +%% % +%% % defn +%% % TD , I , E |- val_def gives E_x :: :: check_val_def :: check_val_def_ +%% % {{ com Check a value definition }} +%% % by +%% % +%% % TD,E,{} |- letbind gives {</xi|->ti//i/>},S_c,S_N +%% % %TODO, check S_N constraints +%% % I |- S_c gives semC +%% % </FV(ti) SUBSET tnvs//i/> +%% % FV(semC) SUBSET tnvs +%% % ------------------------------------------------------------ :: val +%% % TD,I,E1 |- let targets_opt letbind gives {</xi |-> <forall tnvs. semC => ti, let>//i/>} +%% % +%% % </TD,E,E_l |- funcli gives {xi|->ti},S_ci,S_Ni//i/> +%% % I |- S_c gives semC +%% % </FV(ti) SUBSET tnvs//i/> +%% % FV(semC) SUBSET tnvs +%% % compatible overlap(</xi|->ti//i/>) +%% % E_l = {</xi|->ti//i/>} +%% % ------------------------------------------------------------ :: recfun +%% % TD,I,E |- let rec targets_opt </funcli//i/> gives {</xi|-><forall tnvs. semC => ti,let>//i/>} +%% % +%% % defns +%% % check_t_instance :: '' ::= +%% % +%% % defn +%% % +%% % TD , ( a1 , .. , an ) |- t instance :: :: check_t_instance :: check_t_instance_ +%% % {{ com Check that $\ottnt{t}$ be a typeclass instance }} +%% % by +%% % +%% % ------------------------------------------------------------ :: var +%% % TD , (a) |- a instance +%% % +%% % ------------------------------------------------------------ :: tup +%% % TD , (a1, ...., an) |- a1 * .... * an instance +%% % +%% % ------------------------------------------------------------ :: fn +%% % TD , (a1, a2) |- a1 -> an instance +%% % +%% % TD(p) gives a'1..a'n +%% % ------------------------------------------------------------ :: tc +%% % TD , (a1, .., an) |- p a1 .. an instance +%% % +%% % defns +%% % check_defs :: '' ::= +%% % +%% % defn +%% % +%% % </ zj // j /> , D1 , E1 |- def gives D2 , E2 :: :: check_def :: check_def_ +%% % {{ com Check a definition }} +%% % by +%% % +%% % +%% % </zj//j/>,TD1,E |- tc </tdi//i/> gives TD2,E_p +%% % </zj//j/>,TD1 u+ TD2,E u+ <{},E_p,{},{}> |- </tdi//i/> gives <E_f,E_x> +%% % ------------------------------------------------------------ :: type +%% % </zj//j/>,<TD1,TC,I>,E |- type </tdi//i/> l gives <TD2,{},{}>,<{},E_p,E_f,E_x> +%% % +%% % TD,I,E |- val_def gives E_x +%% % ------------------------------------------------------------ :: val_def +%% % </zj//j/>,<TD,TC,I>,E |- val_def l gives empty,<{},{},{},E_x> +%% % +%% % </TD,E1,E_l |- rulei gives {xi|->ti},S_ci,S_Ni//i/> +%% % %TODO Check S_N constraints +%% % I |- </S_ci//i/> gives semC +%% % </FV(ti) SUBSET tnvs//i/> +%% % FV(semC) SUBSET tnvs +%% % compatible overlap(</xi|->ti//i/>) +%% % E_l = {</xi|->ti//i/>} +%% % E2 = <{},{},{},{</xi |-><forall tnvs. semC => ti,let>//i/>}> +%% % ------------------------------------------------------------ :: indreln +%% % </zj//j/>,<TD,TC,I>,E1 |- indreln targets_opt </rulei//i/> l gives empty,E2 +%% % +%% % </zj//j/> x,D1,E1 |- defs gives D2,E2 +%% % ------------------------------------------------------------ :: module +%% % </zj//j/>,D1,E1 |- module x l1 = struct defs end l2 gives D2,<{x|->E2},{},{},{}> +%% % +%% % E1(id) gives E2 +%% % ------------------------------------------------------------ :: module_rename +%% % </zj//j/>,D,E1 |- module x l1 = id l2 gives empty,<{x|->E2},{},{},{}> +%% % +%% % TD,E |- typ ~> t +%% % FV(t) SUBSET </ai//i/> +%% % FV(</a'k//k/>) SUBSET </ai//i/> +%% % </TC,E |- idk ~> pk//k/> +%% % E' = <{},{},{},{x|-><forall </ai//i/>. </(pk a'k)//k/> => t,val>}> +%% % ------------------------------------------------------------ :: spec +%% % </zj//j/>,<TD,TC,I>,E |- val x l1 : forall </ai l''i//i/>. </idk a'k l'k//k/> => typ l2 gives empty,E' +%% % +%% % </TD,E1 |- typi ~> ti//i/> +%% % </FV(ti) SUBSET a//i/> +%% % :formula_p_eq: p = </zj.//j/>x +%% % E2 = <{},{x|->p},{},{</yi |-><forall a. (p a) => ti,method>//i/>}> +%% % TC2 = {p|-></yi//i/>} +%% % p NOTIN dom(TC1) +%% % ------------------------------------------------------------ :: class +%% % </zj//j/>,<TD,TC1,I>,E1 |- class (x l a l'') </val yi li : typi li//i/> end l' gives <{},TC2,{}>,E2 +%% % +%% % E = <E_m,E_p,E_f,E_x> +%% % TD,E |- typ' ~> t' +%% % TD,(</ai//i/>) |- t' instance +%% % tnvs = </ai//i/> +%% % duplicates(tnvs) = emptyset +%% % </TC,E |- idk ~> pk//k/> +%% % FV(</a'k//k/>) SUBSET tnvs +%% % E(id) gives p +%% % TC(p) gives </zj//j/> +%% % I2 = { </=> (pk a'k)//k/> } +%% % </TD,I union I2,E |- val_defn gives E_xn//n/> +%% % disjoint doms(</E_xn//n/>) +%% % </E_x(xk) gives <forall a''. (p a'') => tk,method>//k/> +%% % {</xk |-> <forall tnvs. => {a''|->t'}(tk),let>//k/>} = </E_xn//n/> +%% % :formula_xs_eq:</xk//k/> = </zj//j/> +%% % I3 = {</(pk a'k) => (p t')//k/>} +%% % (p {</ai |-> a'''i//i/>}(t')) NOTIN I +%% % ------------------------------------------------------------ :: instance_tc +%% % </zj//j/>,<TD,TC,I>,E |- instance forall </ai l'i//i/>. </idk a'k l''k//k/> => (id typ') </val_defn ln//n/> end l' gives <{},{},I3>,empty +%% % +%% % defn +%% % </ zj // j /> , D1 , E1 |- defs gives D2 , E2 :: :: check_defs :: check_defs_ +%% % {{ com Check definitions, given module path, definitions and environment }} +%% % by +%% % +%% % % TODO: Check compatibility for duplicate definitions +%% % +%% % ------------------------------------------------------------ :: empty +%% % </zj//j/>,D,E |- gives empty,empty +%% % +%% % :check_def: </zj//j/>,D1,E1 |- def gives D2,E2 +%% % </zj//j/>,D1 u+ D2,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3 +%% % ------------------------------------------------------------ :: relevant_def +%% % </zj//j/>,D1,E1 |- def semisemi_opt </defi semisemi_opti // i/> gives D2 u+ D3, E2 u+ E3 +%% % +%% % E1(id) gives E2 +%% % </zj//j/>,D1,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3 +%% % ------------------------------------------------------------ :: open +%% % </zj//j/>,D1,E1 |- open id l semisemi_opt </defi semisemi_opti // i/> gives D3,E3 +%% % + diff --git a/src/parse_ast.ml b/src/parse_ast.ml new file mode 100644 index 00000000..b5f38aa4 --- /dev/null +++ b/src/parse_ast.ml @@ -0,0 +1,441 @@ +(* generated by Ott 0.22 from: l2_parse.ott *) + + +type text = string + +type l = + | Unknown + | Trans of string * l option + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +type ml_comment = + | Chars of string + | Comment of ml_comment list + +type lex_skip = + | Com of ml_comment + | Ws of string + | Nl + +type lex_skips = lex_skip list option + +let pp_lex_skips ppf sk = + match sk with + | None -> () + | Some(sks) -> + List.iter + (fun sk -> + match sk with + | Com(ml_comment) -> + (* TODO: fix? *) + Format.fprintf ppf "(**)" + | Ws(r) -> + Format.fprintf ppf "%s" r (*(Ulib.Text.to_string r)*) + | Nl -> Format.fprintf ppf "\\n") + sks + +let combine_lex_skips s1 s2 = + match (s1,s2) with + | (None,_) -> s2 + | (_,None) -> s1 + | (Some(s1),Some(s2)) -> Some(s2@s1) + +type terminal = lex_skips + + +type x = terminal * text (* identifier *) +type ix = terminal * text (* infix identifier *) + +type +base_kind_aux = (* base kind *) + BK_type of terminal (* kind of types *) + | BK_nat of terminal (* kind of natural number size expressions *) + | BK_order of terminal (* kind of vector order specifications *) + | BK_effects of terminal (* kind of effect sets *) + + +type +effect_aux = (* effect *) + Effect_rreg of terminal (* read register *) + | Effect_wreg of terminal (* write register *) + | Effect_rmem of terminal (* read memory *) + | Effect_wmem of terminal (* write memory *) + | Effect_undef of terminal (* undefined-instruction exception *) + | Effect_unspec of terminal (* unspecified values *) + | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *) + + +type +id_aux = (* Identifier *) + Id of x + | DeIid of terminal * x * terminal (* remove infix status *) + + +type +base_kind = + BK_aux of base_kind_aux * l + + +type +effect = + Effect_aux of effect_aux * l + + +type +id = + Id_aux of id_aux * l + + +type +kind_aux = (* kinds *) + K_kind of (base_kind * terminal) list + + +type +atyp_aux = (* expression of all kinds *) + ATyp_id of id (* identifier *) + | ATyp_constant of terminal * int (* constant *) + | ATyp_times of atyp * terminal * atyp (* product *) + | ATyp_sum of atyp * terminal * atyp (* sum *) + | ATyp_exp of terminal * terminal * atyp (* exponential *) + | ATyp_inc of terminal (* increasing (little-endian) *) + | ATyp_dec of terminal (* decreasing (big-endian) *) + | ATyp_set of terminal * (effect * terminal) list * terminal (* effect set *) + | ATyp_wild of terminal (* Unspecified type *) + | ATyp_fn of atyp * terminal * atyp * atyp (* Function type (first-order only in user code) *) + | ATyp_tup of (atyp * terminal) list (* Tuple type *) + | ATyp_app of id * (atyp) list (* type constructor application *) + +and atyp = + ATyp_aux of atyp_aux * l + + +type +kind = + K_aux of kind_aux * l + + +type +'a nexp_constraint_aux = (* constraint over kind $_$ *) + NC_fixed of atyp * terminal * atyp + | NC_bounded_ge of atyp * terminal * atyp + | NC_bounded_le of atyp * terminal * atyp + | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal + + +type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) + + +type +'a nexp_constraint = + NC_aux of 'a nexp_constraint_aux * 'a annot + + +type +kinded_id = + KOpt_aux of kinded_id_aux * l + + +type +'a typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of terminal * (kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal + | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type +lit_aux = (* Literal constant *) + L_unit of terminal * terminal (* $() : _$ *) + | L_zero of terminal (* $_ : _$ *) + | L_one of terminal (* $_ : _$ *) + | L_true of terminal (* $_ : _$ *) + | L_false of terminal (* $_ : _$ *) + | L_num of terminal * int (* natural number constant *) + | L_hex of terminal * string (* bit vector constant, C-style *) + | L_bin of terminal * string (* bit vector constant, C-style *) + | L_string of terminal * string (* string constant *) + + +type +'a typquant = + TypQ_aux of 'a typquant_aux * 'a annot + + +type +lit = + L_aux of lit_aux * l + + +type +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * atyp + + +type +'a pat_aux = (* Pattern *) + P_lit of lit (* literal constant pattern *) + | P_wild of terminal (* wildcard *) + | P_as of terminal * 'a pat * terminal * id * terminal (* named pattern *) + | P_typ of terminal * atyp * 'a pat * terminal (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * ('a pat) list (* union constructor pattern *) + | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *) + | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *) + | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *) + | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *) + | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *) + +and 'a pat = + P_aux of 'a pat_aux * 'a annot + +and 'a fpat_aux = (* Field pattern *) + FP_Fpat of id * terminal * 'a pat + +and 'a fpat = + FP_aux of 'a fpat_aux * 'a annot + + +type +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot + + +type +'a exp_aux = (* Expression *) + E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of terminal * atyp * terminal * 'a exp (* cast *) + | E_app of 'a exp * ('a exp) list (* function application *) + | E_app_infix of 'a exp * id * 'a exp (* infix function application *) + | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *) + | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *) + | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *) + | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) + | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *) + | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *) + | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *) + | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *) + | E_list of terminal * ('a exp * terminal) list * terminal (* list *) + | E_cons of 'a exp * terminal * 'a exp (* cons *) + | E_record of terminal * 'a fexps * terminal (* struct *) + | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *) + | E_field of 'a exp * terminal * id (* field projection from struct *) + | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *) + | E_let of 'a letbind * terminal * 'a exp (* let expression *) + | E_assign of 'a lexp * terminal * 'a exp (* imperative assignment *) + +and 'a exp = + E_aux of 'a exp_aux * 'a annot + +and 'a lexp_aux = (* lvalue expression *) + LEXP_id of id (* identifier *) + | LEXP_vector of 'a lexp * terminal * 'a exp * terminal (* vector element *) + | LEXP_vector_range of 'a lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *) + | LEXP_field of 'a lexp * terminal * id (* struct field *) + +and 'a lexp = + LEXP_aux of 'a lexp_aux * 'a annot + +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * terminal * 'a exp + +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot + +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp * terminal) list * terminal * bool + +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * terminal * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) + LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *) + | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *) + +and 'a letbind = + LB_aux of 'a letbind_aux * 'a annot + + +type +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp + + +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec of terminal (* recursive *) + + +type +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of terminal + + +type +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * terminal + + +type +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal + + +type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot + + +type +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot + + +type +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot + + +type +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of terminal * int (* single index *) + | BF_range of terminal * int * terminal * terminal * int (* index range *) + | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l + + +type +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l + + +type +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list + + +type +'a type_def_aux = (* Type definition body *) + TD_abbrev of terminal * id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *) + | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* struct type definition *) + | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* union type definition *) + | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) + | TD_register of terminal * id * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) + + +type +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * 'a typschm * id + + +type +'a val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * 'a typschm * id + + +type +'a fundef = + FD_aux of 'a fundef_aux * 'a annot + + +type +'a type_def = + TD_aux of 'a type_def_aux * 'a annot + + +type +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot + + +type +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot + + +type +'a def_aux = (* Top-level definition *) + DEF_type of 'a type_def (* type definition *) + | DEF_fundef of 'a fundef (* function definition *) + | DEF_val of 'a letbind (* value definition *) + | DEF_spec of 'a val_spec (* top-level type constraint *) + | DEF_default of 'a default_typing_spec (* default kind and type assumptions *) + | DEF_reg_dec of terminal * terminal * id (* register declaration *) + | DEF_scattered_function of terminal * terminal * rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *) + | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *) + | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *) + | DEF_scattered_unioncl of terminal * id * terminal * terminal * id (* scattered union definition member *) + | DEF_scattered_end of terminal * id (* scattered definition end *) + + +type +'a def = + DEF_aux of 'a def_aux * 'a annot + + +type +'a typ_lib_aux = (* library types and syntactic sugar for them *) + Typ_lib_unit of terminal (* unit type with value $()$ *) + | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) + | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *) + | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *) + | Typ_lib_string of terminal * string (* UTF8 strings *) + | Typ_lib_enum of terminal * terminal * terminal * terminal (* natural numbers _ .. _+_-1, ordered by _ *) + | Typ_lib_enum1 of terminal * terminal * terminal (* sugar for \texttt{enum nexp 0 inc} *) + | Typ_lib_enum2 of terminal * terminal * terminal * terminal * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) + | Typ_lib_vector of terminal * terminal * terminal * terminal * terminal (* vector of _, indexed by natural range *) + | Typ_lib_vector2 of atyp * terminal * terminal * terminal (* sugar for vector indexed by [ _ ] *) + | Typ_lib_vector3 of atyp * terminal * terminal * terminal * terminal * terminal (* sugar for vector indexed by [ _.._ ] *) + | Typ_lib_list of terminal * atyp (* list of _ *) + | Typ_lib_set of terminal * atyp (* finite set of _ *) + | Typ_lib_reg of terminal * atyp (* mutable register components holding _ *) + + +type +'a ctor_def_aux = (* Datatype constructor definition clause *) + CT_ct of id * terminal * 'a typschm + + +type +'a defs = (* Definition sequence *) + Defs of ('a def) list + + +type +'a typ_lib = + Typ_lib_aux of 'a typ_lib_aux * l + + +type +'a ctor_def = + CT_aux of 'a ctor_def_aux * 'a annot + + + diff --git a/src/parser.mly b/src/parser.mly index dc024970..7f15b149 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -53,16 +53,15 @@ open Ast let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos()) let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n) -let tloc t = Typ_l(t,loc ()) -let nloc n = Length_l(n,loc ()) -let lloc l = Lit_l(l,loc ()) let ploc p = Pat_l(p,loc ()) let eloc e = Expr_l(e,loc ()) let lbloc lb = Letbind(lb,loc ()) let bkloc k = BK_aux(k,loc ()) let kloc k = K_aux(k,loc ()) -let nloc n = Nexp_aux(k,loc ()) +let tloc t = ATyp_aux(t,loc ()) +let lloc l = L_aux(l,loc ()) + let dloc d = DEF_aux(d,loc ()) @@ -165,10 +164,6 @@ id: { mk_pre_x_l $1 $2 $3 (loc ()) } | Lparen IN Rparen { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen MEM Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen MinusMinusGt Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } | Lparen AmpAmp Rparen { mk_pre_x_l $1 $2 $3 (loc ()) } | Lparen BarBar Rparen @@ -181,20 +176,8 @@ id: { mk_pre_x_l $1 $2 $3 (loc ()) } | Lparen GtEq Rparen { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen PlusX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen StarX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen GtEqX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen EqualX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen StarstarX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } | Lparen At Rparen { mk_pre_x_l $1 $2 $3 (loc ()) } - | Lparen AtX Rparen - { mk_pre_x_l $1 $2 $3 (loc ()) } atomic_kind: | TYPE @@ -212,64 +195,54 @@ kind: | atomic_kind MinusGt kind { ($1,$2)::$3 } -atomic_nexp_no_id: - | Num - { nloc (Nexp_constant(fst $1, snd$1)) } - | Lparen nexp Rparen - { $2 } - -atomic_nexp: - | id - { nloc (Nexp_var (fst $1, snd $1)) } - | atomic_nexp_no_id - { $1 } - -star_nexp: - | atomic_nexp - { $1 } - | atomic_nexp Star star_nexp - { nloc (Nexp_times($1, fst $2, $3)) } - -exp_nexp: - | star_nexp - { $1 } - | Num StarStar nexp - { if (2 = (fst $1)) - then nloc (Nexp_exp((fst $1,snd $1),$2,$3)) - else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") } - -nexp: - | exp_nexp - { $1 } - | exp_nexp Plus nexp - { nloc (Nexp_sum($1,fst $2,$3)) } +effect: + | id + { (match id with + | Id_aux(Id(s,t),l) -> + Effect_aux + ((match s with + | "rreg" -> (Effect_rreg t) + | "wreg" -> (Effect_wreg t) + | "rmem" -> (Effect_rmem t) + | "wmem" -> (Effect_wmem t) + | "undef" -> (Effect_undef t) + | "unspec" -> (Effect_unspec t) + | "nondet" -> (Effect_nondet t) + | _ -> Parse_error_locn(l, "Invalid effect")),l) + | _ -> Parse_error_locn(loc () , "Invalid effect")) } + +effect_list: + | effect + { [($1,None)] } + | effect Comma effect_list + { ($1,Some($2))::$3 } atomic_typ: - | Under - { tloc (Typ_wild($1)) } | id - { tloc (Typ_var(A_l((fst $1, snd $1), loc()))) } + { tloc (Atyp_var (fst $1, snd $1)) } + | Num + { tloc (Atyp_constant(fst $1, snd$1)) } + | Pure + { tloc (Atyp_pure($1)) } + | Under + { tloc (ATyp_wild($1)) } + | Lcurly effect_list Rcurly + { tloc (ATyp_effects($1,$2,$3)) } | Lparen typ Rparen - { tloc (Typ_paren($1,$2,$3)) } - -appt_typ : - | atomic_typ - { $1 } - | atomic_nexp - { tloc (Typ_Nexps($1)) } + { $2 } atomic_typs: - | appt_typ + | atomic_typ { [$1] } - | appt_typ atomic_typs + | atomic_typ atomic_typs { $1::$2 } app_typ: | atomic_typ { $1 } | id atomic_typs - { tloc (Typ_app($1,$2)) } - + { tloc (ATyp_app($1,$2)) } + star_typ_list: | app_typ { [($1,None)] } @@ -282,14 +255,31 @@ star_typ: | [] -> assert false | [(t,None)] -> t | [(t,Some _)] -> assert false - | ts -> tloc (Typ_tup(ts)) } + | ts -> tloc (ATyp_tup(ts)) } + +exp_typ: + | star_typ + { $1 } + | Num StarStar nexp + { if (2 = (fst $1)) + then tloc (ATyp_exp((fst $1,snd $1),$2,$3)) + else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") } + +nexp_typ: + | exp_typ + { $1 } + | exp_typ Plus typ + { tloc (ATyp_sum($1,fst $2,$3)) } typ: - | star_typ + | nexp_typ { $1 } - | star_typ Arrow typ - { tloc (Typ_fn($1,$2,$3)) } - + | star_typ MinusGt typ id + { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_id($4))))) } + | star_typ MinusGt typ Pure + { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_pure($4))))) } + | star_typ MinusGt typ Lcurly effect_list Rcurly + { tloc (ATyp_fn($1,$2,$3,(tloc (ATyp_effects($4,$5,$6))))) } lit: | True @@ -302,10 +292,6 @@ lit: { lloc (L_string(fst $1, snd $1)) } | Lparen Rparen { lloc (L_unit($1,$2)) } - | HashZero - { lloc (L_zero($1)) } - | HashOne - { lloc (L_one($1)) } | Bin { lloc (L_bin(fst $1, snd $1)) } | Hex |