ple_list03.smt2

(fixpoint "--rewrite")

(define ints2 (): [int] = { 
   Cons 1 (Cons 20 Nil)
})

(define filter (lq1 : func(0 , [a##a29r;bool]),  lq2 : [a##a29r]) : [a##a29r] = {
  if (isNil lq2) then Nil else (
      if (lq1 (head lq2)) 
        then (Cons (head lq2) (filter lq1 (tail lq2))) 
        else (filter lq1 (tail lq2)))
})

(define ints0 () : [int] = { 
    Cons 0 (Cons 1 (Cons 2 Nil))
})

(define isPos (lq1 : int) : bool = {
    lq1 > 0
})


(match isCons Cons x xs = (true))
(match isNil  Cons x xs = (false))
(match isCons Nil       = (false))
(match isNil  Nil       = (true))
(match tail Cons x xs   = (xs))
(match head Cons x xs   = (x))

(constant isCons (func(1 , [[@(0)], bool])))
(constant isNil  (func(1 , [[@(0)], bool])))
(constant Nil    (func(1 , [[@(0)]])))
(constant tail   (func(1 , [[@(0)], [@(0)]])))
(constant head   (func(1 , [[@(0)], @(0)])))
(constant ints0   [int])
(constant ints2   [int])
(constant filter  (func(1 , [func(0 , [@(0), bool]), [@(0)], [@(0)]])))
                
(constant isPos  (func(0 , [int, bool])))
(constant Cons   (func(1 , [@(0), [@(0)], [@(0)]])))
(constant Nil    (func(1 , [[@(0)]])))

(constraint
  ((filter isPos ints0 == ints2))
)