formatting

3 files changed, 194 insertions, 192 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index e7ad9b1..643ce8f 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -53,10 +53,10 @@ let import_trace filename first =
     raise VeritLexer.Eof
   with
     | VeritLexer.Eof ->
-      close_in chan;
-      let first =
-        let aux = VeritSyntax.get_clause !first_num in
-        match first, aux.value with
+       close_in chan;
+       let first =
+         let aux = VeritSyntax.get_clause !first_num in
+          match first, aux.value with
           | Some (root,l), Some (fl::nil) ->
             if Form.equal l fl then
               aux
@@ -132,17 +132,16 @@ let call_verit rt ro fl root =
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro fl;
   close_out outchan;
-  let logfilename = (Filename.chop_extension filename)^".vtlog" in
-
-  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof="^logfilename^" "^filename in
+  let logfilename = Filename.chop_extension filename ^ ".vtlog" in
+  let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename in
   Format.eprintf "%s@." command;
   let t0 = Sys.time () in
   let exit_code = Sys.command command in
   let t1 = Sys.time () in
   Format.eprintf "Verit = %.5f@." (t1-.t0);
   if exit_code <> 0 then
-    failwith ("Verit.call_verit: command "^command^
-	      " exited with code "^(string_of_int exit_code));
+    failwith ("Verit.call_verit: command " ^ command ^
+	        " exited with code " ^ string_of_int exit_code);
   try
     import_trace logfilename (Some root)
   with
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 3741339..126a02b 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -21,7 +21,8 @@ val theorem : Names.identifier -> string -> string -> unit
 val checker : string -> string -> unit
 val export :
   out_channel ->
-  SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit
+  SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl ->
+  SmtAtom.Form.t -> unit
 val call_verit :
   SmtAtom.Btype.reify_tbl ->
   SmtAtom.Op.reify_tbl ->
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 07a8a74..e03cbec 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -31,32 +31,34 @@ type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2
 
 let get_eq l =
   match Form.pform l with
-    | Fatom ha ->
-      (match Atom.atom ha with
-        | Abop (BO_eq _,a,b) -> (a,b)
-        | _ -> failwith "VeritSyntax.get_eq: equality was expected")
-    | _ -> failwith "VeritSyntax.get_eq: equality was expected"
+  | Fatom ha ->
+     (match Atom.atom ha with
+      | Abop (BO_eq _,a,b) -> (a,b)
+      | _ -> failwith "VeritSyntax.get_eq: equality was expected")
+  | _ -> failwith "VeritSyntax.get_eq: equality was expected"
 
 let get_at l =
   match Form.pform l with
-    | Fatom ha -> ha
-    | _ -> failwith "VeritSyntax.get_eq: equality was expected"
+  | Fatom ha -> ha
+  | _ -> failwith "VeritSyntax.get_eq: equality was expected"
 
 let is_eq l =
   match Form.pform l with
-    | Fatom ha ->
-      (match Atom.atom ha with
-        | Abop (BO_eq _,_,_) -> true
-        | _ -> false)
-    | _ -> failwith "VeritSyntax.get_eq: atom was expected"
+  | Fatom ha ->
+     (match Atom.atom ha with
+      | Abop (BO_eq _,_,_) -> true
+      | _ -> false)
+  | _ -> failwith "VeritSyntax.get_eq: atom was expected"
 
 
 (* Transitivity *)
 
