diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 420 |
1 files changed, 3 insertions, 417 deletions
diff --git a/language/l2.ott b/language/l2.ott index bc2f0c8d..d6f8cfed 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1,4 +1,4 @@ -indexvar n , i , j ::= +indexvar n , m , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} @@ -832,6 +832,8 @@ val_spec :: 'VS_' ::= {{ com Value type specification }} {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec + | val extern typschm id = string :: :: extern_spec + {{ com Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked }} default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} @@ -882,282 +884,6 @@ defs :: '' ::= | def1 .. defn :: :: Defs - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Machinery for typing rules % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -grammar - -k :: 'Ki_' ::= -{{ com Internal kinds }} - | K_Typ :: :: typ - | K_Nat :: :: nat - | K_Ord :: :: ord - | K_Efct :: :: efct - | K_Val :: :: val {{ com Representing values, for use in identifier checks }} - | K_Lam ( k0 .. kn -> k' ) :: :: ctor - | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} - -t , u :: 'T_' ::= {{ phantom }} -{{ com Internal types }} - | id :: :: var - | t1 -> t2 effects tag S_N :: :: fn {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }} - | ( t1 * .... * tn ) :: :: tup - | id t_args :: :: app - -tag :: 'Tag_' ::= {{ phantom }} -{{ com Data indicating where the function arises and thus information necessary in compilation }} - | None :: :: empty - | Ctor :: :: ctor {{ com Data constructor from a type union }} - | Extern :: :: extern {{ com External function, specied only with a val statement }} - | _ :: :: dontcare - -ne :: 'Ne_' ::= - {{ com internal numeric expressions }} - | id :: :: var - | num :: :: const - | ne1 * ne2 :: :: mult - | ne1 + ... + nen :: :: add - | 2 ** ne :: :: exp - | ( - ne ) :: :: unary -%% %% | ne1 + ... + nen :: M :: addmany -%% %% {{ ocaml (assert false) }} -%% %% {{ hol ARB }} -%% %% {{ lem (sumation_nes [[ne1...nen]]) }} - | bitlength ( bin ) :: M :: cbin - {{ ocaml (asssert false) }} - {{ hol ARB }} - {{ lem (blength [[bin]]) }} - | bitlength ( hex ) :: M :: chex - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (hlength [[hex]]) }} - | length ( pat1 ... patn ) :: M :: cpat - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (Ne_const (List.length [[pat1...patn]])) }} - | length ( exp1 ... expn ) :: M :: cexp - {{ hol ARB }} - {{ ocaml (assert false) }} - {{ lem (Ne_const (List.length [[exp1...expn]])) }} - - t_arg :: 't_arg_' ::= {{ phantom }} - {{ com Argument to type constructors }} - | t :: :: typ - | ne :: :: nexp - | effects :: :: effect - | order :: :: order - - t_args :: '' ::= {{ phantom }} - {{ com Arguments to type constructors }} - | t_arg1 ... t_argn :: :: T_args - - nec :: 'Nec_' ::= - {{ com Numeric expression constraints }} - | ne <= ne' :: :: lteq - | ne = ne' :: :: eq - | ne >= ne' :: :: gteq - -%% %% embed -%% %% {{ lem -%% %% -%% %% val t_subst_t : list (tnv * t) -> t -> t -%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t -%% %% val ftv_t : t -> list tnv -%% %% val ftv_tm : list t -> list tnv -%% %% val ftv_s : list (p*tnv) -> list tnv -%% %% val compatible_overlap : list (x*t) -> bool -%% %% -%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*) -%% %% let normalize n = n -%% %% -%% %% let blength (_,bit) = Ne_const 8 -%% %% let hlength (_,bit) = Ne_const 8 -%% %% -%% %% let rec sumation_nes nes = match nes with -%% %% | [ a; b] -> Ne_add a b -%% %% | x :: y -> Ne_add x (sumation_nes y) -%% %% end -%% %% -%% %% }} -%% %% -%% %% grammar -%% %% -%% %% -%% %% names :: '' ::= {{ phantom }} -%% %% {{ hol x set }} -%% %% {{ lem set x }} -%% %% {{ ocaml Set.Make(String).t }} -%% %% {{ com Sets of names }} -%% %% | { x1 , .. , xn } :: :: Names -%% %% {{ hol (LIST_TO_SET [[x1..xn]]) }} -%% %% {{ lem (set_from_list [[x1..xn]]) }} -%% %% -%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::= -%% %% {{ hol (p#tnv) list }} -%% %% {{ lem list (p*tnv) }} -%% %% % {{ com Typeclass constraint lists }} -%% %% % | ( p1 tnv1 ) .. ( pn tnvn ) :: :: SemC_concrete -%% %% % {{ hol ([[p1 tnv1..pn tnvn]]) }} -%% %% % {{ lem ([[p1 tnv1..pn tnvn]]) }} -%% %% -%% %% env_tag :: '' ::= -%% %% {{ com Tags for the (non-constructor) value descriptions }} -%% %% % | method :: :: method -%% %% % {{ com Bound to a method }} -%% %% | val :: :: spec -%% %% {{ com Specified with val }} -%% %% | let :: :: def -%% %% {{ com Defined with let or indreln }} -%% %% -%% %% v_desc :: 'V_' ::= -%% %% {{ com Value descriptions }} -%% %% | < forall tnvs . t_multi -> p , ( x of names ) > :: :: constr -%% %% {{ com Constructors }} -%% %% | < forall tnvs . semC => t , env_tag > :: :: val -%% %% {{ com Values }} -%% %% -%% %% f_desc :: 'F_' ::= -%% %% | < forall tnvs . p -> t , ( x of names ) > :: :: field -%% %% {{ com Fields }} -%% %% -%% %% embed -%% %% {{ hol -%% %% load "fmaptreeTheory"; -%% %% val _ = -%% %% Hol_datatype -%% %% `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`; -%% %% -%% %% val _ = Define ` -%% %% env_union e1 e2 = -%% %% let i1 = item e1 in -%% %% let m1 = map e1 in -%% %% let i2 = item e2 in -%% %% let m2 = map e2 in -%% %% FTNode <| env_p:=FUNION i1.env_p i2.env_p; -%% %% env_f:=FUNION i1.env_f i2.env_f; -%% %% env_v:=FUNION i1.env_v i2.env_v |> -%% %% (FUNION m1 m2)`; -%% %% }} -%% %% {{ lem -%% %% type env = -%% %% | EnvEmp -%% %% | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc) -%% %% -%% %% val env_union : env -> env -> env -%% %% let env_union e1 e2 = -%% %% match (e1,e2) with -%% %% | (EnvEmp,e2) -> e2 -%% %% | (e1,EnvEmp) -> e1 -%% %% | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) -> -%% %% Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2) -%% %% end -%% %% -%% %% }} -%% %% -%% %% grammar -%% %% -%% %% xs :: '' ::= {{ phantom }} -%% %% {{ hol string list }} -%% %% {{ lem list string }} -%% %% | x1 .. xn :: :: Xs -%% %% {{ hol [[x1..xn]] }} -%% %% {{ lem [[x1..xn]] }} -%% %% -S_N {{ tex \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.fold_right union_map [[S_N1..S_Nn]] Pmap.empty) }} - {{ 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 }} - - I :: '' ::= {{ phantom }} - {{ com Information given by type checking an expression; tag only reflects the immediate exp }} - | < S_N , effects > :: :: I - | Ie :: :: Iempty {{ com Empty constraints, effetcs }} {{ tex {\ottnt{I}_{\epsilon} } }} - | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effects, setting None for the tag }} - - E :: '' ::= {{ phantom }} - {{ hol ((string,env_body) fmaptree) }} - {{ lem env }} - {{ com Environments }} - | < E_t , E_r , E_k > :: :: E - {{ hol arb }} - {{ lem (Env [[E_k]] [[E_r]] [[E_t]]) }} - | empty :: M :: E_empty - {{ hol arb }} - {{ lem EnvEmp }} - {{ ocaml assert false }} - - E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::= {{ phantom }} - {{ hol (id-> k) }} - {{ lem map id k }} - {{ com Kind environments }} - | { id1 |-> k1 , .. , idn |-> kn } :: :: concrete - {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 k1 .. idn kn]]) }} - {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 k1 .. idn kn]] Pmap.empty) }} - | E_k1 u+ .. u+ E_kn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} - {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }} - {{ ocaml (assert false) }} - - E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} - {{ hol (id |-> t) }} - {{ lem map x f_desc }} - {{ com Type environments }} - | { id1 |-> t1 , .. , idn |-> tn } :: :: base - {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 t1 .. idn tn]]) }} - {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 t1 .. idn tn]] Pmap.empty) }} - | ( E_t1 u+ .... u+ E_tn ) :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} - {{ lem (List.fold_right union_map [[E_t1....E_tn]] Pmap.empty) }} - {{ ocaml (assert false) }} - | u+ E_t1 .. E_tn :: M :: multi_union - {{ hol arb }} - {{ lem arb }} - {{ ocaml assert false }} - | E_t u- E_t1 .. E_tn :: M :: multi_set_minus - {{ hol arb }} {{ lem arb }} {{ ocaml assert false }} - | ( E_t1 inter .... inter E_tn ) :: M :: intersect - {{ hol arb }} - {{ lem syntax error }} - {{ ocaml (assert false) }} - | inter E_t1 .. E_tn :: M :: multi_inter - {{ hol arb }} - {{ lem arb }} - {{ ocaml assert false }} - - - field_typs :: 'FT_' ::= {{ phantom }} - {{ com Record fields }} - | id1 : t1 , .. , idn : tn :: :: fields - - E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} - {{ hol (id |-> t) }} - {{ lem map x f_desc }} - {{ com Record environments }} - | { { field_typs1 } |-> t1 , .. , { field_typsn } |-> tn } :: :: concrete - {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} - {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) Pmap.empty) }} - | E_r1 u+ .. u+ E_rn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} - {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }} - {{ ocaml (assert false) }} - terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} @@ -1231,144 +957,4 @@ terminals :: '' ::= | consistent_decrease :: :: cd {{ tex \ottkw{consistent\_decrease}~ }} -ts :: ts_ ::= {{ phantom }} - | t1 , .. , tn :: :: lst - -formula :: formula_ ::= - | judgement :: :: judgement - - | formula1 .. formulan :: :: dots - - | E_k ( id ) gives k :: :: lookup_k - {{ com Kind lookup }} - {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }} - {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }} - - | E_t ( id ) gives t :: :: lookup_t - {{ com Type lookup }} - {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }} - {{ lem Pmap.find [[id]] [[E_t]] = [[t]] }} - - | E_k ( id ) <-| k :: :: update_k - {{ com Update the kind associated with id to k }} - - | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r - {{ com Record lookup }} - - | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt - {{ com Record looup by type }} - - | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint - {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} - {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]]) }} - - | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint - {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} - {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} - - | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many - {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM - E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }} - {{ lem disjoint_all (List.map Pmap.domain [[E_t1 .... E_tn]]) }} - {{ com Pairwise disjoint domains }} -%% %% -%% %% | compatible overlap ( x1 |-> t1 , .. , xn |-> tn ) :: :: E_l_compat -%% %% {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m = FST __n) ==> (SND __m = SND __n)) }} -%% %% {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} -%% %% {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }} -%% %% -%% %% | duplicates ( tnvs ) = emptyset :: :: no_dups_tnvs -%% %% {{ hol (ALL_DISTINCT [[tnvs]]) }} -%% %% {{ lem (duplicates [[tnvs]]) = [ ] }} -%% %% -%% %% | duplicates ( x1 , .. , xn ) = emptyset :: :: no_dups -%% %% {{ hol (ALL_DISTINCT [[x1..xn]]) }} -%% %% {{ lem (duplicates [[x1..xn]]) = [ ] }} - - | id NOTIN dom ( E_k ) :: :: notin_dom_k - {{ hol ([[id]] NOTIN FDOM [[E_k]]) }} - {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }} - - | id NOTIN dom ( E_t ) :: :: notin_dom_t - {{ hol ([[id]] NOTIN FDOM [[E_t]]) }} - {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }} - - | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields -%% %% -%% %% -%% %% | FV ( t ) SUBSET tnvs :: :: FV_t -%% %% {{ com Free type variables }} -%% %% {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }} -%% %% {{ lem subst (ftv_t [[t]]) [[tnvs]] }} -%% %% -%% %% | FV ( t_multi ) SUBSET tnvs :: :: FV_t_multi -%% %% {{ com Free type variables }} -%% %% {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }} -%% %% {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]] }} -%% %% -%% %% | FV ( semC ) SUBSET tnvs :: :: FV_semC -%% %% {{ com Free type variables }} -%% %% {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }} -%% %% {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} -%% %% -%% %% | inst 'IN' I :: :: inst_in -%% %% {{ hol (MEM [[inst]] [[I]]) }} -%% %% {{ lem ([[inst]] IN [[I]]) }} -%% %% -%% %% | ( p t ) NOTIN I :: :: notin_I -%% %% {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }} -%% %% {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }} -%% %% - - | num1 lt ... lt numn :: :: increasing - - | num1 gt ... gt numn :: :: decreasing - - | E_k1 = E_k2 :: :: E_k_eqn - {{ ichl ([[E_k1]] = [[E_k2]]) }} - - | E_t1 = E_t2 :: :: E_t_eqn - {{ ichl ([[E_t1]] = [[E_t2]]) }} - - | E1 = E2 :: :: E_eqn - {{ ichl ([[E1]] = [[E2]]) }} - - | S_N1 = S_N2 :: :: S_N_eqn - {{ ichl ([[S_N1]] = [[S_N2]]) }} - -%% %% | TD1 = TD2 :: :: TD_eqn -%% %% {{ ichl ([[TD1]] = [[TD2]]) }} -%% %% -%% %% | TC1 = TC2 :: :: TC_eqn -%% %% {{ ichl ([[TC1]] = [[TC2]]) }} -%% %% -%% %% | I1 = I2 :: :: I_eqn -%% %% {{ ichl ([[I1]] = [[I2]]) }} -%% %% -%% %% | names1 = names2 :: :: names_eq -%% %% {{ ichl ([[names1]] = [[names2]]) }} -%% %% - | t1 = t2 :: :: t_eq - {{ ichl ([[t1]] = [[t2]]) }} - | ne1 = ne2 :: :: ne_eq - {{ ichl ([[ne1]] = [[ne2]]) }} -%% %% -%% %% | t_subst1 = t_subst2 :: :: t_subst_eq -%% %% {{ ichl ([[t_subst1]] = [[t_subst2]]) }} -%% %% -%% %% | p1 = p2 :: :: p_eq -%% %% {{ ichl ([[p1]] = [[p2]]) }} -%% %% -%% %% | xs1 = xs2 :: :: xs_eq -%% %% {{ ichl ([[xs1]] = [[xs2]]) }} -%% %% -%% %% | tnvs1 = tnvs2 :: :: tnvs_eq -%% %% {{ ichl ([[tnvs1]] = [[tnvs2]]) }} - -% Substitutions and freevars are not correctly generated for the OCaml ast.ml -%substitutions -%multiple t a :: t_subst -% -%freevars -%t a :: ftv |