From d4d8691cd71651c778eacd6cc8d7ecc6f51d41df Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Jun 2009 14:42:56 +0000 Subject: [PATCH] matitaprover is almost there --- .../binaries/matitaprover/matitaprover.ml | 59 ++- .../binaries/matitaprover/tptp_cnf.ml | 456 +----------------- .../binaries/matitaprover/tptp_cnf.mli | 4 +- .../components/ng_paramodulation/pp.ml | 36 +- 4 files changed, 95 insertions(+), 460 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 344db716d..5a438c7b6 100644 --- 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 ef5136c9e..51ed32431 100644 --- 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 ecf930bc4..9e56414d4 100644 --- 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 537ad02c1..bba9a26ae 100644 --- 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 "@[{"; 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 "@[{"; 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 = -- 2.39.2