From: Alberto Griggio Date: Thu, 21 Jul 2005 11:47:50 +0000 (+0000) Subject: modifications/fixes for the integration with auto X-Git-Tag: V_0_7_2~129 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;p=helm.git modifications/fixes for the integration with auto --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 9d30e7020..321f5fba7 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -1,86 +1,36 @@ -BIN_DIR = /usr/local/bin +PACKAGE = paramodulation -TEST_REQUIRES = \ +REQUIRES = \ helm-registry \ - helm-tactics \ helm-cic_transformations \ - helm-cic_textual_parser2 - -REQUIRES = $(TEST_REQUIRES) - -OCAMLOPTIONS = \ - -package "$(REQUIRES)" -predicates "$(PREDICATES)" #-pp camlp4o -thread -OCAMLFIND = ocamlfind -OCAMLDEBUGOPTIONS = -g -OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) -OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = $(OCAMLFIND) ocamldep #-pp camlp4o -OCAMLDEBUG = wowcamldebug - -LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -TEST_LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) -TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) - -all: saturation -opt: saturation.opt + helm-tactics \ + helm-cic_textual_parser2 \ + mysql INTERFACE_FILES = \ utils.mli \ inference.mli -DEPOBJS = \ - $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ trie.ml \ path_indexing.ml \ discrimination_tree.ml \ - test_indexing.ml \ indexing.ml \ saturation.ml -TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ - trie.cmo \ - path_indexing.cmo \ - discrimination_tree.cmo \ - indexing.cmo \ - saturation.cmo -TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ - trie.cmo \ - path_indexing.cmo \ - discrimination_tree.cmo \ - test_indexing.cmo -# REGTESTOBJS = $(TESTOBJS) regtest.cmo -# TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo - -$(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) -$(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) - -depend: - $(OCAMLDEP) $(DEPOBJS) > .depend - -saturation: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -thread -linkpkg -o $@ $(TOPLEVELOBJS) -saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) - -test_indexing: $(TESTOBJS) $(TEST_LIBRARIES) - $(OCAMLC) -linkpkg -o $@ $(TESTOBJS) +# saturate_main.ml +# test_indexing.ml -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: - $(OCAMLC) -c $< -.mli.cmi: - $(OCAMLC) -c $< -.ml.cmx: - $(OCAMLOPT) -c $< -$(TOPLEVELOBJS): $(LIBRARIES) -$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) +include ../Makefile.common -clean: - rm -f *.cm[iox] *.o saturation{,.opt} regtest{,.opt} testlibrary{,.opt} +PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) \ + saturate_main.cmo +PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) \ + saturate_main.cmx -ifneq ($(MAKECMDGOALS), depend) - include .depend -endif +saturate: $(PARAMOD_OBJS) $(LIBRARIES) + $(OCAMLC) -thread -linkpkg -o $@ $(PARAMOD_OBJS) +saturate.opt: $(PARAMOD_OBJS_OPT) $(LIBRARIES) + $(OCAMLOPT) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 254a42332..dc87e7503 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -41,59 +41,6 @@ module PosEqSet = Set.Make(OrderedPosEquality);; module DiscriminationTree = Trie.Make(PSMap);; - -(* -module DiscriminationTree = struct - type key = path_string - type t = Node of PosEqSet.t option * (t PSMap.t) - - let empty = Node (None, PSMap.empty) - - let rec find l t = - match (l, t) with - | [], Node (None, _) -> raise Not_found - | [], Node (Some v, _) -> v - | x::r, Node (_, m) -> find r (PSMap.find x m) - - let rec mem l t = - match (l, t) with - | [], Node (None, _) -> false - | [], Node (Some _, _) -> true - | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false - - let add l v t = - let rec ins = function - | [], Node (_, m) -> Node (Some v, m) - | x::r, Node (v, m) -> - let t' = try PSMap.find x m with Not_found -> empty in - let t'' = ins (r, t') in - Node (v, PSMap.add x t'' m) - in - ins (l, t) - - let rec remove l t = - match (l, t) with - | [], Node (_, m) -> Node (None, m) - | x::r, Node (v, m) -> - try - let t' = remove r (PSMap.find x m) in - let m' = if t' = empty then PSMap.remove x m else PSMap.add x t' m in - Node (v, m') - with Not_found -> - t - - let rec fold f t acc = - let rec traverse revp t acc = match t with - | Node (None, m) -> - PSMap.fold (fun x -> traverse (x::revp)) m acc - | Node (Some v, m) -> - f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc) - in - traverse [] t acc - -end -*) - let string_of_discrimination_tree tree = let rec to_string level = function diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index f15a0cee6..64a96f82a 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -116,6 +116,8 @@ let get_candidates mode tree term = Discrimination_tree.PosEqSet.elements s in (* print_candidates mode term res; *) +(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) +(* print_newline (); *) let t2 = Unix.gettimeofday () in indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); res @@ -148,7 +150,7 @@ let rec find_matches metasenv context ugraph lift_amount term = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in try - let r = + let r = Inference.matching (metasenv @ metas) context term (S.lift lift_amount c) ugraph in let t2 = Unix.gettimeofday () in diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 1252c6069..23347e24c 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -435,6 +435,7 @@ let rec is_simple_term = function | Cic.Appl l -> List.for_all is_simple_term l | Cic.Meta (i, l) -> check_irl 1 l | Cic.Rel _ -> true + | Cic.Const _ -> true | _ -> false ;; @@ -455,9 +456,6 @@ let unification_simple metasenv context t1 t2 ugraph = let module U = CicUnification in let lookup = lookup_subst in let rec occurs_check subst what where = - (* Printf.printf "occurs_check %s %s" *) - (* (CicPp.ppterm what) (CicPp.ppterm where); *) - (* print_newline (); *) match where with | t when what = t -> true | C.Appl l -> List.exists (occurs_check subst what) l @@ -467,49 +465,15 @@ let unification_simple metasenv context t1 t2 ugraph = | _ -> false in let rec unif subst menv s t = -(* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *) -(* (print_subst subst); *) -(* print_newline (); *) let s = match s with C.Meta _ -> lookup s subst | _ -> s and t = match t with C.Meta _ -> lookup t subst | _ -> t in - (* Printf.printf "after apply_subst: %s %s\n%s" *) - (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *) - (* print_newline (); *) match s, t with | s, t when s = t -> subst, menv | C.Meta (i, _), C.Meta (j, _) when i > j -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> raise (U.UnificationFailure "Inference.unification.unif") -(* | C.Meta (i, l), C.Meta (j, l') -> *) -(* let _, _, ty = CicUtil.lookup_meta i menv in *) -(* let _, _, ty' = CicUtil.lookup_meta j menv in *) -(* let binding1 = lookup s subst in *) -(* let binding2 = lookup t subst in *) -(* let subst, menv = *) -(* if binding1 != s then *) -(* if binding2 != t then *) -(* unif subst menv binding1 binding2 *) -(* else *) -(* if binding1 = t then *) -(* subst, menv *) -(* else *) -(* ((j, (context, binding1, ty'))::subst, *) -(* List.filter (fun (m, _, _) -> j <> m) menv) *) -(* else *) -(* if binding2 != t then *) -(* if s = binding2 then *) -(* subst, menv *) -(* else *) -(* ((i, (context, binding2, ty))::subst, *) -(* List.filter (fun (m, _, _) -> i <> m) menv) *) -(* else *) -(* ((i, (context, t, ty))::subst, *) -(* List.filter (fun (m, _, _) -> i <> m) menv) *) -(* in *) -(* subst, menv *) - | C.Meta (i, l), t -> let _, _, ty = CicUtil.lookup_meta i menv in let subst = @@ -532,19 +496,6 @@ let unification_simple metasenv context t1 t2 ugraph = | _, _ -> raise (U.UnificationFailure "Inference.unification.unif") in let subst, menv = unif [] metasenv t1 t2 in - (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *) - (* print_newline (); *) -(* let rec fix_term = function *) -(* | (C.Meta (i, l) as t) -> *) -(* lookup t subst *) -(* | C.Appl l -> C.Appl (List.map fix_term l) *) -(* | t -> t *) -(* in *) -(* let rec fix_subst = function *) -(* | [] -> [] *) -(* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *) -(* in *) -(* List.rev (fix_subst subst), menv, ugraph *) List.rev subst, menv, ugraph ;; @@ -668,6 +619,8 @@ let matching metasenv context t1 t2 ugraph = (* (\* print_newline (); *\) *) (* subst, menv, ug *) (* else *) +(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *) +(* print_newline (); *) try let subst, metasenv, ugraph = (* CicUnification.fo_unif metasenv context t1 t2 ugraph *) @@ -693,6 +646,7 @@ let matching metasenv context t1 t2 ugraph = with e -> (* Printf.printf "failed to match %s %s\n" *) (* (CicPp.ppterm t1) (CicPp.ppterm t2); *) +(* print_endline (Printexc.to_string e); *) raise MatchingFailure ;; @@ -1085,7 +1039,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = C.Appl ((C.Rel index)::args) in ( match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when UriManager.eq uri eq_uri -> Printf.printf "OK: %s\n" (CicPp.ppterm term); let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in @@ -1094,7 +1049,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = Some e, (newmeta+1) | _ -> None, newmeta ) - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when UriManager.eq uri eq_uri -> let t1 = S.lift index t1 and t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 in @@ -1117,22 +1073,41 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = +let equations_blacklist = + List.fold_left + (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s) + UriManager.UriSet.empty [ + "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; + "cic:/Coq/Init/Logic/trans_eq.con"; + "cic:/Coq/Init/Logic/f_equal.con"; + "cic:/Coq/Init/Logic/f_equal2.con"; + "cic:/Coq/Init/Logic/f_equal3.con"; + "cic:/Coq/Init/Logic/sym_eq.con" + ] +;; + +let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in let candidates = - List.map - (fun uri -> - let t = CicUtil.term_of_uri uri in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - t, ty) + List.fold_left + (fun l uri -> + if UriManager.UriSet.mem uri equations_blacklist then + l + else + let t = CicUtil.term_of_uri uri in + let ty, _ = + CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph + in + (t, ty)::l) + [] (MetadataQuery.equations_for_goal ~dbd status) in let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in let iseq uri = - uri == eq_uri1 || uri == eq_uri2 + (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) in let rec aux newmeta = function | [] -> [], newmeta @@ -1141,7 +1116,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = match termty with | C.Prod (name, s, t) -> let head, newmetas, args, newmeta = - ProofEngineHelpers.saturate_term newmeta [] [] termty + ProofEngineHelpers.saturate_term newmeta [] context termty in let p = if List.length args = 0 then @@ -1277,10 +1252,20 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = ;; +let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term = + let iseq uri = UriManager.eq uri eq_uri in + match term with + | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true + | _ -> false +;; + + exception TermIsNotAnEquality;; -let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function - | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> +let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term = + let iseq uri = UriManager.eq uri eq_uri in + match term with + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 0695fbc9e..b7a10fe34 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -66,6 +66,8 @@ exception TermIsNotAnEquality;; val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> equality +val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool + (** superposition_left env target source returns a list of new clauses inferred with a left superposition step @@ -103,4 +105,5 @@ val extract_differing_subterms: val build_proof_term: equality -> Cic.term val find_library_equalities: - dbd:Mysql.dbd -> ProofEngineTypes.status -> int -> equality list * int + dbd:Mysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + equality list * int diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 94f26a7e6..ec7634d94 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -2,6 +2,14 @@ open Inference;; open Utils;; +(* set to false to disable paramodulation inside auto_tac *) +let connect_to_auto = true;; + +let debug = true;; + +let debug_print = if debug then prerr_endline else ignore;; + + (* profiling statistics... *) let infer_time = ref 0.;; let forward_simpl_time = ref 0.;; @@ -277,7 +285,7 @@ let prune_passive howmany (active, _) passive = and ratio = float_of_int !weight_age_ratio in let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.)) and in_age = int_of_float (howmany /. (ratio +. 1.)) in - Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age; + debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age); let symbols, card = match active with | (Negative, e)::_ -> @@ -732,12 +740,13 @@ let rec given_clause env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate); prune_passive selection_estimate active passive ) else passive @@ -761,15 +770,14 @@ let rec given_clause env passive active = given_clause env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); + debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current)); Success (Some current, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print "\n================================================"; + debug_print (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -867,12 +875,13 @@ let rec given_clause_fullred env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate); prune_passive selection_estimate active passive ) else passive @@ -896,15 +905,14 @@ let rec given_clause_fullred env passive active = given_clause_fullred env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); + debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current)); Success (Some current, env) ) else ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + debug_print "\n================================================"; + debug_print (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env sign current active in @@ -945,31 +953,31 @@ let rec given_clause_fullred env passive active = if k < (kept - 1) then processed_clauses := !processed_clauses + (kept - 1 - k); -(* let _ = *) -(* Printf.printf "active:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) -(* (string_of_equality ~env e)) (fst active)))); *) -(* print_newline (); *) -(* in *) -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new':\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) neg) @ *) -(* (List.map *) -(* (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) pos))); *) -(* print_newline (); *) -(* in *) + let _ = + debug_print ( + Printf.sprintf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) (fst active))))) + in + let _ = + match new' with + | neg, pos -> + debug_print ( + Printf.sprintf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos)))) + in match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in +(* let (_, ns), (_, ps), _ = passive in *) (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -986,31 +994,14 @@ let rec given_clause_fullred env passive active = ;; -let get_from_user ~(dbd:Mysql.dbd) = - let rec get () = - match read_line () with - | "" -> [] - | t -> t::(get ()) - in - let term_string = String.concat "\n" (get ()) in - let env, metasenv, term, ugraph = - List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 - in - term, metasenv, ugraph -;; - - let given_clause_ref = ref given_clause;; -let main () = +let main dbd term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in - let dbd = Mysql.quick_connect - ~host:"localhost" ~user:"helm" ~database:"mowgli" () in - let term, metasenv, ugraph = get_from_user ~dbd in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in let proof, goals = status in @@ -1019,7 +1010,8 @@ let main () = let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in let library_equalities, maxm = - find_library_equalities ~dbd (proof, goal') (maxm+1) in + find_library_equalities ~dbd context (proof, goal') (maxm+1) + in maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = @@ -1036,7 +1028,9 @@ let main () = let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in let active = make_active () in - let passive = make_passive [term_equality] equalities in + let passive = + make_passive [term_equality] (equalities @ library_equalities) + in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -1060,16 +1054,7 @@ let main () = | Failure -> Printf.printf "NO proof found! :-(\n\n" | Success (Some goal, env) -> - Printf.printf "OK, found a proof!\n"; let proof = Inference.build_proof_term goal in - (* REMEMBER: we have to instantiate meta_proof, we should use - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); -(* print_endline (PP.ppterm proof); *) - - print_endline (string_of_float (finish -. start)); let newmetasenv = List.fold_left (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities @@ -1079,12 +1064,23 @@ let main () = let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in + Printf.printf "OK, found a proof!\n"; + (* REMEMBER: we have to instantiate meta_proof, we should use + apply the "apply" tactic to proof and status + *) + let names = names_of_context context in + print_endline (PP.pp proof names); + (* print_endline (PP.ppterm proof); *) + + print_endline (string_of_float (finish -. start)); Printf.printf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" (CicPp.pp type_of_goal names) (CicPp.pp ty names) (string_of_bool - (fst (CicReduction.are_convertible context type_of_goal ty ug))); + (fst (CicReduction.are_convertible + context type_of_goal ty ug))); with e -> + Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; in () @@ -1115,109 +1111,109 @@ let main () = ;; -let saturation_tactic status = +exception Failure of string + +let saturate dbd (proof, goal) = let module C = Cic in - let saturation_tac (proof, goal) = - maxmeta := 0; -(* if List.length goals <> 1 then *) -(* raise (ProofEngineTypes.Fail "There should be only one open goal"); *) - -(* let goal' = List.hd goals in *) - let goal' = goal in - let uri, metasenv, meta_proof, term_to_prove = proof in - let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let equalities, maxm = find_equalities context proof in - maxmeta := maxm+2; - let new_meta_goal, metasenv, type_of_goal = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let _, context, ty = CicUtil.lookup_meta goal' metasenv in - Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); - print_newline (); - Cic.Meta (maxm+1, irl), - (maxm+1, context, ty)::metasenv, - ty + maxmeta := 0; + let goal' = goal in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let equalities, maxm = find_equalities context proof in + let library_equalities, maxm = + find_library_equalities ~dbd context (proof, goal') (maxm+2) + in + maxmeta := maxm+2; + let new_meta_goal, metasenv, type_of_goal = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in +(* try *) + let term_equality = equality_of_term new_meta_goal goal in + let active = make_active () in + let passive = + make_passive [term_equality] (equalities @ library_equalities) in - let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in - try - let term_equality = equality_of_term new_meta_goal goal in -(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) - let active = make_active () in - let passive = make_passive [term_equality] equalities in - let res = given_clause_fullred env passive active in - match res with - | Success (Some goal, env) -> - Printf.printf "OK, found a proof!\n"; - let proof = Inference.build_proof_term goal in - let names = names_of_context context in - print_endline (CicPp.pp proof names); - let newmetasenv = - let i1 = - match new_meta_goal with - | C.Meta (i, _) -> i | _ -> assert false + let res = given_clause_fullred env passive active in + match res with + | Success (Some goal, env) -> + debug_print "OK, found a proof!"; + let proof = Inference.build_proof_term goal in + let names = names_of_context context in + let newmetasenv = + let i1 = + match new_meta_goal with + | C.Meta (i, _) -> i | _ -> assert false + in +(* let i2 = *) +(* match meta_proof with *) +(* | C.Meta (i, _) -> i *) +(* | t -> *) +(* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *) +(* (CicPp.pp meta_proof names) (string_of_int goal'); *) +(* print_newline (); *) +(* assert false *) +(* in *) + List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv + in + let newstatus = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in - let i2 = - match meta_proof with - | C.Meta (i, _) -> i | _ -> assert false + debug_print (CicPp.pp proof [](* names *)); + debug_print + (Printf.sprintf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug)))); + let equality_for_replace t1 i = + match t1 with + | C.Meta (n, _) -> n = i + | _ -> false in - List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv - in - let newstatus = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph - in - Printf.printf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))); - ((uri, newmetasenv, proof, term_to_prove), []) - with e -> - raise (ProofEngineTypes.Fail - "Found a proof, but it doesn't typecheck") - in - newstatus - | _ -> - raise (ProofEngineTypes.Fail "NO proof found") - with e -> - raise (ProofEngineTypes.Fail "saturation failed") - in - ProofEngineTypes.mk_tactic saturation_tac + let real_proof = + ProofEngineReduction.replace + ~equality:equality_for_replace + ~what:[goal'] ~with_what:[proof] + ~where:meta_proof + in + debug_print ( + Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" + (match uri with Some uri -> UriManager.string_of_uri uri + | None -> "") + (print_metasenv newmetasenv) + (CicPp.pp real_proof [](* names *)) + (CicPp.pp term_to_prove names)); + ((uri, newmetasenv, real_proof, term_to_prove), []) + with e -> + debug_print "THE PROOF DOESN'T TYPECHECK!!!"; + debug_print (CicPp.pp proof names); + raise (Failure "Found a proof, but it doesn't typecheck") + in + newstatus + | _ -> + raise (Failure "NO proof found") +(* with e -> *) +(* raise (Failure "saturation failed") *) ;; +(* dummy function called within matita to trigger linkage *) +let init () = ();; -let configuration_file = ref "../../matita/matita.conf.xml";; - -let _ = - let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) - and set_sel v = symbols_ratio := v; symbols_counter := v; - and set_conf f = configuration_file := f - and set_lpo () = Utils.compare_terms := lpo - and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred b = use_fullred := b - and set_time_limit v = time_limit := float_of_int v - in - Arg.parse [ - "-f", Arg.Bool set_fullred, - "Enable/disable full-reduction strategy (default: enabled)"; - - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; - - "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio, default: 2)"; - - "-c", Arg.String set_conf, "Configuration file (for the db connection)"; - - "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; - - "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; - "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; - ] (fun a -> ()) "Usage:" -in -Helm_registry.load_from !configuration_file; -main () +(* UGLY SIDE EFFECT... *) +if connect_to_auto then ( + AutoTactic.paramodulation_tactic := saturate; + AutoTactic.term_is_equality := Inference.term_is_equality; +);;