From db6923a1f3951cb8bd6feb3c40588d4627c8d1a2 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Sat, 28 Dec 2019 15:38:42 +0200 Subject: [PATCH] Add support for mutually recursive types with type parameters --- elab.ml | 56 +++++++++++++++++------- regression.1ml | 114 +++++++++++++++++++++++++++++++++++++++++++++++++ sub.ml | 22 ++++++++++ 3 files changed, 177 insertions(+), 15 deletions(-) diff --git a/elab.ml b/elab.ml index 069e126b..f4232e14 100644 --- a/elab.ml +++ b/elab.ml @@ -122,6 +122,27 @@ and paths_row ta ps = function ts1 @ ts2 +let rec_from_extyp typ label s = + match s with + | ExT([], t) -> + let rec find_rec = function + | AppT(t, ts) -> + let rec_t, unroll_t, roll_t, ak = find_rec t in + rec_t, AppT(unroll_t, ts), AppT(roll_t, ts), ak + | RecT(ak, unroll_t) as rec_t -> + rec_t, unroll_t, rec_t, ak + | DotT(t, lab) -> + let rec_t, unroll_t, roll_t, ak = find_rec t in + rec_t, DotT(unroll_t, lab), DotT(roll_t, lab), ak + | _ -> + error typ.at ("non-recursive type for " ^ label ^ ":" + ^ " " ^ Types.string_of_extyp s) in + find_rec t + | _ -> + error typ.at ("non-recursive type for " ^ label ^ ":" + ^ " " ^ Types.string_of_extyp s) + + (* Instantiation *) let rec instantiate env t e = @@ -386,15 +407,18 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain | EL.RollE(var, typ) -> let s, zs1 = elab_typ env typ l in - let t, ak, t' = - match s with - | ExT([], (RecT(ak, t') as t)) -> t, ak, t' - | _ -> error typ.at "non-recursive type for rolling" in + let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "rolling" s in + let var_t = lookup_var env var in + let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in let _, zs2, f = - try sub_typ env (lookup_var env var) (subst_typ (subst [ak] [t]) t') [] - with Sub e -> error var.at ("rolled value does not match annotation") in - ExT([], t), Pure, zs1 @ zs2, - IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ t) + try sub_typ env var_t unroll_t [] + with Sub e -> + error var.at ("rolled value does not match annotation:" + ^ " " ^ Types.string_of_typ var_t ^ " " + ^ "<" + ^ " " ^ Types.string_of_typ unroll_t) in + ExT([], roll_t), Pure, zs1 @ zs2, + IL.RollE(IL.AppE(f, IL.VarE(var.it)), erase_typ roll_t) | EL.IfE(var, exp1, exp2, typ) -> let t0, zs0, ex = elab_instvar env var in @@ -489,13 +513,15 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2)); | EL.UnrollE(var, typ) -> let s, zs1 = elab_typ env typ l in - let t, ak, t' = - match s with - | ExT([], (RecT(ak, t') as t)) -> t, ak, t' - | _ -> error typ.at "non-recursive type for rolling" in - let _, zs2, f = try sub_typ env (lookup_var env var) t [] with Sub e -> - error var.at ("unrolled value does not match annotation") in - ExT([], subst_typ (subst [ak] [t]) t'), Pure, zs1 @ zs2, + let rec_t, unroll_t, roll_t, ak = rec_from_extyp typ "unrolling" s in + let var_t = lookup_var env var in + let _, zs2, f = try sub_typ env var_t roll_t [] with Sub e -> + error var.at ("unrolled value does not match annotation:" + ^ " " ^ Types.string_of_typ var_t ^ " " + ^ "<" + ^ " " ^ Types.string_of_typ roll_t) in + let unroll_t = subst_typ (subst [ak] [rec_t]) unroll_t in + ExT([], unroll_t), Pure, zs1 @ zs2, IL.UnrollE(IL.AppE(f, IL.VarE(var.it))) | EL.RecE(var, typ, exp1) -> diff --git a/regression.1ml b/regression.1ml index 28c41272..34705eca 100644 --- a/regression.1ml +++ b/regression.1ml @@ -35,3 +35,117 @@ type_error { Impure : () => {type t; existentials: t} = fun () => {type t = bool; existentials = true} :> {type t = bool; existentials: t}; }; + +;; + +Mutually = { + T = rec (R: { + Even: {type t _}; + Odd: {type t _}; + }) => { + Even = { + type t x = {head: x; tail: R.Odd.t x}; + }; + Odd = { + type t x = opt (R.Even.t x); + }; + }; + + V = rec (R: { + Even: { + make 'x: x => T.Odd.t x => T.Even.t x; + size 'x: T.Even.t x -> int; + }; + Odd: { + make 'x: opt (T.Even.t x) => T.Odd.t x; + size 'x: T.Odd.t x -> int; + }; + }) => { + Even = { + make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x = + @(T.Even.t x) {head; tail}; + size 'x (v: T.Even.t x) = 1 + R.Odd.size v.@(T.Even.t _).tail; + }; + Odd = { + make 'x (v: opt (T.Even.t x)) : T.Odd.t x = @(T.Odd.t x) v; + size 'x (v: T.Odd.t x) = + caseopt v.@(T.Odd.t x) + (fun () => 0) + (fun e => R.Even.size e); + }; + }; +}; + +Mutually = { + Even = {...Mutually.T.Even; ...Mutually.V.Even}; + Odd = {...Mutually.T.Odd; ...Mutually.V.Odd}; + + one = Odd.size (Odd.make (some (Even.make true (Odd.make none)))); +}; + +;; + +Hungry = { + type eat a = rec eat_a => a -> eat_a; + + eater 'a: eat a = rec (eater: eat a) => @(eat a) (fun a => eater); + + (<+) eater x = eater.@(eat _) x; + + do eater <+ 1 <+ 2; +}; + +PolyRec = { + type l a = rec (type t) => alt a t; + ...rec {type t a} => {type t a = alt a (t (type (a, a)))}; + + t_int = t int; + + hmm (x: t int) = casealt (x.@(t int)); + + t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0)))); +}; + +N :> { + type Z; + type S _; +} = { + type Z = {}; + type S _ = {}; +}; + +ListN = let + type I (type x) (type p _) (type t _ _) = { + nil : p N.Z; + (::) 'n : x -> t x n -> p (N.S n); + }; + type T x n (type t _ _) = (type p _) => I x p t -> p n; +in { + ...rec {type t _ _} => {type t x n = 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); +}; + +ListN = { + ...ListN; + 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/sub.ml b/sub.ml index 89727d54..001bc175 100644 --- a/sub.ml +++ b/sub.ml @@ -141,6 +141,10 @@ let rec sub_typ env t1 t2 ps = ts, zs, IL.TupE(List.map2 (fun (l, _) f -> l, IL.AppE(f, IL.DotE(e1, l))) tr2 fs) + | TupT(tr1), TupT(tr2) -> + let zs = equal_row env tr1 tr2 ps in + [], zs, e1 + | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) -> if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2))); let env' = add_typs aks2 env in @@ -176,6 +180,17 @@ let rec sub_typ env t1 t2 ps = raise (Sub (Mismatch(t1, t2))) in [], zs, e1 + | LamT(aks1, t1'), LamT(aks2, t2') -> + if List.length aks1 <> List.length aks2 || + List.exists2 (fun ak1 ak2 -> snd ak1 <> snd ak2) aks1 aks2 then + raise (Sub (Mismatch(t1, t2))); + let zs = try + equal_typ (add_typs aks2 env) + (subst_typ (subst aks1 (varTs aks2)) t1') t2' + with Sub e -> + raise (Sub (Mismatch(t1, t2))) + in [], lift env zs, e1 + | RecT(ak1, t1'), RecT(ak2, t2') -> if snd ak1 <> snd ak2 then raise (Sub (Mismatch(t1, t2))); @@ -309,3 +324,10 @@ and equal_extyp env s1 s2 = let _, zs2, _ = try sub_extyp env s2 s1 [] with Sub e -> raise (Sub (Right e)) in zs1 @ zs2 + +and equal_row env tr1 tr2 ps = + let _, zs1, _ = + try sub_row env tr1 tr2 ps with Sub e -> raise (Sub (Left e)) in + let _, zs2, _ = + try sub_row env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in + zs1 @ zs2