---------------
-- builtins ---
---------------
defn char : prop  -- builtin

defn putChar    :  char -> prop -- builtin
   | putCharImp = [A] putChar A

-- for sequencing io actions
fixity left 1 ,
defn io : prop
   | do = io
   | ,  = io -> prop -> io 

defn run : io -> prop
  >| runDo = run do
  >| runSeq = [A][B] run (A , B) <- run A 
                         	 <- B

defn readLine    : (string -> io) -> prop -- builtin 
   | readLineImp = [Foo : string -> io] [A : string] readLine Foo <- run (Foo A)

defn string : prop
  as list char

---------------
-- searches ---
---------------
defn any : {A : prop} (A -> prop) -> prop
   | is = [a : prop][V : a][F : a -> prop] F V -> any { A = a } F


defn openAny : [A][F : A -> prop] any F -> [V : A] F V -> prop
   | openAnyDef = [A][F : A -> prop][V : A][FV : F V] openAny A F (is A V F FV) V FV

defn sopen : {a : prop }{f : a -> prop} [V : a] {fv : f V} (exists v : a . f v) -> prop 
  as ?\a : prop . ?\ f : a -> prop . \vt : a . ?\ fv : f vt . \an : (exists v : a . f v) . open a f an vt fv


fixity lambda free
defn free : [A : prop] (A -> prop) -> prop
  as \a : prop . any { A = a }

--------------------------
--- useful combinators ---
--------------------------
fixity right 0 $
defn $ : {at bt:prop} (at -> bt) -> at -> bt
  as ?\ at bt . \ f . \a . f a


fixity right 0 @
defn @ : {at bt ct:prop} (bt -> ct) -> (at -> bt) -> at -> ct
  as ?\at bt ct : prop . \f : bt -> ct . \ g : at -> bt . \ a : at . f (g a)

defn flip : {at bt ct : prop} (at -> bt -> ct) -> bt -> at -> ct
  as ?\ at bt ct : prop . \ foo . \ b . \ a . foo a b

-------------------
--- Constraints ---
-------------------
fixity none 1 =:=
defn =:= : {Q} Q -> Q -> prop
  >| eq = [a : prop][b:a] (=:=) {Q = a} b b

-- searching for these is SLOW
fixity none 0 /\
defn /\ : prop -> prop -> prop
  >| and = [a b : prop] a -> b -> a /\ b

fixity none 0 \/
defn \/ : prop -> prop -> prop
   | or1 = [a b:prop] a -> a \/ b
   | or2 = [a b:prop] b -> a \/ b

fixity left 0 ==
-- currently we can't do any inference inside of definitional signatures
defn == : {q : prop} (q -> prop) -> q -> prop 
  as ?\q . \foo : q -> prop . \v : q . foo v


--------------
--- concat ---
--------------
defn concatable : [M : prop] (M -> M -> M -> prop) -> prop
   | concatableNat = concatable natural add
   | concatableList = [A] concatable (list A) concatList


-- it correctly infers 169, and M (but it eta expands Foo when it infers it) !!
fixity right 3 ++
defn ++ : {M}{Foo}{cm : concatable M Foo} M -> M -> M -> prop
  >| ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] 
              (++) {Foo = Foo} M1 M2 M3 
            <- concatable M Foo 
            <- Foo M1 M2 M3 

-------------
--- Order ---
-------------
defn orderable : [M : prop] (M -> M -> prop) -> prop
  >| orderableNatural = orderable natural lte-nat

fixity right 3 =< 
defn =< : {M : prop}{Foo: M -> M -> prop}{co : orderable M Foo} M -> M -> prop
  >| ooimp = [M][Foo : M -> M -> prop] [M1 M2 : M] 
           (=<) {M = M} M1 M2 
          <- orderable M Foo
          <- Foo M1 M2

---------------------
--- Unary Numbers ---
---------------------
defn natural  : prop
   | zero = natural
   | succ = natural -> natural

query findSat0 = free A : natural . A =:= zero

defn add   : natural -> natural -> natural -> prop
  >| add_z = [N] add zero N N
  >| add_s = [N M R] add N M R -> add (succ N) M (succ R)

query add0 = add (succ zero) zero (succ zero)

query add1 = succ zero ++ zero == succ zero

-- sub N M R is N - M = R
defn sub   : natural -> natural -> natural -> prop
   | sub_by_add = [N M R] sub N M R <- add M R N


defn lte-nat : natural -> natural -> prop
  >| leqZero = [B] lte-nat zero B
  >| leqSucc = [A B] lte-nat (succ A) (succ B) <- lte-nat A B

fixity none 3 <
defn < : natural -> natural -> prop
  >| ltZero = [B] zero < succ B
  >| ltSucc = [A B] succ A < succ B <- A < B

query add2 = exists A : natural . add (succ zero) zero A

query add3 = any $ add (succ zero) zero

query findSat1 = succ zero =< succ (succ zero)

query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)

-------------
--- Maybe ---
-------------

defn maybe : prop -> prop
   | nothing = {a} maybe a
   | just = {a} a -> maybe a

-------------
--- Lists ---
-------------
defn list : prop -> prop
   | nil  = {a} list a
   | cons = {a} a -> list a -> list a

defn concatList : {A} list A -> list A -> list A -> prop
  >| concatListNil  = [T][L:list T] concatList {A = T} nil L L
  >| concatListCons = [T][A B C : list T][V:T] concatList (cons V A) B (cons V C) <- concatList A B C

----------------
--- printing ---
----------------

defn putStr : string -> prop
  >| putStr_Nil = putStr $ nil {a = char}
  >| putStr_Cons = [v:char][l: string] 
                   putStr $ cons {a = char} v l 
                <- putChar v
                <- putStr l

----------------
--- Booleans ---
----------------
defn bool : prop
   | true = bool
   | false = bool

defn if : bool -> bool
  as \b . b

fixity none 1 |:|
defn |:| : {t:prop} t -> t -> (t -> t -> t) -> t
  as ?\t : prop . \a b : t. \f : t -> t -> t. f a b


fixity none 0 ==>
defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop
  >| thentrue  = [a : prop][f: _ -> a] (true ==> f)  (f (\a1 a2 : a . a1))
  >| thenfalse = [b : prop][f: _ -> b] (false ==> f) (f (\a1 a2 : b . a2))

defn not : bool -> bool -> prop
  as \zq . if zq ==> false |:| true

defn ismain : prop 
  as run $ do 
         , putStr "hey!\n"
         , readLine (\A . do 
   	 , putStr A
         , putStr "\nbye!\n")

-- query main = ismain