Main.kind

main : ∀(A: *) ∀(x: (List A)) (List A)
= λA λx x








//main : (List U64)
//= [1 (log "A" 2) 3]


















//main : Nat
//= let map = #Node{#Some{47244640257} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{4294967302} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{60129542145} #Leaf{} #Leaf{}}} #Node{#Some{34359738370} #Leaf{} #Node{#Some{103079215110} #Leaf{} #Leaf{}}}} #Node{#Some{17179869189} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{90194313222} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{90194313217} #Leaf{} #Leaf{}}} #Node{#Some{4} #Leaf{} #Node{#Some{111669149697} #Leaf{} #Leaf{}}}}} #Node{#Some{8589934597} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{60129542150} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{77309411334} #Leaf{} #Leaf{}}} #Node{#Some{34359738369} #Leaf{} #Node{#Some{115964116993} #Leaf{} #Leaf{}}}} #Node{#Some{25769803778} #Node{#None{} #Leaf{} #Node{#Some{85899345921} #Leaf{} #Leaf{}}} #Node{#Some{60129542146} #Leaf{} #Leaf{}}}}} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{51539607557} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{73014444034} #Leaf{} #Leaf{}}} #Node{#Some{4} #Leaf{} #Node{#Some{115964116993} #Leaf{} #Leaf{}}}} #Node{#Some{4} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{94489280517} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{90194313218} #Leaf{} #Leaf{}}} #Node{#Some{47244640257} #Leaf{} #Leaf{}}}} #Node{#Some{12884901894} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Node{#None{} #Leaf{} #Node{#Some{68719476741} #Leaf{} #Leaf{}}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Leaf{}} #Node{#Some{90194313217} #Leaf{} #Leaf{}}} #Node{#Some{47244640258} #Leaf{} #Node{#Some{115964116994} #Leaf{} #Leaf{}}}} #Node{#Some{25769803777} #Node{#None{} #Leaf{} #Node{#Some{98784247810} #Leaf{} #Leaf{}}} #Node{#Some{98784247809} #Leaf{} #Leaf{}}}}}} :: (BinMap U64)
  ////(BinMap/invert _ map)
  //let lst = (BinMap/to_list _ map)
  //(List/length _ lst)




//main : (Map U64) & U64 & U64
//= let map = { 1:10 2:20 | 0 }
  //put x0  = map[1] := 100
  //get x1  = map[2]
  //(map, x0, x1)







//foo : U64 -> U64
//= λ{
  //0: 0
  //1: 10
  //2: 20
  //3: 30
  //4+k: k
//}

//main : U64 = (foo 50)










//StateU64 : * -> * = (State U64)
//StateU64/bind : ∀(A: *) ∀(B: *) (StateU64 A) -> (A -> (StateU64 B)) -> (StateU64 B) = (State/bind U64)
//StateU64/pure : ∀(A: *) A -> (StateU64 A) = (State/pure U64)
//StateU64/swap : U64 -> (State U64 U64) = (State/swap U64)

//main : (StateU64 U64)
//= do StateU64 {
  //ask x = (StateU64/swap 1)
  //ask y = (StateU64/swap 2)
  //ask z = (StateU64/swap 3)
  //ret (+ x (+ y z))
//}


















//main : (IO Unit)
//= do IO {
  //ask (IO/print "hello")
  //ask (IO/print "world!")
  //ask x = (IO/swap 42 1)
  //ask y = (IO/swap 42 2)
  //ask z = (IO/swap 42 3)
  //ask (IO/print (String/join "" ["x: " (U64/to_string x)]))
  //ask (IO/print (String/join "" ["y: " (U64/to_string y)]))
  //ask (IO/print (String/join "" ["z: " (U64/to_string z)]))
  //ret #Unit
//}






//Main : ∀(str: String) Char
//= λstr match str {
  //#Cons{h t}: h
  //#Nil: 'a'
//}




//main : ∀(b: Bool) U64
//= λb
  //let x = match b { #True: 0 #False: 1 } :: U64
  //x







// TODO: inspired on double, create a fib function with U64 inputs
// it must be a tail recursive function
// remember the switch syntax is:
// switch n { 0: ... _{np}: ... } // here, np is n_1
// it can NOT have more than 2 cases.

//o bλ__0 match __0 {#Pair:λ__0 match __0 {#A:λv 5 #B:λv 6 } }
//~λx0 match x0 {#Pair:λ__0 match __0 {#A:λv 5 #B:λv 6 } }

