matitaprover is almost there

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 344db716d94661a3f1213cae86bf14852caa77fd..5a438c7b6fa700d9a139669b32765db58530bb60 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -1,23 +1,60 @@
 let main () =
-  let problem_file = ref "" in
+  let problem_file = ref "no-file-given" in
+  let tptppath = ref "./" in
   Arg.parse [
+   "--tptppath", Arg.String (fun p -> tptppath := p), "[path]  TPTP lib root"
    ] (fun x -> problem_file := x) "matitaprover [problemfile]";
-  let hypotheses, goal = Tptp_cnf.parse !problem_file in
-  let module B : Terms.Blob = struct
-        type t = Ast.atom
+  let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
+  let goal = match goals with [x] -> x | _ -> assert false in
+  let module B : Terms.Blob with type t = Ast.term = struct
+        type t = Ast.term
         let eq a b = a = b
         let compare = Pervasives.compare
-        let eqP = Ast.True
-        let pp x = ""
-        let embed x = Terms.Var 0
-        let saturate x y = Terms.Var 0,Terms.Var 0
+        let eqP = Ast.Constant "=="
+        let pp = function
+          | Ast.Constant x -> x
+          | Ast.Variable _ -> assert false
+          | Ast.Function _ -> assert false
+        ;;
+        let embed x = 
+          let rec aux m = function
+            | Ast.Variable name ->
+                (try m, List.assoc name m
+                 with Not_found -> 
+                    let t = Terms.Var (List.length m) in
+                    (name,t)::m, t)
+            | Ast.Constant _ as t -> m, Terms.Leaf t
+            | Ast.Function (name,args) -> 
+                let m, args = 
+                  HExtlib.list_mapi_acc 
+                    (fun x _ m -> aux m x) m args
+                in
+                m, Terms.Node (Terms.Leaf (Ast.Constant name):: args) 
+          in
+            aux [] x
+        ;;
+        let saturate bo ty = 
+          let vars, ty = embed ty in
+          let _, bo = embed bo in
+          let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
+          bo, ty
+        ;;
+        let embed t = snd(embed t);;
+
   end
   in
   let module P = Paramod.Paramod(B) in
+  let module Pp = Pp.Pp(B) in
   let bag = Terms.M.empty, 0 in
