# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597457012 -32400
# Node ID 4b131e351170ed7abc41321d088a968f005f3b20
# Parent  17cd0e70e931ae2694667edffa08377bb9e458ab
continuation based skolem

diff -r 17cd0e70e931 -r 4b131e351170 clausal.agda
--- a/clausal.agda	Sat Aug 15 10:18:55 2020 +0900
+++ b/clausal.agda	Sat Aug 15 11:03:32 2020 +0900
@@ -44,37 +44,21 @@
 --    enough unused functions and constants for skolemization necessary
 --    assuming non overrupping quantified variables
 
-record Skolem : Set where
-   field 
-     st : Statement
-     cl : List Const
-     fl : List Func
-     vr : List Var
-
 {-# TERMINATING #-} 
 skolem  : List Const → List Func → (sbst : Expr  → Var →  Expr  → Expr  ) → Statement → Statement
-skolem cl fl sbst s = Skolem.st (skolemv record { st = s ; cl = cl ; fl = fl ; vr = [] })  where
-   skolemv : Skolem → Skolem
-   skolemv S with Skolem.vr S | Skolem.st S 
-   skolemv S | v | All x => s  = record S1 { st = All x => Skolem.st S1 } where
-        S1 : Skolem 
-        S1 = skolemv record S { st = s ;  vr = x ∷ v } 
-   skolemv S | [] | (Exist x => s) with Skolem.cl S
-   ... | [] = S
-   ... | sk ∷ cl = skolemv record S { st = subst-prop s sbst x (Expr.const sk) ; cl = cl }
-   skolemv S | (v ∷ t) | (Exist x => s)  with Skolem.fl S
-   ... | [] = S
-   ... | sk ∷ fl = skolemv record S { st = subst-prop s sbst x (func sk (mkarg v t )) ; fl = fl }  where
+skolem cl fl sbst s = skolemv1 ( λ s cl fl vr → s ) s cl fl []  where
+   skolemv1 : (Statement → List Const → List Func → List Var → Statement ) → Statement → List Const → List Func → List Var → Statement
+   skolemv1 next (All x => s )   cl fl vl              = skolemv1 next s cl fl ( x ∷ vl) 
+   skolemv1 next (Exist x => s ) [] fl []              = skolemv1 next s [] fl [] 
+   skolemv1 next (Exist x => s ) (sk ∷ cl ) fl []      = skolemv1 next (subst-prop s sbst x (Expr.const sk)) cl fl [] 
+   skolemv1 next (Exist x => s ) cl [] (v ∷ t)         = skolemv1 next s cl [] (v ∷ t)
+   skolemv1 next (Exist x => s ) cl (sk ∷ fl) (v ∷ t)  = skolemv1 next (subst-prop s sbst x (func sk (mkarg v t) )) cl fl (v ∷ t)  where
       mkarg : (v : Var) (vl : List Var ) → Expr
       mkarg v []  = var v
       mkarg v (v1 ∷ t )  = var v , mkarg v1 t
-   skolemv S | v | s /\ s₁ = record S2 { st = Skolem.st S1 /\ Skolem.st S2 }  where
-        S1 = skolemv record S {st = s}
-        S2 = skolemv record S1 {st = s₁}
-   skolemv S | v | s \/ s₁ = record S2 { st = Skolem.st S1 \/ Skolem.st S2 }  where
-        S1 = skolemv record S {st = s}
-        S2 = skolemv record S1 {st = s₁}
-   skolemv S | _ | _ = S
+   skolemv1 next (s /\ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s /\ s₁) ) s₁ ) s 
+   skolemv1 next (s \/ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s \/ s₁) ) s₁ ) s 
+   skolemv1 next s cl fl vl                            = next s cl fl vl 
 
 -- remove universal quantifiers
 univout  : Statement → Statement