~ejb/thon

b6eff33c18bf436fc41bfe3a444a57acc28460d7 — Evan Bergeron 8 months ago b0d1b0c master
Add singleton bst and start bst insert
3 files changed, 110 insertions(+), 0 deletions(-)

A examples/bst.thon
A examples/singletonbst.thon
M thon.sml
A examples/bst.thon => examples/bst.thon +68 -0
@@ 0,0 1,68 @@
let decr : nat -> nat =
  \ x : nat ->
    ifz x of
      Z -> Z
    | S p -> p
in let sub : nat -> nat -> nat =
  \ x : nat ->
  \ y : nat ->
    rec y of
      Z -> x
    | prevRec -> (decr prevRec)
in let lt : nat -> nat -> nat =
  \ x : nat ->
  \ y : nat ->
  ifz (sub y x) of
    Z -> Z
  | S p -> S Z
in let nil : u node. (unit | (nat * (node * node))) =
  fold u node. (unit | (nat * (node * node)))
  with left unit : (unit | (nat * ((u node. (unit | (nat * (node * node)))) * (u node. (unit | (nat * (node * node)))))))
in let insert : nat -> (u node. (unit | (nat * (node * node)))) ->  (u node. (unit | (nat * (node * node)))) =
    \ n : nat ->
    \ bst : (u node. (unit | (nat * (node * node)))) ->
    case (unfold bst) of
        empty -> (
            fold u node. (unit | (nat * (node * node)))
            with right
            (n, (* put the number in the tree *)
                (
                    (*nil node*)
                    fold u node. (unit | (nat * (node * node)))
                    with left unit : (
                        unit
                    | (nat * ((u node. (unit | (nat * (node * node)))) *
                                (u node. (unit | (nat * (node * node))))
                            )
                        )
                    )
                    ,
                    (*nil node*)
                    fold u node. (unit | (nat * (node * node)))
                    with left unit : (
                        unit
                    | (nat * ((u node. (unit | (nat * (node * node)))) *
                                (u node. (unit | (nat * (node * node))))
                            )
                        )
                    )
                )
            ) : (
                unit
            | (nat * ((u node. (unit | (nat * (node * node)))) *
                        (u node. (unit | (nat * (node * node))))
                    )
                )
            )
        )
    | natAndNodeAndNode -> (
        let thisNode : nat = fst natAndNodeAndNode in
        let leftNode : (u node. (unit | (nat * (node * node)))) = fst (snd natAndNodeAndNode) in
        let rightNode : (u node. (unit | (nat * (node * node)))) = snd (snd natAndNodeAndNode) in
        (* OK so this program is not done yet - in the recursive case we just return the empty bst...
         * need to ponder how to recurse in this case. *)
        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)))))))
    )
in insert

A examples/singletonbst.thon => examples/singletonbst.thon +31 -0
@@ 0,0 1,31 @@
fold u node. (unit | (nat * (node * node)))
with right
(Z,
    (
        (*nil node*)
        fold u node. (unit | (nat * (node * node)))
        with left unit : (
            unit
          | (nat * ((u node. (unit | (nat * (node * node)))) *
                    (u node. (unit | (nat * (node * node))))
                   )
            )
        )
        ,
        (*nil node*)
        fold u node. (unit | (nat * (node * node)))
        with left unit : (
            unit
          | (nat * ((u node. (unit | (nat * (node * node)))) *
                    (u node. (unit | (nat * (node * node))))
                   )
            )
        )
    )
) : (
    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 +11 -0
@@ 1030,6 1030,17 @@ val Fold
                       Prod (Nat,Prod (TypVar ("node",0),TypVar ("node",0)))))))),
        TmUnit)) : Ast.Exp = runFile "/home/evan/thon/examples/emptybst.thon";

val bstType : Ast.Typ = typeof (parseFile "/home/evan/thon/examples/singletonbst.thon");

val TyRec
    ("node",Plus (Unit,Prod (Nat,Prod (TypVar ("node",0),TypVar ("node",0)))))
    : Ast.Typ = bstType;

val bstInsertType : Ast.Typ = typeof (parseFile "/home/evan/thon/examples/bst.thon");
val Arr(Nat, (Arr(bstType1, bstType2))) = bstInsertType;
val true = (bstType = bstType1);
val true = (bstType = bstType2);

in
()
end