-let rec list_find_remove p l =
-  match l with
-    | [] -> raise Not_found
-    | t::q -> if p t then (t,q) else let (a,l) = list_find_remove p q in (a,t::l)
+let rec list_find_remove p = function
+    [] -> raise Not_found
+  | h::t -> if p h
+            then h, t
+            else let (a, rest) = list_find_remove p t in
+                 a, h::rest
 
 let rec process_trans a b prem res =
   if List.length prem = 0 then (
@@ -75,77 +77,77 @@ let rec process_trans a b prem res =
 let mkTrans p =
   let (concl,prem) = List.partition Form.is_pos p in
   match concl with
-    |[c] ->
-      let a,b = get_eq c in
-      let prem_val = List.map (fun l -> (l,get_eq l)) prem in
-      let cert = (process_trans a b prem_val []) in
-      Other (EqTr (c,cert))
-    |_ -> failwith "VeritSyntax.mkTrans: no conclusion or more than one conclusion in transitivity"
+  |[c] ->
+    let a,b = get_eq c in
+    let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+    let cert = (process_trans a b prem_val []) in
+    Other (EqTr (c,cert))
+  |_ -> failwith "VeritSyntax.mkTrans: no conclusion or more than one conclusion in transitivity"
 
 
 (* Congruence *)
 
 let rec process_congr a_args b_args prem res =
   match a_args,b_args with
-    | a::a_args,b::b_args ->
-      (* if a = b *)
-      (* then process_congr a_args b_args prem (None::res) *)
-      (* else *)
-        let (l,(a',b')) = List.find (fun (l,(a',b')) -> ((Atom.equal a a') && (Atom.equal b b'))||((Atom.equal a b') && (Atom.equal b a'))) prem in
-        process_congr a_args b_args prem ((Some l)::res)
-    | [],[] -> List.rev res
-    | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application"
+  | a::a_args,b::b_args ->
+     (* if a = b *)
+     (* then process_congr a_args b_args prem (None::res) *)
+     (* else *)
+     let (l,(a',b')) = List.find (fun (l,(a',b')) -> ((Atom.equal a a') && (Atom.equal b b'))||((Atom.equal a b') && (Atom.equal b a'))) prem in
+     process_congr a_args b_args prem ((Some l)::res)
+  | [],[] -> List.rev res
+  | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application"
 
 
 let mkCongr p =
   let (concl,prem) = List.partition Form.is_pos p in
   match concl with
-    |[c] ->
-      let a,b = get_eq c in
-      let prem_val = List.map (fun l -> (l,get_eq l)) prem in
-      (match Atom.atom a, Atom.atom b with
-        | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
-          let a_args = [a1;a2] in
-          let b_args = [b1;b2] in
-          let cert = process_congr a_args b_args prem_val [] in
-          Other (EqCgr (c,cert))
-        | Auop (aop,a), Auop (bop,b) when (aop = bop) ->
-          let a_args = [a] in
-          let b_args = [b] in
-          let cert = process_congr a_args b_args prem_val [] in
+  |[c] ->
+    let a,b = get_eq c in
+    let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+    (match Atom.atom a, Atom.atom b with
+     | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
+        let a_args = [a1;a2] in
+        let b_args = [b1;b2] in
+        let cert = process_congr a_args b_args prem_val [] in
+        Other (EqCgr (c,cert))
+     | Auop (aop,a), Auop (bop,b) when (aop = bop) ->
+        let a_args = [a] in
+        let b_args = [b] in
+        let cert = process_congr a_args b_args prem_val [] in
+        Other (EqCgr (c,cert))
+     | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
+        if indexed_op_index a_f = indexed_op_index b_f then
+          let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
           Other (EqCgr (c,cert))
-        | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
-          if indexed_op_index a_f = indexed_op_index b_f then
-            let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
-            Other (EqCgr (c,cert))
-          else failwith "VeritSyntax.mkCongr: left function is different from right fucntion"
-        | _, _ -> failwith "VeritSyntax.mkCongr: atoms are not applications")
-    |_ -> failwith "VeritSyntax.mkCongr: no conclusion or more than one conclusion in congruence"
+        else failwith "VeritSyntax.mkCongr: left function is different from right fucntion"
+     | _, _ -> failwith "VeritSyntax.mkCongr: atoms are not applications")
+  |_ -> failwith "VeritSyntax.mkCongr: no conclusion or more than one conclusion in congruence"
 
 
 let mkCongrPred p =
   let (concl,prem) = List.partition Form.is_pos p in
   let (prem,prem_P) = List.partition is_eq prem in
   match concl with
-    |[c] ->
-      (match prem_P with
-        |[p_p] ->
-          let prem_val = List.map (fun l -> (l,get_eq l)) prem in
-          (match Atom.atom (get_at c), Atom.atom (get_at p_p) with
-            | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
-              let a_args = [a1;a2] in
-              let b_args = [b1;b2] in
-              let cert = process_congr a_args b_args prem_val [] in
-              Other (EqCgrP (p_p,c,cert))
-            | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
-              if indexed_op_index a_f = indexed_op_index b_f then
-                let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
-                Other (EqCgrP (p_p,c,cert))
-              else failwith "VeritSyntax.mkCongrPred: unmatching predicates"
-            | _ -> failwith "VeritSyntax.mkCongrPred : not pred app")
-        |_ ->  failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence")
-    |[] ->  failwith "VeritSyntax.mkCongrPred: no conclusion in congruence"
-    |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence"
+  |[c] ->
+    (match prem_P with
+     |[p_p] ->
+       let prem_val = List.map (fun l -> (l,get_eq l)) prem in
+       (match Atom.atom (get_at c), Atom.atom (get_at p_p) with
+        | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) ->
+           let a_args = [a1;a2] in
+           let b_args = [b1;b2] in
+           let cert = process_congr a_args b_args prem_val [] in
+           Other (EqCgrP (p_p,c,cert))
+        | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
+           if indexed_op_index a_f = indexed_op_index b_f then
+             let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
+             Other (EqCgrP (p_p,c,cert))
+           else failwith "VeritSyntax.mkCongrPred: unmatching predicates"
+        | _ -> failwith "VeritSyntax.mkCongrPred : not pred app")
+     |_ ->  failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence")
+  |[] ->  failwith "VeritSyntax.mkCongrPred: no conclusion in congruence"
+  |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence"
 
 
 (* Linear arithmetic *)
@@ -154,29 +156,29 @@ let mkMicromega cl =
   let _tbl, _f, cert = Lia.build_lia_certif cl in
   let c =
     match cert with
-      | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this"
-      | Some c -> c in
+    | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this"
+    | Some c -> c in
   Other (LiaMicromega (cl,c))
 
 
 let mkSplArith orig cl =
   let res =
     match cl with
-      | res::nil -> res
-      | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the resulting clause" in
+    | res::nil -> res
+    | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the resulting clause" in
   try
     let orig' =
       match orig.value with
-        | Some [orig'] -> orig'
-        | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in
+      | Some [orig'] -> orig'
+      | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in
     let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in
     let c =
       match cert with
-        | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this"
-        | Some c -> c in
+      | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this"
+      | Some c -> c in
     Other (SplArith (orig,res,c))
   with
-    | _ -> Other (ImmFlatten (orig, res))
+  | _ -> Other (ImmFlatten (orig, res))
 
 
 (* Elimination of operators *)
@@ -184,8 +186,8 @@ let mkSplArith orig cl =
 let mkDistinctElim old value =
   let rec find_res l1 l2 =
     match l1,l2 with
-      | t1::q1,t2::q2 -> if t1 == t2 then find_res q1 q2 else t2
-      | _, _ -> assert false in
+    | t1::q1,t2::q2 -> if t1 == t2 then find_res q1 q2 else t2
+    | _, _ -> assert false in
   let l1 = match old.value with
     | Some l -> l
     | None -> assert false in
@@ -204,108 +206,108 @@ let clear_clauses () = Hashtbl.clear clauses
 let mk_clause (id,typ,value,ids_params) =
   let kind =
     match typ with
-      (* Roots *)
-      | Inpu -> Root
-      (* Cnf conversion *)
-      | True -> Other SmtCertif.True
-      | Fals -> Other False
-      | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 ->
-        (match value with
-          | l::_ -> Other (BuildDef l)
-          | _ -> assert false)
-      | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 ->
-        (match value with
-          | l::_ -> Other (BuildDef2 l)
-          | _ -> assert false)
-      | Orn | Andp ->
-        (match value,ids_params with
-          | l::_, [p] -> Other (BuildProj (l,p))
-          | _ -> assert false)
-      | Impn1 ->
-        (match value with
-          | l::_ -> Other (BuildProj (l,0))
-          | _ -> assert false)
-      | Impn2 ->
-        (match value with
-          | l::_ -> Other (BuildProj (l,1))
-          | _ -> assert false)
-      | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
-        (match ids_params with
-          | [id] -> Other (ImmBuildDef (get_clause id))
-          | _ -> assert false)
-      | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 ->
-        (match ids_params with
-          | [id] -> Other (ImmBuildDef2 (get_clause id))
-          | _ -> assert false)
-      | And | Nor ->
-        (match ids_params with
-          | [id;p] -> Other (ImmBuildProj (get_clause id,p))
-          | _ -> assert false)
-      | Nimp1 ->
-        (match ids_params with
-          | [id] -> Other (ImmBuildProj (get_clause id,0))
-          | _ -> assert false)
-      | Nimp2 ->
-        (match ids_params with
-          | [id] -> Other (ImmBuildProj (get_clause id,1))
-          | _ -> assert false)
-      (* Equality *)
-      | Eqre -> mkTrans value
-      | Eqtr -> mkTrans value
-      | Eqco -> mkCongr value
-      | Eqcp -> mkCongrPred value
-      (* Linear integer arithmetic *)
-      | Dlge | Lage | Lata -> mkMicromega value
-      | Lade               -> mkMicromega value (* TODO: utiliser un solveur plus simple *)
-      | Dlde ->
-        (match value with
-          | l::_ -> Other (LiaDiseq l)
-          | _ -> assert false)
-      (* Resolution *)
-      | Reso ->
-        (match ids_params with
-          | cl1::cl2::q ->
-            let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
-            Res res
-          | _ -> assert false)
-      (* Simplifications *)
-      | Tpal ->
-        (match ids_params with
-          | id::_ -> Same (get_clause id)
-          | _ -> assert false)
-      | Tple ->
-        (match ids_params with
-          | id::_ -> Same (get_clause id)
-          | _ -> assert false)
-      | Tpde ->
-        (match ids_params with
-          | id::_ -> mkDistinctElim (get_clause id) value
-          | _ -> assert false)
-      | Tpsa | Tlap ->
-        (match ids_params with
-          | id::_ -> mkSplArith (get_clause id) value
-          | _ -> assert false)
-      (* Holes in proofs *)
-      | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
-       (* Not implemented *)
-      | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
-      | Fins -> failwith "VeritSyntax.ml: rule forall_inst not implemented yet"
-      | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
-      | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
-      | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
-      | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet"
-      | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet"
-      | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
-      | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
-      | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
-      | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet"
-      | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
-      | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
-      | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
-      | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet"
-      | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
-      | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
-      | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
+    (* Resolution *)
+    | Reso ->
+       (match ids_params with
+        | cl1::cl2::q ->
+           let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in
+           Res res
+        | _ -> assert false)
+    (* Roots *)
+    | Inpu -> Root
+    (* Cnf conversion *)
+    | True -> Other SmtCertif.True
+    | Fals -> Other False
+    | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 ->
+       (match value with
+        | l::_ -> Other (BuildDef l)
+        | _ -> assert false)
+    | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 ->
+       (match value with
+        | l::_ -> Other (BuildDef2 l)
+        | _ -> assert false)
+    | Orn | Andp ->
+       (match value,ids_params with
+        | l::_, [p] -> Other (BuildProj (l,p))
+        | _ -> assert false)
+    | Impn1 ->
+       (match value with
+        | l::_ -> Other (BuildProj (l,0))
+        | _ -> assert false)
+    | Impn2 ->
+       (match value with
+        | l::_ -> Other (BuildProj (l,1))
+        | _ -> assert false)
+    | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
+       (match ids_params with
+        | [id] -> Other (ImmBuildDef (get_clause id))
+        | _ -> assert false)
+    | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 ->
+       (match ids_params with
+        | [id] -> Other (ImmBuildDef2 (get_clause id))
+        | _ -> assert false)
+    | And | Nor ->
+       (match ids_params with
+        | [id;p] -> Other (ImmBuildProj (get_clause id,p))
+        | _ -> assert false)
+    | Nimp1 ->
+       (match ids_params with
+        | [id] -> Other (ImmBuildProj (get_clause id,0))
+        | _ -> assert false)
+    | Nimp2 ->
+       (match ids_params with
+        | [id] -> Other (ImmBuildProj (get_clause id,1))
+        | _ -> assert false)
+    (* Equality *)
+    | Eqre -> mkTrans value
+    | Eqtr -> mkTrans value
+    | Eqco -> mkCongr value
+    | Eqcp -> mkCongrPred value
+    (* Linear integer arithmetic *)
+    | Dlge | Lage | Lata -> mkMicromega value
+    | Lade               -> mkMicromega value (* TODO: utiliser un solveur plus simple *)
+    | Dlde ->
+       (match value with
+        | l::_ -> Other (LiaDiseq l)
+        | _ -> assert false)
+    (* Simplifications *)
+    | Tpal ->
+       (match ids_params with
+        | id::_ -> Same (get_clause id)
+        | _ -> assert false)
+    | Tple ->
+       (match ids_params with
+        | id::_ -> Same (get_clause id)
+        | _ -> assert false)
+    | Tpde ->
+       (match ids_params with
+        | id::_ -> mkDistinctElim (get_clause id) value
+        | _ -> assert false)
+    | Tpsa | Tlap ->
+       (match ids_params with
+        | id::_ -> mkSplArith (get_clause id) value
+        | _ -> assert false)
+    (* Holes in proofs *)
+    | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
+    (* Not implemented *)
+    | Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
+    | Fins -> failwith "VeritSyntax.ml: rule forall_inst not implemented yet"
+    | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet"
+    | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet"
+    | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet"
+    | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet"
+    | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet"
+    | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet"
+    | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet"
+    | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet"
+    | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet"
+    | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet"
+    | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet"
+    | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet"
+    | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet"
+    | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet"
+    | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet"
+    | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet"
   in
   let cl =
     (* TODO: change this into flatten when necessary *)