//~λ__0 match __0 {#Pair:λ__0 match __0 {#A:λv 5 #B:λv 6 } }
//~λx0 match x0 {#Pair:λfst0 λsnd1 match fst0 {#A:5 #B:6 } }

//main : Bool = (String/eq "(" ")")

//main : Bits = (String/to_bits "o")
//main : Bits = (Bits/concat [#O{#I{#E}} #I{#O{#E}}])


//main : ∀(x: (Pair U64 U64)) (Pair U64 U64)
//| state =
  //let #Pair{input index} = state
  //#Pair{input index}


//data T {
  //#A
  //#B
//}

//// \/ TODO: this compiles worse. investigate
//Foo : ∀(x: (Pair T U64)) U64
//| #Pair{#A v} = v
//| #Pair{#B v} = v

//Foo : ∀(x: (Pair T U64)) U64
//= λ{
  //#Pair: λ{
    //#A: λb b
    //#B: λb b
  //}
//}


//Foo : ∀(x: (Pair T U64)) U64
//= λ{
  //#Pair: λa λb (match a {
    //#A: λb b
    //#B: λb b
  //} b)
//}



//Foo : ∀(x: (Pair T U64)) U64
//= λ{
  //#Pair: λa λb ((λ{
    //#A: b
    //#B: b
  //} :: T -> U64) a)
//}


//Foo : ∀(x: (Pair T U64)) U64
//= λx match x {
  //#Pair{k v}: match k {
    //#A: v
    //#B: v
  //}
//}

//main : U64 = (Foo #Pair{#A 5})



//fib/go : ∀(n: U64) ∀(a: U64) ∀(b: U64) U64
//= λn λa λb
  //switch n {
    //0: a
    //_{pred}: (fib/go pred b (+ a b))
  //}

//// create fib now
//fib : ∀(n: U64) U64
//= λn (fib/go n 0 1)

//// create a main
//main : U64
//= let x = (fib/go 0)
  //let y = (fib/go 0 0)
  //let z = (fib/go 0 0 0)
  //(fib 1000000)



//Foo : ∀(x: (Maybe (Pair U64 U64))) U64
//= λx match x {
  //#Some{pair}: match pair {
    //#Pair{a b}: match (U64/is_zero a) {
      //#True: (Foo x)
      //#False: 0
    //}
  //}
  //#None: 0
//}


//main : (Maybe U64)
//= do Maybe {
  //ask x = #Some{1}
  //ask y = #Some{2}
  //ret (+ x y)
//}



//Foo : ∀(m: Nat) ∀(n: Nat) Bool
//| #Zero    #Zero    = #True
//| #Succ{m} #Succ{n} = (Foo m n)
//| x        y        = #False

//Bar : U64 -> U64 -> U64 -> U64
//| a b c = a

//double : ∀(n: Nat) ∀(r: Nat) Nat
//| n r = match n {
  //#Zero: r
  //#Succ: λnp (double np #Succ{#Succ{r}})
//}
//main : Nat = (double #20 #0)


//double : ∀(n: U64) ∀(r: U64) U64
//= λn λr
  //switch n {
    //0: r
    //_{pred}: (double pred (+ r 2))
  //}

//main : U64 = (double 1000000 0)





//Main : (Pair String *) -> (Pair (List U64) *)
//| str = str

//main : String/View
//= #View { "// Comment 1\/ Comment 2\nabc" }


//main = Parser/parse_unicode_escape






//main : (Pair/Pair U64 U64)
//= #Pair { foo 13 }

//use Bool/ as Bool/
//use U64/ as U64/
//use Parser/ as Parser/
//use Pair/ as Pair/

//foo : (Pair/Parser Unit) = ?oxi

//affer : (Parser/Parser U64)
//= when U64/eq 50 {
  //'(' : do Parser/Monad {
    //ask foo
    //ret 12
  //}
  //'{' : ?b
  //'*' : ?c
  //_   : ?d
//}

//main : U64
//= when U64/eq 35 {
  //0  : 0
  //10 : 100
  //20 : 200
  //30 : 300
  //_  : 999
//}

//use Bool/ as Bool/

//Foo : Bool -> Bool
//| #True = #False
//| other   = #True

//Main : Bool
//= (Foo #False)

//| #True = ?a

//use Nat/ as Nat/
//use String/ as String/

//Main
//: String/View
//= #View{ "\nI'm a (λx x) \nThat's nice!\n" }

