From 4de22917afd18df543e3281bb463ed51f2cfab61 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Jun 2009 21:23:44 +0000 Subject: [PATCH] better doc --- .../binaries/matitaprover/matitaprover.ml | 13 ++++++++++--- .../components/binaries/matitaprover/tptp_cnf.ml | 13 +++++++------ .../components/binaries/matitaprover/tptp_cnf.mli | 13 +++++++++++++ 3 files changed, 30 insertions(+), 9 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 2a5f9fdb0..499ecb273 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -31,7 +31,7 @@ hash "==";; hash "_";; let problem_file = ref "no-file-given";; -let tptppath = ref "./";; +let tptppath = ref "/";; let seconds = ref 300;; let fail_msg () = @@ -50,10 +50,17 @@ let main () = ("[path] TPTP lib root, default " ^ !tptppath); "--timeout", Arg.Int (fun p -> seconds := p), ("[seconds] timeout, default " ^ string_of_int !seconds); - ] (fun x -> problem_file := x) "matitaprover [problemfile]"; + ] (fun x -> problem_file := x) " +Matitaprover is the first order automatic prover that equips the +Matita interactive theorem prover (http://matita.cs.unibo.it). + +Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1 + +usage: matitaprover [options] problemfile"; 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 = leaf and type input = Ast.term = struct + let module B : Terms.Blob + with type t = leaf and type input = Ast.term = struct type t = leaf let eq a b = a == b let compare (a,_) (b,_) = Pervasives.compare a b diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml index bebce17e7..ffac76585 100644 --- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml +++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml @@ -17,12 +17,13 @@ let trans_formulae ~neg = function (* HELPERS *) let resolve ~tptppath s = let resolved_name = - if Filename.check_suffix s ".p" then - (assert (String.length s > 5); - let prefix = String.sub s 0 3 in - tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s) - else - tptppath ^ "/" ^ s + if tptppath = "/" then s else + if Filename.check_suffix s ".p" then + (assert (String.length s > 5); + let prefix = String.sub s 0 3 in + tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s) + else + tptppath ^ "/" ^ s in if HExtlib.is_regular resolved_name then resolved_name diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.mli b/helm/software/components/binaries/matitaprover/tptp_cnf.mli index 9e56414d4..48b57dbd7 100644 --- a/helm/software/components/binaries/matitaprover/tptp_cnf.mli +++ b/helm/software/components/binaries/matitaprover/tptp_cnf.mli @@ -1,3 +1,16 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) + val parse: tptppath:string -> string -> (Ast.term * Ast.term) list * (Ast.term * Ast.term) list -- 2.39.2