From b1cad8b13cf247a9e93d3177a6205fd1851030c6 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Sun, 2 Feb 2020 22:24:56 +0200 Subject: [PATCH] Add simple recursive bindings --- basis/list.1ml | 11 ++-- elab.ml | 9 ++- examples/fc.1ml | 4 +- examples/hoas.1ml | 4 +- examples/trie.1ml | 4 +- lexer.mll | 26 +++++--- parser.mly | 18 +++++- prelude/index.1ml | 4 +- readme.1ml | 18 +++--- regression.1ml | 84 ++++++++++++++------------ russo.1ml | 16 ++--- syntax.ml | 147 +++++++++++++++++++++++++++++++++++++++++++++- talk.1ml | 12 ++-- 13 files changed, 264 insertions(+), 93 deletions(-) diff --git a/basis/list.1ml b/basis/list.1ml index 395fd9c0..3d006bee 100644 --- a/basis/list.1ml +++ b/basis/list.1ml @@ -7,18 +7,15 @@ isNil = case {nil = true, _::_ = false} head = case {nil = none, x::_ = some x} tail = case {nil = none, _::xs = some xs} -foldr (::) nil = rec loop => case {nil, x::xs = x::loop xs} +rec foldr (::) nil = case {nil, x::xs = x::foldr (::) nil xs} -foldl xss = rec (loop: _ -> _) => fun s => case { - nil = s - x :: xs = loop (xss x s) xs -} +rec foldl (::) nil = case {nil, x::xs = foldl (::) (x::nil) xs} length = foldl (const 1 >> (+)) 0 -nth = rec (loop: _ -> _) => fun n => case { +rec nth n = case { nil = none - x :: xs = if n == 0 then some x else loop (n-1) xs + x :: xs = if n == 0 then some x else nth (n-1) xs } revPrependTo = foldl (::) diff --git a/elab.ml b/elab.ml index 30bffa4f..0680c760 100644 --- a/elab.ml +++ b/elab.ml @@ -406,6 +406,12 @@ Trace.debug (lazy ("[VarE] s = " ^ string_of_norm_extyp (ExT([], lookup_var env let s, zs = elab_typ env typ "" in ExT([], TypT(s)), Pure, zs, IL.LamE("_", erase_extyp s, IL.TupE[]) + | EL.PathE(exp) -> + let s, p, zs, e = elab_exp env exp l in + if p = Impure then + error exp.at "impure type expression"; + s, p, zs, e + | EL.StrE(bind) -> elab_bind env bind l @@ -581,7 +587,8 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2)); ("recursive expression diverges: " ^ Sub.string_of_error e) in (* TODO: syntactic restriction *) - s2, Pure, lift_warn exp.at t2 (add_typs aks3 env) (zs1 @ zs2 @ zs3 @ zs4 @ zs5), + s2, Pure, + lift_warn exp.at t2 (add_typs aks2 env) (zs1 @ zs2 @ zs3 @ zs4 @ zs5), IL.RecE(var.it, erase_typ t2, e) | _ -> let t2, zs2 = elab_pathexp env1 exp1 l in diff --git a/examples/fc.1ml b/examples/fc.1ml index 20317435..a6270830 100644 --- a/examples/fc.1ml +++ b/examples/fc.1ml @@ -17,7 +17,7 @@ GADTs = { 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} + rec type t a = wrap (m: I t) ~> m.case a I = I t t case (m: I) (e: t _) = e m @@ -67,4 +67,4 @@ FunctionalDependences = { combine 'a (f: T a) (g: T a) : T a = fun (type F _) => f F << g F } -Newtype = rec {type T} => {type T = T ~> T} +Newtype = {rec type T = T ~> T} diff --git a/examples/hoas.1ml b/examples/hoas.1ml index a958a343..e9bca29e 100644 --- a/examples/hoas.1ml +++ b/examples/hoas.1ml @@ -17,7 +17,7 @@ let 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} + rec 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 } :> { @@ -41,7 +41,7 @@ Fact = Fix <| Lam fun f => Lam fun x => (Val 1) (Bin (*) x (App f (Bin (-) x (Val 1)))) -eval = rec (eval 'x: t x ~> x) => case (type fun t => t) { +rec eval 'x: t x ~> x = case (type fun t => t) { Bin f x y = f (eval x) (eval y) If b c a = eval if eval b then c else a App f x = eval f (eval x) diff --git a/examples/trie.1ml b/examples/trie.1ml index c1173329..5a912297 100644 --- a/examples/trie.1ml +++ b/examples/trie.1ml @@ -8,7 +8,7 @@ FunctionalTrie = { 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} + rec type t k v = wrap (m: I t) ~> m.case k v I = I t t @@ -17,7 +17,7 @@ FunctionalTrie = { alt l r : t _ _ = fun (m: I) => m.alt l r pair lr : t _ _ = fun (m: I) => m.pair lr - lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) => + rec lookup 'k 'v: t k v ~> k ~> opt v = case { type case k v = k ~> opt v unit m {} = m diff --git a/lexer.mll b/lexer.mll index f02ff917..1ac7fc13 100644 --- a/lexer.mll +++ b/lexer.mll @@ -112,10 +112,14 @@ module Offside = struct if column < indent - 2 then error "offside" else emit token >> get >>= inside_braces break false indent + | AND -> + if column < indent then error "offside" else + emit token >> + get >>= inside_braces break false indent | _ -> if column < indent then error "offside" else emit_if (column = indent && insert) COMMA >> - nest (token, column) >> + nest false (token, column) >> get >>= inside_braces break (token <> LOCAL) indent and inside_local insert indent (token, column) = @@ -132,7 +136,7 @@ module Offside = struct emit IN else emit_if (column = indent && insert) COMMA >> - nest (token, column) >> + nest false (token, column) >> get >>= inside_local (token <> LOCAL) indent and inside_let insert indent (token, column) = @@ -151,12 +155,13 @@ module Offside = struct inside_in false column (token, column) else emit_if (column = indent && insert) COMMA >> - nest (token, column) >> + nest false (token, column) >> get >>= inside_let (token <> LOCAL) indent and inside_in insert indent (token, column) = match token with - | RBRACE | COMMA | IN | EOF | RPAR | ELSE | THEN -> unget (token, column) + | RBRACE | COMMA | IN | EOF | RPAR | ELSE | THEN | EQUAL -> + unget (token, column) | SEMI -> if column < indent - 2 then error "offside" else emit token >> @@ -170,7 +175,7 @@ module Offside = struct let slack = slack_of token in if column < indent - slack then unget (token, column) else emit_if (slack = 0 && column = indent && insert) SEMI >> - nest (token, column) >> + nest true (token, column) >> get >>= inside_in (slack = 0 && indent <= column) indent and inside_parens indent (token, column) = @@ -180,7 +185,7 @@ module Offside = struct emit token >> get >>= inside_parens indent | _ -> - nest (token, column) >> + nest true (token, column) >> get >>= inside_in false indent >> get >>= inside_parens indent @@ -203,8 +208,8 @@ module Offside = struct emit ELSE >> emit LBRACE >> emit RBRACE >> unget (token, column) - and nest (token, column) = - (match token with FUN | REC | IF -> emit LPAR | _ -> unit) >> + and nest is_expr (token, column) = + (match token with (FUN | REC | IF) when is_expr -> emit LPAR | _ -> unit) >> emit token >> match token with | LBRACE -> @@ -220,9 +225,11 @@ module Offside = struct | DARROW -> get >>= fun (token, column) -> inside_in false column (token, column) >> - emit RPAR + if is_expr then emit RPAR else unit | EQUAL | DO -> get >>= fun (token, column) -> inside_in false column (token, column) + | TYPE_ERROR -> + get >>= fun (token, column) -> inside_in false column (token, column) | IF -> inside_if column >> emit RPAR @@ -278,6 +285,7 @@ rule token = parse | "import" { IMPORT } | "primitive" { PRIMITIVE } | "rec" { REC } + | "and" { AND } | "then" { THEN } | "type" { TYPE } | "with" { WITH } diff --git a/parser.mly b/parser.mly index 5df9fc81..ebc2e7ef 100644 --- a/parser.mly +++ b/parser.mly @@ -26,7 +26,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s)) %} %token HOLE PRIMITIVE -%token FUN REC LET IN DO WRAP TYPE ELLIPSIS +%token FUN REC AND LET IN DO WRAP TYPE ELLIPSIS %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS %token EQUAL COLON SEAL ARROW SARROW DARROW %token WITH @@ -511,12 +511,24 @@ atbind : { $2 } */ ; +atbinds : + | atbind + { $1 } + | atbind AND atbinds + { seqB($1, $3)@@at() } +; +recbind : + | atbind + { $1 } + | REC atbinds + { recB($2)@@at() } +; bind : | { EmptyB@@at() } - | atbind + | recbind { $1 } - | atbind COMMA bind + | recbind COMMA bind { seqB($1, $3)@@at() } | LOCAL bind IN bind { letB($2, $4)@@at() } diff --git a/prelude/index.1ml b/prelude/index.1ml index b7185c9c..6a74d43c 100644 --- a/prelude/index.1ml +++ b/prelude/index.1ml @@ -10,7 +10,7 @@ Fun = { type t a b = a ~> b id x = x const x _ = x - bot = rec (bot: _ -> _) => fun x => bot x + rec bot: _ -> _ = fun x => bot x curry f x y = f (x, y) uncurry f (x, y) = f x y flip f x y = f y x @@ -55,7 +55,7 @@ Pair = { } List = { - ...rec {type t _} => {type t x = Opt.t (x, t x)} + rec type t x = Opt.t (x, t x) nil = Opt.none hd :: tl = Opt.some (hd, tl) case {nil, ::} = Opt.case { diff --git a/readme.1ml b/readme.1ml index c1b0b30b..38e07b95 100644 --- a/readme.1ml +++ b/readme.1ml @@ -46,8 +46,8 @@ p = f (fun x => x) -type stream = rec t => {hd : int, tl : () ~> opt t} ;; creates rec type -single x : stream = {hd = x, tl = fun () => none} ;; b : t rolls value into t +rec type stream t = {hd : t, tl : () ~> opt (stream t)} ;; creates rec type +single x : stream _ = {hd = x, tl = fun () => none} ;; b : t rolls value into t {hd = n} = single 5 ;; pattern match rec value do Int.print n ;; or: do Int.print (single 7).hd ;; access rec value @@ -55,18 +55,16 @@ do Int.print (single 7).hd ;; access rec value -count = rec self => fun i => - if i <> 0 then self (i - 1) +rec count i = + if i <> 0 then count (i - 1) -repeat = rec self => fun x : stream => - {hd = x, tl = fun () => some (self x)} +rec repeat x : stream _ = + {hd = x, tl () = some (repeat x)} -{even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => { - even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))} - odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))} -} +rec even x : stream _ = {hd = x, tl () = some (odd (x + 1))} +and odd x : stream _ = {hd = x, tl () = some (even (x + 1))} diff --git a/regression.1ml b/regression.1ml index 6220a0c1..3012add2 100644 --- a/regression.1ml +++ b/regression.1ml @@ -226,48 +226,54 @@ type_error rec (R: {}) => { kaboom () = R } -Kaboom = rec (R: rec R => {kaboom: () ~> R}) : (= R) => {kaboom () = R} +rec Kaboom : rec R => {kaboom: () ~> R} = {kaboom () = Kaboom} + +rec isEven n = n == 0 || isOdd (n-1) +and isOdd n = n == 1 || (n <> 0 && isEven (n-1)) ;; Mutually = let - T = rec (R: { - Even: {type t _} - Odd: {type t _} - }) => { - Even = { - type t x = {head: x, tail: R.Odd.t x} + T = { + rec Even = { + type t x = {head: x, tail: Odd.t x} } - Odd = { - type t x = opt (R.Even.t x) + and Odd = { + type t x = opt (Even.t x) } } in { - ...rec (R: { - Even: { - size 'x: T.Even.t x ~> int - } - Odd: { - size 'x: T.Odd.t x ~> int - } - }) => { - Even = { - ...T.Even - make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x = - {head, tail} - size 'x (v: T.Even.t x) = 1 + R.Odd.size v.tail - } - Odd = { - ...T.Odd - make 'x (v: opt (T.Even.t x)) : T.Odd.t x = v - size 'x (v: T.Odd.t x) = - v |> Opt.case { - none = 0 - some e = R.Even.size e - } - } + rec Even = { + make head (tail: T.Odd.t _) : T.Even.t _ = {head, tail} + size (v: T.Even.t _) = 1 + Odd.size v.tail + ...T.Even + } + and Odd = { + make (v: opt (T.Even.t _)) : T.Odd.t _ = v + size (v: T.Odd.t _) = + v |> Opt.case { + none = 0 + some = Even.size + } + ...T.Odd } +(; + rec Even = { + type t x = {head: x, tail: Odd.t x} + make head (tail: Odd.t _) : t _ = {head, tail} + size (v: t _) = 1 + Odd.size v.tail + } + and Odd = { + type t x = opt (Even.t x) + make (v: opt (Even.t _)) : t _ = v + size (v: t _) = + v |> Opt.case { + none = 0 + some = Even.size + } + } +;) one = Odd.size (Odd.make (some (Even.make true (Odd.make none)))) } @@ -295,9 +301,9 @@ AnnotRecType = { } Hungry = { - type eat a = rec eat_a => a ~> eat_a + rec type eat a = a ~> eat a - eater 'a = rec (eater: eat a) : eat a => fun a => eater + rec eater 'a: eat a = fun a => eater do eater 1 2 do eater 1 2 3 @@ -310,8 +316,8 @@ type_error rec {type t _, type u _} => { type_error type rec t => t PolyRec = { - type l a = rec (type t) => a | t - ...rec {type t a} => {type t a = a | t (a, a)} + rec type l a = a | l a + rec type t a = a | t (a, a) t_int = t int @@ -333,7 +339,7 @@ ListN = let :: 'n : x ~> t x n ~> p (N.S n) } in { - ...rec {type t _ _} => {type t x n = wrap (type p _) -> I x p t ~> p n} + rec type t x n = wrap (type p _) -> I x p t ~> p n case 'x 'n (type p _) (cs: I x p t) (e : t _ _) = e p cs @@ -351,9 +357,9 @@ in { ListN = { ...ListN - map 'x 'y (xy: x ~> y) = rec (map 'n: t x n ~> t y n) => + rec map 'x 'y 'n (xy: x ~> y) : t x n ~> t y n = case (t _) { nil - x :: xs = xy x :: map xs + x :: xs = xy x :: map xy xs } } diff --git a/russo.1ml b/russo.1ml index 90133049..956e1e72 100644 --- a/russo.1ml +++ b/russo.1ml @@ -30,11 +30,11 @@ ArraySucc (A : ARRAY) = { else (a.1, A.update a.2 (i / 2) x) } -MkArray = rec (mkArray : int ~> ARRAY) => fun n => - if n == 0 then ArrayZero else ArraySucc (mkArray (n - 1)) : ARRAY +rec MkArray n = + if n == 0 then ArrayZero else ArraySucc (MkArray (n - 1)) : ARRAY printArray 't (A : ARRAY) (pr : t ~> ()) a = - let loop = rec loop => fun i => + let rec loop i = if i == A.dim then print "\n" else @@ -67,13 +67,13 @@ type STREAM = { } divides k n = - let loop = rec loop => fun i => (i * k == n) || ((i * k < n) && loop (i + 1)) + let rec loop i = (i * k == n) || ((i * k < n) && loop (i + 1)) loop 1 sift (S : STREAM) :> STREAM = { type state = S.state divisor = S.value S.start - filter = rec filter => fun s => + rec filter s = if divides divisor (S.value s) then filter (S.next s) else s start = filter S.start next s = filter (S.next s) @@ -92,10 +92,10 @@ Sieve :> STREAM = { value (S :# state) = S.value S.start } -nthstate = rec (nthstate : int ~> Sieve.state) => fun n => +rec nthstate n = if n == 0 then Sieve.start else Sieve.next (nthstate (n -1)) nthprime n = Sieve.value (nthstate n) -printprimes = rec loop => fun n => - if n == 0 then () else loop (n - 1) ; Int.print (nthprime n) ; print "\n" +rec printprimes n = + if n <> 0 then printprimes (n - 1) ; Int.print (nthprime n) ; print "\n" do printprimes 20 diff --git a/syntax.ml b/syntax.ml index e5169916..71df3c9d 100644 --- a/syntax.ml +++ b/syntax.ml @@ -42,6 +42,7 @@ and exp' = | VarE of var | PrimE of Prim.const | TypE of typ + | PathE of exp | StrE of bind | FunE of var * typ * exp * impl | WrapE of var * typ @@ -106,7 +107,7 @@ let opt fn (e, t) = let typE(t) = match t.it with - | PathT(e) -> e.it + | PathT(e) -> PathE(e) | _ -> TypE(t) let pathT(e) = @@ -400,6 +401,7 @@ let label_of_exp e = | VarE _ -> "VarE" | PrimE _ -> "PrimE" | TypE _ -> "TypE" + | PathE _ -> "PathE" | StrE _ -> "StrE" | FunE _ -> "FunE" | WrapE _ -> "WrapE" @@ -458,6 +460,7 @@ and string_of_exp e = | VarE(x) -> node' [string_of_var x] | PrimE(c) -> node' [Prim.string_of_const c] | TypE(t) -> node' [string_of_typ t] + | PathE(e) -> node' [string_of_exp e] | StrE(b) -> node' [string_of_bind b] | FunE(x, t, e, i) -> node' [string_of_var x; string_of_typ t; string_of_exp e; string_of_impl i] @@ -509,6 +512,7 @@ and imports_exp exp = | VarE _ -> [] | PrimE _ -> [] | TypE typ -> imports_typ typ + | PathE exp -> imports_exp exp | StrE bind -> imports_bind bind | FunE(_, typ, exp, _) -> imports_typ typ @ imports_exp exp | WrapE(_, typ) -> imports_typ typ @@ -529,3 +533,144 @@ and imports_bind bind = | VarB(_, exp) -> imports_exp exp | InclB exp -> imports_exp exp | TypeAssertB(_, exp) -> imports_exp exp + +(* rec ... and ... *) + +let rec extract_sig_exp e = + (match e.it with + | StrE(b) -> StrT(extract_sig_bind true b) + | TypE _ -> TypT + | PathE _ -> TypT + | FunE(v, td, e, i) -> + let tc = extract_sig_exp e in + let p = + if i.it == Impl then Pure else + match e.it with + | FunE _ -> Pure + | TypE _ -> Pure + | PathE _ -> Pure + | _ -> Impure in + FunT(v, td, tc, p@@e.at, i) + | AnnotE(e, t) -> t.it + | _ -> HoleT)@@e.at + +and extract_sig_bind tail b = + (match b.it with + | EmptyB -> EmptyD + | SeqB(bl, br) -> seqD(extract_sig_bind false bl, extract_sig_bind tail br) + | VarB(v, e) -> VarD(v, extract_sig_exp e) + | InclB(e) -> + if tail then EmptyD else error b.at "... only allowed at end inside rec" + | TypeAssertB _ -> EmptyD)@@b.at + +let rec extract_subst p d = + match d.it with + | EmptyD -> [] + | SeqD(dl, dr) -> extract_subst p dl @ extract_subst p dr + | VarD(v, _) -> [(v.it, DotE(p, v))] + | InclD(_) -> assert false + +let rec map_bind fn b = + (match b.it with + | EmptyB -> EmptyB + | SeqB(bl, br) -> seqB(map_bind fn bl, map_bind fn br) + | VarB(v, e) -> VarB(v, fn e) + | InclB(e) -> assert false + | TypeAssertB(p, e) -> TypeAssertB(p, fn e))@@b.at + +let rec generalize_bind p d = + (match d.it with + | EmptyD -> EmptyB + | SeqD(dl, dr) -> seqB(generalize_bind p dl, generalize_bind p dr) + | VarD(v, t) -> VarB(v, generalize_exp (DotE(p, v)@@v.at) t) + | InclD(_) -> assert false)@@d.at + +and generalize_exp p t = + (match t.it with + | StrT(d) -> StrE(seqB(InclB(p)@@t.at, generalize_bind p d)@@t.at) + | _ -> p.it)@@t.at + +type 'a subst = (string * 'a) list + +let subst_exp_var (s: 'a subst) (v: var) = + try List.assoc v.it s with Not_found -> VarE(v) + +let drop_subst v s = List.filter (fun (v', _) -> v.it <> v') s + +let rec subst_exp_typ s t = + (match t.it with + | PathT(e) -> PathT(subst_exp_exp s e) + | PrimT(s) -> PrimT(s) + | TypT -> TypT + | HoleT -> HoleT + | StrT(d) -> + let _, d = subst_exp_dec true s d in + StrT(d) + | FunT(v, td, tr, e, i) -> + FunT(v, subst_exp_typ s td, subst_exp_typ (drop_subst v s) tr, e, i) + | WrapT(t) -> WrapT(subst_exp_typ s t) + | EqT(e) -> EqT(subst_exp_exp s e) + | AsT(tl, tr) -> AsT(subst_exp_typ s tl, subst_exp_typ s tr) + | WithT(t, vs, e) -> WithT(subst_exp_typ s t, vs, subst_exp_exp s e) + )@@t.at + +and subst_exp_dec tail s d = + match d.it with + | EmptyD -> s, EmptyD@@d.at + | SeqD(dl, dr) -> + let s, dl = subst_exp_dec false s dl in + let s, dr = subst_exp_dec tail s dr in + s, SeqD(dl, dr)@@d.at + | VarD(v, t) -> + drop_subst v s, VarD(v, subst_exp_typ s t)@@d.at + | InclD(t) -> + if tail then s, InclD(subst_exp_typ s t)@@d.at + else error d.at "... only allowed at end inside rec" + +and subst_exp_exp s e = + (match e.it with + | VarE(v) -> subst_exp_var s v + | PrimE(s) -> PrimE(s) + | TypE(t) -> TypE(subst_exp_typ s t) + | PathE(e) -> PathE(subst_exp_exp s e) + | StrE(b) -> + let _, b = subst_exp_bind true s b in + StrE(b) + | FunE(v, t, e, i) -> + FunE(v, subst_exp_typ s t, subst_exp_exp (drop_subst v s) e, i) + | WrapE(v, t) -> wrapE(subst_exp_var s v@@e.at, subst_exp_typ s t) + | RollE(v, t) -> rollE(subst_exp_var s v@@e.at, subst_exp_typ s t) + | IfE(v, ec, ea) -> + ifE(subst_exp_var s v@@e.at, subst_exp_exp s ec, subst_exp_exp s ea) + | DotE(e, v) -> DotE(subst_exp_exp s e, v) + | AppE(vf, va) -> appE(subst_exp_var s vf@@e.at, subst_exp_var s va@@e.at) + | UnwrapE(v, t) -> unwrapE(subst_exp_var s v@@e.at, subst_exp_typ s t) + | UnrollE(v, t) -> unrollE(subst_exp_var s v@@e.at, subst_exp_typ s t) + | RecE(v, t, e) -> RecE(v, subst_exp_typ s t, subst_exp_exp ((v.it, VarE(v))::s) e) + | ImportE(p) -> ImportE(p) + | AnnotE(e, t) -> AnnotE(subst_exp_exp s e, subst_exp_typ s t) + )@@e.at + +and subst_exp_bind tail s b = + match b.it with + | EmptyB -> s, EmptyB@@b.at + | SeqB(bl, br) -> + let s, bl = subst_exp_bind false s bl in + let s, br = subst_exp_bind tail s br in + s, SeqB(bl, br)@@b.at + | VarB(v, e) -> + drop_subst v s, VarB(v, subst_exp_exp s e)@@b.at + | InclB(e) -> + if tail then s, InclB(subst_exp_exp s e)@@b.at + else error b.at "... only allowed at end inside rec" + | TypeAssertB(p, e) -> + s, TypeAssertB(p, subst_exp_exp s e)@@b.at + +let recB(b) = + let d = extract_sig_bind false b in + let r = uniq_var()@@b.at in + let rv = VarE(r)@@b.at in + let s = extract_subst rv d in + let b' = b |> map_bind (subst_exp_exp s) in + letB(VarB(r, RecE(r, StrT(d)@@b.at, StrE(b')@@b.at)@@b.at)@@b.at, + generalize_bind rv d) diff --git a/talk.1ml b/talk.1ml index 8d40f1e8..381458c4 100644 --- a/talk.1ml +++ b/talk.1ml @@ -101,15 +101,13 @@ do map : 'a -> 'b -> (m: type -> type) -> (M: MONAD m) -> (a ~> b) ~> m a ~> m b ;; Objects -...rec {type point} => { - type point = { - getX : () ~> int - getY : () ~> int - move : int ~> int ~> point - } +rec type point = { + getX : () ~> int + getY : () ~> int + move : int ~> int ~> point } -newpoint = rec (newpoint : int -> int -> point) => fun x y : point => { +rec newpoint x y : point = { getX () = x getY () = y move dx dy = newpoint (x + dx) (y + dy)