test.stray

let id : forall (A : *). A -> A = λA x. x;
let cnst : forall (A : *) (B:*). A -> B -> A = \A B x y. x;

const Bool : *;
const t : Bool;
const f : Bool;
const not : Bool -> Bool;
const and : Bool -> Bool -> Bool;
const or : Bool -> Bool -> Bool;
const impl : Bool -> Bool -> Bool;
const equiv : Bool -> Bool -> Bool;
const ∀ : forall a:*. (a -> Bool) -> Bool;
const ∃ : forall a:*. (a -> Bool) -> Bool;
const eq : forall a:*. a -> a -> Bool;
const hchoice : forall a:*. (a -> Bool) -> a;

const Natural : *;
free 0 : Bool -> Natural;
let boolnat : * = Bool -> Natural;

-- Church natural numbers
let Nat  : * = forall N:*. (N -> N) -> N -> N;
let zero : Nat = \N s z. z;
let five : Nat = \N s z. s (s (s (s (s z))));
let add'  : Nat -> Nat -> Nat = \m n f x. m f (n f x);
let add  : Nat -> Nat -> Nat = \a b N s z. a N s (b N s z);
let mul  : Nat -> Nat -> Nat = \a b N s z. a N (b N s) z;
let exp : Nat -> Nat -> Nat = \a b N. b (N -> N) (a N);
let succ : Nat -> Nat = \a N s z. s (a N s z);

-- let pred : Nat -> Nat = \a N s z. a (\g h. h (g s)) (\u. z) (\u. u)
-- annotatated lambda example. need to figure out the arg types, this is wrong
-- let pred : Nat -> Nat = \a N s z. a N (\(g:(N->N)->N) (h:N->N->N). h (g s)) (\(u:N). z) (\(u:N). u);

-- Sum and Product types, system Fω
-- idea: encode type as a function of n args, where n is the number of constructors
let Sum : * -> * -> * = \A B. forall C:*. (A -> C) -> (B -> C) -> C;
let left : forall (a:*) (b:*). a -> Sum a b = \(a:*) (b:*) (v:a) (c:*). \(l:a->c) (r:b->c). l v;
let right : forall (a:*) (b:*). b -> Sum a b = \(a:*) (b:*) (v:b) (c:*). \(l:a->c) (r:b->c). r v;
let Product : * -> * -> * = \A B. forall C:*. (A -> B -> C) -> C;
let pair : forall (a:*) (b:*). a -> b -> Product a b = \(a:*) (b:*) (x:a) (y:b) (c:*) (p:a -> b -> c). p x y;
let fst : forall (a:*) (b:*). Product a b -> a = \(a:*) (b:*) (p:Product a b). p a (\(x:a) (y:b). x);
let snd : forall (a:*) (b:*). Product a b -> b = \(a:*) (b:*) (p:Product a b). p b (\(x:a) (y:b). y);
let split : forall (a:*) (b:*) (r:*). (a -> b -> r) -> Product a b -> r = \a b r f p. p r f;

-- Lists, system Fω
-- again, type constructor reflects the type of corresponding term constructors
let List : * -> * = \(a:*). forall ϕ:* -> *. ϕ a -> (a -> ϕ a -> ϕ a) -> ϕ a;
let nil : forall (a:*). List a = \(a:*) (ϕ:* -> *) (n:ϕ a) (c:a -> ϕ a -> ϕ a). n;
let cons : forall (a:*). a -> List a -> List a = \(a:*) (x:a) (xs:List a) (ϕ:* -> *) (n:ϕ a) (c:a -> ϕ a -> ϕ a). c x (xs ϕ n c);
let foldr : forall (a:*) (b:*). (a -> b -> b) -> b -> List a -> b = \(a:*) (b:*) (f:a->b->b) (n:b) (xs:List a). xs (\y:*.b) n f;
let foldl : forall (a:*) (b:*). (b -> a -> b) -> b -> List a -> b = \(a:*) (b:*) (f:b->a->b) (n:b) (xs:List a). foldr a (b -> b) (\(x:a) (g:b -> b) (v:b). g (f v x)) (\x:b. x) xs n;
let map : forall (a:*) (b:*). (a -> b) -> List a -> List b = \(a:*) (b:*) (f:a -> b) (xs:List a). foldr a (List b) (\(x:a) (r:List b). cons b (f x) r) (nil b) xs;
let append : forall (a:*). List a -> List a -> List a = \(a:*) (xs:List a) (ys:List a). foldr a (List a) (cons a) ys xs;
let reverse : forall (a:*). List a -> List a = \(a:*) (xs:List a). foldl a (List a) (\(r:List a) (x:a). cons a x r) (nil a) xs;

