From aea03a2edc011e4046022800af8d6100087c67c2 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 | 4 ++ examples/fc.1ml | 22 ++----- examples/hoas.1ml | 36 +++--------- examples/tiv.1ml | 116 +++++++++++++++++++++++++++++++++++++ examples/trie.1ml | 23 ++------ lexer.mll | 1 + parser.mly | 5 ++ prelude/index.1mls | 5 ++ regression.1ml | 139 ++++++++++++++++++++++++++++++++++++++++++++ syntax.ml | 141 +++++++++++++++++++++++++++++++++++++++++++++ 11 files changed, 431 insertions(+), 65 deletions(-) create mode 100644 examples/tiv.1ml diff --git a/Makefile b/Makefile index fea2dc6f..2d333780 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 import elab \ + lib source prim fomega types env syntax \ + parser lexer iL erase trace sub import elab \ lambda compile \ main NOMLI = syntax iL main import diff --git a/elab.ml b/elab.ml index a0a16799..0f086448 100644 --- a/elab.ml +++ b/elab.ml @@ -599,6 +599,7 @@ 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.ImportE(path) -> (match Import.resolve (Source.at_file path) path.it with | None -> Source.error path.at ("\""^path.it^"\" does not resolve to a file") @@ -612,6 +613,9 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t)); appE(FunE(x'@@t.at, t, VarE(x'@@t.at)@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at in elab_exp env exp l + | 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)} s1 = ?Xt:*->*, Xu:*->*->*. !b:*. [= b] -> {t : [= Xt b], u : !a:*. [= a] => [= Xu b a]} diff --git a/examples/fc.1ml b/examples/fc.1ml index 20317435..a9ee414a 100644 --- a/examples/fc.1ml +++ b/examples/fc.1ml @@ -9,26 +9,14 @@ local import "prelude" ;; clarity. GADTs = { - Exp = { - local - type I (type t _) = { - type case _ - Zero : case int - Succ : t int ~> case int - Pair 'a 'b : t a ~> t b ~> case (a, b) - } - ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a} - I = I t - t - case (m: I) (e: t _) = e m - Zero : t _ = fun (m: I) => m.Zero - Succ x : t _ = fun (m: I) => m.Succ x - Pair l r : t _ = fun (m: I) => m.Pair l r + Exp = data case t _ :> { + Zero : case int + Succ : t int ~> case int + Pair 'a 'b : t a ~> t b ~> case (a, b) } eval = rec (eval 'a: Exp.t a ~> a) => - Exp.case { - type case x = x + Exp.case (type fun x => x) { Zero = 0 Succ x = eval x + 1 Pair l r = (eval l, eval r) diff --git a/examples/hoas.1ml b/examples/hoas.1ml index a958a343..f398e77b 100644 --- a/examples/hoas.1ml +++ b/examples/hoas.1ml @@ -5,35 +5,13 @@ local import "prelude" ;; ;; https://github.com/palladin/idris-snippets/blob/master/src/HOAS.idr -let - type I (type case _) (type t _) = { - Val 'x : x ~> case x - Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z - If 'x : t Bool.t ~> t x ~> t x ~> case x - App 'x 'y : t (x ~> y) ~> t x ~> case y - Lam 'x 'y : (t x ~> t y) ~> case (x ~> y) - Fix 'x 'y : t ((x ~> y) ~> x ~> y) ~> case (x ~> y) - } - type J (type t _) = {type case _, ...I case t} - type T (type t _) x = (c: J t) ~> c.case x - ...{ - ...rec {type t _} => {type t x = wrap T t x} - case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs} - mk (fn: T t _) = fn - } :> { - type t _ - case 'x: (type case _) -> I case t -> t x ~> case x - mk 'x: T t x -> t x - } - J = J t -in { - t, case - Val 'x (v: x) = mk fun (e: J) => e.Val v - Bin 'x 'y 'z (f: x ~> y ~> z) (l: t x) (r: t y) = mk fun (e: J) => e.Bin f l r - If 'x (b: t Bool.t) (c: t x) (a: t x) = mk fun (e: J) => e.If b c a - App 'x 'y (f: t (x ~> y)) (a: t x) = mk fun (e: J) => e.App f a - Lam 'x 'y (f: t x ~> t y) = mk fun (e: J) => e.Lam f - Fix 'x 'y (f: t ((x ~> y) ~> x ~> y)) = mk fun (e: J) => e.Fix f +data case t _ :> { + Val 'x : x ~> case x + Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z + If 'x : t Bool.t ~> t x ~> t x ~> case x + App 'x 'y : t (x ~> y) ~> t x ~> case y + Lam 'x 'y : (t x ~> t y) ~> case (x ~> y) + Fix 'x 'y : t ((x ~> y) ~> x ~> y) ~> case (x ~> y) } Fact = Fix <| Lam fun f => Lam fun x => diff --git a/examples/tiv.1ml b/examples/tiv.1ml new file mode 100644 index 00000000..3e950dd6 --- /dev/null +++ b/examples/tiv.1ml @@ -0,0 +1,116 @@ +local import "prelude" + +;; As 1ML is powerful enough to encode GADTs we can define a value independent +;; type representation or a deep embedding of type constructors. + +type iso a b = {to: a ~> b, from: b ~> a} + +Rep = { + data case t _ :> { + bool: case bool + char: case char + int : case int + text: case text + unit: case unit + + alt 'x 'y: t x ~> t y ~> case (alt x y) + ~~> 'x 'y: t x ~> t y ~> case (x ~> y) + pair 'x 'y: t x ~> t y ~> case (x, y) + + iso 'x 'y: iso x y ~> t y ~> case x + + lazy 'x: ({} ~> t x) ~> case x + } + + defaults (type t _) (default 'a: t a) = { + bool = default + char = default + int = default + unit = default + text = default + + alt _ _ = default + _ ~~> _ = default + pair _ _ = default + + iso _ _ = default + + lazy _ = default + } + + local i = {to = Opt.case {none = inl {}, some = inr} + from = Alt.case {inl {} = none, inr = some}} + opt a = iso i (alt unit a) + + local i = {to = List.case {nil = inl {}, x :: xs = inr (x, xs)} + from = Alt.case {inl {} = nil, inr (x, xs) = x::xs}} + list v = rec vs => lazy fun {} => iso i (alt unit (pair v vs)) +} + +;; Generic toText + +ToText = {type t x = x ~> text} + +toText = rec (toText 'x: Rep.t x ~> ToText.t x) => Rep.case ToText.t { + bool = Bool.toText + char c = "'" ++ Text.fromChar c ++ "'" + int = Int.toText + text t = "\"" ++ t ++ "\"" + unit {} = "{}" + + alt aT bT = Alt.case { + inl a = "(inl " ++ toText aT a ++ ")" + inr b = "(inr " ++ toText bT b ++ ")" + } + + (_ ~~> _) _ = "" + + pair aT bT (a, b) = "(" ++ toText aT a ++ ", " ++ toText bT b ++ ")" + + iso ab bT = ab.to >> toText bT + + lazy th = toText (th {}) +} + +println rep x = print (toText rep x ++ "\n") + +do let ...Rep + println int 101 + println (pair bool text) (true, "that") + println (opt bool) (some false) + println (iso {to i = i <> 0, from b = if b then 1 else 0} bool) 1 + println (list int) (3 :: (1 :: (4 :: nil))) + +;; Generic eq + +Eq = {type t x = x ~> x ~> bool} + +eq = rec (eq 'x: Rep.t x ~> Eq.t x) => Rep.case Eq.t { + bool = Bool.== + char = Char.== + int = Int.== + text = Text.== + unit _ _ = true + + alt aT bT l r = l |> Alt.case { + inl l = r |> Alt.case {inl = eq aT l, inr _ = false} + inr l = r |> Alt.case {inl _ = false, inr = eq bT l} + } + + (_ ~~> _) _ _ = false + + pair aT bT (l1, l2) (r1, r2) = eq aT l1 r1 && eq bT l2 r2 + + iso ab bT l r = eq bT (ab.to l) (ab.to r) + + lazy th l r = eq (th {}) l r +} + +do let ...Rep + test t l r = print ("eq " ++ toText t l ++ + " " ++ toText t r ++ + " = " ++ toText bool (eq t l r) ++ "\n") + test int 101 42 + test (pair int bool) (1, true) (1, true) + test (list int) (3 :: (1 :: nil)) (4 :: (1 :: nil)) + test (list int) (4 :: (2 :: nil)) (4 :: (2 :: nil)) diff --git a/examples/trie.1ml b/examples/trie.1ml index c1173329..ff64b907 100644 --- a/examples/trie.1ml +++ b/examples/trie.1ml @@ -1,25 +1,14 @@ local import "prelude" FunctionalTrie = { - local - type I (type t _ _) = { - type case _ _ - unit 'v : opt v ~> case {} v - alt 'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v - pair 'v 'k1 'k2 : t k1 (t k2 v) ~> case (k1, k2) v - } - ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v} - I = I t - - t - case (m: I) (e: t _ _) = e m - unit vO : t _ _ = fun (m: I) => m.unit vO - alt l r : t _ _ = fun (m: I) => m.alt l r - pair lr : t _ _ = fun (m: I) => m.pair lr + data case t _ _ :> { + unit 'v : opt v ~> case {} v + alt 'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v + pair 'v 'k1 'k2 : t k1 (t k2 v) ~> case (k1, k2) v + } lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) => - case { - type case k v = k ~> opt v + case (type fun k v => k ~> opt v) { unit m {} = m alt ta tb = Alt.case {inl = lookup ta, inr = lookup tb} pair ta (a, b) = lookup ta a |> Opt.case {none, some tb = lookup tb b} diff --git a/lexer.mll b/lexer.mll index 084cd91d..af9fb752 100644 --- a/lexer.mll +++ b/lexer.mll @@ -263,6 +263,7 @@ rule token = parse | "_" { HOLE } | "&&" { LOGICAL_AND } | "as" { AS } + | "data" { DATA } | "do" { DO } | "else" { ELSE } | "type_error" { TYPE_ERROR } diff --git a/parser.mly b/parser.mly index 5bdf2bba..0e9b97cd 100644 --- a/parser.mly +++ b/parser.mly @@ -39,6 +39,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s)) %token IMPORT %token WRAP_OP UNWRAP_OP %token ROLL_OP UNROLL_OP +%token DATA %token EOF @@ -424,6 +425,8 @@ annexp : { $2($1, $3)@@at() } ; exp : + | DATA name name typparamlist annexp_op typ + { dataE($2, $3, $4, $5, $6, at())@@at() } | LET bind IN exp { letE($2, $4)@@at() } | IF exp THEN exp ELSE exp @@ -504,6 +507,8 @@ atbind : { InclB(letE($2, $4)@@at())@@at() } | IMPORT TEXT { InclB(ImportE($2@@ati 2)@@at())@@at() } + | DATA name name typparamlist annexp_op typ + { InclB(dataE($2, $3, $4, $5, $6, at())@@at())@@at() } /* | LPAR bind RPAR { $2 } diff --git a/prelude/index.1mls b/prelude/index.1mls index b5117f18..c2c196a5 100644 --- a/prelude/index.1mls +++ b/prelude/index.1mls @@ -83,6 +83,10 @@ Text: { print: t ~> {} } +Unit: { + type t = {} +} + Zero: { type t } @@ -94,6 +98,7 @@ type int = Int.t type list a = List.t a type opt a = Opt.t a type text = Text.t +type unit = Unit.t type zero = Zero.t % * + - / : int -> int -> int diff --git a/regression.1ml b/regression.1ml index 34624c0f..a0918d2f 100644 --- a/regression.1ml +++ b/regression.1ml @@ -309,6 +309,112 @@ PolyRec = { t0 = inr (inl (0, 0) : t (int, int)) : t int } +;; + +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 + ...{ + ...rec {type t _} => {type t x = wrap T t x} + case 'x (type case _) (cs: I t case) (e: t _) = + e {case, ...cs} + mk 'x (c: T t x) = c + } :> { + 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 { + ...rec {type t _} => {type t x = wrap T t x} + case '(type case) 'x 'n (cs: I case t x) (e: t x) = + e {case, ...cs} + mk 'x (c: T t x) = c + 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 _ @@ -346,3 +452,36 @@ ListN = { x :: xs = xy x :: map xs } } + +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 { + ...rec {type t _ _} => {type t x n = wrap T t x n} + case (type case _) 'x 'n (cs: I case t x) (e: t x n) = + e {case, ...cs} + mk 'x 'n (c: T t x n) = c + 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' = { + data case t x _ :> { + nil : case N.Z + (::) 'n : x ~> t x n ~> case (N.S n) + } + + map 'x 'y 'n (xy: x -> y) = rec (map 'n: t x n ~> t y n) => + case (t y) { + nil + x :: xs = xy x :: map xs + } +} diff --git a/syntax.ml b/syntax.ml index fed2580e..e7bab293 100644 --- a/syntax.ml +++ b/syntax.ml @@ -54,6 +54,7 @@ and exp' = | RecE of var * typ * exp | ImportE of path | AnnotE of exp * typ + | WithEnvE of (Env.env -> exp) and bind = (bind', unit) phrase and bind' = @@ -334,6 +335,143 @@ let rollP(p, t2) = infer = None; annot = Some t2} +(* 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 seqDs = function + | [] -> EmptyD + | d::ds -> (List.fold_left (fun s d -> seqD(s, d)@@d.at) d ds).it + +let seqBs = 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 p = varP(var "_"@@atH) in (p.bind, 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(seqDs[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 p = varP(c_v) in (p.bind, 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(seqDs[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(seqBs[VarB(impure_v, impure_c)@@at; + VarB(ex_v, ex_c)@@at; + VarB(big_v, big_c)@@at] @@at, + ascribeE(StrE(seqBs[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(seqBs((VarB(small_v, VarE(small_v)@@at)@@at) :: + (VarB(case_v, VarE(case_v)@@at)@@at) :: cons)@@at)@@at)@@at) + (* *) @@ -395,6 +533,7 @@ let label_of_exp e = | RecE _ -> "RecE" | ImportE _ -> "ImportE" | AnnotE _ -> "AnnotE" + | WithEnvE _ -> "WithEnvE" let label_of_bind b = match b.it with @@ -455,6 +594,7 @@ and string_of_exp e = | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e] | ImportE(p) -> node' ["\"" ^ String.escaped p.it ^ "\""] | AnnotE(e, t) -> node' [string_of_exp e; string_of_typ t] + | WithEnvE(_) -> node' [""] and string_of_bind b = let node' = node (label_of_bind b) in @@ -504,6 +644,7 @@ and imports_exp exp = | RecE(_, typ, exp) -> imports_typ typ @ imports_exp exp | ImportE path -> [path] | AnnotE(exp, typ) -> imports_exp exp @ imports_typ typ + | WithEnvE(fn) -> [] and imports_bind bind = match bind.it with