-  let g_passives = assert false in
-  let passives = assert false in
-  ignore(P.paramod bag ~g_passives ~passives);
+  let bag, g_passives = P.mk_goal bag goal in
+  let bag, passives = 
+    HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
+  in
+  prerr_endline "Facts";
+  prerr_endline (String.concat "\n" (List.map Pp.pp_unit_clause passives));
+  prerr_endline "Goal";
+  prerr_endline (Pp.pp_unit_clause g_passives);
+  ignore(P.paramod bag ~g_passives:[g_passives] ~passives);
   ()
 ;;
 

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index ef5136c9e03968ac4324df17748cf858d9695986..51ed32431af6eb699cfe11c72d60f6bb2bc292ef 100644 (file)
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -1,373 +1,18 @@
-module A = Ast;;
-(*
 
-type sort = Prop | Univ;;
-
-let floc = HExtlib.dummy_floc;;
-
-
-let paramod_timeout = ref 600;;
-let depth = ref 10;;
-
-let universe = "Univ" ;;
-let prop = "Prop";;
-
-let kw = [
- "and","myand"
-];;
-
-let mk_ident s =
-  PT.Ident ((try List.assoc s kw with Not_found -> s),None)
-;;
-
-let rec collect_arities_from_term = function
-  | A.Constant name -> [name,(0,Univ)]
-  | A.Variable name -> [name,(0,Univ)]
-  | A.Function (name,l) -> 
-      (name,(List.length l,Univ))::
-        List.flatten (List.map collect_arities_from_term l)
-;;
-
-let rec collect_fv_from_term = function
-  | A.Constant name -> []
-  | A.Variable name -> [name]
-  | A.Function (_,l) -> 
-      List.flatten (List.map collect_fv_from_term l)
-;;
-
-let collect_arities_from_atom a = 
-  let aux = function
-    | A.Proposition name -> [name,(0,Prop)]
-    | A.Predicate (name,args) -> 
-        (name,(List.length args,Prop)) :: 
-          (List.flatten (List.map collect_arities_from_term args))
-    | A.True -> []
-    | A.False -> []
-    | A.Eq (t1,t2) -> 
-        collect_arities_from_term t1 @ collect_arities_from_term t2
-    | A.NotEq (t1,t2) -> 
-        collect_arities_from_term t1 @ collect_arities_from_term t2
-  in
-  HExtlib.list_uniq (List.sort compare (List.flatten (List.map aux a)))
-;;
-  
-let collect_fv_from_atom a = 
-  let aux = function
-    | A.Proposition name -> [name] 
-    | A.Predicate (name,args) -> 
-        name :: List.flatten (List.map collect_fv_from_term args)
-    | A.True -> []
-    | A.False -> []
-    | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
-    | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
-  in
-  let rec aux2 = function
-    | [] -> []
-    | hd::tl -> aux hd @ aux2 tl
-  in
-  HExtlib.list_uniq (List.sort compare (aux2 a))
-;;  
-
-let rec collect_fv_from_formulae = function
-  | A.Disjunction (a,b) -> 
-      collect_fv_from_formulae a @ collect_fv_from_formulae b
-  | A.NegAtom a 
-  | A.Atom a -> collect_fv_from_atom [a]
-;;
-
-let rec convert_term = function
-  | A.Variable x -> mk_ident x
-  | A.Constant x -> mk_ident x
-  | A.Function (name, args) -> 
-      PT.Appl (mk_ident name :: List.map convert_term args)
-;;
-
-let rec atom_of_formula neg pos = function
-    | A.Disjunction (a,b) ->
-        let neg, pos = atom_of_formula neg pos a in
-        atom_of_formula neg pos b 
-    | A.NegAtom a -> a::neg, pos 
-    | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
-    | A.Atom a -> neg, a::pos
-;;
-
-let atom_of_formula f =
-  let neg, pos = atom_of_formula [] [] f in
-  neg @ pos
-;;
-  
-let rec mk_arrow component tail = function
-  | 0 -> begin
-      match tail with
-      | Prop -> mk_ident prop
-      | Univ -> mk_ident universe
-      end
-  | n -> 
-      PT.Binder 
-        (`Forall,
-          ((mk_ident "_"),Some (mk_ident component)),
-          mk_arrow component tail (n-1))
-;;
-
-let build_ctx_for_arities univesally arities t = 
-  let binder = if univesally then `Forall else `Exists in
-  let rec aux = function
-    | [] -> t
-    | (name,(nargs,sort))::tl ->
-        PT.Binder 
-          (binder,
-            (mk_ident name,Some (mk_arrow universe sort nargs)),
-            aux tl)
-  in
-  aux arities
+let trans_atom ~neg = function 
+  | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
+  | Ast.Eq _ when neg -> assert false
+  | Ast.Eq (a,b) -> Ast.Function ("==",[Ast.Constant "Ω"; a; b])
+  | Ast.NotEq (a,b) when neg -> Ast.Function ("==",[Ast.Constant "Ω"; a; b])
+  | Ast.NotEq _ -> assert false
 ;;
 
-let convert_atom universally a = 
-  let aux = function
-  | A.Proposition p -> mk_ident p
-  | A.Predicate (name,params) -> 
-      PT.Appl ((mk_ident name) :: (List.map convert_term params))
-  | A.True -> mk_ident "True"
-  | A.False -> mk_ident "False"
-  | A.Eq (l,r)
-  | A.NotEq (l,r) -> (* removes the negation *)
-      PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r]
-  in
-  let rec aux2 = function
-    | [] -> assert false
-    | [x] -> aux x
-    | he::tl -> 
-        if universally then 
-          PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl)
-        else
-          PT.Appl [mk_ident "And";aux he;aux2 tl]
-  in
-  let arities = collect_arities_from_atom a in
-  let fv = collect_fv_from_atom a in
-  build_ctx_for_arities universally 
-    (List.filter 
-      (function (x,(0,Univ)) -> List.mem x fv | _-> false) 
-      arities) 
-    (aux2 a)
-;;
-
-let collect_arities atom ctx = 
-  let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in
-  collect_arities_from_atom atoms
+let trans_formulae ~neg = function
+  | Ast.Disjunction _ -> assert false
+  | Ast.Atom a -> trans_atom ~neg a
+  | Ast.NegAtom _ -> assert false
 ;;
 
-let collect_arities_from_formulae f =
-  let rec collect_arities_from_formulae = function
-  | A.Disjunction (a,b) -> 
-      collect_arities_from_formulae a @ collect_arities_from_formulae b
-  | A.NegAtom a 
-  | A.Atom a -> collect_arities_from_atom [a]
-  in
-  HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
-;;
-
-let is_formulae_1eq_negated f =
-  let atom = atom_of_formula f in
-  match atom with
-  | [A.NotEq (l,r)] -> true
-  | _ -> false
-;;  
-
-let collect_fv_1stord_from_formulae f =
-  let arities = collect_arities_from_formulae f in
-  let fv = collect_fv_from_formulae f in
-  List.map fst 
-    (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
-;;
-
-let rec convert_formula fv no_arities context f =
-  let atom = atom_of_formula f in
-  let t = convert_atom (fv = []) atom in
-  let rec build_ctx n = function
-    | [] -> t
-    | hp::tl -> 
-        PT.Binder 
-          (`Forall,
-            (mk_ident ("H" ^ string_of_int n), 
-              Some (convert_formula [] true [] hp)), 
-            build_ctx (n+1) tl)
-  in
-  let arities = if no_arities then [] else collect_arities atom context in
-  build_ctx_for_arities true arities (build_ctx 0 context) 
-;;
-
-let check_if_atom_is_negative = function
-  | A.True -> false
-  | A.False -> true
-  | A.Proposition _ -> false
-  | A.Predicate _ -> false
-  | A.Eq _ -> false
-  | A.NotEq _ -> true
-;;
-
-let rec check_if_formula_is_negative = function
-  | A.Disjunction (a,b) ->
-      check_if_formula_is_negative a && check_if_formula_is_negative b
-  | A.NegAtom a -> not (check_if_atom_is_negative a)
-  | A.Atom a -> check_if_atom_is_negative a
-;;
-
-let ng_generate_tactics fv ueq_case context arities =
-  [ GA.Executable(floc,GA.NTactic(floc, 
-     [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
-  @      
-  (HExtlib.list_mapi
-   (fun (name,_) _-> 
-     GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
-       GA.NDot(floc)])))
-   arities)
-  @
-  (HExtlib.list_mapi
-   (fun _ i-> 
-     GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
-   context)
-  @
-(if fv <> [] then     
-  (List.flatten
-    (List.map 
-      (fun _ -> 
-        [GA.Executable(floc,GA.NTactic(floc, 
-          [GA.NApply (floc,
-            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
-              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
-         GA.Executable(floc,GA.NTactic(floc, 
-          [GA.NPos (floc,[2])]))])
-      fv)) 
- else [])@
-  [GA.Executable(floc,GA.NTactic(floc, [
-    if (*ueq_case*) true then
-        GA.NAuto (floc,(
-          HExtlib.list_mapi 
-            (fun _ i -> 
-               mk_ident ("H" ^ string_of_int i)) 
-            context    
-                ,[]))
-    else
-        GA.NAuto (floc,([],[
-                "depth",string_of_int 5;
-                "width",string_of_int 5;
-                "size",string_of_int 20;
-                "timeout",string_of_int 10;
-        ]))
- ;
-  GA.NSemicolon(floc)]));
-(*
-  GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
-    GA.Assumption floc)), GA.Dot(floc)))
-*)
-  ]@
-(if fv <> [] then     
-  (List.flatten
-    (List.map 
-      (fun _ -> 
-              [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
-               GA.NSkip floc; GA.NMerge floc]))])
-      fv)) 
- else [])@
-    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
-                                        GA.NSemicolon(floc)]))]@
-  [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
-;;
-
-let generate_tactics fv ueq_case =
-  [GA.Executable(floc,GA.Tactic(floc, Some
-   (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
-(if fv <> [] then     
-  (List.flatten
-    (List.map 
-      (fun _ -> 
-        [GA.Executable(floc,GA.Tactic(floc, Some
-          (GA.Exists floc),GA.Branch floc));
-         GA.Executable(floc,GA.Tactic(floc, None,
-          (GA.Pos (floc,[2]))))])
-      fv)) 
- else [])@
-  [GA.Executable(floc,GA.Tactic(floc, Some (
-    if true (*ueq_case*) then
-        GA.AutoBatch (floc,([],["paramodulation","";
-        "timeout",string_of_int !paramod_timeout]))
-    else
-        GA.AutoBatch (floc,([],[
-                "depth",string_of_int 5;
-                "width",string_of_int 5;
-                "size",string_of_int 20;
-                "timeout",string_of_int 10;
-        ]))
-  ),
-    GA.Semicolon(floc)));
-  GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
-    GA.Assumption floc)), GA.Dot(floc)))
-  ]@
-(if fv <> [] then     
-  (List.flatten
-    (List.map 
-      (fun _ -> 
-        [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
-         GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
-         (GA.Merge floc)))])
-      fv)) 
- else [])@
-  [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
-   GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
-;;
-
-let convert_ast ng statements context = function
-  | A.Comment s -> 
-      let s = String.sub s 1 (String.length s - 1) in
-      let s = 
-        if s.[String.length s - 1] = '\n' then
-          String.sub s 0 (String.length s - 1)
-        else 
-          s
-      in
-      statements @ [GA.Comment (floc,GA.Note (floc,s))],
-      context
-  | A.Inclusion (s,_) ->
-      statements @ [
-        GA.Comment (
-          floc, GA.Note (
-            floc,"Inclusion of: " ^ s))], context
-  | A.AnnotatedFormula (name,kind,f,_,_) -> 
-      match kind with
-      | A.Axiom 
-      | A.Hypothesis ->
-          statements, f::context
-      | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
-          statements, f::context
-      | A.Negated_conjecture ->
-          let ueq_case = is_formulae_1eq_negated f in
-          let fv = collect_fv_1stord_from_formulae f in 
-          let old_f = f in
-          let f = 
-            PT.Binder 
-             (`Forall,
-               (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), 
-               convert_formula fv false context f)
-          in
-          let o = PT.Theorem (`Theorem,name,f,None) in
-          (statements @ 
-          [ GA.Executable(floc,GA.Command(floc,
-             (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
-          if ng then 
-            ng_generate_tactics fv ueq_case context
-              (let atom = atom_of_formula old_f in collect_arities atom context)
-          else generate_tactics fv ueq_case),
-          context
-      | A.Definition 
-      | A.Lemma 
-      | A.Theorem 
-      | A.Conjecture
-      | A.Lemma_conjecture 
-      | A.Plain 
-      | A.Unknown -> assert false
-;;
 
 (* HELPERS *)
 let resolve ~tptppath s = 
@@ -389,79 +34,30 @@ let resolve ~tptppath s =
 ;;
 
 (* MAIN *)
-let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
-  paramod_timeout := timeout;
-  depth := def_depth;
+let parse ~tptppath filename =
   let rec aux = function
     | [] -> []
-    | ((A.Inclusion (file,_)) as hd) :: tl ->
+    | (Ast.Inclusion (file,_)) :: tl ->
         let file = resolve ~tptppath file in
         let lexbuf = Lexing.from_channel (open_in file) in
         let statements = Parser.main Lexer.yylex lexbuf in
-        hd :: aux (statements @ tl)
+        aux (statements @ tl)
     | hd::tl -> hd :: aux tl
   in
-  let statements = aux [A.Inclusion (filename,[])] in
-  let grafite_ast_statements,_ = 
-    List.fold_left 
-      (fun (st, ctx) f -> 
-        let newst, ctx = convert_ast ng st ctx f in
-        newst, ctx)
-      ([],[]) statements 
-  in
-  let pp t = 
-    (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
-     * which will show up using the following command line:
-     * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
-    let width = max_int in
-    let term_pp prec content_term =
-      let pres_term = TermContentPres.pp_ast content_term in
-      let lookup_uri = fun _ -> None in
-      let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
-      let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
-      Pcre.substitute 
-       ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x) 
-       s
+  let statements = aux [Ast.Inclusion (filename,[])] in
+  let positives, negatives = 
+    let rec aux p n = function
+      | [] -> p,n
+      | Ast.Comment _ :: tl -> aux p n tl
+      | Ast.AnnotatedFormula (name, (Ast.Axiom | Ast.Hypothesis), f,_,_) :: tl->
+          aux (p@[Ast.Constant name,trans_formulae ~neg:false f]) n tl
+      | Ast.AnnotatedFormula (name, Ast.Negated_conjecture, f,_,_) :: tl ->
+          assert (n = []);
+          aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) tl
+      | _ -> prerr_endline "bad syntax"; assert false
     in
-    CicNotationPp.set_pp_term (term_pp 90);
-    let lazy_term_pp = fun x -> assert false in
-    let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
-    Pcre.replace ~pat:"theorem" ~templ:"ntheorem" 
-     (GrafiteAstPp.pp_statement
-       ~map_unicode_to_tex:false ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t)
-  in
-  let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
-  let extra_statements_start = [
-    (*GA.Executable(floc,GA.Command(floc,
-    GA.Set(floc,"baseuri",buri)))*)]
-  in
-  let preamble = 
-    match raw_preamble with
-    | None -> 
-       pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
-    | Some s -> s buri
-  in
-  let extra_statements_end = [] in
-  let aliases = []
-   (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
-   ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
-   ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
-   ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
-   ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
-   ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
-  in
-  let s1 = List.map pp extra_statements_start in
-  let s2 = 
-    List.map 
-     (fun (n,s) -> 
-       LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
-     aliases
+      aux [] [] statements
   in
-  let s3 = List.map pp grafite_ast_statements in
-  let s4 = List.map pp extra_statements_end in
-  String.concat "\n" (s1@[preamble]@s2@s3@s4)
+  positives, negatives
 ;;
-*)
 
-let parse _ = assert false;;

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.mli b/helm/software/components/binaries/matitaprover/tptp_cnf.mli
index ecf930bc4ae37600d361e2b899186d3367da9836..9e56414d454ba6b710ea8c1f74c4090c14fcc67f 100644 (file)
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.mli
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.mli
@@ -1 +1,3 @@
-val parse: string -> unit list * unit list
+val parse: 
+      tptppath:string -> string -> 
+         (Ast.term * Ast.term) list * (Ast.term * Ast.term) list

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 537ad02c13e849e6044a1d7a4512f55da4b33d2f..bba9a26aee53ea06c86ca2bf4284f18683476fad 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -93,15 +93,15 @@ let pp_unit_clause ~formatter:f c =
       | Terms.Predicate t ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f t;
-         Format.fprintf f "@;[%s] by %s@]"
-            (String.concat ", " (List.map string_of_int vars))
-            (match proof with
-               | Terms.Exact _ -> "axiom"
-               | Terms.Step (rule, id1, id2, _, p, _) -> 
-                   Printf.sprintf "%s %d with %d at %s" 
-                     (string_of_rule rule)
-                     id1 id2 (String.concat
-                               "," (List.map string_of_int p)))
+          Format.fprintf f "@;[%s] by "
+            (String.concat ", " (List.map string_of_int vars));
+          (match proof with
+           | Terms.Exact t -> pp_foterm f t
+           | Terms.Step (rule, id1, id2, _, p, _) -> 
+               Format.fprintf f "%s %d with %d at %s" 
+                 (string_of_rule rule) id1 id2 (String.concat
+                  "," (List.map string_of_int p)));
+          Format.fprintf f "@]"
       | Terms.Equation (lhs, rhs, ty, comp) ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f ty;
@@ -109,15 +109,15 @@ let pp_unit_clause ~formatter:f c =
          pp_foterm f lhs;
           Format.fprintf f "@;%s@;" (string_of_comparison comp);
          pp_foterm f rhs;
-          Format.fprintf f "@]@;[%s] by %s@]"
-            (String.concat ", " (List.map string_of_int vars))
-            (match proof with
-            | Terms.Exact _ -> "axiom"
-            | Terms.Step (rule, id1, id2, _, p, _) -> 
-                 Printf.sprintf "%s %d with %d at %s" 
-                  (string_of_rule rule)
-                  id1 id2 (String.concat
-                 "," (List.map string_of_int p)))
+          Format.fprintf f "@]@;[%s] by "
+            (String.concat ", " (List.map string_of_int vars));
+          (match proof with
+           | Terms.Exact t -> pp_foterm f t
+           | Terms.Step (rule, id1, id2, _, p, _) -> 
+               Format.fprintf f "%s %d with %d at %s" 
+                 (string_of_rule rule) id1 id2 (String.concat
+                  "," (List.map string_of_int p)));
+          Format.fprintf f "@]"
 ;;
 
 let pp_bag ~formatter:f bag =