~ejb/thon

b0d1b0ca2d44c977aa20bd4b548ed7efe1e4c364 — Evan Bergeron 8 months ago 32a6f73
Add empty binary tree example
2 files changed, 26 insertions(+), 0 deletions(-)

A examples/emptybst.thon
M thon.sml
A examples/emptybst.thon => examples/emptybst.thon +4 -0
@@ 0,0 1,4 @@
(* node is empty or is a nat with two children *)
fold u node. (unit | (nat * (node * node)))
(* take the left case (is empty) *)
with left unit : (unit | (nat * ((u node. (unit | (nat * (node * node)))) * (u node. (unit | (nat * (node * node)))))))
\ No newline at end of file

M thon.sml => thon.sml +22 -0
@@ 1008,6 1008,28 @@ val Zero : Ast.Exp = runFile "/home/evan/thon/examples/eq.thon";

val Succ Zero : Ast.Exp = runFile "/home/evan/thon/examples/len.thon";

val Fold
    (TyRec
       ("node",
        Plus (Unit,Prod (Nat,Prod (TypVar ("node",0),TypVar ("node",0))))),
     PlusLeft
       (Plus
          (Unit, (*empty base or... *)
           Prod (* a nat and... *)
             (Nat,
              Prod (* a node and... *)
                (TyRec
                   ("node",
                    Plus
                      (Unit,
                       Prod (Nat,Prod (TypVar ("node",0),TypVar ("node",0))))),
                 TyRec (* a another node. *)
                   ("node",
                    Plus
                      (Unit,
                       Prod (Nat,Prod (TypVar ("node",0),TypVar ("node",0)))))))),
        TmUnit)) : Ast.Exp = runFile "/home/evan/thon/examples/emptybst.thon";

in
()
end