MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "SolverBugStreamFixed.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.tt : < Bool.tt : Bool >
term  Bool.ff : < Bool.ff : Bool >
term  ifthenelse : Bool -> .[A : Set] -> A -> A -> A
{ ifthenelse Bool.tt [A] a1 a2 = a1
; ifthenelse Bool.ff [A] a1 a2 = a2
}
type  SNat : + Size -> Set
term  SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i >
term  SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i >
type  Nat : Set
type  Nat = SNat #
term  add : Nat -> Nat -> Nat
{ add (SNat.zero [.#]) = \ y -> y
; add (SNat.succ [.#] x) = \ y -> SNat.succ [#] (add x y)
}
term  leq : Nat -> Nat -> Bool
{ leq (SNat.zero [.#]) y = Bool.tt
; leq (SNat.succ [.#] x) (SNat.zero [.#]) = Bool.ff
; leq (SNat.succ [.#] x) (SNat.succ [.#] y) = leq x y
}
type  Stream : ++(A : Set) -> - Size -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : Stream A i) -> < Stream.cons i y1 y2 : Stream A $i >
term  tail : .[A : Set] -> .[i : Size] -> Stream A $i -> Stream A i
{ tail [A] [i] (Stream.cons [.i] x xs) = xs
}
term  head : .[A : Set] -> .[i : Size] -> Stream A $i -> A
{ head [A] [i] (Stream.cons [.i] x xs) = x
}
term  nth : .[A : Set] -> .[i : Size] -> SNat i -> Stream A i -> A
{ nth [A] [i] (SNat.zero [j < i]) xs = head [A] [j] xs
; nth [A] [i] (SNat.succ [j < i] n) xs = nth [A] [j] n (tail [A] [j] xs)
}
term  map : .[A : Set] -> .[B : Set] -> .[i : Size] -> (A -> B) -> Stream A i -> Stream B i
{ map [A] [B] $[i < #] f (Stream.cons [.i] x xl) = Stream.cons [i] (f x) (map [A] [B] [i] f xl)
}
term  zipWith : .[A : Set] -> .[B : Set] -> .[C : Set] -> (A -> B -> C) -> .[i : Size] -> Stream A i -> Stream B i -> Stream C i
{ zipWith [A] [B] [C] f $[i < #] (Stream.cons [.i] a as) (Stream.cons [.i] b bs) = Stream.cons [i] (f a b) (zipWith [A] [B] [C] f [i] as bs)
}
term  merge : .[i : Size] -> (Nat -> Nat -> Bool) -> Stream Nat i -> Stream Nat i -> Stream Nat i
{ merge $[i < #] le (Stream.cons [.i] x xs) (Stream.cons [.i] y ys) = ifthenelse (le x y) [Stream Nat $i] (Stream.cons [i] x (merge [i] le xs (Stream.cons [i] y ys))) (Stream.cons [i] y (merge [i] le (Stream.cons [i] x xs) ys))
}
term  n0 : Nat
term  n0 = SNat.zero [#]
term  n1 : Nat
term  n1 = SNat.succ [#] n0
term  n2 : Nat
term  n2 = SNat.succ [#] n1
term  n3 : Nat
term  n3 = SNat.succ [#] n2
term  n4 : Nat
term  n4 = SNat.succ [#] n3
term  n5 : Nat
term  n5 = SNat.succ [#] n4
term  double : Nat -> Nat
term  double = \ n -> add n n
term  triple : Nat -> Nat
term  triple = \ n -> add n (double n)
term  ham : .[i : Size] -> Stream Nat i
{ ham $[i < #] = Stream.cons [i] n1 (merge [i] leq (map [Nat] [Nat] [i] double (ham [i])) (map [Nat] [Nat] [i] triple (ham [i])))
}
term  fib : .[i : Size] -> Stream Nat i
{ fib $[i < #] = Stream.cons [i] n0 (zipWith [Nat] [Nat] [Nat] add [i] (Stream.cons [i] n1 (fib [i])) (fib [i]))
}
term  fibIter' : (x : Nat) -> (y : Nat) -> .[i : Size] -> Stream Nat i
{ fibIter' x y $[i < #] = Stream.cons [i] x (fibIter' y (add x y) [i])
}
term  fibIter : Stream Nat #
term  fibIter = fibIter' n1 n1 [?14]
term  fibIter4 : Nat
term  fibIter4 = nth [Nat] [#] n4 fibIter
term  fib1 : Nat
term  fib1 = nth [Nat] [#] n1 (fib [#])
term  fib2 : Nat
term  fib2 = nth [Nat] [#] n2 (fib [#])
term  fib3 : Nat
term  fib3 = nth [Nat] [#] n3 (fib [#])
term  fib4 : Nat
term  fib4 = nth [Nat] [#] n4 (fib [#])
term  fib5 : Nat
term  fib5 = nth [Nat] [#] n5 (fib [#])
type  Leq : ^ Nat -> ^ Nat -> Set
term  Leq.lqz : .[x : Nat] -> < Leq.lqz x : Leq (SNat.zero [#]) x >
term  Leq.lqs : .[x : Nat] -> .[y : Nat] -> ^(y2 : Leq x y) -> < Leq.lqs x y y2 : Leq (SNat.succ [#] x) (SNat.succ [#] y) >
type  Increasing : - Size -> ^ Stream Nat # -> Set
term  Increasing.inc : .[i : Size] -> .[x : Nat] -> .[y : Nat] -> ^(y3 : Leq x y) -> .[tl : Stream Nat #] -> ^(y5 : Increasing i (Stream.cons [#] y tl)) -> < Increasing.inc i x y y3 tl y5 : Increasing $i (Stream.cons [#] x (Stream.cons [#] y tl)) >
type  Eq : ++(A : Set) -> ^ A -> ^ A -> Set
term  Eq.refl : .[A : Set] -> .[a : A] -> < Eq.refl a : Eq A a a >
term  proof : Eq (Stream Nat #) (tail [Nat] [#] fibIter) (tail [Nat] [#] fibIter)
term  proof = Eq.refl [tail [Nat] [#] fibIter]
term  succ_ : .[i : Size] -> SNat i -> SNat $i
term  succ_ = [\ i ->] \ x -> SNat.succ [i] x
term  evil : .[i : Size] -> Stream Nat i
{ evil $[i < #] = map [Nat] [Nat] [$i] (succ_ [#]) (Stream.cons [i] (SNat.zero [#]) (evil [i]))
}
term  cons_ : .[A : Set] -> .[i : Size] -> A -> Stream A i -> Stream A $i
term  cons_ = [\ A ->] [\ i ->] \ a -> \ as -> Stream.cons [i] a as
term  dmerge : .[A : Set] -> .[i : Size] -> Stream (Stream A i) i -> Stream A i
{ dmerge [A] $[i < #] (Stream.cons [.i] ys yss) = Stream.cons [i] (head [A] [i] ys) (dmerge [A] [i] (zipWith [A] [Stream A i] [Stream A i] (cons_ [A] [i]) [i] (tail [A] [i] ys) yss))
}
--- evaluating ---
fibIter4 has whnf (head (SNat #) # (tail (SNat #) # (tail (SNat #) # (tail (SNat #) # (tail (SNat #) # (fibIter' n1 n1 ?14))))))
fibIter4 evaluates to head (SNat #) # (tail (SNat #) # (tail (SNat #) # (tail (SNat #) # (tail (SNat #) # (fibIter' (SNat.succ # (SNat.zero #)) (SNat.succ # (SNat.zero #)) ?14)))))
fib1 has whnf SNat.succ{i = #; y1 = SNat.zero{i = #}}
fib1 evaluates to SNat.succ # (SNat.zero #)
fib2 has whnf SNat.succ{i = #; y1 = SNat.zero{i = #}}
fib2 evaluates to SNat.succ # (SNat.zero #)
fib3 has whnf SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.zero{i = #}}}
fib3 evaluates to SNat.succ # (SNat.succ # (SNat.zero #))
fib4 has whnf SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.zero{i = #}}}}
fib4 evaluates to SNat.succ # (SNat.succ # (SNat.succ # (SNat.zero #)))
fib5 has whnf SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.succ{i = #; y1 = SNat.zero{i = #}}}}}}
fib5 evaluates to SNat.succ # (SNat.succ # (SNat.succ # (SNat.succ # (SNat.succ # (SNat.zero #)))))
--- closing "SolverBugStreamFixed.ma" ---