(* Delphin test file.  Functions related to Mini-ML
   Author: Carsten Schuermann
*)


add :: world (base) 
	all {N:exp} all {M:exp} exists {K:exp} true

fun add (A.z) M = <M, <>>
  | add ((A.s) N) M = 
    let 
	val <K, <>> = add N M
    in	
	<(A.s) K, <>>
    end


count :: world (param base)
	  all^ {e:exp} all^ {t:tp} all {P : of e t} 
	  exists {N : exp} true

fun count (B.of_z) = <B.z, <>>


  | count ((A:param T).u) = 
    choose (B:base)
    in 
      <(B.s) (B.z), <>>
    end

  | count ((B.of_fn) T1 T2 E P) =
    new (a: param T1)
    in
      count (P (a.x) (a.u))
    end
  | count ((B.of_fix) T E D) = 
    new (a: param T)
    in
      count (D (a.x) (a.u))
    end
  | count ((B.of_s) E P) = count P 
  | count ((B.of_app) E1 E2 T1 T2 D1 D2) = 
    let 
      val <N1, <>> = count D1 
      val <N2, <>> = count D2
    in
      add N1 N2
    end
 

new (b:base)

val <X, <>> = count ((b.of_s) (b.z) (b.of_z))
(* val <Y, <>> = count ((b.of_fix) (b.nat) ([x] x) ([x][u] u)) *)