More fixes

althelf/alethe.smt3

@@ -76,24 +76,24 @@
   :match-conclusion CL
 )
 
-% TODO: side condition, vars
-(declare-rule bind ((ctx Bool) (T Type) (phi T) (phi' T))
+% TODO: side condition
+(declare-rule bind ((ctx Context) (xs VarList) (ys VarList) (T Type) (phi T) (phi' T))
   :assumption ctx
   :premises ((cl (= phi phi')))
   :requires ((check_bind ctx xs ys) true)
   :match-conclusion (cl (= (forall xs phi) (forall ys phi')))
 )
 
-% TODO: side condition, vars
-(declare-rule sko_ex ((ctx Bool) (phi Bool) (psi Bool))
+% TODO: side condition
+(declare-rule sko_ex ((ctx Context) (xs VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :requires ((check_sko_ex ctx xs) true)
   :match-conclusion (cl (= (exists xs phi) psi))
 )
 
-% TODO: side condition, vars
-(declare-rule sko_forall ((ctx Bool) (phi Bool) (psi Bool))
+% TODO: side condition
+(declare-rule sko_forall ((ctx Context) (xs VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :requires ((check_sko_forall ctx xs) true)
@@ -101,21 +101,21 @@
 )
 
 % TODO: side condition
-(declare-rule forall_inst ((ctx Bool) (phi Bool) (psi Bool))
+(declare-rule forall_inst ((ctx Bool) (xs VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :requires ((check_sko_forall ctx xs) true)
   :match-conclusion (cl (= (forall xs phi) psi))
 )
 
-% TODO: side condition, vars
-(declare-rule forall_inst ((P Bool) (P' Bool))
+% TODO: side condition
+(declare-rule forall_inst ((P Bool) (P' Bool) (xs VarList))
   :requires ((check_forall_inst xs P P') true)
   :match-conclusion (cl (or (not (forall xs P) P')))
 )
 
 % TODO: side condition
-(declare-rule refl ((T Type) (t1 T) (t2 T))
+(declare-rule refl ((ctx Context) (T Type) (t1 T) (t2 T))
   :premises (ctx)
   :requires ((check_refl ctx t1 t2) true)
   :match-conclusion (cl (= t1 t2))
@@ -156,8 +156,7 @@
   :match-conclusion CL
 )
 
-% TODO: vars
-(declare-rule qnt_cnf ((phi Bool) (phi' Bool))
+(declare-rule qnt_cnf ((phi Bool) (phi' Bool) (xs VarList) (xs' VarList))
   :match-conclusion (cl (or (not (forall xs phi)) (forall xs' phi')))
 )
 
@@ -449,10 +448,12 @@
   :match-conclusion (cl (= l r))
 )
 
-% TODO (needs scope)
-(declare-rule onepoint ()
-  :args ()
-  :conclusion true
+% TODO: sidecondition
+(declare-rule onepoint ((ctx Context) (xs VarList) (ys VarList) (Q (-> VarList Bool Bool)) (T Type) (phi T) (phi' T))
+  :assumption ctx
+  :premises ((cl (= phi phi')))
+  :requires ((check_onepoint Q ctx xs ys phi phi') true)
+  :match-conclusion (cl (= (Q xs phi) (Q ys phi')))
 )
 
 % TODO: sidecondition
@@ -509,10 +510,10 @@
   :match-conclusion (cl (= l r))
 )
 
-% TODO (needs scope)
+% TODO: We don't have a representation of Let!
 (declare-rule let ()
-  :args ()
-  :conclusion true
+  :premise-list Eqs and
+  :match-conclusion true
 )
 
 % TODO: sidecondition