From 1ba1175defbe92441344703b39ce9e17db4c63a9 Mon Sep 17 00:00:00 2001 From: Mark Wassell Date: Tue, 17 Oct 2017 15:22:22 +0100 Subject: Start of alignment of Ott definition with new implementation of type checker and syntax changes --- language/Makefile | 2 +- language/l2.ott | 53 +- language/l2_rules.ott | 1552 ++++++++----------------------------------------- 3 files changed, 274 insertions(+), 1333 deletions(-) (limited to 'language') diff --git a/language/Makefile b/language/Makefile index 77aa5607..081d90a7 100644 --- a/language/Makefile +++ b/language/Makefile @@ -18,7 +18,7 @@ type_system.pdf: doc_in.tex type_system.tex pdflatex type_system.tex pdflatex type_system.tex -l2.tex: l2.ott l2_terminals_non_tt.ott l2_typ.ott l2_rules.ott +l2.tex: l2.ott l2_rules.ott # l2_terminals_non_tt.ott l2_typ.ott l2_rules.ott $(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott diff --git a/language/l2.ott b/language/l2.ott index c78c66f8..559242ea 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -120,6 +120,7 @@ id :: '' ::= | bit :: M :: bit {{ ichlo (Id "bit") }} | unit :: M :: unit {{ ichlo (Id "unit") }} | nat :: M :: nat {{ ichlo (Id "nat") }} + | int :: M :: int {{ ichlo (Id "int") }} | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }} | range :: M :: range {{ ichlo (Id "range") }} | atom :: M :: atom {{ ichlo (Id "atom") }} @@ -135,8 +136,15 @@ id :: '' ::= % 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. - +% targets use alphabetical infix operators. + +% Vector builtins + | vector_access :: M :: vector_access + | vector_update :: M :: vector_update + | vector_update_subrange :: M :: vector_update_subrange + | vector_subrange :: M :: vector_subrange + | vector_append :: M :: vector_append + kid :: '' ::= {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} {{ aux _ l }} @@ -243,6 +251,7 @@ typ :: 'Typ_' ::= % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }} + | exist kid1 , .. , kidn , n_constraint . typ :: :: exist % TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker | id < typ_arg1 , .. , typ_argn > :: :: app {{ com type constructor application }} @@ -258,11 +267,12 @@ typ :: 'Typ_' ::= % probably some sugar for vector types, using [ ] similarly to enums: % (but with .. not : in the former, to avoid confusion...) | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} -{{ com sugar for vector indexed by \texttt{[|} [[nexp]] \texttt{|]} }} +{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$ \texttt{|]} }} | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} -{{ com sugar for vector indexed by \texttt{[|} [[nexp]]..[[nexp']] \texttt{|]} }} +{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }} | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} + | register [ id ] :: S :: register % ...so bit [ nexp ] etc is just an instance of that % | List < typ > :: :: list {{ com list of [[typ]] }} % | Set < typ > :: :: set {{ com finite set of [[typ]] }} @@ -271,7 +281,7 @@ typ :: 'Typ_' ::= % not sure how first-class it should be, though % use "reg word32" etc for the types of vanilla registers - + typ_arg :: 'Typ_arg_' ::= {{ com type constructor arguments of all kinds }} {{ aux _ l }} @@ -987,7 +997,8 @@ exp :: 'E_' ::= {{ com conditional }} | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} - + | while exp1 do exp2 :: :: while + | repeat exp1 until exp2 :: :: until | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} @@ -1069,15 +1080,15 @@ exp :: 'E_' ::= {{ com imperative assignment }} | sizeof nexp :: :: sizeof - {{ com the value of [[nexp]] at run time }} + {{ com the value of $[[nexp]]$ at run time }} - | return exp :: :: return {{ com return [[exp]] from current function }} + | return exp :: :: return {{ com return $[[exp]]$ from current function }} % this can be used to break out of for loops | exit exp :: :: exit {{ com halt all current execution }} %, potentially calling a system, trap, or interrupt handler with exp | assert ( exp , exp' ) :: :: assert - {{ com halt with error [[exp']] when not [[exp]] }} + {{ com halt with error $[[exp']]$ when not $[[exp]]$ }} % exp' is optional? | ( exp ) :: S :: paren {{ ichlo [[exp]] }} | ( annot ) exp :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} @@ -1090,7 +1101,7 @@ exp :: 'E_' ::= | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} | return_int ( exp ) :: I :: internal_return {{ com For internal use to embed into monad definition }} | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} - + | constraint n_constraint :: :: constraint i_direction :: 'I' ::= | IInc :: :: Inc | IDec :: :: Dec @@ -1127,7 +1138,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} -{{ com sugared form of above for explicit tuple [[exp]] }} +{{ com sugared form of above for explicit tuple $[[exp]]$ }} | ( typ ) id :: :: cast {{ com cast }} | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} @@ -1271,10 +1282,10 @@ letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} | let typschm pat = exp :: :: val_explicit - {{ com let, explicit type ([[pat]] must be total)}} + {{ com let, explicit type ($[[pat]]$ must be total)}} % at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here | let pat = exp :: :: val_implicit - {{ com let, implicit type ([[pat]] must be total)}} + {{ com let, implicit type ($[[pat]]$ must be total)}} val_spec :: 'VS_' ::= @@ -1379,16 +1390,16 @@ terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} -% | >= :: :: geq -% % {{ tex \ensuremath{\geq} }} + | >= :: :: geq + {{ tex \ensuremath{\geq} }} % {{ tex \ottsym{\textgreater=} }} % {{ com \texttt{>=} }} -% | '<=' :: :: leq -% % {{ tex \ensuremath{\leq} }} + | '<=' :: :: leq + {{ tex \ensuremath{\leq} }} % {{ tex \ottsym{\textless=} }} % {{ com \texttt{<=} }} -% | -> :: :: arrow -% % {{ tex \ensuremath{\rightarrow} }} + | -> :: :: arrow + {{ tex \ensuremath{\rightarrow} }} % {{ tex \ottsym{-\textgreater} }} % {{ com \texttt{->} }} | ==> :: :: Longrightarrow @@ -1415,10 +1426,10 @@ terminals :: '' ::= | emptyset :: :: emptyset {{ tex \ensuremath{\emptyset} }} % | < :: :: lt -% % {{ tex \ensuremath{\langle} }} + {{ tex \ensuremath{\langle} }} % {{ tex \ottsym{<} }} % | > :: :: gt -% % {{ tex \ensuremath{\rangle} }} + {{ tex \ensuremath{\rangle} }} % {{ tex \ottsym{>} }} | lt :: :: mathlt {{ tex < }} diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 7fb54c9a..95e6dba1 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -1,1461 +1,391 @@ -grammar - -formula :: formula_ ::= - | judgement :: :: judgement - - | formula1 .. formulan :: :: dots - - | E_k ( tid ) gives kinf :: :: lookup_k - {{ com Kind lookup }} - {{ hol (FLOOKUP [[E_k]] [[tid]] = SOME [[kinf]]) }} - {{ lem Map.lookup [[tid]] [[E_k]] = Just [[kinf]] }} - - | E_a ( tid ) gives tinf :: :: lookup_a_t - | E_a ( tid ) gives ne :: :: lookup_a_ne - - - | E_t ( id ) gives tinf :: :: lookup_t - {{ com Type lookup }} - {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[tinf]]) }} - {{ lem Map.lookup [[id]] [[E_t]] = Just [[tinf]] }} - | E_t ( id ) gives overload tinf : tinf1 ... tinfn :: :: lookup_over_t - {{ com Overloaded type lookup }} - - | E_k ( tid ) <-| k :: :: update_k - {{ com Update the kind associated with id to k }} - {{ lem [[true]] (*TODO: update_k needs to be rewritten*) }} - - | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r - {{ com Record lookup }} - {{ lem [[true]] (*TODO write a proper lookup for E_r *) }} - - | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt - {{ com Record looup by type }} - {{ lem [[true]] (* write a proper lookup for E_r *) }} - - | E_e ( t ) gives enumerate_map :: :: lookup_e - {{ com Enumeration lookup by type }} - {{ lem Map.lookup [[t]] [[E_e]] = Just [[enumerate_map]] }} - - | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint - {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} - {{ lem disjoint (Map.domain [[E_t1]]) (Map.domain [[E_t2]]) }} - - | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint - {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} - {{ lem disjoint (Map.domain [[E_f1]]) (Map.domain [[E_f2]]) }} - - | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many - {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM - E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }} - {{ lem disjoint_all (List.map Map.domain [[E_t1 .... E_tn]]) }} - {{ com Pairwise disjoint domains }} - - | id NOTIN dom ( E_k ) :: :: notin_dom_k - {{ hol ([[id]] NOTIN FDOM [[E_k]]) }} - {{ lem Pervasives.not (Map.member [[id]] [[E_k]]) }} - | id NOTIN dom ( E_t ) :: :: notin_dom_t - {{ hol ([[id]] NOTIN FDOM [[E_t]]) }} - {{ lem Pervasives.not (Map.member [[id]] [[E_t]]) }} - | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields - {{ lem ((Set.fromList [[id0 t0..idn tn]]) subset (Set.fromList [[id'0 t'0..id'i t'i]])) }} - - | num1 lt ... lt numn :: :: increasing - - | num1 gt ... gt numn :: :: decreasing - - | exp1 == exp2 :: :: exp_eqn - {{ ichl ([[exp1]] = [[exp2]]) }} - - | E_k1 == E_k2 :: :: E_k_eqn - {{ ichl ([[E_k1]] = [[E_k2]]) }} +grammar - | E_k1 ~= E_k2 :: :: E_k_approx - {{ lem ([[E_k1]] = [[E_k2]]) (* Todo, not quite equality *) }} - {{ ich arb }} +mut :: 'mut_' ::= + | immutable :: :: immutable + | mutable :: :: mutable - | E_t1 == E_t2 :: :: E_t_eqn - {{ ichl ([[E_t1]] = [[E_t2]]) }} +lvar :: 'lvar_' ::= + | register typ :: :: register + | enum typ :: :: enum + | local mut typ :: :: local + | union typquant typ :: :: union + | unbound :: :: unbound + - | E_r1 == E_r2 :: :: E_r_eqn - {{ ichl ([[E_r1]] = [[E_r2]]) }} - | E_e1 == E_e2 :: :: E_e_eqn - {{ ichl ([[E_e1]] = [[E_e2]]) }} - - | E_d1 == E_d2 :: :: E_d_eqn - {{ ichl ([[E_d1]] = [[E_d2]]) }} +G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::= {{ com Type environment }} + | empty :: :: empty {{ tex \epsilon }} {{ com Empty context }} + | G , x1 : typ1 , .. , xn : typn :: :: type_list {{ com List of variables and their types }} +% | G , x1 : k1 , .. , xn : kn :: :: kind_list {{ com List of variables and their kinds }} + | G , kid1 , .. , kidn :: :: kid_list +% | G , quant_item1 , .. , quant_itemn :: :: quant_list +% | G , { nec1 , .. , necn } :: :: constraint_list {{ com Constraints }} + | G , G1 .. Gn :: :: merge {{ com Merge or disjoint union }} + | G , id : lvar :: :: add_local - | E1 == E2 :: :: E_eqn - {{ ichl ([[E1]] = [[E2]]) }} - | S_N1 == S_N2 :: :: S_N_eqn - {{ ichl ([[S_N1]] = [[S_N2]]) }} - - | id == 'id :: :: id_eq - | x1 NOTEQ x2 :: :: id_neq - | lit1 NOTEQ lit2 :: ::lit_neq - | I1 == I2 :: :: I_eqn - {{ ichl ([[I1]] = [[I2]]) }} - - | effect1 == effect2 :: :: Ef_eqn - {{ ichl ([[effect1]] = [[effect2]]) }} - - | t1 == t2 :: :: t_eq - {{ ichl ([[t1]] = [[t2]]) }} - | ne == ne' :: :: ne_eq - {{ ichl ([[ne]] = [[ne']]) }} - | kid == fresh_kid ( E_d ) :: :: kid_eq - {{ ichl ([[kid]] = fresh_kid [[E_d]]) }} +formula :: formula_ ::= + | judgement :: :: judgement + | formula1 .. formulan :: :: dots + | G ( id ) = lvar :: :: lookup_id + | G ( typ1 , id ) = typ2 :: :: lookup_record_field + | G ( typ1 ) = typ2 :: :: lookup_typ + | nexp = length [|| exp , exp1 , .. , expn ||] :: :: vector_length + | order_inc :: :: default_order_inc + | order_dec :: :: default_order_dec + | G |= nexp1 <= nexp2 :: :: prove_lteq defns -check_t :: '' ::= + declarative :: '' ::= defn -E_k |-t t ok :: :: check_t :: check_t_ -{{ lemwcf witness type check_t_witness; check check_t_w_check; }} -{{ com Well-formed types }} - by - - E_k('x) gives K_Typ - ------------------------------------------------------------ :: var - E_k |-t 'x ok - - E_k('x) gives K_infer - E_k('x) <-| K_Typ - ------------------------------------------------------------ :: varInfer - E_k |-t 'x ok - - E_k |-t t1 ok - E_k |-t t2 ok - E_k |-e effect ok - ------------------------------------------------------------ :: fn - E_k |-t t1 -> t2 effect ok - - E_k |-t t1 ok .... E_k |-t tn ok - ------------------------------------------------------------ :: tup - E_k |-t (t1 , .... , tn) ok - - E_k(x) gives K_Lam(k1..kn -> K_Typ) - E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok - ------------------------------------------------------------ :: app - E_k |-t x < t_arg1 .. t_argn > ok - -defn -E_k |-e effect ok :: :: check_ef :: check_ef_ -{{ com Well-formed effects }} -{{ lemwcf witness type check_ef_witness; check check_ef_w_check; }} -by - -E_k('x) gives K_Efct ------------------------------------------------------------ :: var -E_k |-e 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Efct ------------------------------------------------------------- :: varInfer -E_k |-e 'x ok - -------------------------------------------------------------- :: set -E_k |-e { base_effect1 , .. , base_effectn } ok - -defn -E_k |-n ne ok :: :: check_n :: check_n_ -{{ com Well-formed numeric expressions }} -{{ lemwcf witness type check_n_witness; check check_n_w_check; }} -by - -E_k(x) gives K_Nat ------------------------------------------------------------ :: id -E_k |-n x ok - -E_k('x) gives K_Nat ------------------------------------------------------------ :: var -E_k |-n 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Nat ------------------------------------------------------------- :: varInfer -E_k |-n 'x ok - ------------------------------------------------------------ :: num -E_k |-n num ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------ :: sum -E_k |-n ne1 + ne2 ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------ :: minus -E_k |-n ne1 - ne2 ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------- :: mult -E_k |-n ne1 * ne2 ok - -E_k |-n ne ok ------------------------------------------------------------- :: exp -E_k |-n 2 ** ne ok - -defn -E_k |-o order ok :: :: check_ord :: check_ord_ -{{ com Well-formed numeric expressions }} -{{ lemwcf witness type check_ord_witness; check check_ord_w_check; }} + G |- typ1 ~< typ2 :: :: subtype :: subtype_ + {{ com $[[typ1]]$ is a subtype of $[[typ2]]$ }} + {{ tex [[G]] \vdash [[typ1]] \preccurlyeq [[typ2]] }} by -E_k('x) gives K_Ord ------------------------------------------------------------ :: var -E_k |-o 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Ord ------------------------------------------------------------- :: varInfer -E_k |-o 'x ok +----------------- :: refl +G |- typ ~< typ ------------------------------------------------------------- :: inc -E_k |-o inc ok - ------------------------------------------------------------- :: dec -E_k |-o dec ok - -defn -E_k , k |- t_arg ok :: :: check_targs :: check_targs_ -{{ com Well-formed type arguments kind check matching the application type variable }} -{{ lemwcf witness type check_targs_witness; check check_targs_w_check; }} -by +--------------------- :: wild +G |- _ ~< _ -E_k |-t t ok ---------------------------------------------------------- :: typ -E_k , K_Typ |- t ok -E_k |-e effect ok ---------------------------------------------------------- :: eff -E_k , K_Efct |- effect ok -E_k |-n ne ok ---------------------------------------------------------- :: nat -E_k , K_Nat |- ne ok +------------- :: id +G |- id ~< id -E_k |-o order ok ---------------------------------------------------------- :: ord -E_k, K_Ord |- order ok +G |- typ1 ~< typ'1 .. G |- typn ~< typ'n +--------------------------------------------------- :: tuple +G |- (typ1 , .. , typn ) ~< (typ'1, .. , typ'n) -defns -convert_kind :: '' ::= defn -E_k |- kind ~> k :: :: convert_kind :: convert_kind_ -{{ lemwcf witness type convert_kind_witness; check convert_kind_w_check; }} +G |-l lit => typ :: :: infer_lit :: infer_lit_ +{{ com Infer that type of $[[lit]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash_l [[lit]] \Rightarrow [[typ]] }} by --------------------- :: Typ -E_k |- Type ~> K_Typ - -defns -convert_typ :: '' ::= - -defn -E_d |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_ -{{ com Convert source quantifiers to kind environments and constraints }} -{{ lemwcf witness type convert_quants_witness; check convert_quants_w_check; }} -by -E_k |- kind ~> k ------------------------------------------------------------ :: kind - |- kind 'x ~> {'x |-> k}, {} +----------------------------- :: unit +G |-l () => unit -E_k('x) gives k ------------------------------------------------------------ :: nokind - |- 'x ~> {'x |-> k},{} +-------------------- :: zero +G |-l bitzero => bit -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: eq -E_d |- nexp1 = nexp2 ~> {}, {ne1 = ne2} +-------------------- :: one +G |-l bitone => bit -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: gteq -E_d |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: lteq -E_d |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} +---------------------- :: num +G |-l num => atom < num > ------------------------------------------------------------ :: in -E_d |- 'x IN {num1 , ... , numn} ~> {}, {'x IN {num1 , ..., numn}} -defn -E_d |- typschm ~> t , E_k , S_N :: :: convert_typschm :: convert_typschm_ -{{ com Convert source types with typeschemes to internal types and kind environments }} -{{ lemwcf witness type convert_typschm_witness; check convert_typschm_w_check; }} -by +---------------------- :: true +G |-l true => bool -E_d |- typ ~> t ------------------------------------------------------------ :: noquant -E_d |- typ ~> t,{},{} -E_d |- quant_item1 ~> E_k1, S_N1 ... E_d |- quant_itemn ~> E_kn, S_Nn -E_k == E_k1 u+ ... u+ E_kn -E_d u+ |- typ ~> t ------------------------------------------------------------ :: quant -E_d |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k, S_N1 u+ ... u+ S_Nn +---------------------- :: false +G |-l false => bool defn -E_d |- typ ~> t :: :: convert_typ :: convert_typ_ -{{ com Convert source types to internal types }} -{{ lemwcf witness type convert_typ_witness; check convert_typ_w_check; }} +G |- lexp := exp => typ -| D :: :: bind_assignment :: bind_assignment_ +{{ com Bind assignment returning updated environment }} +{{ tex [[G]] \vdash [[lexp]] := [[exp]] \Rightarrow [[typ]] \dashv [[D]] }} by - -E_k('x) gives K_Typ ------------------------------------------------------------- :: var - |- 'x ~> 'x - -E_k(x) gives K_Typ ------------------------------------------------------------- :: id - |- x ~> x - -E_d |- typ1 ~> t1 -E_d |- typ2 ~> t2 ------------------------------------------------------------- :: fn -E_d |- typ1->typ2 effectkw effect ~> t1->t2 effect - -E_d |- typ1 ~> t1 .... E_d |- typn ~> tn ------------------------------------------------------------- :: tup -E_d |- ( typ1 , .... , typn ) ~> (t1 , .... , tn) -E_k(x) gives K_Lam (k1..kn -> K_Typ) -,k1 |- typ_arg1 ~> t_arg1 .. ,kn |- typ_argn ~> t_argn ------------------------------------------------------------- :: app - |- x ~> x + +G |- exp => typ +G |- id <= typ -| D +------------------------------- :: id +G |- id := exp => unit -| D defn -E_d , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ -{{ com Convert source type arguments to internals }} -{{ lemwcf witness type convert_targ_witness; check convert_targ_w_check; }} -by - -E_d |- typ ~> t -------------------------------------- :: typ -E_d, K_Typ |- typ ~> t - -defn -|- nexp ~> ne :: :: convert_nexp :: convert_nexp_ -{{ com Convert and normalize numeric expressions }} -{{ lemwcf witness type convert_nexp_witness; check convert_nexp_w_check; }} +G |- pat <= typ -| D :: :: bind_pat :: bind_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} by -------------------------------------------------------------- :: id -|- x ~> x - ------------------------------------------------------------- :: var -|- 'x ~> 'x +G |- lit <= typ +------------------- :: lit +G |- lit <= typ -| G ------------------------------------------------------------- :: num -|- num ~> num +%% FIXME do add_local +G(id) = local mutable typ' +---------------------- :: local +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------- :: mult -|- nexp1 * nexp2 ~> ne1 * ne2 +G(id) = unbound +---------------------- :: unbound +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: add -|- nexp1 + nexp2 ~> ne1 + ne2 -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: sub -|- nexp1 - nexp2 ~> ne1 - ne2 +G(id) = enum typ' +G |- typ' ~< typ +---------------------- :: enum +G |- id <= typ -| G -|- nexp ~> ne ------------------------------------------------------------- :: exp -|- 2** nexp ~> 2 ** ne -defn -E_d |-n ne ~= ne' :: :: conforms_to_ne :: conforms_to_ne_ -by - -E_k |-n ne ok ------------------------------------------------------------- :: refl - |-n ne ~= ne - -E_d |-n ne1 ~= ne2 -E_d |-n ne2 ~= ne3 ------------------------------------------------------------- :: trans -E_d |-n ne1 ~= ne3 +---------------------- :: wild +G |- _ <= typ -| G -E_d |-n ne2 ~= ne1 -------------------------------------------------------------- :: assoc -E_d |-n ne1 ~= ne2 -E_a(x) gives ne - |-n ne ~= ne' ------------------------------------------------------------- :: abbrev - |-n x ~= ne' +%% FIXME Should be fold? +G |- pat1 <= typ1 -| G1 .. G |- patn <= typn -| Gn +------------------------------------------------------- :: tup +G |- (pat1 , .. , patn ) <= (typ1 , .. , typn ) -| G , G1 .. Gn -:formula_ne_eq: num == num' ------------------------------------------------------------ :: constants -E_d |-n num ~= num' ------------------------------------------------------------- :: rest -E_d |-n ne ~= ne' defn -E_d |- t ~= t' :: :: conforms_to :: conforms_to_ -{{ com Relate t and t' when t can be used where t' is expected without consideration for non-constant nats }} +G |- pat => typ -| D :: :: infer_pat :: infer_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} by -E_k |-t t ok ------------------------------------------------------------- :: refl - |- t ~= t - -E_d |- t1 ~= t2 -E_d |- t2 ~= t3 ------------------------------------------------------------- :: trans -E_d |- t1 ~= t3 - ------------------------------------------------------------- :: var -E_d |- 'x ~= t - ------------------------------------------------------------- :: var2 -E_d |- t ~= 'x - -E_a(x) gives u - |- u ~= t ------------------------------------------------------------- :: abbrev - |- x ~= t - -E_a(x) gives u - |- t ~= u ------------------------------------------------------------- :: abbrev2 - |- t ~= x - - -E_d |- t1 ~= u1 .... E_d |- tn ~= un ------------------------------------------------------------- :: tup -E_d |- (t1,....,tn) ~= (u1,....,un) +G(id) = enum typ +-------------------- :: id +G |- id => typ -| G -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -,k1 |- t_arg1 ~= t_arg'1 .. ,kn |- t_argn ~= t_arg'n ------------------------------------------------------------- :: app - |- x ~= x +G |- pat <= typ -| D +------------------------------- :: typ +G |- (typ) pat => typ -| D ------------------------------------------------------------- :: atom -E_d |- atom ~= range ------------------------------------------------------------- :: atom2 -E_d |- range ~= atom - -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u - |- x ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev - |- x < t_arg1 .. t_argn> ~= x' - -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u - |- u [ t_arg1/tid1 .. t_argn/tidn ] ~= x ------------------------------------------------------------- :: appAbbrev2 - |- x' < t_arg1 .. t_argn> ~= x - -E_d |- t ~= u ------------------------------------------------------------- :: register -E_d |- register ~= u - -E_d |- t ~= u ------------------------------------------------------------- :: reg -E_d |- reg ~= u +G |-l lit => typ +----------------------- :: lit +G |- lit => typ -| G defn -E_d , k |- t_arg ~= t_arg' :: :: targconforms :: targconforms_ -{{ lemwcf witness type check_targeq_witness; check check_targeq_w_check; }} +G |-i id => typ :: :: infer_id :: infer_id_ +{{ com Infer type of indentifier }} +{{ tex [[G]] \vdash_i [[id]] \Rightarrow [[typ]] }} by -E_d |- t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |- t ~= t' - -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |- ne ~= ne' - -defn -E_d |-c t ~= t' :: :: conforms_to_upto_coerce :: conforms_to_upto_coerce_ -{{ com Relate t and t' when t can be used where t' is expected upto applying coercions to t }} -by -E_d |- t ~= t' -------------------------------------------------------------- :: base -E_d |-c t ~= t' +G(id) = local mut typ +---------------------- :: local +G |-i id => typ -E_d |-n ne2 ~= one -------------------------------------------------------------- :: bitToVec -E_d |-c bit ~= vector -E_d |-n ne2 ~= one -------------------------------------------------------------- :: vecToBit -E_d |-c vector ~= bit +G(id) = enum typ +---------------------- :: enum +G |-i id => typ -------------------------------------------------------------- :: vecToAtom -E_d |-c vector ~= atom -------------------------------------------------------------- :: vecToRange -E_d |-c vector ~= range +G(id) = register typ +---------------------- :: register +G |-i id => typ -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToRange - |-c x ~= range -E_e(x) gives enumerate_map -------------------------------------------------------------- :: rangeToEnum - |-c range ~= x +G(id) = union typquant typ +------------------------------------- :: union +G |-i id => typ -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToAtom - |-c x ~= atom +defn +G |-f exp . id => typ :: :: infer_field :: infer_field_ +{{ tex [[G]] \vdash_f [[exp]] . [[id]] \Rightarrow [[typ]] }} +by -E_e(x) gives enumerate_map -------------------------------------------------------------- :: atomToEnum - |-c atom ~= x -E_d |-c t1 ~= u1 .... E_d |-c tn ~= un ------------------------------------------------------------- :: tup -E_d |-c (t1,....,tn) ~= (u1,....,un) +G |- exp => typ1 +G ( typ1 ) = register [ id2 ] +G ( id2 ) = (base,top,ranges) +ranges ( id ) = vec_typ +---------------------------- :: register +G |-f exp . id => vec_typ -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -,k1 |-c t_arg1 ~= t_arg'1 .. ,kn |-c t_argn ~= t_arg'n ------------------------------------------------------------- :: app - |-c x ~= x -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u - |-c x ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev - |-c x < t_arg1 .. t_argn> ~= x' +G |- exp => typ1 +G ( typ1 , id ) = typ +---------------------------- :: record +G |-f exp . id => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u - |-c u [ t_arg1/tid1 .. t_argn/tidn ] ~= x ------------------------------------------------------------- :: appAbbrev2 - |-c x' < t_arg1 .. t_argn> ~= x -E_d |-c t ~= u ------------------------------------------------------------- :: register -E_d |-c register ~= u -E_d |-c t ~= u ------------------------------------------------------------- :: reg -E_d |-c reg ~= u defn -E_d , k |-c t_arg ~= t_arg' :: :: targconforms_coerce :: targconforms_coerce_ + G |- exp => typ :: :: infer_exp :: infer_exp_ +{{ com Infer that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Rightarrow [[typ]] }} by -E_d |-c t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |-c t ~= t' -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |-c ne ~= ne' +G |- exp1 <= unit ... G |- expn <= unit +------------------------------------------ :: nondet +G |- nondet { exp1 ; ... ; expn } => unit -defn -E_d |- select ( conformsto ( t , t' ) ) of tinflist gives tinflist' :: :: selectoverload :: so_ -{{ tex [[select]]_{[[conformsto]] ([[t]],[[t']])} ([[tinflist]]) [[gives]] [[tinflist']] }} -by +G |-i id => typ +---------------- :: id +G |- id => typ -E_d |- ti ~= ti' -E_d |- tj' ~= tj -E_d |- select (full(ti,tj)) of tinf0 .. tinfm tinf'0 .. tinf'n gives empty ---------------------------------------------------------- :: full -E_d |- select (full( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag, ti' -> tj' effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> tj' -E_d |- ti ~= ti' -E_d |- select (parm(ti,tj)) of tinf0 .. tinfm gives empty --------------------------------------------------------- :: parm -E_d |- select (parm( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag,ti' -> t effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> t +G |-l lit => typ +---------------- :: lit +G |- lit => typ -defn -E_d , widening |- t ~< t' : t'' , S_N :: :: consistent_typ :: consistent_typ_ -{{ com t is consistent with t' if they match if t can be used where t' is needed after the constraints are solved, with no coercions needed. t'' is the consistent type when widening is required }} -by -E_k |-t t ok ------------------------------------------------------------- :: refl -,widening |- t ~< t:t,{} - -E_d,widening |- t1 ~< t3:t4, S_N1 -E_d,widening |- t4 ~< t2: t5, S_N2 ------------------------------------------------------------- :: trans -E_d,widening |- t1 ~< t2: t5, S_N1 u+ S_N2 - -E_a(x) gives {},S_N1,tag,u -,widening |- u ~< t:t', S_N ------------------------------------------------------------- :: abbrev -,widening |- x ~< t : t', S_N u+ S_N1 - -E_a(x) gives {},S_N1,tag,u -,widening |- t ~< u: t', S_N' ------------------------------------------------------------- :: abbrev2 -,widening |- t ~< x : t', S_N u+ S_N1 - ------------------------------------------------------------- :: var -E_d,widening |- 'x ~< t:t, {} - ------------------------------------------------------------- :: var2 -E_d,widening |- t ~< 'x: t, {} - -E_d,widening |- t1 ~< u1:u'1, S_N1 .... E_d,widening |- tn ~< un:u'n, S_Nn ------------------------------------------------------------- :: tup -E_d,widening |- (t1,....,tn) ~< (u1,....,un): (u'1,....,u'n), S_N1 u+ .... u+ S_Nn +----------------------------------- :: sizeof +G |- sizeof nexp => atom < nexp > ------------------------------------------------------------ :: range -E_d,widening |- range ~< range: range, { ne3 <= ne1, ne2 <= ne4 } +-------------------------------------------- :: constraint +G |- constraint n_constraint => bool ----------------------------------------------------------- :: atomRange -E_d,(nums,_) |- atom ~< range: atom, { ne1 <= ne, ne <= ne2 } +G |-f exp . id => typ +------------------------ :: field +G |- exp . id => typ ----------------------------------------------------------- :: atom -E_d,(none,_) |- atom ~< atom: atom, { ne1 = ne2 } +G |- exp1 => typ1 .... G |- expn => typn +---------------------------------------------------------- :: tuple +G |- ( exp1 , .... , expn ) => (typ1 , .... , typn ) -num1 lt num2 ----------------------------------------------------------- :: atomWidenConst -E_d,(nums,_) |- atom ~< atom: range, {} -num2 lt num1 ---------------------------------------------------------- :: atomWidenConst2 -E_d,(nums,_) |- atom ~< atom: range, {} ----------------------------------------------------------- :: rangeAtom -E_d,widening |- range ~< atom<'x>: atom<'x>, { ne1 <= 'x, 'x <= ne2 } -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vector -E_d,(_,none) |- vector ~< vector : vector, {ne2=ne4, ne1=ne3} u+ S_N +G |- lexp := exp => typ -| D +-------------------- :: assign +G |- lexp := exp => typ -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vectorWiden -E_d,(_,vectors) |- vector ~< vector : vector, {ne2=ne4} u+ S_N -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -,widening,k1 |- t_arg1 ~< t_arg'1,S_N1 .. ,widening,kn |- t_argn ~< t_arg'n,S_Nn ------------------------------------------------------------- :: app -,widening |- x ~< x :x, S_N1 u+ .. u+ S_Nn -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -,widening |- x ~< u [ t_arg'1/tid1 .. t_arg'm/tidm ]: t ,S_N2 ------------------------------------------------------------- :: appAbbrev -,widening |- x < t_arg1 .. t_argn> ~< x' : x', S_N u+ S_N2 +---------------------------- :: record_update +G |- lexp . id := exp => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -,widening |- u [ t_arg'1/tid1 .. t_arg'm/tidm ] ~< x : t ,S_N2 ------------------------------------------------------------- :: appAbbrev2 -,widening |- x' ~< x < t_arg1 .. t_argn> :x, S_N u+ S_N2 -defn -E_d , widening , k |- t_arg ~< t_arg' , S_N :: :: targ_consistent :: targ_consistent_ -by +G |- exp <= typ +----------------------- :: cast +G |- ( typ ) exp => typ -E_d,widening |- t ~< t': t'', S_N ------------------------------------------------------------- :: typ -E_d,widening, K_Typ |- t ~< t',S_N ------------------------------------------------------------ :: nexp -E_d,widening, K_Nat |- ne ~< ne',{ne=ne'} -defn -E_d , widening, t' |- exp : t gives t'' , exp' , S_N , effect :: :: coerce_typ :: coerce_typ_ -{{ lemwcf witness type coerce_typ_witness; check coerce_typ_w_check; }} -by +G |- :E_app: id ( exp1 , exp2 ) => typ +-------------------------------- :: app_infix +G |- exp1 id exp2 => typ -E_d, widening, u1 |- id1 : t1 gives u1, exp1, S_N1,effect1 .. E_d,widening, un|- idn: tn gives un,expn, S_Nn,effectn -exp' == switch exp { case (id1, .., idn) -> (exp1,..,expn) } --------------------------------------- :: tuple -E_d, widening, (u1 , .. , un) |- exp : (t1 , .. , tn) gives (u1 , .. , un), exp', S_N1 u+ .. u+ S_Nn, pure - -E_d,(nums,vectors) |- u ~< t: t',S_N -exp' == (annot) exp -------------------------------------------------- :: vectorUpdateStart -E_d, widening, vector< ne1 ne2 order t > |- exp : vector gives vector , exp', S_N u+ {ne2=ne4}, pure - -E_d, (none,none) |- u ~< bit:bit, S_N -exp' == to_num exp --------------------------------------------------- :: toNum -E_d,widening, range |- exp : vector gives range, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure - -exp' == to_vec exp --------------------------------------- :: fromNum -E_d,widening, vector |- exp: range gives vector,exp', {ne3 = zero, ne4 <= 2** ne2}, pure - -E_d |- typ ~> t -exp' == (typ) exp -E_d,widening, u |- exp':t gives t',exp'', S_N, pure --------------------------------------- :: readReg -E_d,widening, u |- exp : register gives t', exp'', S_N, {rreg} - -exp' == :E_tup_app: msb(exp) --------------------------------------- :: accessVecBit -E_d,widening, bit |- exp : vector gives bit,exp', { ne1=one},pure - -E_d,widening |- range ~< range: t,S_N -exp' == switch exp { case bitzero -> numZero case bitone -> numOne} --------------------------------------- :: bitToNum -E_d,widening, range |- exp : bit gives range, exp',S_N,pure - -E_d,widening |- range ~< range: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBit -E_d, widening, bit |- exp : range gives bit, exp',S_N,pure - -E_d,(nums,none) |- atom ~< range: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBitAtom -E_d,widening, bit |- exp : atom gives bit, exp',S_N,pure - -E_e(x) gives { idi//i/> } -exp' == switch exp { idi//i/> } -ne3 == count( ) ------------------------------------------------- :: toEnumerate -,widening, x |- exp : range gives x,exp', {ne1<=zero,ne2<=ne3},pure - -E_e(x) gives { idi//i/> } -exp' == switch exp { numi//i/> } -ne3 == count( ) -,(nums,none) |- range ~< range:t, S_N ------------------------------------------------- :: fromEnumerate -,widening,range |- exp: x gives range, exp', S_N,pure - -E_d,widening |- t ~< u: u', S_N --------------------------------------- :: eq -E_d,widening, u |- exp: t gives u', exp, S_N,pure +--------------------------------------- :: app +G |- :E_app: id (exp1 , .. , expn ) => typ -defns -check_lit :: '' ::= - -defn -widening , t |- lit : t' => exp , S_N :: :: check_lit :: check_lit_ -{{ com Typing literal constants, coercing to expected type t }} -by - - ------------------------------------------------------------ :: num -widening, range |- num : atom < num > => num , { ne <= num, num <= ne' } - ------------------------------------------------------------ :: numToVec -widening, vector |- num : atom < num > => to_vec num , { num + one <= 2**ne' } +G |- exp1 => bool +G |- exp2 => unit +------------------------------- :: while_loop +G |- while exp1 do exp2 => unit - ------------------------------------------------------------ :: numbitzero -widening, bit |- numZero : atom < zero > => bitzero, {} +G |- exp1 => unit +G |- exp2 => bool +------------------------------- :: until_loop +G |- repeat exp1 until exp2 => unit - ------------------------------------------------------------ :: numbitone -widening, bit |- numOne : atom < one > => bitone, {} - - ------------------------------------------------------------- :: string -widening, string |- :L_string: string : :T_string_typ: string => :E_lit: string, {} +G |- exp1 => range +G |- exp2 => range +G |= nexp1' <= nexp2 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_inc +G |- foreach ( id from exp1 to exp2 by exp3 in inc ) exp4 => unit - ne == bitlength(hex) - ------------------------------------------------------------ :: hex -widening, vector |- hex : vector< ne1 ne order bit> => hex, {ne=ne2} +G |- exp1 => range +G |- exp2 => range +G |= nexp2' <= nexp1 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_dec +G |- foreach ( id from exp1 to exp2 by exp3 in dec ) exp4 => unit -ne == bitlength(bin) - ------------------------------------------------------------ :: bin -widening,vector |- bin : vector< ne1 ne order bit> => bin, {ne=ne2} - ------------------------------------------------------------ :: unit -widening, unit |- () : unit => unit, {} +G |- foreach ( id from exp1 to exp2 by exp3 in inc) exp4 => typ +----------------------------------------------------------------------- :: forup +G |- foreach ( id from exp1 to exp2 by exp3 ) exp4 => typ - ------------------------------------------------------------ :: bitzero -widening, bit |- bitzero : bit => bitzero, {} - ------------------------------------------------------------ :: bitone -widening, bit |- bitone : bit => bitzero, {} +G |- foreach ( id from exp1 to exp2 by numOne in inc) exp3 => typ +----------------------------------------------------------------------- :: forupbyone +G |- foreach ( id from exp1 to exp2 ) exp3 => typ ------------------------------------------------------------- :: undef -widening, t |- undefined : t => undefined, {} -defns -check_pat :: '' ::= - -defn -E , t |- pat : t' gives pat' , E_t , S_N :: :: check_pat :: check_pat_ -{{ com Typing patterns, building their binding environment }} -by +G |- foreach ( id from exp1 to exp2 by exp3 in dec) exp4 => typ +--------------------------------------------------------------------------- :: fordown +G |- foreach ( id from exp1 downto exp2 by exp3 ) exp4 => typ -lit NOTEQ undefined -(none,none),t |- lit : u => lit',S_N -E_d,(nums,none) |- u ~< t: t', S_N' ------------------------------------------------------------- :: lit -, t |- lit : t' gives lit', {}, S_N u+ S_N' - ------------------------------------------------------------- :: wild -E, t |- _ : t gives _, {}, {} - -E,t |- pat : u gives pat',E_t1,S_N -id NOTIN dom(E_t1) ------------------------------------------------------------- :: as -E,t |- (pat as id) : u gives (pat' as id), (E_t1 u+ {id|->t}),S_N - -E_t(id) gives {}, {}, Default, t' -,t' |- pat : t gives pat', E_t1,S_N -E_d,(none,none) |- t' ~< u : u', S_N' ------------------------------------------------------------- :: asDefault -,u |- (pat as id) : t gives (pat' as id), (E_t1 u+ {id|->t'}),S_N u+ S_N' - -E_d |- typ ~> t -,t |- pat : t gives pat',E_t1,S_N ------------------------------------------------------------- :: typ -,u |- (typ) pat : t gives pat',E_t1,S_N - -E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, (u'1,..,u'n) -> x < t_arg1 .. t_argm > pure -(u1,..,un) -> x pure == (u'1,..,u'n) -> x pure [t_arg1/tid1 .. t_argm/tidm] -,u1 |- pat1 : t1 gives pat'1,E_t1,S_N1 .. ,un |- patn : tn gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,vectors) |- x ~< t: t', S_N ------------------------------------------------------------- :: constr -,t |- id(pat1, .., patn) : x gives id(pat'1, ..,pat'n), u+ E_t1 .. E_tn, S_N u+ S_N1 u+ .. u+ S_Nn - - -E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, unit -> x < t_arg1 .. t_argm > pure -unit -> x pure == unit -> x pure [t_arg1/tid1 .. t_argm/tidm] -E_d,(nums,vectors) |- x ~< t: t', S_N -------------------------------------------------------------- :: identConstr -, t |- :P_id: id : t gives :P_id: id, {}, S_N - -E_t(id) gives {},{},Default,t -E_d,(nums,vectors) |- t ~< u: u', S_N ------------------------------------------------------------- :: varDefault -,u |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),S_N - ------------------------------------------------------------- :: var -,t |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),{} - -E_r() gives x< t_args>, () ->,ti |- pati : ui gives pat'i, E_ti,S_Ni//i/> -disjoint doms() -,(nums,vectors) |- x ~< t: t', S_N ------------------------------------------------------------- :: record ->,t |- { semi_opt } : x gives { semi_opt }, :E_t_multi_union: u+ , S_N u+ - -,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn -disjoint doms(E_t1, ... ,E_tn) -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4==length(pat1 ... patn) -S_N ==S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: vector -, vector |- [ pat1, ..., patn ] : vector< ne3 ne4 order u> gives [ pat'1, ..., pat'n ], (E_t1 u+ ... u+ E_tn), S_N u+ S_N' u+ {ne2=ne4} - -,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4 == length(pat1 ... patn) -disjoint doms(E_t1 , ... , E_tn) -num1 lt ... lt numn -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: indexedVectorInc -, vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 inc t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1<=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn - -,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4 == length(pat1 ... patn) -disjoint doms(E_t1 , ... , E_tn) -num1 gt ... gt numn -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: indexedVectorDec -, vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 dec t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1>=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn - -, vector |- pat1 : vector< ne''1 ne'1 order u1> gives pat'1, E_t1,S_N1 ... , vector |- pat1 : vector< ne''n ne'n order u1> gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -disjoint doms(E_t1 , ... , E_tn) -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: vectorConcat -, vector |- pat1 : ... : patn : vector gives pat'1 : ... : pat'n, (E_t1 u+ ... u+ E_tn),{ne'1 + ... + ne'n <= ne2} u+ S_N u+ S_N' - -E,t1 |- pat1 : u1 gives pat'1,E_t1,S_N1 .... E,tn |- patn : un gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------- :: tup -E,(t1, .... , tn) |- (pat1, ...., patn) : (u1 , .... , un) gives (pat'1, .... , pat'n), (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn - -,t |- pat1 : u1 gives pat'1,E_t1,S_N1 .. ,t |- patn : un gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,none) |- u1 ~< t:t',S_N'1 .. E_d,(nums,none) |- un ~< t:t',S_N'n -disjoint doms(E_t1 , .. , E_tn) -S_N == S_N1 u+ .. u+ S_Nn -S_N' == S_N'1 u+ .. u+ S_N'n ------------------------------------------------------------- :: list -, list |- [||pat1, .., patn ||] : list< t> gives [|| pat'1, .. , pat'n ||],(E_t1 u+ .. u+ E_tn),S_N u+ S_N' +G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3 => typ +------------------------------------------------------------------------- :: fordownbyone +G |- foreach ( id from exp1 downto exp2 ) exp3 => typ -defns -check_exp :: '' ::= - -defn -E , t , widening |- exp : t' gives exp' , I , E_t :: :: check_exp :: check_exp_ -{{ com Typing expressions, collecting nexp constraints, effects, and new bindings }} -by +G |- exp1 => (flows,constrs) +G , flows , constrs |- exp2 => typ +G , flows , negate constrs |- exp3 <= typ +-------------------------------------------- :: if +G |- if exp1 then exp2 else exp3 => typ -E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, unit -> x pure -u == x [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N ------------------------------------------------------------ :: unaryCtor -,t,widening |- id : x gives id, ,{} - -E_t(id) gives {}, {},tag,u -E_d,widening,t |- id : u gives t', exp, S_N, effect ------------------------------------------------------------- :: localVar -,t,widening |- id : u gives id, ,{} - -E_t(id) gives {tid1|->kinf1, .., tidn |-> kinfn}, S_N,tag,u' -u == u'[t_arg1/tid1 .. t_argn/tidn] -E_d,widening,t |- id : u gives t', exp, S_N', effect ------------------------------------------------------------- :: otherVar -,t,widening |- id : u gives id,,{} - -E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, t'' -> x pure -t' -> u pure == t'' -> x pure [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N -,t,widening |- exp : u' gives exp, ,E_t' ------------------------------------------------------------- :: ctor -,t,widening |- :E_app: id(exp) : t gives :E_app: id(exp'), ,{} - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -ui == ( implicit, t0 , .. , tm ) -,(t0,..,tm),widening |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' -E_d,widening,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: appImplicit -,t,widening |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ u+ , E_t - - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -,ui,widening |- exp : ui' gives exp',I,E_t' -E_d,widening,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: app -,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ u+ , E_t - -E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -,ui,widening |- exp : ui' gives exp',I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t,widening |- :E_app: id (exp) : t' gives exp'',I', E_t'' ------------------------------------------------------------- :: appOverload -,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ I' u+ u+ , E_t - -E_t(id) gives {tid0 |-> kinf0, .. ,tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d,widening,t |- :E_app_infix: exp1' id exp2' : uj gives uj', exp, S_N', effect' ------------------------------------------------------------- :: infix_app -,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ u+ , E_t - -E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t, widening |- :E_app_infix: exp1 id exp2 : t' gives exp, I',E_t'' ------------------------------------------------------------- :: infix_appOverload -,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ I u+ u+ , E_t - - -E_r() gives x, ->,ti,widening |- expi : ui gives exp'i,,E_t//i/> -,widening |- ui ~< ti: t'i,S_N'i//i/> -S_N == u+ -S_N' == u+ ------------------------------------------------------------- :: record ->,t,widening |- { semi_opt} : x gives{ semi_opt}, u+ >, {} - ->,t,widening |- exp : x gives exp', I,E_t -E_r(x) gives ->,ti,widening |- expi : ui gives expi',Ii,E_t//i/> - SUBSET -,widening |- ui ~< ti: t''i,S_N'i//i/> ------------------------------------------------------------- :: recup -> ,t,widening |- { exp with semi_opt } : x gives {exp' with }, I u+ , E_t - -,t,(nums,none) |- exp1 : u1 gives exp'1,I1,E_t' ... ,t,(nums,none) |- expn : un gives exp'n,In,E_t' -E_d,(nums,none) |- u1 ~< t: t', S_N1 ... E_d,(nums,none) |- un ~< t: t', S_Nn -length(exp1 ... expn) == ne -S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------- :: vector -E, vector, widening |- [ exp1 , ... , expn ] : vector gives [exp'1,...,exp'n], u+ I1 u+ ... u+ In , E_t - -E, vector,(nums,none) |- exp1 : vector gives exp'1,I1,E_t -E, range,(none,vectors) |- exp2 : range gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetInc -E, t,widening |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1<=ne3,ne3+ne3'<=ne1+ne1'},pure>,E_t - -E, vector,(nums,none) |- exp1 : vector gives exp'1,I1,E_t -E, range,(none,vectors) |- exp2 : range gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetDec -E, t,widening |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1>=ne3,ne3+(-ne3')<=ne1+(-ne1')},pure>,E_t - -E, vector,(nums,none) |- exp1 : vector gives exp'1, I1,E_t -E, range,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range ,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubInc -E, vector,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t - -E, vector,(nums,none) |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t -E, range,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range ,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubDec -E, vector,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t - -E, vector,(nums,none) |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t -E, range,(none,vectors) |- exp1 : range gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupInc -E, vector,widening |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 inc u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne2 >= ne4},pure>,E_t - -E, vector,(nums,none) |- exp : vector gives exp',I,E_t -E, range,(none,vectors) |- exp1 : range gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupDec -E, vector,widening |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 dec u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 >= ne3, ne2 >= ne4},pure>,E_t - -E,vector,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom,(none,vectors) |- exp1 : atom gives exp1',I1,E_t -E,atom,(none,vectors) |- exp2 : atom gives exp2', I2,E_t -E,vector,(nums,vectors) |- exp3 : vector gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> ------------------------------------------------------------- :: vecrangeupInc -E,vector,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom,(none,vectors) |- exp1 : atom gives exp1',I1,E_t -E,atom,(none,vectors) |- exp2 : atom gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> ------------------------------------------------------------- :: vecrangeupvalueInc -E,vector,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom,(none,vectors) |- exp1 : atom gives exp1',I1,E_t -E,atom,(none,vectors) |- exp2 : atom gives exp2', I2,E_t -E,vector,(nums,vectors) |- exp3 : vector gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupDec -E,vector,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom,(none,vectors) |- exp1 : atom gives exp1',I1,E_t -E,atom,(none,vectors) |- exp2 : atom gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupvalueDec -E,vector,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E_r (x) gives id : u ->,t'',widening |- exp : x< t_args> gives exp', I,E_t -E_d,widening,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------- :: field ->,t,widening |- exp.id : u gives exp1',I u+ ,E_t - -,t'',widening |- exp : u gives exp',I,E_t -,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/> -,t,widening |- expi : u''i gives exp'i,Ii,E_t'i//i/> ------------------------------------------------------------- :: case -,t,widening |- switch exp { expi//i/> }: u gives switch exp' { exp'i//i/> }, I u+ //i/>, E_t - -,t'',widening |- exp : u gives exp',I,E_t -E_d |- typ ~> t' -E_d,widening,t' |- exp' : u gives u', exp'', S_N,effect -E_d,widening,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------- :: typed -,t,widening |- (typ) exp : t gives exp''',I u+ ,E_t - - |- letbind gives letbind', E_t1, S_N, effect, {} -<(E_t u+ E_t1),E_d>,t,widening |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------- :: let -,t,widening |- letbind in exp : t gives letbind' in exp', u+ I2, E_t - -E,t1,widening |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn,widening |- expn : un gives expn',In,E_tn ------------------------------------------------------------- :: tup -E,(t1, ...., tn),widening |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t - -,t,(nums,none) |- exp1 : u1 gives exp1', I1,E_t1 .. ,t,(nums,none) |- expn : un gives expn', In,E_tn -E_d,(nums,none) |- u1 ~< t:t',S_N1 .. E_d,(nums,none) |- un ~< t:t',S_Nn ------------------------------------------------------------- :: list -,list,widening |- [||exp1, .., expn ||] : list gives [|| exp1', .., expn' ||], u+ I1 u+ .. u+ In, E_t - -E,bit,widening |- exp1 : bit gives exp1',I1,E_t' -E,t,widening |- exp2 : u1 gives exp2',I2,E_t2 -E,t,widening |- exp3 : u2 gives exp3',I3,E_t3 -E_d,widening |- u1 ~< t:t',S_N1 -E_d,widening |- u2 ~< t:t',S_N2 ------------------------------------------------------------- :: if -,t,widening |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) - -,range,widening |- exp1 : range< ne7 ne8> gives exp1', I1,E_t -,range,widening |- exp2 : range< ne9 ne10> gives exp2', I2,E_t -,range,widening |- exp3 : range< ne11 ne12> gives exp3',I3,E_t -<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit,widening |- exp4 : t gives exp4',I4,E_t' ------------------------------------------------------------ :: for -,unit,widening |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t - -E,t,widening |- exp1 : u gives exp1',I1,E_t -E,list,widening |- exp2 : list gives exp2',I2,E_t ------------------------------------------------------------- :: cons -E,list,widening |- exp1 :: exp2 : list gives exp1'::exp2', I1 u+ I2,E_t - -widening,t |- lit : u => exp,S_N ------------------------------------------------------------- :: lit -E,t,widening |- lit : u gives exp,,E_t - -,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: blockbase -,unit,widening |- { exp } : unit gives {exp'}, I, E_t - -,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- { } : unit gives {}, I2, E_t2 ------------------------------------------------------------- :: blockrec -,unit,widening |- { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t - -,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: nondetbase -,unit,widening |- nondet { exp } : unit gives {exp'}, I, E_t - -,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- nondet { } : unit gives {}, I2, E_t2 ------------------------------------------------------------- :: nondetrec -,unit,widening |- nondet { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t - -E,t,widening |- exp:u gives exp', I1, E_t1 -E,widening |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------- :: assign -E,unit,widening |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 +G |- :E_app: vector_access ( exp , exp' ) => typ +------------------------------ :: vector_access +G |- exp [ exp' ] => typ -defn -E , widening |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ -{{ com Check the left hand side of an assignment }} -by -E_t(id) gives register ----------------------------------------------------------- :: wreg -,widening |- id : t gives id,<{},{ wreg }>, E_t - -E_t(id) gives reg ----------------------------------------------------------- :: wlocl -,widening |- id : t gives id,Ie, E_t - -E_t(id) gives t ----------------------------------------------------------- :: var -,widening |- id : t gives id,Ie,E_t - -id NOTIN dom(E_t) ----------------------------------------------------------- :: wnew -,widening |- id : t gives id,Ie, {id |-> reg} - -E_t(id) gives register -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wregCast -,widening |- (typ) id : t gives id,, E_t - -E_t(id) gives reg -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wloclCast -,widening |- (typ) id : t gives id,, E_t - -E_t(id) gives t -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: varCast -,widening |- (typ) id : t gives id,,E_t - -id NOTIN dom(E_t) -E_d |- typ ~> t ----------------------------------------------------------- :: wnewCast -, widening |- (typ) id : t gives id,Ie, {id |-> reg} - - -E_t(id) gives E_k, S_N, Extern, (t1, .. ,tn, t) -> t' {, wmem, } -,(t1, .. , tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wmem -,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ ,E_t - -E_t(id) gives E_k, S_N, Extern, (t1, ..,tn,t) -> t' {, wreg, } -,(t1,..,tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wregCall -,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ ,E_t - -E,atom,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector gives lexp',I2,E_t ----------------------------------------------------------- :: wbitInc -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t - -E,atom,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector gives lexp',I2,E_t ----------------------------------------------------------- :: wbitDec -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t - -E,atom,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceInc -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne3<=ne1, ne3+ne4<= ne2 + (-ne1)},pure> ,E_t - -E,atom,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceDec -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne1<=ne3, ne3 + (-ne4)<= ne1 + (-ne2)},pure> ,E_t - - -E_r (x) gives id : t ->,widening |- lexp : x gives lexp',I,E_t ----------------------------------------------------------- :: wrecord ->,widening |- lexp.id : t gives lexp'.id,I,E_t +G |- :E_app: vector_subrange ( exp , exp1 , exp2 ) => typ +--------------------------- :: vector_subrange +G |- exp [ exp1 .. exp2 ] => typ -defn -E |- letbind gives letbind' , E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ -{{ com Build the environment for a let binding, collecting index constraints }} -by - - |- typschm ~> t,E_k2,S_N ->,t |- pat : u gives pat',E_t1, S_N1 ->,t,(none,none) |- exp : u' gives exp', ,E_t2 -,(none,none) |- u' ~< u, S_N3 ------------------------------------------------------------- :: val_annot -> |- let typschm pat = exp gives let typschm pat' = exp', E_t1, S_N u+ S_N1 u+ S_N2 u+ S_N3, effect, E_k2 - -,t |- pat : u gives pat',E_t1,S_N1 -<(E_t u+ E_t1),E_d>,u |- exp : u' gives exp',,E_t2 ------------------------------------------------------------- :: val_noannot - |- let pat = exp gives let pat' = exp', E_t1, S_N1 u+ S_N2, effect,{} -defns -check_defs :: '' ::= - -defn -E_d |- type_def gives E :: :: check_td :: check_td_ -{{ com Check a type definition }} -by +G |- :E_app: vector_update ( exp , exp1 , exp2 ) => typ +---------------------------------- :: vector_update +G |- :E_vector_update: [ exp with exp1 = exp2] => typ -E_d |- typschm ~> t,E_k,S_N ------------------------------------------------------------ :: abbrev -E_d |- typedef id name_scm_opt = typschm gives <{},<{},{id |-> E_k, S_N, None,t},{},{}>> - -E_d |- typ1 ~> t1 .. E_d |- typn ~> tn -E_r == { {id1:t1, .., idn:tn} |-> x } ------------------------------------------------------------ :: unquant_record -E_d |- typedef x name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{x |-> K_Typ},{},E_r,{}>> - - |- quant_itemi ~>E_ki, S_Ni//i/> -,E_a,E_r,E_e> |- typ1 ~> t1 .. ,E_a,E_r,E_e> |- typn ~> tn -{ x'1 |-> k1, .. ,x'm |-> km } == u+ -E_r1 == { {id1:t1, .., idn:tn} |-> {x'1 |-> k1, ..,x'm |-> km}, u+, None, x< :t_arg_typ: x'1 .. :t_arg_typ: x'm> } -E_k1' == { x |-> K_Lam (k1 .. km -> K_Typ) } ------------------------------------------------------------ :: quant_record - |- typedef x name_scm_opt = const struct forall . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},> - -E_t == { id1 |-> {},{},Ctor,t1 -> x pure , ..., idn |-> {},{},Ctor, tn -> x pure } -E_k1 == { x |-> K_Typ } - |- typ1 ~> t1 ... |- typn ~> tn ------------------------------------------------------------- :: unquant_union - |- typedef x name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives > - - |- quant_itemi ~> E_ki, S_Ni//i/> -{ x'1 |-> k1, ... , x'm |-> km } == u+ -E_k' == { x |-> K_Lam (k1 ... km -> K_Typ) } u+ - |- typ1 ~> t1 ... |- typn ~> tn -t == x < :t_arg_typ: x'1 ... :t_arg_typ: x'm> -E_t == { id1 |-> E_k', u+, Ctor, t1 -> t pure, ... , idn |-> E_k', u+, Ctor, tn -> t pure } ------------------------------------------------------------- :: quant_union - |- typedef id name_scm_opt = const union forall . { typ1 id1 ; ... ; typn idn semi_opt } gives > - -% Save these as enumerations for coercion -E_t == {id1 |-> x, ..., idn |-> x} -E_e == { x |-> { num1 |-> id1 ... numn |-> idn} } -------------------------------------------------------------- :: enumerate -E_d |- typedef x name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives K_Typ},{},{},E_e>> -defn -E |- fundef gives fundef' , E_t , S_N :: :: check_fd :: check_fd_ -{{ com Check a function definition }} -by +G |- :E_app: vector_update_subrange ( exp , exp1 , exp2 , exp3 ) => typ +------------------------------------------ :: vector_update_subrange +G |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] => typ -E_t(id) gives E_k',S_N',Global, t1 -> t effect - E_ki,S_Ni//i/> -S_N'' == u+ -E_k' == -E_d1 == u+ E_d -E_d1 |- typ ~> u -E_d1 |- u ~< t, S_N2 -,t1 |- patj : uj gives patj',E_tj,S_N'''j//j/> -,u |- expj : u' gives expj',,E_t'j//j/> -S_N''''' == S_N2 u+ -effect == u+ -S_N == resolve ( S_N' u+ S_N'' u+ S_N''''') -------------------------------------------------------------- :: rec_function - |- function rec forall . typ effectkw effect gives function rec forall . typ effectkw effect ,E_t, S_N - -E_t(id) gives E_k', S_N', Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -,t1 |- patj : uj gives pat',E_tj,S_N''j//j/> -,u |- expj : uj' gives expj',,E_t'j//j/> -effect == u+ -S_N == resolve (S_N2 u+ S_N' u+ ) -------------------------------------------------------------- :: rec_function2 - |- function rec typ effectkw effect gives function rec typ effectkw effect ,E_t, S_N - - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ -E_k' == E_k u+ - |- typ ~> t ->, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k', S_N', Global, t1 -> t effect}) ->,t |- expj : u'j gives expj', ,E_t'j//j/> -effect == u+ -S_N == resolve (S_N' u+ ) -------------------------------------------------------------- :: rec_function_no_spec -> |- function rec forall . typ effectkw effect gives function rec forall . typ effectkw effect , E_t', S_N - -E_d |- typ ~> t -, t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {}, {}, Global, t1 -> t effect}) -,t |- expj : uj' gives expj', ,E_t'j//j/> -effect == u+ -S_N == resolve (u+ ) -------------------------------------------------------------- :: rec_function_no_spec2 - |- function rec typ effectkw effect gives function rec typ effectkw effect , E_t', S_N - -E_t(id) gives E_k',S_N',Global, t1 -> t effect - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' == u+ -E_k'' == - |- typ ~> u - |- u ~< t, S_N2 ->, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> ->,t |- expj : uj' gives expj', ,E_t'j//j/> -S_N'''' == u+ -effect == u+ -S_N == resolve ( S_N' u+ S_N'' u+ S_N'''') -------------------------------------------------------------- :: function -> |- function forall . typ effectkw effect gives function forall . typ effectkw effect , E_t, S_N - -E_t(id) gives {}, S_N1, Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -,t1 |- patj : uj gives patj,E_tj,S_N'j//j/> -, u |- expj : uj' gives expj', ,E_t'j//j/> -effect == u+ -S_N == resolve (S_N1 u+ S_N2 u+ ) -------------------------------------------------------------- :: function2 - |- function typ effectkw effect gives function typ effectkw effect , E_t, S_N - - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ -E_k'' == E_k u+ - |- typ ~> t ->,t1 |- patj : uj gives patj,E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k'', S_N', Global, t1 -> t effect}) ->,t |- expj : uj' gives expj', ,E_t'j//j/> -effect == u+ -S_N == resolve (S_N' u+ ) -------------------------------------------------------------- :: function_no_spec -> |- function forall . typ effectkw effect gives function forall . typ effectkw effect , E_t', S_N - -E_d |- typ ~> t -,t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {},S_N, Global, t1 -> t effect}) -,t |- expj : uj' gives exp', ,E_t'j//j/> -effect == u+ -S_N == resolve (u+ ) -------------------------------------------------------------- :: function_no_spec2 - |- function typ effectkw effect gives function typ effectkw effect , E_t', S_N +G |- :E_app: vector_append ( exp1 , exp2 ) => typ +----------------------------------- :: vector_append +G |- exp1 : exp2 => typ -defn -E |- val_spec gives E_t :: :: check_spec :: check_spec_ -{{ com Check a value specification }} -by -E_d |- typschm ~> t, E_k1, S_N --------------------------------------------------------- :: val_spec - |- val typschm id gives {id |-> E_k1,S_N,Global,t } +order_inc +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_inc +G |- [|| exp , exp1 , .. , expn ||] => typ [ numZero <: nexp ] -E_d |- typschm ~> t, E_k1, S_N --------------------------------------------------------- :: extern - |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} +order_dec +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_dec +G |- [|| exp , exp1 , .. , expn ||] => typ [ nexp :> numZero ] -defn -E_d |- default_spec gives E_t , E_k1 :: :: check_default :: check_default_ -{{ com Check a default typing specification }} -by -E_k |- base_kind ~> k ------------------------------------------------------------- :: kind - |- default base_kind 'x gives {}, {'x |-> k default } +G |- exp1 <= bool +G |- exp2 <= string +----------------------------------- :: assert +G |- assert (exp1, exp2 ) => unit -E_d |- typschm ~> t,E_k1,S_N ------------------------------------------------------------- :: typ -E_d |- default typschm id gives {id |-> E_k1,S_N,Default,t},{} defn - -E |- def gives def' , E' :: :: check_def :: check_def_ -{{ com Check a definition }} + G |- exp <= typ :: :: check_exp :: check_exp_ +{{ com Check that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Leftarrow [[typ]] }} by -E_d |- type_def gives E ---------------------------------------------------------- :: tdef -|- type_def gives type_def, u+ E -E |- fundef gives fundef', E_t,S_N ---------------------------------------------------------- :: fdef -E |- fundef gives fundef', E u+ +G |- exp1 <= unit ... G |- expn <= unit +G |- exp <= typ +----------------------------------- :: block +G |- { exp1; ... ; expn ; exp } <= typ -E |- letbind gives letbind', {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k -S_N1 == resolve(S_N) ---------------------------------------------------------- :: vdef -E |- letbind gives letbind', E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty> -E |- val_spec gives E_t ---------------------------------------------------------- :: vspec -E |- val_spec gives val_spec, E u+ -E_d |- default_spec gives E_t1, E_k1 ---------------------------------------------------------- :: default - |- default_spec gives default_spec, <(E_t u+ E_t1),E_d u+ > - -E_d |- typ ~> t ----------------------------------------------------------- :: register - |- register typ id gives register typ id, <(E_t u+ {id |-> register}),E_d> - -%TODO Add alias checking - -defn -E |- defs gives defs' , E' :: :: check_defs :: check_defs_ -{{ com Check definitions, potentially given default environment of built-in library }} -by - -:check_def: E |- def gives def', E1 -E u+ E1 |- gives , E2 ------------------------------------------------------------- :: defs -E |- def gives def' , E2 + -- cgit v1.2.3 From 74b6c74b7407f7141796cb109c750f86659d1d2d Mon Sep 17 00:00:00 2001 From: Mark Wassell Date: Mon, 23 Oct 2017 10:48:05 +0100 Subject: Aligning Ott generated AST with actual ast.ml. Almost a drop-in replacement but problem with aux introduced 'a type variables --- language/l2.ml | 471 +++++++++++++++---------------------------- language/l2.ott | 542 +++++++++++--------------------------------------- language/l2_rules.ott | 39 +++- 3 files changed, 314 insertions(+), 738 deletions(-) (limited to 'language') diff --git a/language/l2.ml b/language/l2.ml index 13cb2567..8f041dc7 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,18 +1,33 @@ -(* generated by Ott 0.25 from: l2.ott *) +(* generated by Ott 0.26 from: l2.ott *) +type text = string + +type l = Parse_ast.l + type 'a annot = l * 'a +type loop = While | Until + -type x = string (* identifier *) -type ix = string (* infix identifier *) +type x = text (* identifier *) +type ix = text (* infix identifier *) type base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effect (* kind of effect sets *) + + +type +base_kind = + BK_aux of base_kind_aux * Parse_ast.l + + +type +kind_aux = (* kinds *) + K_kind of (base_kind) list type @@ -21,14 +36,14 @@ kid_aux = (* kinded IDs: $_$, $_$, $_$, and $_$ variables *) type -id_aux = (* identifier *) +id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) type -base_kind = - BK_aux of base_kind_aux * Parse_ast.l +kind = + K_aux of kind_aux * Parse_ast.l type @@ -41,31 +56,6 @@ id = Id_aux of id_aux * Parse_ast.l -type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type -nexp_aux = (* numeric expression, of kind $_$ *) - Nexp_id of id (* abbreviation identifier *) - | Nexp_var of kid (* variable *) - | Nexp_constant of int (* constant *) - | Nexp_times of nexp * nexp (* product *) - | Nexp_sum of nexp * nexp (* sum *) - | Nexp_minus of nexp * nexp (* subtraction *) - | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* for internal use only *) - -and nexp = - Nexp_aux of nexp_aux * Parse_ast.l - - -type -kind = - K_aux of kind_aux * Parse_ast.l - - type base_effect_aux = (* effect *) BE_rreg (* read register *) @@ -87,6 +77,21 @@ base_effect_aux = (* effect *) | BE_lret (* local return; not user-writable *) +type +nexp_aux = (* numeric expression, of kind $_$ *) + Nexp_id of id (* abbreviation identifier *) + | Nexp_var of kid (* variable *) + | Nexp_constant of int (* constant *) + | Nexp_times of nexp * nexp (* product *) + | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction *) + | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* for internal use only *) + +and nexp = + Nexp_aux of nexp_aux * Parse_ast.l + + type base_effect = BE_aux of base_effect_aux * Parse_ast.l @@ -115,14 +120,6 @@ effect = Effect_aux of effect_aux * Parse_ast.l -type -n_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of nexp * nexp - | NC_bounded_ge of nexp * nexp - | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of kid * (int) list - - type kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) @@ -130,13 +127,24 @@ kinded_id_aux = (* optionally kind-annotated identifier *) type -n_constraint = - NC_aux of n_constraint_aux * Parse_ast.l +kinded_id = + KOpt_aux of kinded_id_aux * Parse_ast.l type -kinded_id = - KOpt_aux of kinded_id_aux * Parse_ast.l +n_constraint_aux = (* constraint over kind $_$ *) + NC_equal of nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_not_equal of nexp * nexp + | NC_set of kid * (int) list + | NC_or of n_constraint * n_constraint + | NC_and of n_constraint * n_constraint + | NC_true + | NC_false + +and n_constraint = + NC_aux of n_constraint_aux * Parse_ast.l type @@ -146,19 +154,23 @@ quant_item_aux = (* kinded identifier or $_$ constraint *) type -quant_item = - QI_aux of quant_item_aux * Parse_ast.l - - -type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* empty *) +lit_aux = (* literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) + | L_real of string type -typquant = - TypQ_aux of typquant_aux * Parse_ast.l +quant_item = + QI_aux of quant_item_aux * Parse_ast.l type @@ -168,6 +180,7 @@ typ_aux = (* type expressions, of kind $_$ *) | Typ_var of kid (* type variable *) | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple *) + | Typ_exist of (kid) list * n_constraint * typ | Typ_app of id * (typ_arg) list (* type constructor application *) and typ = @@ -177,49 +190,20 @@ and typ_arg_aux = (* type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order - | Typ_arg_effect of effect and typ_arg = Typ_arg_aux of typ_arg_aux * Parse_ast.l -type -lit_aux = (* literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_string of string (* string constant *) - | L_undef (* undefined-value constant *) - - -type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ - - -type -index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - BF_aux of index_range_aux * Parse_ast.l - - type lit = L_aux of lit_aux * Parse_ast.l type -typschm = - TypSchm_aux of typschm_aux * Parse_ast.l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* empty *) type @@ -229,13 +213,14 @@ type | P_as of 'a pat * id (* named pattern *) | P_typ of typ * 'a pat (* typed pattern *) | P_id of id (* identifier *) + | P_var of 'a pat * kid (* bind pattern to type variable *) | P_app of id * ('a pat) list (* union constructor pattern *) | P_record of ('a fpat) list * bool (* struct pattern *) | P_vector of ('a pat) list (* vector pattern *) - | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *) | P_vector_concat of ('a pat) list (* concatenated vector pattern *) | P_tup of ('a pat) list (* tuple pattern *) | P_list of ('a pat) list (* list pattern *) + | P_cons of 'a pat * 'a pat (* Cons patterns *) and 'a pat = P_aux of 'a pat_aux * 'a annot @@ -247,6 +232,11 @@ and 'a fpat = FP_aux of 'a fpat_aux * 'a annot +type +typquant = + TypQ_aux of typquant_aux * Parse_ast.l + + type name_scm_opt_aux = (* optional variable naming-scheme constraint *) Name_sect_none @@ -259,6 +249,11 @@ type_union_aux = (* type union constructors *) | Tu_ty_id of typ * id +type +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ + + type name_scm_opt = Name_sect_aux of name_scm_opt_aux * Parse_ast.l @@ -269,14 +264,24 @@ type_union = Tu_aux of type_union_aux * Parse_ast.l +type +typschm = + TypSchm_aux of typschm_aux * Parse_ast.l + + +type +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * Parse_ast.l + + type 'a kind_def_aux = (* Definition body for elements of kind *) KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression abbreviation *) - | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) - | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) - | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type @@ -298,165 +303,11 @@ type TD_aux of 'a type_def_aux * 'a annot -type -ne = (* internal numeric expressions *) - Ne_id of x - | Ne_var of x - | Ne_const of int - | Ne_inf - | Ne_mult of ne * ne - | Ne_add of (ne) list - | Ne_minus of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type -t = (* Internal types *) - T_id of x - | T_var of x - | T_fn of t * t * effect - | T_tup of (t) list - | T_app of x * t_args - | T_abbrev of t * t - -and t_arg = (* Argument to type constructors *) - T_arg_typ of t - | T_arg_nexp of ne - | T_arg_effect of effect - | T_arg_order of order - -and t_args = (* Arguments to type constructors *) - T_args of (t_arg) list - - -type -k = (* Internal kinds *) - Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_ctor of (k) list * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type -tid = (* A type identifier or type variable *) - Tid_id of id - | Tid_var of kid - - -type -kinf = (* Whether a kind is default or from a local binding *) - Kinf_k of k - | Kinf_def of k - - -type -nec = (* Numeric expression constraints *) - Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * (int) list - | Nec_cond of (nec) list * (nec) list - | Nec_branch of (nec) list - - -type -tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) - Tag_empty - | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) - | Tag_set (* Denotes an expression that mutates a local variable *) - | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) - | Tag_global (* Globally let-bound or enumeration based value/variable *) - | Tag_ctor (* Data constructor from a type union *) - | Tag_extern of string option (* External function, specied only with a val statement *) - | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) - | Tag_spec - | Tag_enum of int - | Tag_alias - | Tag_unknown of string option (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) - - -type -tinf = (* Type variables, type, and constraints, bound to an identifier *) - Tinf_typ of t - | Tinf_quant_typ of e_k * s_N * tag * t - - -type -conformsto = (* how much conformance does overloading need *) - Conformsto_full - | Conformsto_parm - - -type -widennum = - Widennum_widen - | Widennum_dont - | Widennum_dontcare - - -type -widenvec = - Widenvec_widen - | Widenvec_dont - | Widenvec_dontcare - - -type -widening = (* Should we widen vector start locations, should we widen atoms and ranges *) - Widening_w of widennum * widenvec - - -type -tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) - Tinfs_empty - | Tinfs_ls of (tinf) list - - -type -i = (* Information given by type checking an expression *) - I of s_N * effect - | Iempty (* Empty constraints, effect *) - | Singleunion of i * i - | Iunion of (i) list (* Unions the constraints and effect *) - - -type -e = (* Definition environment and lexical environment *) - E of e_t * e_d - | E_union of e * e - - -type -i_direction = - IInc - | IDec - - type 'a reg_id_aux = RI_id of id -type -ctor_kind = - C_Enum of nat - | C_Union - - -type -reg_form = - Form_Reg of id * tannot * i_direction - | Form_SubReg of id * reg_form * index_range - - -type -'a reg_id = - RI_aux of 'a reg_id_aux * 'a annot - - type 'a exp_aux = (* expression *) E_block of ('a exp) list (* sequential block *) @@ -468,6 +319,8 @@ type | E_app_infix of 'a exp * id * 'a exp (* infix function application *) | E_tuple of ('a exp) list (* tuple *) | E_if of 'a exp * 'a exp * 'a exp (* conditional *) + | E_loop of loop * 'a exp * 'a exp + | E_until of 'a exp * 'a exp | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *) | E_vector of ('a exp) list (* vector (indexed from 0) *) | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *) @@ -484,10 +337,12 @@ type | E_case of 'a exp * ('a pexp) list (* pattern matching *) | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) - | E_sizeof of nexp (* the value of nexp at run time *) - | E_return of 'a exp (* return 'a exp from current function *) + | E_sizeof of nexp (* the value of $nexp$ at run time *) + | E_return of 'a exp (* return $'a exp$ from current function *) | E_exit of 'a exp (* halt all current execution *) - | E_assert of 'a exp * 'a exp (* halt with error 'a exp when not 'a exp *) + | E_throw of 'a exp + | E_try of 'a exp * ('a pexp) list + | E_assert of 'a exp * 'a exp (* halt with error $'a exp$ when not $'a exp$ *) | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *) @@ -497,25 +352,11 @@ type | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of 'a exp (* For internal use to embed into monad definition *) - | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *) + | E_constraint of n_constraint and 'a exp = E_aux of 'a exp_aux * 'a annot -and value = (* interpreter evaluated value *) - V_boxref of nat * t - | V_lit of lit - | V_tuple of (value) list - | V_list of (value) list - | V_vector of nat * i_direction * (value) list - | V_vector_sparse of nat * nat * i_direction * ((nat * value)) list * value - | V_record of t * ((id * value)) list - | V_ctor of id * t * ctor_kind * value - | V_unknown - | V_register of reg_form - | V_register_alias of tannot alias_spec * tannot - | V_track of value * reg_form_set - and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) | LEXP_memory of id * ('a exp) list (* memory or register write via function call *) @@ -549,30 +390,21 @@ and 'a opt_default = and 'a pexp_aux = (* pattern match *) Pat_exp of 'a pat * 'a exp + | Pat_when of 'a pat * 'a exp * 'a exp and 'a pexp = Pat_aux of 'a pexp_aux * 'a annot and 'a letbind_aux = (* let binding *) - LB_val_explicit of typschm * 'a pat * 'a exp (* let, explicit type ('a pat must be total) *) - | LB_val_implicit of 'a pat * 'a exp (* let, implicit type ('a pat must be total) *) + LB_val of 'a pat * 'a exp (* let, implicit type ($'a pat$ must be total) *) and 'a letbind = LB_aux of 'a letbind_aux * 'a annot -and 'a alias_spec_aux = (* register alias expression forms *) - AL_subreg of 'a reg_id * id - | AL_bit of 'a reg_id * 'a exp - | AL_slice of 'a reg_id * 'a exp * 'a exp - | AL_concat of 'a reg_id * 'a reg_id - -and 'a alias_spec = - AL_aux of 'a alias_spec_aux * 'a annot - type -'a funcl_aux = (* function clause *) - FCL_Funcl of id * 'a pat * 'a exp +'a reg_id = + RI_aux of 'a reg_id_aux * 'a annot type @@ -581,20 +413,29 @@ rec_opt_aux = (* optional recursive annotation for functions *) | Rec_rec (* recursive *) +type +effect_opt_aux = (* optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + type tannot_opt_aux = (* optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * typ type -effect_opt_aux = (* optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect +'a funcl_aux = (* function clause *) + FCL_Funcl of id * 'a pat * 'a exp type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a alias_spec_aux = (* register alias expression forms *) + AL_subreg of 'a reg_id * id + | AL_bit of 'a reg_id * 'a exp + | AL_slice of 'a reg_id * 'a exp * 'a exp + | AL_concat of 'a reg_id * 'a reg_id type @@ -603,25 +444,23 @@ rec_opt = type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l +effect_opt = + Effect_opt_aux of effect_opt_aux * Parse_ast.l type -effect_opt = - Effect_opt_aux of effect_opt_aux * Parse_ast.l +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l type -'a val_spec_aux = (* value type specification *) - VS_val_spec of typschm * id (* specify the type of an upcoming definition *) - | VS_extern_no_rename of typschm * id (* specify the type of an external function *) - | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type -'a fundef_aux = (* function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot type @@ -633,6 +472,22 @@ type | SD_scattered_end of id (* scattered definition end *) +type +'a dec_spec_aux = (* register declarations *) + DEC_reg of typ * id + | DEC_alias of id * 'a alias_spec + | DEC_typ_alias of typ * id * 'a alias_spec + + +type +'a val_spec_aux = VS_val_spec of typschm * id * string option * bool + + +type +'a fundef_aux = (* function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list + + type 'a default_spec_aux = (* default kinding or typing assumption *) DT_order of order @@ -641,35 +496,35 @@ type type -'a dec_spec_aux = (* register declarations *) - DEC_reg of typ * id - | DEC_alias of id * 'a alias_spec - | DEC_typ_alias of typ * id * 'a alias_spec +prec = + Infix + | InfixL + | InfixR type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot type -'a scattered_def = - SD_aux of 'a scattered_def_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type -'a default_spec = - DT_aux of 'a default_spec_aux * Parse_ast.l +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type -'a dec_spec = - DEC_aux of 'a dec_spec_aux * 'a annot +'a default_spec = + DT_aux of 'a default_spec_aux * Parse_ast.l type @@ -683,6 +538,8 @@ and 'a def = (* top-level 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_fixity of prec * int * id (* fixity declaration *) + | DEF_overload of id * (id) list (* operator overload specification *) | DEF_default of 'a default_spec (* default kind and type assumptions *) | DEF_scattered of 'a scattered_def (* scattered function and type definition *) | DEF_reg_dec of 'a dec_spec (* register declaration *) diff --git a/language/l2.ott b/language/l2.ott index 559242ea..e8d8a9b7 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1,3 +1,7 @@ +%% +%% Grammar for user language. Generates ./src/ast.ml +%% + indexvar n , m , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} @@ -43,11 +47,24 @@ metavar regexp ::= {{ hol string }} {{ com Regular expresions, as a string literal }} +metavar real ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com Real number literal }} + embed {{ ocaml +type text = string + +type l = Parse_ast.l + type 'a annot = l * 'a +type loop = While | Until + }} embed @@ -75,7 +92,7 @@ val subst : forall 'a. list 'a -> list 'a -> bool }} metavar x , y , z ::= - {{ ocaml string }} + {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com identifier }} @@ -84,7 +101,7 @@ metavar x , y , z ::= metavar ix ::= {{ lex alphanum }} - {{ ocaml string }} + {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com infix identifier }} @@ -112,7 +129,7 @@ annot :: '' ::= {{ hol unit }} id :: '' ::= - {{ com identifier }} + {{ com Identifier }} {{ aux _ l }} | x :: :: id | ( deinfix x ) :: D :: deIid {{ com remove infix status }} @@ -138,12 +155,18 @@ id :: '' ::= % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. -% Vector builtins - | vector_access :: M :: vector_access - | vector_update :: M :: vector_update - | vector_update_subrange :: M :: vector_update_subrange - | vector_subrange :: M :: vector_subrange - | vector_append :: M :: vector_append +% Vector builtins + | vector_access :: M :: vector_access {{ ichlo (Id "vector_access") }} + | vector_update :: M :: vector_update {{ ichlo (Id "vector_update") }} + | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }} + | vector_subrange :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }} + | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} + +% Comparison builtins + | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }} + | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }} + | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }} + | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }} kid :: '' ::= {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} @@ -161,10 +184,10 @@ grammar base_kind :: 'BK_' ::= {{ com base kind}} {{ aux _ l }} - | Type :: :: type {{ com kind of types }} - | Nat :: :: nat {{ com kind of natural number size expressions }} + | Type :: :: type {{ com kind of types }} + | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} - | Effect :: :: effect {{ com kind of effect sets }} + kind :: 'K_' ::= {{ com kinds}} @@ -272,7 +295,7 @@ typ :: 'Typ_' ::= {{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }} | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} - | register [ id ] :: S :: register +% | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }} % ...so bit [ nexp ] etc is just an instance of that % | List < typ > :: :: list {{ com list of [[typ]] }} % | Set < typ > :: :: set {{ com finite set of [[typ]] }} @@ -288,7 +311,6 @@ typ_arg :: 'Typ_arg_' ::= | nexp :: :: nexp | typ :: :: typ | order :: :: order - | effect :: :: effect % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ @@ -317,10 +339,15 @@ grammar n_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} - | nexp = nexp' :: :: fixed + | nexp = nexp' :: :: equal | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le - | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded + | nexp != nexp' :: :: not_equal + | kid 'IN' { num1 , ... , numn } :: :: set + | n_constraint \/ n_constraint' :: :: or + | n_constraint /\ n_constraint' :: :: and + | true :: :: true + | false :: :: false % 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 @@ -422,17 +449,17 @@ kind_def :: 'KD_' ::= {{ aux _ annot }} {{ auxparam 'a }} | Def kind id name_scm_opt = nexp :: :: nabbrev {{ com $[[Nat]]$-expression abbreviation }} - | Def kind id name_scm_opt = typschm :: D :: abbrev - {{ com type abbreviation }} {{ texlong }} - | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record - {{ com struct type definition }} {{ texlong }} - | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant - {{ com union type definition}} {{ texlong }} - | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum - {{ com enumeration type definition}} {{ texlong }} - - | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} +% | Def kind id name_scm_opt = typschm :: D :: abbrev +% {{ com type abbreviation }} {{ texlong }} +% | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record +% {{ com struct type definition }} {{ texlong }} +% | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant +% {{ com union type definition}} {{ texlong }} +% | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum +% {{ com enumeration type definition}} {{ texlong }} +% +% | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} @@ -477,7 +504,8 @@ lit :: 'L_' ::= % Should undefined be of type bit[alpha] or alpha[beta] or just alpha? | string :: :: string {{ com string constant }} | undefined :: :: undef {{ com undefined-value constant }} - + | real :: :: real + semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} {{ ocaml bool }} {{ lem bool }} @@ -513,11 +541,10 @@ pat :: 'P_' ::= % C-style | ( typ ) pat :: :: typ {{ com typed pattern }} - | id :: :: id {{ com identifier }} - -% + | pat kid :: :: var + {{ com bind pattern to type variable }} | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} @@ -535,8 +562,8 @@ pat :: 'P_' ::= | [ pat1 , .. , patn ] :: :: vector {{ com vector pattern }} - | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed - {{ com vector pattern (with explicit indices) }} +% | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed +% {{ com vector pattern (with explicit indices) }} % cf ntoes for this | pat1 : .... : patn :: :: vector_concat @@ -547,9 +574,9 @@ pat :: 'P_' ::= | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren -{{ ichlo [[pat]] }} -% | pat1 '::' pat2 :: :: cons -% {{ com Cons patterns }} + {{ ichlo [[pat]] }} + | pat1 '::' pat2 :: :: cons + {{ com Cons patterns }} % XXX Is this still useful? fpat :: 'FP_' ::= @@ -593,355 +620,6 @@ end grammar -k :: 'Ki_' ::= -{{ com Internal kinds }} - | K_Typ :: :: typ - | K_Nat :: :: nat - | K_Ord :: :: ord - | K_Efct :: :: efct - | K_Lam ( k0 .. kn -> k' ) :: :: ctor - | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} - -t , u :: 'T_' ::= -{{ com Internal types }} - | x :: :: id - | ' x :: :: var - | t1 -> t2 effect :: :: fn - | ( t1 , .... , tn ) :: :: tup - | x < t_args > :: :: app - | t |-> t1 :: :: abbrev - | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} - | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} - | atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }} - | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} - | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} - | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }} - | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }} - | bit :: S :: bit_typ {{ ichlo T_id "bit" }} - | string :: S :: string_typ {{ ichlo T_id "string" }} - | unit :: S :: unit_typ {{ ichlo T_id "unit" }} - | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} - -optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} - | x :: :: optx_x - {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} - | :: :: optx_none - {{ lem Nothing }} {{ ocaml None }} - - -tag :: 'Tag_' ::= -{{ com Data indicating where the identifier arises and thus information necessary in compilation }} - | None :: :: empty - | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} - | Set :: :: set {{ com Denotes an expression that mutates a local variable }} - | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} - | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} - | Ctor :: :: ctor {{ com Data constructor from a type union }} - | Extern optx :: :: extern {{ com External function, specied only with a val statement }} - | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} - | Spec :: :: spec - | Enum num :: :: enum - | Alias :: :: alias - | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} - -ne :: 'Ne_' ::= - {{ com internal numeric expressions }} - | x :: :: id - | ' x :: :: var - | num :: :: const - | infinity :: :: inf - | ne1 * ne2 :: :: mult - | ne1 + ... + nen :: :: add - | ne1 - ne2 :: :: minus - | 2 ** ne :: :: exp - | ( - ne ) :: :: unary - | zero :: S :: zero - {{ ichlo (Ne_const 0) }} - | one :: S :: one - {{ ichlo (Ne_const 1) }} - | bitlength ( bin ) :: M :: cbin - {{ ocaml (asssert false) }} - {{ hol ARB }} - {{ lem (blength [[bin]]) }} - | bitlength ( hex ) :: M :: chex - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (hlength [[hex]]) }} - | count ( num0 ... numi ) :: M :: length {{ichlo "todo" }} - | length ( pat1 ... patn ) :: M :: cpat - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (Ne_const (List.length [[pat1...patn]])) }} - | length ( exp1 ... expn ) :: M :: cexp - {{ hol ARB }} - {{ ocaml (assert false) }} - {{ lem (Ne_const (List.length [[exp1...expn]])) }} - - t_arg :: 't_arg_' ::= - {{ com Argument to type constructors }} - | t :: :: typ - | ne :: :: nexp - | effect :: :: effect - | order :: :: order - | fresh :: M :: freshvar {{ ichlo T_arg (T_var "fresh") }} - - t_args :: '' ::= {{ lem list t_arg }} - {{ com Arguments to type constructors }} - | t_arg1 ... t_argn :: :: T_args - - nec :: 'Nec_' ::= - {{ com Numeric expression constraints }} - | ne <= ne' :: :: lteq - | ne = ne' :: :: eq - | ne >= ne' :: :: gteq - | ' x 'IN' { num1 , ... , numn } :: :: in - | nec0 .. necn -> nec'0 ... nec'm :: :: cond - | nec0 ... necn :: :: branch - -S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} - {{ hol nec list }} - {{ lem list nec }} - {{ com nexp constraint lists }} - | { nec1 , .. , necn } :: :: Sn_concrete - {{ hol [[nec1 .. necn]] }} - {{ lem [[nec1 .. necn]] }} - | S_N1 u+ .. u+ S_Nn :: M :: SN_union - {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }} - {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }} - {{ ocaml (assert false) }} - | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing - {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }} - {{ ocaml (assert false) }} - {{ ichl todo }} - | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing - {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }} - {{ ocaml assert false }} - {{ ichl todo }} - | resolve ( S_N ) :: :: resolution - {{ lem [[S_N]] (* Write constraint solver *) }} - - - E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} - {{ lem definition_env }} - {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }} - | < E_k , E_a , E_r , E_e > :: :: base - {{ hol arb }} - {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} - | empty :: :: empty - {{ hol arb }} - {{ lem DenvEmp }} - | E_d u+ E_d' :: :: union - {{ hol arb }} - {{ lem (denv_union [[E_d]] [[E_d']]) }} - - kinf :: 'kinf_' ::= - {{ com Whether a kind is default or from a local binding }} - | k :: :: k - | k default :: :: def - - tid :: 'tid_' ::= - {{ com A type identifier or type variable }} - | id :: :: id - | kid :: :: var - - E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} - {{ hol (tid-> kinf) }} - {{ lem (map tid kinf) }} - {{ com Kind environments }} - | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete - {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} - {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} - | E_k1 u+ .. u+ E_kn :: M :: union - {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} - {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }} - {{ ocaml (assert false) }} - | E_k u- E_k1 .. E_kn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} - {{ ocaml assert false }} - - tinf :: 'tinf_' ::= - {{ com Type variables, type, and constraints, bound to an identifier }} - | t :: :: typ - | E_k , S_N , tag , t :: :: quant_typ - -tinflist :: 'tinfs_' ::= - {{ com In place so that a list of tinfs can be referred to without the dot form }} - | empty :: :: empty - | tinf1 ... tinfn :: :: ls - -conformsto :: 'conformsto_' ::= - {{ com how much conformance does overloading need }} - | full :: :: full - | parm :: :: parm - -widenvec :: 'widenvec_' ::= - | vectors :: :: widen - | none :: :: dont - | _ :: :: dontcare - -widennum :: 'widennum_' ::= - | nums :: :: widen - | none :: :: dont - | _ :: :: dontcare - -widening :: 'widening_' ::= - {{ com Should we widen vector start locations, should we widen atoms and ranges }} - | ( widennum , widenvec ) :: :: w - - E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::= {{ phantom }} - {{ hol tid |-> tinf}} - {{ lem map tid tinf }} - | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete - | E_a1 u+ .. u+ E_an :: :: union - - field_typs :: 'FT_' ::= {{ phantom }} - {{ lem list (id * t) }} - {{ com Record fields }} - | id1 : t1 , .. , idn : tn :: :: fields - {{ lem [[id1 t1..idn tn]] }} - - E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} - {{ hol (id*t) |-> tinf) }} - {{ lem map (list (id*t)) tinf }} - {{ com Record environments }} - | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete - {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} - | E_r1 u+ .. u+ E_rn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} - {{ ocaml (assert false) }} - - enumerate_map :: '' ::= {{ phantom }} - {{ lem (list (nat*id)) }} - | { num1 |-> id1 ... numn |-> idn } :: :: enum_map - {{ lem [[num1 id1...numn idn]] }} - - E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} - {{ lem (map t (list (nat*id))) }} - {{ com Enumeration environments }} - | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} - | E_e1 u+ .. u+ E_en :: :: union - {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} - - -embed -{{ lem - type definition_env = - | DenvEmp - | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) - -}} - -grammar - - E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} - {{ hol (id |-> tinf) }} - {{ lem map id tinf }} - {{ com Type environments }} - | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base - {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} - | { id |-> overload tinf conformsto : tinf1 , ... , tinfn } :: :: overload - | ( E_t1 u+ .... u+ E_tn ) :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | u+ E_t1 .. E_tn :: M :: multi_union - {{ hol arb }} - {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - | E_t u- id1 .. idn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} - {{ ocaml assert false }} - | ( E_t1 inter .... inter E_tn ) :: M :: intersect - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | inter E_t1 .. E_tn :: M :: multi_inter - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - - -ts :: ts_ ::= {{ phantom }} - {{ lem list t }} - | t1 , .. , tn :: :: lst - -embed -{{ lem -let blength (bit) = Ne_const 8 -let hlength (bit) = Ne_const 8 - - type env = - | EnvEmp - | Env of (map id tinf) * definition_env - - type inf = - | Iemp - | Inf of (list nec) * effect - - val denv_union : definition_env -> definition_env -> definition_env - let denv_union de1 de2 = - match (de1,de2) with - | (DenvEmp,de2) -> de2 - | (de1,DenvEmp) -> de1 - | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> - Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) - end - - val env_union : env -> env -> env - let env_union e1 e2 = - match (e1,e2) with - | (EnvEmp,e2) -> e2 - | (e1,EnvEmp) -> e1 - | ((Env te1 de1),(Env te2 de2)) -> - Env (te1 union te2) (denv_union de1 de2) - end - -let inf_union i1 i2 = - match (i1,i2) with - | (Iemp,i2) -> i2 - | (i1,Iemp) -> i1 - | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) - end - -let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) - -}} - -grammar - - E :: '' ::= - {{ hol ((string,env_body) fmaptree) }} - {{ lem env }} - {{ com Definition environment and lexical environment }} - | < E_t , E_d > :: :: E - {{ hol arb }} - {{ lem (Env [[E_t]] [[E_d]]) }} - | empty :: M :: E_empty - {{ hol arb }} - {{ lem EnvEmp }} - {{ ocaml assert false }} - | E u+ E' :: :: E_union - {{ lem (env_union [[E]] [[E']]) }} - - I :: '' ::= {{ lem inf }} - {{ com Information given by type checking an expression }} - | < S_N , effect > :: :: I - {{ lem (Inf [[S_N]] [[effect]]) }} - | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} - {{ lem Iemp }} - | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }} - | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} - {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % @@ -959,7 +637,9 @@ tannot :: '' ::= {{ phantom }} {{ ocaml tannot }} {{ lem tannot }} - +loop :: loop ::= {{ phantom }} + | while :: :: while + | until :: :: until exp :: 'E_' ::= @@ -997,8 +677,9 @@ exp :: 'E_' ::= {{ com conditional }} | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} - | while exp1 do exp2 :: :: while - | repeat exp1 until exp2 :: :: until + | loop exp1 exp2 :: :: loop + | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} + | repeat exp1 until exp2 S :: :: until {{ ichlo [[ loop until exp2 exp1 ]] }} | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} @@ -1086,6 +767,8 @@ exp :: 'E_' ::= % this can be used to break out of for loops | exit exp :: :: exit {{ com halt all current execution }} + | throw exp :: :: throw + | try exp catch pexp1 .. pexpn :: :: try %, potentially calling a system, trap, or interrupt handler with exp | assert ( exp , exp' ) :: :: assert {{ com halt with error $[[exp']]$ when not $[[exp]]$ }} @@ -1099,38 +782,26 @@ exp :: 'E_' ::= | comment exp :: I :: comment_struc {{ com For generated structured comments }} | let lexp = exp in exp' :: I :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} - | return_int ( exp ) :: I :: internal_return {{ com For internal use to embed into monad definition }} - | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} + | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} +% | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} | constraint n_constraint :: :: constraint -i_direction :: 'I' ::= - | IInc :: :: Inc - | IDec :: :: Dec - -ctor_kind :: 'C_' ::= - | C_Enum nat :: :: Enum - | C_Union :: :: Union - -reg_form :: 'Form_' ::= - | Reg id tannot i_direction :: :: Reg - | SubReg id reg_form index_range :: :: SubReg - -reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} - -alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} - -value :: 'V_' ::= {{ com interpreter evaluated value }} - | Boxref nat t :: :: boxref - | Lit lit :: :: lit - | Tuple ( value1 , ... , valuen ) :: :: tuple - | List ( value1 , ... , valuen ) :: :: list - | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector - | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse - | Record t ( id1 value1 , ... , idn valuen ) :: :: record - | V_ctor id t ctor_kind value1 :: :: ctor - | Unknown :: :: unknown - | Register reg_form :: :: register - | Register_alias alias_spec_tannot tannot :: :: register_alias - | Track value reg_form_set :: :: track + +%i_direction :: 'I' ::= +% | IInc :: :: Inc +% | IDec :: :: Dec + +%ctor_kind :: 'C_' ::= +% | C_Enum nat :: :: Enum +% | C_Union :: :: Union + +%reg_form :: 'Form_' ::= +% | Reg id tannot i_direction :: :: Reg +% | SubReg id reg_form index_range :: :: SubReg + +%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} + +%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} + lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} @@ -1167,7 +838,8 @@ opt_default :: 'Def_val_' ::= pexp :: 'Pat_' ::= {{ com pattern match }} {{ aux _ annot }} {{ auxparam 'a }} - | pat -> exp :: :: exp + | pat -> exp :: :: exp + | pat when exp1 -> exp :: :: when % apparently could use -> or => for this. %% % psexp :: 'Pats' ::= @@ -1244,7 +916,7 @@ grammar tannot_opt :: 'Typ_annot_opt_' ::= {{ com optional type annotation for functions}} {{ aux _ l }} -% | :: :: none + | :: :: none % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return | typquant typ :: :: some @@ -1281,22 +953,27 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} - | let typschm pat = exp :: :: val_explicit - {{ com let, explicit type ($[[pat]]$ must be total)}} +% | let typschm pat = exp :: :: val_explicit +% {{ com let, explicit type ($[[pat]]$ must be total)}} % at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here - | let pat = exp :: :: val_implicit + | let pat = exp :: :: val {{ com let, implicit type ($[[pat]]$ must be total)}} - val_spec :: 'VS_' ::= {{ com value type specification }} {{ aux _ annot }} {{ auxparam 'a }} - | val typschm id :: :: val_spec + {{ ocaml VS_val_spec of typschm * id * string option * bool }} + | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} - | val extern typschm id :: :: extern_no_rename + {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} + | val cast typschm id :: S :: cast + {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }} + | val extern typschm id :: S :: extern_no_rename {{ com specify the type of an external function }} - | val extern typschm id = string :: :: extern_spec + {{ ocaml (VS_val_spec [[typschm]] [[id]] (Some [[id]]) false) }} + | val extern typschm id = string :: S :: extern_spec {{ com specify the type of a function from Lem }} + {{ ocaml (VS_val_spec [[typschm]] [[id]] (Some [[string]]) false) }} %where the string must provide an explicit path to the required function but will not be checked default_spec :: 'DT_' ::= @@ -1357,6 +1034,11 @@ dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +prec :: '' ::= + | infix :: :: Infix + | infixl :: :: InfixL + | infixr :: :: InfixR + def :: 'DEF_' ::= {{ com top-level definition }} {{ auxparam 'a }} @@ -1370,6 +1052,10 @@ def :: 'DEF_' ::= {{ com value definition }} | val_spec :: :: spec {{ com top-level type constraint }} + | fix prec num id :: :: fixity + {{ com fixity declaration }} + | overload id [ id1 ; ... ; idn ] :: :: overload + {{ com operator overload specification }} | default_spec :: :: default {{ com default kind and type assumptions }} | scattered_def :: :: scattered diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 95e6dba1..9e1b79fb 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -206,6 +206,39 @@ G ( typ1 , id ) = typ G |-f exp . id => typ +defn +G |- exp1 => n_constraint :: :: infer_flow :: infer_flow_ +by + + +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lteq +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 <= nexp2 + + +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gteq +G |- :E_app: gteq_atom_atom ( x , y ) => nexp1 >= nexp2 + +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lt +G |- :E_app: lt_atom_atom ( x , y ) => nexp1 + numOne <= nexp2 + +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gt +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 >= nexp2 + numOne + + +G |- id => range +G |- y => atom < nexp > +------------------------------------------------------------------------------- :: lt_range_atom +G |- :E_app: lt_range_atom ( id , y ) => range < nexp1 , min (nexp - 1 , nexp2 ) > + + defn @@ -321,9 +354,9 @@ G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3 => typ G |- foreach ( id from exp1 downto exp2 ) exp3 => typ -G |- exp1 => (flows,constrs) -G , flows , constrs |- exp2 => typ -G , flows , negate constrs |- exp3 <= typ +G |- exp1 => n_constraint +%G , flows , constrs |- exp2 => typ +%G , flows , negate constrs |- exp3 <= typ -------------------------------------------- :: if G |- if exp1 then exp2 else exp3 => typ -- cgit v1.2.3