//use Block/ as BK/
//use Bool/ as Bool/
//use Empty/ as EM/
//use Equal/ as EQ/
//use Maybe/ as MB/
//use Pair/ as Pair/
//use / as /

//IsTrue
//: ∀(b: Bool)
  //*
//= λb data[b]{
  //#Indeed : (IsTrue #True)
//}

//Main
//: ∀(x: Bool)
  //∀(t: (IsTrue x))
  //Bool
//= λ{
  //#True: λ{
    //#Indeed: #True
  //}
  //#False: λ{
    //#Indeed: #void
  //}
//}

//Main
//: ∀(p: (Pair U64 Bool))
  //∀(k: (Maybe (Pair U64 Bool)))
  //(Maybe U64)
//= λp λk do Maybe {
  //ask x = #Some{50}
  //ask y = #Some{20}
  //ret (+ x y)
//}

//use Maybe/ as Maybe/

//Main
//: (Maybe U64)
//= do Maybe/Monad/ {
  //ask x = #Some { 50 }
  //ask y = #Some { 20 }
  //ret ?a
//}

//use List/ as List/
//use Nat/ as Nat/
//use String/ as String/

//Main
//: String
//= "foo bar"

//use Pair/ as Pair/
//use Bool/ as Bool/

//Main
//: ∀(f: ∀(x: Bool) Bool)
  //Nat
//= λf match (f #True) {
  //#True: ?a
  //#False: ?b
//}

////∀(fx: Bool) (P 

//Aux
//: ∀(P: ∀(x: Bool) *)
  //∀(Fx: Bool)
  //(P Fx)
//= λP λ{
  //#True: ?t
  //#False: ?f
//}
  







//ct0 = λx match x {
  //#Succ: λm λx match x {
    //#Succ: λn ((Foo m) n)
    //#_: λy #False{}
  //}
  //#Zero: λx match x {
    //#Zero:#True{}
    //#_:λy #False{}
  //}
  //#_:*
//}

//ct1 = λm λn λv2 λv3 match m {#Succ:λm match n {#Succ:λn ((Foo m) n) #_:#False{} } #Zero:match n {#Zero:#True{} #_:#False{} } #_:* }





//pull λx match x {#Succ:λm λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } #Zero:λx match x {#Zero:#True{} #_:λy #False{} } #_:* } ### dep=0 ari=0 skp=0
//pull match m {#Succ:λm λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } #Zero:λx match x {#Zero:#True{} #_:λy #False{} } #_:* } ### dep=1 ari=1 skp=0
//pull λm λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } ### dep=1 ari=1 skp=1
//pull λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } ### dep=2 ari=1 skp=0
//pull match n {#Succ:λn ((Foo m) n) #_:λy #False{} } ### dep=3 ari=2 skp=0
//pull λn ((Foo m) n) ### dep=3 ari=2 skp=1
//pull ((Foo m) n) ### dep=4 ari=2 skp=0
//pull λy #False{} ### dep=3 ari=2 skp=1
//pull #False{} ### dep=4 ari=2 skp=0
//WARNING: inconsistent cross_branch lambda count on: match n {#Succ:λn ((Foo m) n) #_:λy #False{} }
//pull λx match x {#Zero:#True{} #_:λy #False{} } ### dep=1 ari=1 skp=0
//pull match n {#Zero:#True{} #_:λy #False{} } ### dep=2 ari=2 skp=0
//pull #True{} ### dep=2 ari=2 skp=0
//pull λy #False{} ### dep=2 ari=2 skp=1
//pull #False{} ### dep=3 ari=2 skp=0
//WARNING: inconsistent cross_branch lambda count on: match m {#Succ:λm λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } #Zero:λx match x {#Zero:#True{} #_:λy #False{} } #_:* }
//pull * ### dep=1 ari=1 skp=1
//ct0 = λx match x {#Succ:λm λx match x {#Succ:λn ((Foo m) n) #_:λy #False{} } #Zero:λx match x {#Zero:#True{} #_:λy #False{} } #_:* }
//ct1 = λm λn λv2 λv3 match m {#Succ:λm match n {#Succ:λn ((Foo m) n) #_:λy #False{} } #Zero:match n {#Zero:#True{} #_:λy #False{} } #_:* }
//pull ((Foo #Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } }) #Succ{pred:#Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } } }) ### dep=0 ari=0 skp=0
//ct0 = ((Foo #Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } }) #Succ{pred:#Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } } })
//ct1 = ((Foo #Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } }) #Succ{pred:#Succ{pred:#Succ{pred:#Succ{pred:#Zero{} } } } })