// #![recursion_limit="128"]
// #[macro_use]
// extern crate fungi_lang;

// #[test]
// pub fn trie () {
//   use std::thread;
//   let child =
//     thread::Builder::new().stack_size(64 * 1024 * 1024).spawn(move || { 
//       trie2()
//     });
//   let _ = child.unwrap().join();
// }
// pub fn trie2() {
//     use std::rc::Rc;
//     use fungi_lang::ast::*;
//     use fungi_lang::bitype::*;
//     use fungi_lang::vis::*;


//     let bundle : Bundle = fgi_bundle![
//     //let trie_ast = fgi_exp![
//         decls {
//             /// Optional natural numbers:
//             type OpNat = (+ Unit + Nat );
            
//             /// Levels (as numbers), for level trees.
//             type Lev = ( Nat )

//             /// Abstracted vector, represents an array of Nats
//             type NatVec = ( Unit )
                
//             /// Sequences (balanced binary level trees), whose leaves
//             /// are optional vectors of natural numbers:
//             type Seq = (
//                 rec seq. foralli (X,Y):NmSet.
//                     (+ (+ Unit + NatVec)
//                      + (exists (X1,X2,X3)   :NmSet | ((X1%X2%X3)=X:NmSet).
//                         exists (Y1,Y2,Y3,Y4):NmSet | ((Y1%Y2%Y3%Y4)=Y:NmSet).
//                         x Nm[X1] x Lev
//                         x Ref[Y1](seq[X2][Y2])
//                         x Ref[Y3](seq[X3][Y4]))
//                     )
//             );                
                
//             /// Sets (balanced binary hash tries), whose leaves are
//             /// optional natural numbers:
//             type Set = (
//                 rec set. foralli (X,Y):NmSet.
//                     (+ (+ Unit + NatVec)
//                      + (exists (X1,X2,X3)   :NmSet | ((X1%X2%X3)=X:NmSet).
//                         exists (Y1,Y2,Y3,Y4):NmSet | ((Y1%Y2%Y3%Y4)=Y:NmSet).
//                         x Nm[X1]
//                         x Ref[Y1](set[X2][Y2])
//                         x Ref[Y3](set[X3][Y4]))
//                     )
//             );                

//             /// Structural recursion over a binary tree (output names and pointers):
//             idxtm    Bin   = (#x:Nm.         {x,@1} % {x,@2}  );
//             idxtm WS_Bin   = (#x:NmSet.{@!}( (Bin) x         ));

//             /// Same as above but only one side
//             idxtm WS_Bin_1 = ( #x:NmSet.{@!}(x * {@1}))
//             idxtm WS_Bin_2 = ( #x:NmSet.{@!}(x * {@2}))

//             /// Trie_join: Index functions for output names and pointers:
//             idxtm    Join  = (#x:NmSet.    ( (Bin)((Bin)^* x))); // one app minimum
//             idxtm WS_Join  = (#x:NmSet.{@!}( {Join}  x       ));

//             /// Trie_of_seq: Index functions for output names and pointers:
//             idxtm    Trie  = (#x:NmSet.    ( {Join} x        ));
//             idxtm WS_Trie  = (#x:NmSet.{@!}( {Join} x        ));
//         }

//         let join_vecs:( Thk[0] foralli (X,Y):NmSet.
//             0 Nm[X] -> 0 NatVec -> 0 NatVec ->
//             {{WS_Bin} X; 0} F Set[X][{WS_Bin} X]
//         ) = {
//             ret thunk #nm. #v1. #v2.
//             let lr:(Ref[{WS_Bin_1}X] Set[0][0]) = { ref {nm, (@1)} inj1 inj2 v1 }
//             let rr:(Ref[{WS_Bin_2}X] Set[0][0]) = { ref {nm, (@2)} inj1 inj2 v2 }
//             ret inj2 pack (X,0,0,{WS_Bin_1}X,0,{WS_Bin_2}X,0)
//                 (nm,0,lr,rr)
//         }
        
//         let split_vec:( Thk[0] foralli (X,Y):NmSet.
//             0 Nm[X] -> 0 NatVec ->
//             {{WS_Bin} X; 0} F Set[X][{WS_Bin} X]
//         ) = {
//             ret thunk #nm. #vec.
//             let vs : (x NatVec x NatVec) = {
//                 // vector ops with `vec`
//                 // split `vec` appropriate to trie
//                 unimplemented
//             }
//             let (v1,v2) = {ret vs}
//             let bin = { {force join_vecs} nm v1 v2 }
//             ret bin
//         }
        
//         // let join:(
//         //     Thk[0] foralli (X0, X1, X2, Y1, Y2):NmSet.
//         //         0 Nm[X0] ->
//         //         0 Set[X1][Y1] ->
//         //         0 Set[X2][Y2] ->
//         //     {
//         //         ({WS_Bin} X0)
//         //         % ({WS_Join} (X1%X2))
//         //     ;
//         //         Y1 % Y2
//         //         % ({WS_Bin} X0)
//         //         % ({WS_Join} (X1%X2))
//         //     }
//         //     F Set
//         //         [(Join)(X1 % X2)]
//         //         [{WS_Join}(X1 % X2)]
//         // ) = {
//         //     ret thunk fix join. #nm. #set1. #set2. match set1 {
//         //         on1 => { match set2 {
//         //             on2  => { unimplemented }
//         //             bin2 => { unimplemented }
//         //         }}
//         //         bin1 => { match set2 {
//         //             on2  => { unimplemented }
//         //             bin2 => {
//         //                 // XXX
//         //                 unimplemented
//         //             }
//         //         }}
//         //     }
//         // }

//         // let trie:(
//         //     Thk[0] foralli (X,Y):NmSet.
//         //         0 Seq[X][Y] ->
//         //     {
//         //         {WS_Trie} X
//         //             ;
//         //         Y % ( {WS_Trie} X )
//         //     }
//         //     F Set[X][{WS_Trie} X]
//         // ) = {
//         //     ret thunk fix trie. #seq. match seq {
//         //         on => { ret roll inj1 on }
//         //         bin => {
//         //             unpack (X1,X2,X3,Y1,Y2,Y3,Y4) bin = bin
//         //             let (n,lev,l,r) = {ret bin}
//         //             let (rsl, _l) = { memo{n,(@1)}{ {force trie}[X2][Y2]{!l} } }
//         //             let (rsr, _r) = { memo{n,(@2)}{ {force trie}[X3][Y4]{!r} } }
//         //             let trie      = { ws (nmfn [#x:Nm. ~n * x]) {
//         //                 {force join}
//         //                 [({Trie}X2)][({Trie}X3)][({WS_Trie}X2)][({WS_Trie}X3)]
//         //                 {!rsl} {!rsr}
//         //             }}
//         //             ret trie
//         //         }
//         //     }
//         // }

//         ret 0
//     ];

//     // println!("trie AST");
//     // println!("-------------");
//     // println!("{:?}", trie_ast);
//     // let typed = synth_exp(&Ext::empty(), &Ctx::Empty, &trie_ast);
//     // println!("trie typing derivation");
//     // println!("----------------------");
//     // println!("typing success: {:?}", typed.clas.is_ok());
//     // println!("{:?}", typed);

//     write_bundle("target/trie.fgb", &bundle);
// }