-- type level equality, system Fω
let Eql : * -> * -> * = \(a:*) (b:*). forall c:*->*. c a -> c b;
let refl : forall a:*. Eql a a = \(a:*) (ϕ:* -> *). \x:ϕ a. x;
let symm : forall (a:*) (b:*). Eql a b -> Eql b a = \(a:*) (b:*) (e:forall ϕ:* -> *. ϕ a -> ϕ b). e (\y:*. Eql y a) (refl a);
let trans : forall (a:*) (b:*) (c:*). Eql a b -> Eql b c -> Eql a c = \(a:*) (b:*) (c:*) (ab:Eql a b) (bc:Eql b c). bc (Eql a) ab;
let lift : forall  (a:*) (b:*) (ϕ:* -> *). Eql a b -> Eql (ϕ a) (ϕ b) = \(a:*) (b:*) (ϕ:* -> *) (e: Eql a b). e (\y:*. Eql (ϕ a) (ϕ y)) (refl (ϕ a));

let some_list : List Nat = append Nat (cons Nat five (cons Nat five (nil Nat))) (cons Nat zero (nil Nat));

let ten      : Nat = add five five;
let hundred  : Nat = mul ten ten;

-- let eta_expanded : forall (A : *). A -> A = \A x y. y x;
-- ghci> ab_conv ctx.lvl (get_def ctx "n_") (get_def ctx "n__")
-- True
let n_ : (Bool -> Nat) -> (Bool -> Nat) = \y x.y x;
let n__ : (Bool -> Nat) -> (Bool -> Nat) = \y. y;
let nftest : boolnat -> (Bool -> Natural) = \y. ?0;

let ttt : (Bool -> Natural) -> (Bool -> Natural) = \y x.y x;
let ttt' : (Bool -> Natural) -> (Bool -> Natural) = \y. \x. y x;

-- should not typecheck
-- let cnst_wrong : forall (A : *) (B:*). A -> A -> B = \A B x y. x;
-- let cnst_wrong_ : forall (A : *) (B:*). B -> A -> A = \A B x y. x;

-- example 2
-- ghci> pp_substitutions ctx $ xx !! 0
-- "       ?0 : Bool -> Natural -- User
--         ?1 : A -> C -- Substituted λ x. ?3 x (?4 x)
--         ?2 : B -> C -- Substituted λ x. ?3 (?5 x) x
--         ?3 : A -> B -> C -- Ident
--         ?4 : A -> B -- Substituted λ x. b
--         ?5 : B -> A -- Substituted λ x. a
-- "
-- ghci> xx = get_n_unif 39 ctx (Uc (get_const_def_partial ctx "lc", get_const_def_partial ctx "rc"))
-- TODO:works, but first 39 seem similar and 40/ident loops
-- -> clarify whether success leaves have to be different substitutions
const A : *;
const B : *;
const C : *;
const a : A;
const b : B;
const h : C -> C;
free 1 : A -> C; -- F
free 2 : B -> C; -- G
let lc : C = hundred C h (?1 a);
let rc : C = hundred C h (?2 b);

-- example 1
free 3 : C;
let lc' : C = ?3;
let rc' : C = h ?3;

-- iter example from Bentkamp:
-- F (\x. x) (f a) = F f a
free 4 : (A -> A) -> A -> A;
const f'' : A -> A;
let lc'' : A = ?4 (\x. x) (f'' a);
let rc'' : A = ?4 f'' a;
-- mit unifier F |-> \u v. u v
-- Iteration: F |-> \u v. H u v (u (G u v))
-- Elimination: H |-> \x y z. H' z
-- Decompose
-- Huet proj: G |-> \u v. v

-- f X ?= G a
-- mgu: X ↦ H a, G ↦ λu. f (H u)
free 5 : A; --X
free 6 : A -> A; --G
let lc''' : A = f'' ?5;
let rc''' : A = ?6 a;

-- encoding check (O(j) should just be f)
const h' : C -> C;
let j : C -> C = λx. h' x;
let j' : Nat = add ten five;

-- const Bool : *;
-- const Natural : *;

formula
    (?4 (\x. x) (f'' a) = ?4 f'' a);