From: Enrico Tassi Date: Thu, 25 Jun 2009 13:08:35 +0000 (+0000) Subject: initial import of standalone matitaprover binary X-Git-Tag: make_still_working~3800 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c9b8f3ba2c86446d44160ae494bc85624bc5eaf;p=helm.git initial import of standalone matitaprover binary --- diff --git a/helm/software/components/binaries/matitaprover/_tags b/helm/software/components/binaries/matitaprover/_tags new file mode 100644 index 000000000..031f71886 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/_tags @@ -0,0 +1 @@ +: use_str, use_unix diff --git a/helm/software/components/binaries/matitaprover/ast.ml b/helm/software/components/binaries/matitaprover/ast.ml new file mode 120000 index 000000000..ddba86734 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/ast.ml @@ -0,0 +1 @@ +../../tptp_grafite/ast.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/discrimination_tree.ml b/helm/software/components/binaries/matitaprover/discrimination_tree.ml new file mode 120000 index 000000000..fcc11a6f8 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/discrimination_tree.ml @@ -0,0 +1 @@ +../../extlib/discrimination_tree.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/discrimination_tree.mli b/helm/software/components/binaries/matitaprover/discrimination_tree.mli new file mode 120000 index 000000000..877466d53 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/discrimination_tree.mli @@ -0,0 +1 @@ +../../extlib/discrimination_tree.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foSubst.ml b/helm/software/components/binaries/matitaprover/foSubst.ml new file mode 120000 index 000000000..6083e68e5 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foSubst.ml @@ -0,0 +1 @@ +../../ng_paramodulation/foSubst.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foSubst.mli b/helm/software/components/binaries/matitaprover/foSubst.mli new file mode 120000 index 000000000..4729ffee6 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foSubst.mli @@ -0,0 +1 @@ +../../ng_paramodulation/foSubst.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foUnif.ml b/helm/software/components/binaries/matitaprover/foUnif.ml new file mode 120000 index 000000000..6eb2baad6 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foUnif.ml @@ -0,0 +1 @@ +../../ng_paramodulation/foUnif.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foUnif.mli b/helm/software/components/binaries/matitaprover/foUnif.mli new file mode 120000 index 000000000..805dacde4 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foUnif.mli @@ -0,0 +1 @@ +../../ng_paramodulation/foUnif.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foUtils.ml b/helm/software/components/binaries/matitaprover/foUtils.ml new file mode 120000 index 000000000..3177cefaa --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foUtils.ml @@ -0,0 +1 @@ +../../ng_paramodulation/foUtils.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/foUtils.mli b/helm/software/components/binaries/matitaprover/foUtils.mli new file mode 120000 index 000000000..6f9257913 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/foUtils.mli @@ -0,0 +1 @@ +../../ng_paramodulation/foUtils.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/hExtlib.ml b/helm/software/components/binaries/matitaprover/hExtlib.ml new file mode 120000 index 000000000..88e70084a --- /dev/null +++ b/helm/software/components/binaries/matitaprover/hExtlib.ml @@ -0,0 +1 @@ +../../extlib/hExtlib.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/hExtlib.mli b/helm/software/components/binaries/matitaprover/hExtlib.mli new file mode 120000 index 000000000..36b31ec36 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/hExtlib.mli @@ -0,0 +1 @@ +../../extlib/hExtlib.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/index.ml b/helm/software/components/binaries/matitaprover/index.ml new file mode 120000 index 000000000..bc5880a8f --- /dev/null +++ b/helm/software/components/binaries/matitaprover/index.ml @@ -0,0 +1 @@ +../../ng_paramodulation/index.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/index.mli b/helm/software/components/binaries/matitaprover/index.mli new file mode 120000 index 000000000..4578c0d88 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/index.mli @@ -0,0 +1 @@ +../../ng_paramodulation/index.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/lexer.mll b/helm/software/components/binaries/matitaprover/lexer.mll new file mode 120000 index 000000000..f0e5f3056 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/lexer.mll @@ -0,0 +1 @@ +../../tptp_grafite/lexer.mll \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml new file mode 100644 index 000000000..344db716d --- /dev/null +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -0,0 +1,24 @@ +let main () = + let problem_file = ref "" in + Arg.parse [ + ] (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 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 + end + in + let module P = Paramod.Paramod(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); + () +;; + +main () diff --git a/helm/software/components/binaries/matitaprover/orderings.ml b/helm/software/components/binaries/matitaprover/orderings.ml new file mode 120000 index 000000000..46dbef55c --- /dev/null +++ b/helm/software/components/binaries/matitaprover/orderings.ml @@ -0,0 +1 @@ +../../ng_paramodulation/orderings.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/orderings.mli b/helm/software/components/binaries/matitaprover/orderings.mli new file mode 120000 index 000000000..2fd7665cc --- /dev/null +++ b/helm/software/components/binaries/matitaprover/orderings.mli @@ -0,0 +1 @@ +../../ng_paramodulation/orderings.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/paramod.ml b/helm/software/components/binaries/matitaprover/paramod.ml new file mode 120000 index 000000000..c3c8c3663 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/paramod.ml @@ -0,0 +1 @@ +../../ng_paramodulation/paramod.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/paramod.mli b/helm/software/components/binaries/matitaprover/paramod.mli new file mode 120000 index 000000000..1c44d423f --- /dev/null +++ b/helm/software/components/binaries/matitaprover/paramod.mli @@ -0,0 +1 @@ +../../ng_paramodulation/paramod.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/parser.mly b/helm/software/components/binaries/matitaprover/parser.mly new file mode 120000 index 000000000..934f8b1f8 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/parser.mly @@ -0,0 +1 @@ +../../tptp_grafite/parser.mly \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/pp.ml b/helm/software/components/binaries/matitaprover/pp.ml new file mode 120000 index 000000000..3e02375a4 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/pp.ml @@ -0,0 +1 @@ +../../ng_paramodulation/pp.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/pp.mli b/helm/software/components/binaries/matitaprover/pp.mli new file mode 120000 index 000000000..ae9951173 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/pp.mli @@ -0,0 +1 @@ +../../ng_paramodulation/pp.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/stdpp.ml b/helm/software/components/binaries/matitaprover/stdpp.ml new file mode 100644 index 000000000..7684469f4 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/stdpp.ml @@ -0,0 +1,4 @@ +type location = unit +let first_pos () = 0 +let last_pos () = 0 +let make_loc _ = () diff --git a/helm/software/components/binaries/matitaprover/superposition.ml b/helm/software/components/binaries/matitaprover/superposition.ml new file mode 120000 index 000000000..79fd4a81e --- /dev/null +++ b/helm/software/components/binaries/matitaprover/superposition.ml @@ -0,0 +1 @@ +../../ng_paramodulation/superposition.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/superposition.mli b/helm/software/components/binaries/matitaprover/superposition.mli new file mode 120000 index 000000000..f1e2dd900 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/superposition.mli @@ -0,0 +1 @@ +../../ng_paramodulation/superposition.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/terms.ml b/helm/software/components/binaries/matitaprover/terms.ml new file mode 120000 index 000000000..eef4768af --- /dev/null +++ b/helm/software/components/binaries/matitaprover/terms.ml @@ -0,0 +1 @@ +../../ng_paramodulation/terms.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/terms.mli b/helm/software/components/binaries/matitaprover/terms.mli new file mode 120000 index 000000000..0e87d2ec6 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/terms.mli @@ -0,0 +1 @@ +../../ng_paramodulation/terms.mli \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml new file mode 100644 index 000000000..ef5136c9e --- /dev/null +++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml @@ -0,0 +1,467 @@ +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 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 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 = + 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 + in + if HExtlib.is_regular resolved_name then + resolved_name + else + begin + prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")"); + exit 1 + end +;; + +(* MAIN *) +let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () = + paramod_timeout := timeout; + depth := def_depth; + let rec aux = function + | [] -> [] + | ((A.Inclusion (file,_)) as hd) :: 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) + | 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 + 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 + 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) +;; +*) + +let parse _ = assert false;; diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.mli b/helm/software/components/binaries/matitaprover/tptp_cnf.mli new file mode 100644 index 000000000..ecf930bc4 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/tptp_cnf.mli @@ -0,0 +1 @@ +val parse: string -> unit list * unit list diff --git a/helm/software/components/binaries/matitaprover/trie.ml b/helm/software/components/binaries/matitaprover/trie.ml new file mode 120000 index 000000000..d09f5ace4 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/trie.ml @@ -0,0 +1 @@ +../../extlib/trie.ml \ No newline at end of file diff --git a/helm/software/components/binaries/matitaprover/trie.mli b/helm/software/components/binaries/matitaprover/trie.mli new file mode 120000 index 000000000..d4437ed17 --- /dev/null +++ b/helm/software/components/binaries/matitaprover/trie.mli @@ -0,0 +1 @@ +../../extlib/trie.mli \ No newline at end of file diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index 9ca0ec9a3..a835b247f 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -1,9 +1,11 @@ +cicUniv.cmi: unshare.cmi: cic.cmo deannotate.cmi: cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo -discrimination_tree.cmi: cic.cmo +libraryObjects.cmi: +cic_indexable.cmi: cic.cmo path_indexing.cmi: cic.cmo cicInspect.cmi: cic.cmo cic.cmo: cicUniv.cmi @@ -22,8 +24,8 @@ helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi libraryObjects.cmo: libraryObjects.cmi libraryObjects.cmx: libraryObjects.cmi -discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi -discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi +cic_indexable.cmo: cicUtil.cmi cic.cmo cic_indexable.cmi +cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi path_indexing.cmo: cic.cmo path_indexing.cmi path_indexing.cmx: cic.cmx path_indexing.cmi cicInspect.cmo: cic.cmo cicInspect.cmi diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index f880a0243..8cdd2a86a 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -5,7 +5,7 @@ cicParser.cmi: cic.cmx cicUtil.cmi: cic.cmx helmLibraryObjects.cmi: cic.cmx libraryObjects.cmi: -discrimination_tree.cmi: cic.cmx +cic_indexable.cmi: cic.cmx path_indexing.cmi: cic.cmx cicInspect.cmi: cic.cmx cic.cmo: cicUniv.cmi @@ -24,8 +24,8 @@ helmLibraryObjects.cmo: cic.cmx helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi libraryObjects.cmo: libraryObjects.cmi libraryObjects.cmx: libraryObjects.cmi -discrimination_tree.cmo: cicUtil.cmi cic.cmx discrimination_tree.cmi -discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi +cic_indexable.cmo: cicUtil.cmi cic.cmx cic_indexable.cmi +cic_indexable.cmx: cicUtil.cmx cic.cmx cic_indexable.cmi path_indexing.cmo: cic.cmx path_indexing.cmi path_indexing.cmx: cic.cmx path_indexing.cmi cicInspect.cmo: cic.cmx cicInspect.cmi diff --git a/helm/software/components/cic/Makefile b/helm/software/components/cic/Makefile index c846f3804..07f1d3f14 100644 --- a/helm/software/components/cic/Makefile +++ b/helm/software/components/cic/Makefile @@ -9,7 +9,7 @@ INTERFACE_FILES = \ cicUtil.mli \ helmLibraryObjects.mli \ libraryObjects.mli \ - discrimination_tree.mli \ + cic_indexable.mli \ path_indexing.mli \ cicInspect.mli IMPLEMENTATION_FILES = \ diff --git a/helm/software/components/cic/cic_indexable.ml b/helm/software/components/cic/cic_indexable.ml new file mode 100644 index 000000000..7e98b8c5e --- /dev/null +++ b/helm/software/components/cic/cic_indexable.ml @@ -0,0 +1,81 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: discrimination_tree.ml 8991 2008-09-19 12:47:23Z tassi $ *) + +module CicIndexable : Discrimination_tree.Indexable +with type input = Cic.term and type constant_name = UriManager.uri += struct + + type input = Cic.term + type constant_name = UriManager.uri + open Discrimination_tree + + let ppelem = function + | Constant (uri,arity) -> + "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")" + | Bound (i,arity) -> + "("^string_of_int i ^ "," ^ string_of_int arity^")" + | Variable -> "?" + | Proposition -> "Prop" + | Datatype -> "Type" + | Dead -> "Dead" + ;; + + let path_string_of = + let rec aux arity = function + | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable] + | Cic.Appl (Cic.Lambda _ :: _) -> + [Variable] (* maybe we should b-reduce *) + | Cic.Appl [] -> assert false + | Cic.Appl (hd::tl) -> + aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) + | Cic.Cast (t,_) -> aux arity t + | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable] + (* I think we should CicSubstitution.subst Implicit t *) + | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *) + | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable] + | Cic.Rel i -> [Bound (i, arity)] + | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition] + | Cic.Sort _ -> assert (arity=0); [Datatype] + | Cic.Const _ | Cic.Var _ + | Cic.MutInd _ | Cic.MutConstruct _ as t -> + [Constant (CicUtil.uri_of_term t, arity)] + | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead] + in + aux 0 + ;; + + let compare e1 e2 = + match e1,e2 with + | Constant (u1,a1),Constant (u2,a2) -> + let x = UriManager.compare u1 u2 in + if x = 0 then Pervasives.compare a1 a2 else x + | e1,e2 -> Pervasives.compare e1 e2 + ;; + + let string_of_path l = String.concat "." (List.map ppelem l) ;; +end + diff --git a/helm/software/components/cic/cic_indexable.mli b/helm/software/components/cic/cic_indexable.mli new file mode 100644 index 000000000..fc1f73fbb --- /dev/null +++ b/helm/software/components/cic/cic_indexable.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +module CicIndexable : Discrimination_tree.Indexable +with type input = Cic.term and type constant_name = UriManager.uri + diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml deleted file mode 100644 index faccadf65..000000000 --- a/helm/software/components/cic/discrimination_tree.ml +++ /dev/null @@ -1,234 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* $Id$ *) - -type 'a path_string_elem = - | Constant of 'a * int (* name, arity *) - | Bound of int * int (* rel, arity *) - | Variable (* arity is 0 *) - | Proposition (* arity is 0 *) - | Datatype (* arity is 0 *) - | Dead (* arity is 0 *) -;; - -type 'a path = ('a path_string_elem) list;; - -module type Indexable = sig - type input - type constant_name - val compare: - constant_name path_string_elem -> - constant_name path_string_elem -> int - val string_of_path : constant_name path -> string - val path_string_of : input -> constant_name path -end - -module CicIndexable : Indexable -with type input = Cic.term and type constant_name = UriManager.uri -= struct - - type input = Cic.term - type constant_name = UriManager.uri - - let ppelem = function - | Constant (uri,arity) -> - "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")" - | Bound (i,arity) -> - "("^string_of_int i ^ "," ^ string_of_int arity^")" - | Variable -> "?" - | Proposition -> "Prop" - | Datatype -> "Type" - | Dead -> "Dead" - ;; - - let path_string_of = - let rec aux arity = function - | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable] - | Cic.Appl (Cic.Lambda _ :: _) -> - [Variable] (* maybe we should b-reduce *) - | Cic.Appl [] -> assert false - | Cic.Appl (hd::tl) -> - aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) - | Cic.Cast (t,_) -> aux arity t - | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable] - (* I think we should CicSubstitution.subst Implicit t *) - | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *) - | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable] - | Cic.Rel i -> [Bound (i, arity)] - | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition] - | Cic.Sort _ -> assert (arity=0); [Datatype] - | Cic.Const _ | Cic.Var _ - | Cic.MutInd _ | Cic.MutConstruct _ as t -> - [Constant (CicUtil.uri_of_term t, arity)] - | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead] - in - aux 0 - ;; - - let compare e1 e2 = - match e1,e2 with - | Constant (u1,a1),Constant (u2,a2) -> - let x = UriManager.compare u1 u2 in - if x = 0 then Pervasives.compare a1 a2 else x - | e1,e2 -> Pervasives.compare e1 e2 - ;; - - let string_of_path l = String.concat "." (List.map ppelem l) ;; -end - -let arity_of = function - | Constant (_,a) - | Bound (_,a) -> a - | _ -> 0 -;; - -module type DiscriminationTree = - sig - - type input - type data - type dataset - type constant_name - type t - - val iter : t -> (constant_name path -> dataset -> unit) -> unit - - val empty : t - val index : t -> input -> data -> t - val remove_index : t -> input -> data -> t - val in_index : t -> input -> (data -> bool) -> bool - val retrieve_generalizations : t -> input -> dataset - val retrieve_unifiables : t -> input -> dataset - end - -module Make (I:Indexable) (A:Set.S) : DiscriminationTree -with type constant_name = I.constant_name and type input = I.input -and type data = A.elt and type dataset = A.t = - - struct - - module OrderedPathStringElement = struct - type t = I.constant_name path_string_elem - let compare = I.compare - end - - type constant_name = I.constant_name - type data = A.elt - type dataset = A.t - type input = I.input - - module PSMap = Map.Make(OrderedPathStringElement);; - - type key = PSMap.key - - module DiscriminationTree = Trie.Make(PSMap);; - - type t = A.t DiscriminationTree.t - - let empty = DiscriminationTree.empty;; - - let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;; - - let index tree term info = - let ps = I.path_string_of term in - let ps_set = - try DiscriminationTree.find ps tree with Not_found -> A.empty - in - DiscriminationTree.add ps (A.add info ps_set) tree - ;; - - let remove_index tree term info = - let ps = I.path_string_of term in - try - let ps_set = A.remove info (DiscriminationTree.find ps tree) in - if A.is_empty ps_set then DiscriminationTree.remove ps tree - else DiscriminationTree.add ps ps_set tree - with Not_found -> tree - ;; - - let in_index tree term test = - let ps = I.path_string_of term in - try - let ps_set = DiscriminationTree.find ps tree in - A.exists test ps_set - with Not_found -> false - ;; - - (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is - (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to - skip all its progeny, thus you want to reach t. - - You need to skip as many elements as the sum of all arieties contained - in the progeny of f. - - The input ariety is the one of f while the path is x.g....t - Should be the equivalent of after_t in the literature (handbook A.R.) - *) - let rec skip arity path = - if arity = 0 then path else match path with - | [] -> assert false - | m::tl -> skip (arity-1+arity_of m) tl - ;; - - (* the equivalent of skip, but on the index, thus the list of trees - that are rooted just after the term represented by the tree root - are returned (we are skipping the root) *) - let skip_root = function DiscriminationTree.Node (value, map) -> - let rec get n = function DiscriminationTree.Node (v, m) as tree -> - if n = 0 then [tree] else - PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m [] - in - PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map [] - ;; - - let retrieve unif tree term = - let path = I.path_string_of term in - let rec retrieve path tree = - match tree, path with - | DiscriminationTree.Node (Some s, _), [] -> s - | DiscriminationTree.Node (None, _), [] -> A.empty - | DiscriminationTree.Node (_, map), Variable::path when unif -> - List.fold_left A.union A.empty - (List.map (retrieve path) (skip_root tree)) - | DiscriminationTree.Node (_, map), node::path -> - A.union - (if not unif && node = Variable then A.empty else - try retrieve path (PSMap.find node map) - with Not_found -> A.empty) - (try - match PSMap.find Variable map,skip (arity_of node) path with - | DiscriminationTree.Node (Some s, _), [] -> s - | n, path -> retrieve path n - with Not_found -> A.empty) - in - retrieve path tree - ;; - - let retrieve_generalizations tree term = retrieve false tree term;; - let retrieve_unifiables tree term = retrieve true tree term;; - end -;; - diff --git a/helm/software/components/cic/discrimination_tree.mli b/helm/software/components/cic/discrimination_tree.mli deleted file mode 100644 index a31129306..000000000 --- a/helm/software/components/cic/discrimination_tree.mli +++ /dev/null @@ -1,74 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -type 'a path_string_elem = - | Constant of 'a * int (* name, arity *) - | Bound of int * int (* rel, arity *) - | Variable (* arity is 0 *) - | Proposition (* arity is 0 *) - | Datatype (* arity is 0 *) - | Dead (* arity is 0 *) -;; - -type 'a path = ('a path_string_elem) list;; - -module type Indexable = sig - type input - type constant_name - val compare: - constant_name path_string_elem -> - constant_name path_string_elem -> int - val string_of_path : constant_name path -> string - val path_string_of : input -> constant_name path -end - -module CicIndexable : Indexable -with type input = Cic.term and type constant_name = UriManager.uri - -module type DiscriminationTree = - sig - - type input - type data - type dataset - type constant_name - type t - - val iter : t -> (constant_name path -> dataset -> unit) -> unit - - val empty : t - val index : t -> input -> data -> t - val remove_index : t -> input -> data -> t - val in_index : t -> input -> (data -> bool) -> bool - val retrieve_generalizations : t -> input -> dataset - val retrieve_unifiables : t -> input -> dataset - end - - -module Make (I : Indexable) (A : Set.S) : DiscriminationTree -with type constant_name = I.constant_name and type input = I.input -and type data = A.elt and type dataset = A.t - diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index 6d96e61e2..dcc6377a0 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,3 +1,13 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi @@ -10,6 +20,8 @@ hLog.cmo: hLog.cmi hLog.cmx: hLog.cmi trie.cmo: trie.cmi trie.cmx: trie.cmi +discrimination_tree.cmo: trie.cmi discrimination_tree.cmi +discrimination_tree.cmx: trie.cmx discrimination_tree.cmi hTopoSort.cmo: hTopoSort.cmi hTopoSort.cmx: hTopoSort.cmi refCounter.cmo: refCounter.cmi diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt index 6d96e61e2..dcc6377a0 100644 --- a/helm/software/components/extlib/.depend.opt +++ b/helm/software/components/extlib/.depend.opt @@ -1,3 +1,13 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi @@ -10,6 +20,8 @@ hLog.cmo: hLog.cmi hLog.cmx: hLog.cmi trie.cmo: trie.cmi trie.cmx: trie.cmi +discrimination_tree.cmo: trie.cmi discrimination_tree.cmi +discrimination_tree.cmx: trie.cmx discrimination_tree.cmi hTopoSort.cmo: hTopoSort.cmi hTopoSort.cmx: hTopoSort.cmi refCounter.cmo: refCounter.cmi diff --git a/helm/software/components/extlib/Makefile b/helm/software/components/extlib/Makefile index f4d92191d..4aa36a488 100644 --- a/helm/software/components/extlib/Makefile +++ b/helm/software/components/extlib/Makefile @@ -8,6 +8,7 @@ INTERFACE_FILES = \ patternMatcher.mli \ hLog.mli \ trie.mli \ + discrimination_tree.mli \ hTopoSort.mli \ refCounter.mli \ graphvizPp.mli \ diff --git a/helm/software/components/extlib/discrimination_tree.ml b/helm/software/components/extlib/discrimination_tree.ml new file mode 100644 index 000000000..e0803c350 --- /dev/null +++ b/helm/software/components/extlib/discrimination_tree.ml @@ -0,0 +1,181 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + +type 'a path_string_elem = + | Constant of 'a * int (* name, arity *) + | Bound of int * int (* rel, arity *) + | Variable (* arity is 0 *) + | Proposition (* arity is 0 *) + | Datatype (* arity is 0 *) + | Dead (* arity is 0 *) +;; + +type 'a path = ('a path_string_elem) list;; + +module type Indexable = sig + type input + type constant_name + val compare: + constant_name path_string_elem -> + constant_name path_string_elem -> int + val string_of_path : constant_name path -> string + val path_string_of : input -> constant_name path +end + +let arity_of = function + | Constant (_,a) + | Bound (_,a) -> a + | _ -> 0 +;; + +module type DiscriminationTree = + sig + + type input + type data + type dataset + type constant_name + type t + + val iter : t -> (constant_name path -> dataset -> unit) -> unit + + val empty : t + val index : t -> input -> data -> t + val remove_index : t -> input -> data -> t + val in_index : t -> input -> (data -> bool) -> bool + val retrieve_generalizations : t -> input -> dataset + val retrieve_unifiables : t -> input -> dataset + end + +module Make (I:Indexable) (A:Set.S) : DiscriminationTree +with type constant_name = I.constant_name and type input = I.input +and type data = A.elt and type dataset = A.t = + + struct + + module OrderedPathStringElement = struct + type t = I.constant_name path_string_elem + let compare = I.compare + end + + type constant_name = I.constant_name + type data = A.elt + type dataset = A.t + type input = I.input + + module PSMap = Map.Make(OrderedPathStringElement);; + + type key = PSMap.key + + module DiscriminationTree = Trie.Make(PSMap);; + + type t = A.t DiscriminationTree.t + + let empty = DiscriminationTree.empty;; + + let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;; + + let index tree term info = + let ps = I.path_string_of term in + let ps_set = + try DiscriminationTree.find ps tree with Not_found -> A.empty + in + DiscriminationTree.add ps (A.add info ps_set) tree + ;; + + let remove_index tree term info = + let ps = I.path_string_of term in + try + let ps_set = A.remove info (DiscriminationTree.find ps tree) in + if A.is_empty ps_set then DiscriminationTree.remove ps tree + else DiscriminationTree.add ps ps_set tree + with Not_found -> tree + ;; + + let in_index tree term test = + let ps = I.path_string_of term in + try + let ps_set = DiscriminationTree.find ps tree in + A.exists test ps_set + with Not_found -> false + ;; + + (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is + (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to + skip all its progeny, thus you want to reach t. + + You need to skip as many elements as the sum of all arieties contained + in the progeny of f. + + The input ariety is the one of f while the path is x.g....t + Should be the equivalent of after_t in the literature (handbook A.R.) + *) + let rec skip arity path = + if arity = 0 then path else match path with + | [] -> assert false + | m::tl -> skip (arity-1+arity_of m) tl + ;; + + (* the equivalent of skip, but on the index, thus the list of trees + that are rooted just after the term represented by the tree root + are returned (we are skipping the root) *) + let skip_root = function DiscriminationTree.Node (value, map) -> + let rec get n = function DiscriminationTree.Node (v, m) as tree -> + if n = 0 then [tree] else + PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m [] + in + PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map [] + ;; + + let retrieve unif tree term = + let path = I.path_string_of term in + let rec retrieve path tree = + match tree, path with + | DiscriminationTree.Node (Some s, _), [] -> s + | DiscriminationTree.Node (None, _), [] -> A.empty + | DiscriminationTree.Node (_, map), Variable::path when unif -> + List.fold_left A.union A.empty + (List.map (retrieve path) (skip_root tree)) + | DiscriminationTree.Node (_, map), node::path -> + A.union + (if not unif && node = Variable then A.empty else + try retrieve path (PSMap.find node map) + with Not_found -> A.empty) + (try + match PSMap.find Variable map,skip (arity_of node) path with + | DiscriminationTree.Node (Some s, _), [] -> s + | n, path -> retrieve path n + with Not_found -> A.empty) + in + retrieve path tree + ;; + + let retrieve_generalizations tree term = retrieve false tree term;; + let retrieve_unifiables tree term = retrieve true tree term;; + end +;; + diff --git a/helm/software/components/extlib/discrimination_tree.mli b/helm/software/components/extlib/discrimination_tree.mli new file mode 100644 index 000000000..e979b8e69 --- /dev/null +++ b/helm/software/components/extlib/discrimination_tree.mli @@ -0,0 +1,71 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +type 'a path_string_elem = + | Constant of 'a * int (* name, arity *) + | Bound of int * int (* rel, arity *) + | Variable (* arity is 0 *) + | Proposition (* arity is 0 *) + | Datatype (* arity is 0 *) + | Dead (* arity is 0 *) +;; + +type 'a path = ('a path_string_elem) list;; + +module type Indexable = sig + type input + type constant_name + val compare: + constant_name path_string_elem -> + constant_name path_string_elem -> int + val string_of_path : constant_name path -> string + val path_string_of : input -> constant_name path +end + +module type DiscriminationTree = + sig + + type input + type data + type dataset + type constant_name + type t + + val iter : t -> (constant_name path -> dataset -> unit) -> unit + + val empty : t + val index : t -> input -> data -> t + val remove_index : t -> input -> data -> t + val in_index : t -> input -> (data -> bool) -> bool + val retrieve_generalizations : t -> input -> dataset + val retrieve_unifiables : t -> input -> dataset + end + + +module Make (I : Indexable) (A : Set.S) : DiscriminationTree +with type constant_name = I.constant_name and type input = I.input +and type data = A.elt and type dataset = A.t + diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.ml b/helm/software/components/tactics/paramodulation/equality_indexing.ml index 458433aba..19aae0d29 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.ml +++ b/helm/software/components/tactics/paramodulation/equality_indexing.ml @@ -28,7 +28,7 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t + type t = Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t val empty : t val retrieve_generalizations : t -> Cic.term -> PosEqSet.t val retrieve_unifiables : t -> Cic.term -> PosEqSet.t @@ -36,7 +36,7 @@ module type EqualityIndex = val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t val in_index : t -> Equality.equality -> bool - val iter : t -> (Discrimination_tree.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit + val iter : t -> (Cic_indexable.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit end module DT = @@ -50,7 +50,7 @@ struct module PosEqSet = Set.Make(OrderedPosEquality);; - include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet) + include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet) (* DISCRIMINATION TREES *) @@ -95,7 +95,7 @@ module PT = module PosEqSet = Set.Make(OrderedPosEquality);; - include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet) + include Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet) (* DISCRIMINATION TREES *) diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.mli b/helm/software/components/tactics/paramodulation/equality_indexing.mli index c4b9df0ea..d976843f9 100644 --- a/helm/software/components/tactics/paramodulation/equality_indexing.mli +++ b/helm/software/components/tactics/paramodulation/equality_indexing.mli @@ -26,7 +26,7 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t + type t = Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t val empty : t val retrieve_generalizations : t -> Cic.term -> PosEqSet.t val retrieve_unifiables : t -> Cic.term -> PosEqSet.t @@ -34,7 +34,7 @@ module type EqualityIndex = val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t val in_index : t -> Equality.equality -> bool - val iter : t -> (Discrimination_tree.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit + val iter : t -> (Cic_indexable.CicIndexable.constant_name Discrimination_tree.path -> PosEqSet.t -> unit) -> unit end module DT : EqualityIndex diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index e36cfba49..06d1ada3f 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -31,7 +31,7 @@ module Index : with type elt = Utils.pos * Equality.equality and type t = Equality_indexing.DT.PosEqSet.t type t = - Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t + Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t end val check_for_duplicates : Cic.metasenv -> string -> unit diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index 780b72daf..d20dbda35 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -28,7 +28,7 @@ module Codomain = struct let compare = Pervasives.compare end module S = Set.Make(Codomain) -module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S) +module TI = Discrimination_tree.Make(Cic_indexable.CicIndexable)(S) type universe = TI.t let empty = TI.empty ;;