From 74abb449a443375cc529b6261e284233a95268ce Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Tue, 31 Dec 2019 13:34:40 +0200 Subject: [PATCH] WIP Add derived form for datatypes --- Makefile | 4 +- elab.ml | 2 + lexer.mll | 1 + parser.mly | 15 +++- regression.1ml | 193 +++++++++++++++++++++++++++++++++++++++++++------ syntax.ml | 140 +++++++++++++++++++++++++++++++++++ 6 files changed, 327 insertions(+), 28 deletions(-) diff --git a/Makefile b/Makefile index feb83b03..6e441b22 100644 --- a/Makefile +++ b/Makefile @@ -4,8 +4,8 @@ NAME = 1ml MODULES = \ - lib source prim syntax parser lexer \ - fomega types iL env erase trace sub elab \ + lib source prim fomega types env syntax \ + parser lexer iL erase trace sub elab \ lambda compile \ main NOMLI = syntax iL main diff --git a/elab.ml b/elab.ml index f4232e14..7f9fe3c7 100644 --- a/elab.ml +++ b/elab.ml @@ -560,6 +560,8 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t)); ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3), IL.LetE(e, "_", materialize_typ t) ) + | EL.WithEnvE (toExp) -> + elab_exp env (toExp env) l (* rec (X : (b : type) => {type t; type u a}) fun (b : type) => {type t = (X int.u b, X bool.t); type u a = (a, X b.t)} diff --git a/lexer.mll b/lexer.mll index 376783db..bf9f7f29 100644 --- a/lexer.mll +++ b/lexer.mll @@ -70,6 +70,7 @@ rule token = parse | "_" { HOLE } | "and" { AND } | "as" { AS } + | "data" { DATA } | "do" { DO } | "else" { ELSE } | "end" { END } diff --git a/parser.mly b/parser.mly index 8f1a10c6..8c3029b7 100644 --- a/parser.mly +++ b/parser.mly @@ -35,6 +35,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s)) %token DOT AT TICK %token COMMA SEMI %token TYPE_ERROR +%token DATA %token EOF @@ -305,15 +306,19 @@ infexp : | DO appexp { doE($2)@@at() } ; +ascription : + | COLON + { annotE } + | SEAL + { sealE } +; annexp : | infexp { $1 } | TYPE typ { TypE($2)@@at() } - | annexp COLON typ - { annotE($1, $3)@@at() } - | annexp SEAL typ - { sealE($1, $3)@@at() } + | annexp ascription typ + { $2($1, $3)@@at() } | WRAP infexp COLON typ { wrapE($2, $4)@@at() } | UNWRAP infexp COLON typ @@ -322,6 +327,8 @@ annexp : exp : | annexp { $1 } + | DATA name name typparamlist ascription typ + { dataE($2, $3, $4, $5, $6, at())@@at() } | FUN param paramlist DARROW exp { funE($2::$3, $5)@@at() } | IF exp THEN exp ELSE infexp COLON typ diff --git a/regression.1ml b/regression.1ml index 731e2502..175e5086 100644 --- a/regression.1ml +++ b/regression.1ml @@ -106,6 +106,112 @@ PolyRec = { t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0)))); }; +;; + +IT = data case t _ :> { + Int : Int.t -> case Int.t; + Text : Text.t -> case Text.t; +}; + +IT = let + type I (type t _) (type case _) = { + Int : Int.t -> case Int.t; + Text : Text.t -> case Text.t; + }; + type J (type t _) = {type case _; ...I t case}; + type T (type t _) x = (c: J t) -> c.case x; + ...{ + t = rec (type t _) => fun (type x) => type wrap T t x; + case 'x (type case _) (cs: I t case) e = + (unwrap e.@(t _): wrap T t x) {case; ...cs}; + mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x); + } :> { + type t _; + case 'x: (type case _) => I t case => t x -> case x; + mk 'x: T t x => t x; + }; + J = J t; +in { + t; case; + Int v = mk (fun (r: J) => r.Int v); + Text v = mk (fun (r: J) => r.Text v); +}; + +IT = { + ...IT; + + impossible: t int -> int = case (fun (type t) => t) { + Int x = x; + Text x = x; + }; + + i: int = impossible (Int 9); + ;;t: text = impossible (Text "nine"); +}; + +;; + +Ord = data case t :> { + Lt : case; + Eq : case; + Gt : case; +}; + +Opt = data case t x :> { + None : case; + Some : x -> case; +}; + +Alt = { + ...data case t l r :> { + Left : l -> case; + Right : r -> case; + }; + + ;;Left 'l 'r (v: l) = mk (fun (r: J t l r) => r.Left v); + ;;Right 'l 'r (v: r) = mk (fun (r: J t l r) => r.Right v); +}; + +List = let + ...let + type I (type case) (type t _) x = { + nil : case; + (::) 'n : x -> t x -> case; + }; + type J (type t _) x = {type case; ...I case t x}; + type T (type t _) x = (c: J t x) -> c.case; + in { + t = rec (type t _) => fun (type x) => type wrap T t x; + case '(type case) 'x 'n (cs: I case t x) (e: t x) = + (unwrap e.@(t x): wrap T t x) {case; ...cs}; + mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x); + D = J t; + } :> { + type t _; + case '(type case) 'x 'n: I case t x => t x -> case; + mk 'x: T t x => t x; + type D x = J t x; + }; +in { + t; case; + nil 'x = mk (fun (r: D x) => r.nil); + (::) 'x 'n (v: x) (vs: t x) = mk (fun (r: D x) => r.:: v vs); +}; + +List' = { + ...data case t x :> { + nil : case; + (::) : x -> t x => case; + }; + +;; nil 'x = mk (fun (r: J x) => r.nil); +;; (::) 'x (v: x) (vs: t x) = mk (fun (r: J x) => r.:: v vs); + + isEmpty = case {nil = true; (::) _ _ = false}; +}; + +;; + N :> { type Z; type S _; @@ -114,31 +220,50 @@ N :> { type S _ = {}; }; +ListN'' = let + type I (type case _) (type t _ _) x = { + nil : case N.Z; + (::) 'n : x -> t x n -> case (N.S n); + }; + type J (type t _ _) x = {type case _; ...I case t x}; + type T (type t _ _) x n = (c: J t x) -> c.case n; + in { + t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n; + case (type case _) 'x 'n (cs: I case t x) (e: t x n) = + (unwrap e.@(t x n): wrap T t x n) {case; ...cs}; + mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n); + D = J t; + } :> { + type t _ _; + case (type case _) 'x 'n: I case t x => t x n -> case n; + mk 'x 'n: T t x n => t x n; + type D x = J t x; + }; + ListN = let - type I (type x) (type p _) (type t _ _) = { - nil : p N.Z; - (::) 'n : x -> t x n -> p (N.S n); + ...let + type I (type case _) (type t _ _) x = { + nil : case N.Z; + (::) 'n : x -> t x n -> case (N.S n); + }; + type J (type t _ _) x = {type case _; ...I case t x}; + type T (type t _ _) x n = (c: J t x) -> c.case n; + in { + t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n; + case (type case _) 'x 'n (cs: I case t x) (e: t x n) = + (unwrap e.@(t x n): wrap T t x n) {case; ...cs}; + mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n); + D = J t; + } :> { + type t _ _; + case (type case _) 'x 'n: I case t x => t x n -> case n; + mk 'x 'n: T t x n => t x n; + type D x = J t x; }; - type T x n (type t _ _) = (type p _) => I x p t -> p n; in { - t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t; - - case 'x 'n (type p _) (cs: I x p t) e = - (unwrap e.@(t _ _): wrap T x n t) p cs; - - local - mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t); - in - nil 'x = mk (fun (type p _) (r: I x p t) => r.nil); - (::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs); - end; -} :> { - type t _ _; - - case 'x 'n: (type p _) => I x p t => t x n -> p n; - - nil 'x : t x N.Z; - (::) 'x 'n : x => t x n => t x (N.S n); + t; case; + nil 'x = mk (fun (r: D x) => r.nil); + (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs); }; ListN = { @@ -148,4 +273,28 @@ ListN = { nil = nil; (::) x xs = xy x :: map xs; }; + foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v => + case (fun (type n) => s) { + nil = v; + (::) x xs = foldLeft (sxs v x) xs; + }; + otw = 1 :: (2 :: (3 :: nil)); + sum = foldLeft (+) 0 otw; + otw' = map (fun i => "Int.toText missing") otw; +}; + +ListN' = { + ...data case t x _ :> { + nil : case N.Z; + (::) 'n : x -> t x n -> case (N.S n); + }; + +;; nil 'x = mk (fun (r: D x) => r.nil); +;; (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs); +;; +;; map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) => +;; case (t y) { +;; nil = nil; +;; (::) x xs = xy x :: map xs; +;; }; }; diff --git a/syntax.ml b/syntax.ml index f317ad73..fe337c44 100644 --- a/syntax.ml +++ b/syntax.ml @@ -51,6 +51,7 @@ and exp' = | UnwrapE of var * typ | UnrollE of var * typ | RecE of var * typ * exp + | WithEnvE of (Env.env -> exp) and bind = (bind', unit) phrase and bind' = @@ -315,6 +316,143 @@ let rollP(p, t2) = Some (AsT(t2, PathT(RecE("_"@@t1.at, TypT@@t1.at, TypE(t1.it@@p.at)@@p.at)@@p.at)@@p.at)@@span[p.at; t2.at]) +(* data *) + +let toEP p = + let b, t = (defaultP p).it in + (b, t, Expl@@p.at)@@p.at + +let absTC = function + | [] -> TypT + | ({at} :: _) as tps -> + funT(List.map (function + | {it = ({it = VarB(_, _); at = atH}, t, i); at} -> + (EmptyB@@atH, t, i)@@at + | unnamed -> unnamed) tps, + TypT@@at, + Pure@@at) + +let toCP v tps = + let at = v.at in + annotP(varP(v)@@at, absTC(tps)@@at)@@at + +let appPs f xs = + List.fold_left (fun f tp -> + match tp with + | {it = ({it = VarB(v, _)}, _, _); at} -> appE(f, VarE(v)@@at)@@at + | _ -> assert false) f xs + +let appTPs tc tps = + PathT (appPs tc tps) + +let toImpl = function + | {it = (b, ({it = TypT} as t), i); at} -> (b, t, Impl@@i.at)@@at + | other -> other + +let seqD = function + | [] -> EmptyD + | d::ds -> (List.fold_left (fun s d -> SeqD(s, d)@@d.at) d ds).it + +let seqB = function + | [] -> EmptyB + | b::bs -> (List.fold_left (fun s b -> SeqB(s, b)@@b.at) b bs).it + +let dataE(case_v, small_v, tps, ascribeE, cases, at) = + let ntps, utps, tps = + tps |> List.fold_left (fun (ntps, utps, tps) -> + function + | {it = ({it = EmptyB; at = atH}, t, i); at} -> + let unnamed = let b, _ = varP(var "_"@@atH) in (b, t, i)@@at in + (ntps, utps @ [unnamed], tps @ [unnamed]) + | named -> + (ntps @ [named], utps, tps @ [named])) + ([], [], []) in + let case_tp = toEP (toCP case_v utps) in + let small_p = toCP small_v tps in + let small_tp = toEP small_p in + let impure_v = "I$"@@at in + let impure_c = funE(case_tp::small_tp::ntps, TypE(cases)@@at)@@at in + let impure_t = appTPs (VarE(impure_v)@@at) (case_tp::small_tp::ntps)@@at in + let ex_v = "J$"@@at in + let ex_c = + funE(small_tp::ntps, + TypE(StrT(seqD [VarD(case_v, funT(utps, TypT@@at, Pure@@at)@@at)@@at; + InclD(impure_t)@@at] @@at)@@at)@@at)@@at in + let ex_t = appTPs (VarE(ex_v)@@at) (small_tp::ntps)@@at in + let big_v = "T$"@@at in + let big_c = + let c_v = "c$"@@at in + funE(small_tp::tps, + TypE(funT([let b, _ = varP(c_v) in (b, ex_t, Expl@@at)@@at], + appTPs (DotE(VarE(c_v)@@at, case_v)@@at) utps@@at, + Impure@@at)@@at)@@at)@@at in + let big_t = appTPs (VarE(big_v)@@at) (small_tp::tps)@@at in + let small_c = recE(defaultTP small_p, funE(tps, TypE(WrapT(big_t)@@at)@@at)@@at)@@at in + let small_t = appTPs (VarE(small_v)@@at) tps@@at in + let cs_v = "cs$"@@at in + let cs_p = toEP (annotP(varP(cs_v)@@at, impure_t)@@at) in + let e_v = "e$"@@at in + let e_p = toEP (annotP(varP(e_v)@@at, small_t)@@at) in + let case_e = + funE(List.map toImpl (case_tp::tps) @ [cs_p; e_p], + appE(unwrapE(unrollE(VarE(e_v)@@at, small_t)@@at, WrapT(big_t)@@at)@@at, + StrE(SeqB(VarB(case_v, VarE(case_v)@@at)@@at, + InclB(VarE(cs_v)@@at)@@at)@@at)@@at)@@at)@@at in + let mk_v = "mk$"@@at in + let c_v = "c$"@@at in + let c_p = toEP (annotP(varP(c_v)@@at, big_t)@@at) in + let mk_e = + funE(List.map toImpl tps @ [c_p], + rollE(wrapE(VarE(c_v)@@at, WrapT(big_t)@@at)@@at, small_t)@@at)@@at in + let d_v = "D$"@@at in + let d_e = funE(ntps, appPs (VarE(ex_v)@@at) (small_tp::ntps))@@at in + let seal_e = + StrT(seqD [VarD(small_v, absTC(tps)@@at)@@at; + VarD(case_v, + funT(List.map toImpl (case_tp::tps) @ [cs_p], + funT([e_p], + appTPs (VarE(case_v)@@at) utps @@at, + Impure@@at)@@at, + Pure@@at)@@at)@@at; + VarD(mk_v, funT(List.map toImpl tps @ [c_p], small_t, Pure@@at)@@at)@@at; + VarD(d_v, funT(ntps, EqT(TypE(ex_t)@@at)@@at, Pure@@at)@@at)@@at] @@at)@@at in + letE( + InclB( + letE(seqB [VarB(impure_v, impure_c)@@at; + VarB(ex_v, ex_c)@@at; + VarB(big_v, big_c)@@at] @@at, + ascribeE(StrE(seqB [VarB(small_v, small_c)@@at; + VarB(case_v, case_e)@@at; + VarB(mk_v, mk_e)@@at; + VarB(d_v, d_e)@@at]@@at)@@at, + seal_e)@@at)@@at)@@at, + WithEnvE(fun env -> + let rec find_cases = function + | Types.TypT(Types.ExT(_, t)) -> find_cases t + | Types.FunT(_, _, Types.ExT(_, t), _) -> find_cases t + | Types.StrT(_::cases) -> cases + | _ -> failwith "bug" in + let cases = find_cases (Env.lookup_val d_v.it env) in + let cons = + cases + |> List.map (fun (label, ts) -> + let rec initPs = function + | Types.FunT (_, _, Types.ExT (_, ts), e) -> + (match e with + | Types.Implicit -> initPs ts + | Types.Explicit _ -> + toEP (varP(var "v$"@@at)@@at) :: initPs ts) + | _ -> [] in + let ps = initPs ts in + let r_v = "r$"@@at in + VarB(label@@at, + funE(List.map toImpl ntps @ ps, + appE(VarE(mk_v)@@at, + funE([toEP (annotP(varP(r_v)@@at, appTPs (VarE(d_v)@@at) ntps@@at)@@at)], + appPs (DotE(VarE(r_v)@@at, label@@at)@@at) ps)@@at)@@at)@@at)@@at) in + StrE(seqB ((VarB(small_v, VarE(small_v)@@at)@@at) :: + (VarB(case_v, VarE(case_v)@@at)@@at) :: cons)@@at)@@at)@@at) + (* String conversion *) @@ -367,6 +505,7 @@ let label_of_exp e = | UnwrapE _ -> "UnwrapE" | UnrollE _ -> "UnrollE" | RecE _ -> "RecE" + | WithEnvE _ -> "WithEnvE" let label_of_bind b = match b.it with @@ -425,6 +564,7 @@ and string_of_exp e = | UnwrapE(x, t) -> node' [string_of_var x; string_of_typ t] | UnrollE(x, t) -> node' [string_of_var x; string_of_typ t] | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e] + | WithEnvE(_) -> node' [""] and string_of_bind b = let node' = node (label_of_bind b) in