H=@
-BINARIES=extractor table_creator utilities
+BINARIES=extractor table_creator utilities saturate
all: $(BINARIES:%=rec@all@%)
opt: $(BINARIES:%=rec@opt@%)
--- /dev/null
+H=@
+
+REQUIRES = helm-grafite_parser helm-tactics
+
+INTERFACE_FILES =
+IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN = \
+ saturate saturate.opt
+
+all: saturate
+ $(H)echo -n
+opt: saturate.opt
+ $(H)echo -n
+
+saturate: saturate_main.ml
+ $(H)echo " OCAMLC $<"
+ $(H)$(OCAMLFIND) ocamlc \
+ -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
+
+saturate.opt: saturate_main.ml
+ $(H)echo " OCAMLOPT $<"
+ $(H)$(OCAMLFIND) ocamlopt \
+ -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
+
+clean:
+ $(H)rm -f *.cm[iox] *.a *.o
+ $(H)rm -f saturate saturate.opt
+
+include ../../../Makefile.defs
--- /dev/null
+(* 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$ *)
+
+module Trivial_disambiguate:
+sig
+ exception Ambiguous_term of string Lazy.t
+ (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
+ * choice from the user is needed to disambiguate the term
+ * @raise Ambiguous_term for ambiguous term *)
+ val disambiguate_string:
+ dbd:HMysql.dbd ->
+ ?context:Cic.context ->
+ ?metasenv:Cic.metasenv ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*)
+ string ->
+ ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Cic.metasenv * (* new metasenv *)
+ Cic.term *
+ CicUniv.universe_graph) list (* disambiguated term *)
+end
+=
+struct
+ exception Ambiguous_term of string Lazy.t
+ exception Exit
+ module Callbacks =
+ struct
+ let non p x = not (p x)
+ let interactive_user_uri_choice ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
+ List.filter (non UriManager.uri_is_var) uris
+ let interactive_interpretation_choice interp = raise Exit
+ let input_or_locate_uri ~(title:string) ?id = raise Exit
+ end
+ module Disambiguator = Disambiguate.Make (Callbacks)
+ let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
+ ?(aliases = DisambiguateTypes.Environment.empty) term
+ =
+ let ast =
+ CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
+ in
+ try
+ fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+ ?initial_ugraph ~aliases ~universe:None)
+ with Exit -> raise (Ambiguous_term (lazy term))
+end
+
+let configuration_file = ref "../../../matita/matita.conf.xml";;
+
+let core_notation_script = "../../../matita/core_notation.moo";;
+
+let get_from_user ~(dbd:HMysql.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 (Trivial_disambiguate.disambiguate_string dbd term_string) 0
+ in
+ term, metasenv, ugraph
+;;
+
+let full = ref false;;
+
+let retrieve_only = ref false;;
+
+let demod_equalities = ref false;;
+
+let main () =
+ let module S = Saturation in
+ let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
+ and set_sel v = S.symbols_ratio := v; S.symbols_counter := v;
+ and set_conf f = configuration_file := f
+ and set_ordering o =
+ match o with
+ | "lpo" -> Utils.compare_terms := Utils.lpo
+ | "kbo" -> Utils.compare_terms := Utils.kbo
+ | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
+ | "ao" -> Utils.compare_terms := Utils.ao
+ | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
+ and set_fullred b = S.use_fullred := b
+ and set_time_limit v = S.time_limit := float_of_int v
+ and set_width w = S.maxwidth := w
+ and set_depth d = S.maxdepth := d
+ and set_full () = full := true
+ and set_retrieve () = retrieve_only := true
+ and set_demod_equalities () = demod_equalities := true
+ in
+ Arg.parse [
+ "-full", Arg.Unit set_full, "Enable full mode";
+ "-f", Arg.Bool set_fullred,
+ "Enable/disable full-reduction strategy (default: enabled)";
+
+ "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 4)";
+
+ "-s", Arg.Int set_sel,
+ "symbols-based selection ratio (relative to the weight ratio, default: 0)";
+
+ "-c", Arg.String set_conf, "Configuration file (for the db connection)";
+
+ "-o", Arg.String set_ordering,
+ "Term ordering. Possible values are:\n" ^
+ "\tkbo: Knuth-Bendix ordering\n" ^
+ "\tnr-kbo: Non-recursive variant of kbo (default)\n" ^
+ "\tlpo: Lexicographic path ordering";
+
+ "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)";
+
+ "-w", Arg.Int set_width,
+ Printf.sprintf "Maximal width (default: %d)" !Saturation.maxwidth;
+
+ "-d", Arg.Int set_depth,
+ Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth;
+
+ "-retrieve", Arg.Unit set_retrieve, "retrieve only";
+ "-demod-equalities", Arg.Unit set_demod_equalities, "demod equalities";
+ ] (fun a -> ()) "Usage:";
+ Helm_registry.load_from !configuration_file;
+ ignore (CicNotation2.load_notation [] core_notation_script);
+ ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
+ let dbd = HMysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user")
+ ~database:(Helm_registry.get "db.database")
+ ()
+ in
+ let term, metasenv, ugraph = get_from_user ~dbd in
+ if !retrieve_only then
+ Saturation.retrieve_and_print dbd term metasenv ugraph
+ else if !demod_equalities then
+ Saturation.main_demod_equalities dbd term metasenv ugraph
+ else
+ Saturation.main dbd !full term metasenv ugraph
+;;
+
+let _ =
+ (*try*)
+ main ()
+ (*with exn -> prerr_endline (Printexc.to_string exn)*)
+
| C.Var (uri,exp_named_subst) ->
UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
| C.Meta (n,l1) ->
- "?" ^ (string_of_int n) ^ "[" ^
+ "?" ^ (string_of_int n) (* ^ "[" ^
String.concat " ; "
(List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
- "]"
+ "]" *)
| C.Sort s ->
(match s with
C.Prop -> "Prop"
| Cic.Implicit _ -> string_name
| Cic.Cast (te,ty) -> check_rec ctx string_name te
| Cic.Prod (name,so,dest) ->
- let l_string_name = check_rec ctx string_name so in
+ let _l_string_name = check_rec ctx string_name so in
check_rec (name::ctx) string_name dest
| Cic.Lambda (name,so,dest) ->
let string_name =
| _ -> assert false) in
remove_prefix name string_name
| Cic.MutCase (_,_,_,te,pl) ->
- let strig_name = remove_prefix "match" string_name in
+ let _strig_name = remove_prefix "match" string_name in
let string_name = check_rec ctx string_name te in
List.fold_right (fun t s -> check_rec ctx s t) pl string_name
| Cic.Fix (_,fl) ->
- let strig_name = remove_prefix "fix" string_name in
+ let _strig_name = remove_prefix "fix" string_name in
let names = List.map (fun (name,_,_,_) -> name) fl in
let onames =
List.rev (List.map (function name -> Cic.Name name) names)
List.fold_right
(fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
| Cic.CoFix (_,fl) ->
- let strig_name = remove_prefix "cofix" string_name in
+ let _strig_name = remove_prefix "cofix" string_name in
let names = List.map (fun (name,_,_) -> name) fl in
let onames =
List.rev (List.map (function name -> Cic.Name name) names)
(** wrappers which instantiate fresh loggers *)
+let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
+
let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
- type_of_aux' ~logger ~subst metasenv context t ugraph
+ profiler.HExtlib.profile
+ (type_of_aux' ~logger ~subst metasenv context t) ugraph
let typecheck_obj uri obj =
let logger = new CicLogger.logger in
apply_subst_gen ~appl_fun s t
;;
+let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
+let apply_subst s t =
+ profiler.HExtlib.profile (apply_subst s) t
+
+
let rec apply_subst_context subst context =
(*
incr apply_subst_context_counter;
let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
let type_of_aux' metasenv subst context term ugraph =
let foo () =
try
- CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
+ profile.HExtlib.profile
+ (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
with
CicTypeChecker.TypeCheckerFailure msg ->
let msg =
with
WrongShape -> after_beta_expansion
+let unif_ty = ref true
+
let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
let module S = CicSubstitution in
let module C = Cic in
(lower m1 m2) (upper m1 m2) ugraph
in
begin
- let subst,metasenv,ugraph1 =
+ let subst,metasenv,ugraph1 =
+ if not (!unif_ty) then subst,metasenv,ugraph else
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
let tyt,ugraph1 =
Cic.term -> Cic.term -> CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+ val unif_ty : bool ref
let _ =
if !something_profiled then
at_exit
- (fun _ -> prerr_endline
- (Printf.sprintf "!! %-39s %6s %9s %9s %9s"
- "function" "#calls" "total" "max" "average"))
+ (fun _ ->
+ prerr_endline
+ (Printf.sprintf "!! %39s ---------- --------- --------- ---------"
+ (String.make 39 '-'));
+ prerr_endline
+ (Printf.sprintf "!! %-39s %10s %9s %9s %9s"
+ "function" "#calls" "total" "max" "average"))
let profiling_printings = ref (fun _ -> true)
let set_profiling_printings f = profiling_printings := f
in
at_exit
(fun () ->
- if !profiling_printings s && !total <> 0. then
+ if !profiling_printings s && !calls <> 0 then
begin
something_profiled := true;
prerr_endline
- (Printf.sprintf "!! %-39s %6d %9.4f %9.4f %9.4f"
+ (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f"
s !calls !total !max (!total /. (float_of_int !calls)))
end);
{ profile = profile }
status.LexiconEngine.aliases []
let alias_diff =
- let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in
fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
(** given a uri and a type list (the contructors types) builds a list of pairs
(List.map
(fun t -> (
match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
- (term,graph) -> term
- |_ -> assert false))
+ (term,graph) -> term))
parameters)
in
let consno = List.length cons_list in
Cic.Sort(Cic.Prop))
else
Cic.Sort Cic.Prop
- | _ -> assert false
;;
(* created vars is empty at the beginning *)
-PACKAGE = dummy
-
-LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser,helm-tactics
-
-include ../../../Makefile.defs
-include ../../Makefile.common
-
-all $(PACKAGE).cma :saturate
- @echo -n
-opt $(PACKAGE).cmxa:saturate.opt
- @echo -n
-
-saturate: saturate_main.ml $(LIBRARIES)
- @echo " OCAMLC $<"
- @$(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
-saturate.opt: saturate_main.ml $(LIBRARIES)
- @echo " OCAMLOPT $<"
- @$(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
-
-clean:
- rm -f saturate saturate.opt
+all:
+ @make -C .. $@
+%:
+ @make -C .. $@
CicTypeChecker.type_of_aux' metasenv' context right ugraph;
()
with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline msg;
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
+ CicUtil.Meta_not_found _ as exn ->
+ begin
+ prerr_endline msg;
+ prerr_endline (CicPp.ppterm left);
+ prerr_endline (CicPp.ppterm right);
+ raise exn
+ end
*)
type retrieval_mode = Matching | Unification;;
function
None -> "None"
| Some (t, s, m, u, ((p,e), eq_URI)) ->
- Printf.sprintf "Some: (%s, %s, %s)"
- (Utils.string_of_pos p)
- (Inference.string_of_equality ?env e)
- (CicPp.ppterm t)
+ Printf.sprintf "Some: (%s, %s, %s)"
+ (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e)
+ (CicPp.ppterm t)
;;
let print_res ?env res =
prerr_endline
(String.concat "\n"
(List.map
- (fun (p, e) ->
- Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality ?env e))
- res));
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e))
+ res));
;;
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
let check_res res msg =
match res with
Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
- let eqs = Inference.string_of_equality (snd eq_found) in
- check_disjoint_invariant subst menv msg;
- check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
+ let eqs = Inference.string_of_equality (snd eq_found) in
+ check_disjoint_invariant subst menv msg;
+ check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
;;
else () in
try
CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+ metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
with e ->
prerr_endline msg;
prerr_endline (Inference.string_of_proof proof);
res
;;
+let profiler = HExtlib.profile "P/Indexing.get_candidates"
+
+let get_candidates ?env mode tree term =
+ profiler.HExtlib.profile (get_candidates ?env mode tree) term
let match_unif_time_ok = ref 0.;;
let match_unif_time_no = ref 0.;;
| candidate::tl ->
let pos, (_, proof, (ty, left, right, o), metas) = candidate in
if Utils.debug_metas then
- ignore(check_target context (snd candidate) "find_matches");
+ ignore(check_target context (snd candidate) "find_matches");
if Utils.debug_res then
- begin
- let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
- let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
+ begin
+ let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
+ let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
- check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
- end;
+ check_for_duplicates metas "gia nella metas";
+ check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+ end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
find_matches metasenv context ugraph lift_amount term termty tl
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
with
- | Inference.MatchingFailure as e ->
+ | Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
- | CicUtil.Meta_not_found _ as exn -> raise exn
+ | CicUtil.Meta_not_found _ as exn -> raise exn
in
Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
in
if o <> U.Incomparable then
let res =
- try
- do_match c eq_URI
+ try
+ do_match c eq_URI
with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
- in
- if Utils.debug_res then ignore (check_res res "find1");
- res
+ find_matches metasenv context ugraph lift_amount term termty tl
+ in
+ if Utils.debug_res then ignore (check_res res "find1");
+ res
else
let res =
try do_match c eq_URI
find_matches metasenv context ugraph lift_amount term termty tl
;;
-
(*
as above, but finds all the matching equalities, and the matching condition
can be either Inference.matching or Inference.unification
lift_amount term termty tl
;;
+let find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+=
+ let rc =
+ find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+ in
+ (*prerr_endline "CANDIDATES:";
+ List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+ prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
+ (List.length rc));*)
+ rc
(*
returns true if target is subsumed by some equality in table
try
let r =
Inference.matching menv m context what other ugraph
- in
+ in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
true, subst
else
let rightr =
- match right with
- | Cic.Meta _ -> []
- | _ ->
+ match right with
+ | Cic.Meta _ -> []
+ | _ ->
let rightc = get_candidates Matching table right in
- find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 right ty rightc
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 right ty rightc
in
- ok left rightr
+ ok left rightr
in
(* (if r then *)
(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
-(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
+(* (lazy *)
+(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
+(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
r, s
;;
match term with
| C.Meta _ -> None
| term ->
- let termty, ugraph =
+ let termty, ugraph =
if typecheck then
CicTypeChecker.type_of_aux' metasenv context term ugraph
else
C.Implicit None, ugraph
- in
- let res =
+ in
+ let res =
find_matches metasenv context ugraph lift_amount term termty candidates
- in
+ in
if Utils.debug_res then ignore(check_res res "demod1");
- if res <> None then
+ if res <> None then
res
- else
+ else
match term with
- | C.Appl l ->
- let res, ll =
- List.fold_left
- (fun (res, tl) t ->
- if res <> None then
- (res, tl @ [S.lift 1 t])
- else
- let r =
- demodulation_aux ~from:"1" metasenv context ugraph table
- lift_amount t
- in
- match r with
- | None -> (None, tl @ [S.lift 1 t])
- | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
- (None, []) l
- in (
- match res with
- | None -> None
- | Some (_, subst, menv, ug, eq_found) ->
- Some (C.Appl ll, subst, menv, ug, eq_found)
- )
- | C.Prod (nn, s, t) ->
- let r1 =
- demodulation_aux ~from:"2"
- metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | C.Lambda (nn, s, t) ->
- let r1 =
- demodulation_aux
- metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | t ->
- None
+ | C.Appl l ->
+ let res, ll =
+ List.fold_left
+ (fun (res, tl) t ->
+ if res <> None then
+ (res, tl @ [S.lift 1 t])
+ else
+ let r =
+ demodulation_aux ~from:"1" metasenv context ugraph table
+ lift_amount t
+ in
+ match r with
+ | None -> (None, tl @ [S.lift 1 t])
+ | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
+ (None, []) l
+ in (
+ match res with
+ | None -> None
+ | Some (_, subst, menv, ug, eq_found) ->
+ Some (C.Appl ll, subst, menv, ug, eq_found)
+ )
+ | C.Prod (nn, s, t) ->
+ let r1 =
+ demodulation_aux ~from:"2"
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | C.Lambda (nn, s, t) ->
+ let r1 =
+ demodulation_aux
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | t ->
+ None
in
if Utils.debug_res then ignore(check_res res "demod_aux output");
res
exception Foo
+let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
+
(** demodulation, when target is an equality *)
let rec demodulation_equality ?from newmeta env table sign target =
let module C = Cic in
if Utils.debug_metas then
begin
ignore(check_for_duplicates menv "input1");
- ignore(check_disjoint_invariant subst menv "input2");
+ ignore(check_disjoint_invariant subst menv "input2");
let substs = CicMetaSubst.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
let ty =
let newmenv = (* Inference.filter subst *) menv in
let _ =
if Utils.debug_metas then
- try ignore(CicTypeChecker.type_of_aux'
+ try ignore(CicTypeChecker.type_of_aux'
newmenv context (Inference.build_proof_term newproof) ugraph);
- ()
- with exc ->
+ ()
+ with exc ->
prerr_endline "sempre lui";
prerr_endline (CicMetaSubst.ppsubst subst);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+ prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
- raise exc;
+ raise exc;
else ()
in
let left, right = if is_left then newterm, right else left, newterm in
ignore(check_target context res "buildnew_target output");
!maxmeta, res
in
+ let build_newtarget is_left x =
+ profiler.HExtlib.profile (build_newtarget is_left) x
+ in
let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
| Some t ->
- let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
+ let newmeta, newtarget = build_newtarget true t in
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
+ newmeta, newtarget
+ else
demodulation_equality newmeta env table sign newtarget
| None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
- if Utils.debug_res then check_res res "demod result 1";
- match res with
- | Some t ->
- let newmeta, newtarget = build_newtarget false t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
- demodulation_equality newmeta env table sign newtarget
- | None ->
- newmeta, target
+ let res = demodulation_aux metasenv' context ugraph table 0 right in
+ if Utils.debug_res then check_res res "demod result 1";
+ match res with
+ | Some t ->
+ let newmeta, newtarget = build_newtarget false t in
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
+ (Inference.meta_convertibility_eq target newtarget) then
+ newmeta, newtarget
+ else
+ demodulation_equality newmeta env table sign newtarget
+ | None ->
+ newmeta, target
in
(* newmeta, newtarget *)
newmeta,newtarget
;;
-
(**
Performs the beta expansion of the term "term" w.r.t. "table",
i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
r @ res, lifted_term
;;
+let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
+
+let betaexpand_term metasenv context ugraph table lift_amount term =
+ profiler.HExtlib.profile
+ (betaexpand_term metasenv context ugraph table lift_amount) term
+
let sup_l_counter = ref 1;;
let expansions, _ =
let term = if ordering = U.Gt then left else right in
begin
- let t1 = Unix.gettimeofday () in
- let res = betaexpand_term metasenv context ugraph table 0 term in
- let t2 = Unix.gettimeofday () in
- beta_expand_time := !beta_expand_time +. (t2 -. t1);
- res
+ let t1 = Unix.gettimeofday () in
+ let res = betaexpand_term metasenv context ugraph table 0 term in
+ let t2 = Unix.gettimeofday () in
+ beta_expand_time := !beta_expand_time +. (t2 -. t1);
+ res
end
in
let maxmeta = ref newmeta in
in
(res left right), (res right left)
in
- let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
+ let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
if Utils.debug_metas then
ignore (check_target context (snd eq_found) "buildnew1" );
let time1 = Unix.gettimeofday () in
let w = Utils.compute_equality_weight stat in
(w, newproof, stat, newmenv) in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew3");
+ ignore (check_target context eq' "buildnew3");
let newm, eq' = Inference.fix_metas !maxmeta eq' in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew4");
+ ignore (check_target context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
newmeta, goal
;;
-
(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
(Inference.build_proof_term newproof, bo)
in
- let m = Inference.metas_of_term newterm in
+ (* let m = Inference.metas_of_term newterm in *)
!maxmeta, (newterm, newty, menv)
in
let res =
List.rev subst, menv, ugraph
;;
-let profiler = HExtlib.profile "flatten"
+let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
+let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
+let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
+let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
let metasenv = metasenv1 @ metasenv2 in
let ty = CicMetaSubst.apply_subst subst ty in
(i, (context, term, ty))) subst
in
- let flatten subst = profiler.HExtlib.profile flatten subst in
- let subst = flatten subst in
+ let flatten_fast subst =
+ let resolve_meta (i, (context, term, ty)) subst =
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))
+ in
+ let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
+ let filter j (i,_) = i <> j in
+ let filter a b = profiler4.HExtlib.profile (filter a) b in
+ List.fold_left
+ (fun subst (j,(c,t,ty)) as s ->
+ let s = resolve_meta s subst in
+ s::(List.filter (filter j) subst))
+ subst subst
+ in
+ (*let flatten subst = profiler.HExtlib.profile flatten subst in*)
+ let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
+ (*let subst = flatten subst in*)
+(* let subst = flatten_fast subst in*)
subst, menv, ug
;;
+++ /dev/null
-(* 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$ *)
-
-module Trivial_disambiguate:
-sig
- exception Ambiguous_term of string Lazy.t
- (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
- * choice from the user is needed to disambiguate the term
- * @raise Ambiguous_term for ambiguous term *)
- val disambiguate_string:
- dbd:HMysql.dbd ->
- ?context:Cic.context ->
- ?metasenv:Cic.metasenv ->
- ?initial_ugraph:CicUniv.universe_graph ->
- ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*)
- string ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Cic.metasenv * (* new metasenv *)
- Cic.term *
- CicUniv.universe_graph) list (* disambiguated term *)
-end
-=
-struct
- exception Ambiguous_term of string Lazy.t
- exception Exit
- module Callbacks =
- struct
- let non p x = not (p x)
- let interactive_user_uri_choice ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- List.filter (non UriManager.uri_is_var) uris
- let interactive_interpretation_choice interp = raise Exit
- let input_or_locate_uri ~(title:string) ?id = raise Exit
- end
- module Disambiguator = Disambiguate.Make (Callbacks)
- let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
- ?(aliases = DisambiguateTypes.Environment.empty) term
- =
- let ast =
- CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
- in
- try
- fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
- ?initial_ugraph ~aliases ~universe:None)
- with Exit -> raise (Ambiguous_term (lazy term))
-end
-
-let configuration_file = ref "../../../matita/matita.conf.xml";;
-
-let core_notation_script = "../../../matita/core_notation.moo";;
-
-let get_from_user ~(dbd:HMysql.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 (Trivial_disambiguate.disambiguate_string dbd term_string) 0
- in
- term, metasenv, ugraph
-;;
-
-let full = ref false;;
-
-let retrieve_only = ref false;;
-
-let demod_equalities = ref false;;
-
-let main () =
- let module S = Saturation in
- let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
- and set_sel v = S.symbols_ratio := v; S.symbols_counter := v;
- and set_conf f = configuration_file := f
- and set_ordering o =
- match o with
- | "lpo" -> Utils.compare_terms := Utils.lpo
- | "kbo" -> Utils.compare_terms := Utils.kbo
- | "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
- | "ao" -> Utils.compare_terms := Utils.ao
- | o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
- and set_fullred b = S.use_fullred := b
- and set_time_limit v = S.time_limit := float_of_int v
- and set_width w = S.maxwidth := w
- and set_depth d = S.maxdepth := d
- and set_full () = full := true
- and set_retrieve () = retrieve_only := true
- and set_demod_equalities () = demod_equalities := true
- in
- Arg.parse [
- "-full", Arg.Unit set_full, "Enable full mode";
- "-f", Arg.Bool set_fullred,
- "Enable/disable full-reduction strategy (default: enabled)";
-
- "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 4)";
-
- "-s", Arg.Int set_sel,
- "symbols-based selection ratio (relative to the weight ratio, default: 0)";
-
- "-c", Arg.String set_conf, "Configuration file (for the db connection)";
-
- "-o", Arg.String set_ordering,
- "Term ordering. Possible values are:\n" ^
- "\tkbo: Knuth-Bendix ordering\n" ^
- "\tnr-kbo: Non-recursive variant of kbo (default)\n" ^
- "\tlpo: Lexicographic path ordering";
-
- "-l", Arg.Int set_time_limit, "Time limit in seconds (default: no limit)";
-
- "-w", Arg.Int set_width,
- Printf.sprintf "Maximal width (default: %d)" !Saturation.maxwidth;
-
- "-d", Arg.Int set_depth,
- Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth;
-
- "-retrieve", Arg.Unit set_retrieve, "retrieve only";
- "-demod-equalities", Arg.Unit set_demod_equalities, "demod equalities";
- ] (fun a -> ()) "Usage:";
- Helm_registry.load_from !configuration_file;
- ignore (CicNotation2.load_notation [] core_notation_script);
- ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
- let dbd = HMysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database")
- ()
- in
- let term, metasenv, ugraph = get_from_user ~dbd in
- if !retrieve_only then
- Saturation.retrieve_and_print dbd term metasenv ugraph
- else if !demod_equalities then
- Saturation.main_demod_equalities dbd term metasenv ugraph
- else
- Saturation.main dbd !full term metasenv ugraph
-;;
-
-let _ =
- (*try*)
- main ()
- (*with exn -> prerr_endline (Printexc.to_string exn)*)
-
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
- let w,_,_,_ = hd in
let passive_table =
Indexing.remove_index passive_table hd
in (Positive, hd),
let res = demodulate active_table current in
if Utils.debug_metas then
ignore ((function None -> () | Some (_,x) ->
- Indexing.check_target context x "demod1";()) res);
+ ignore (Indexing.check_target context x "demod1");()) res);
match res with
| None -> None
| Some (sign, newcurrent) ->
;;
+
+
(** simplifies active usign new *)
let backward_simplify_active env new_pos new_table min_weight active =
let active_list, active_table = active in
(* (string_of_equality equality) (CicPp.ppterm gterm))); *)
try
let subst, metasenv', _ =
- let menv = metasenv @ metas @ gmetas in
+ (* let menv = metasenv @ metas @ gmetas in *)
Inference.unification metas gmetas context eqterm gterm ugraph
in
let newproof =
(* given-clause algorithm with lazy reduction strategy *)
let rec given_clause dbd env goals theorems passive active =
- let _,context,_ = env in
+ (* let _,context,_ = env in *)
let goals = simplify_goals env goals active in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems active in *)
)
;;
-
(** given-clause algorithm with full reduction strategy *)
let rec given_clause_fullred dbd env goals theorems passive active =
let goals = simplify_goals env goals ~passive active in
given_clause_fullred dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
- let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ (* let names =
+ List.map (HExtlib.map_option (fun (name,_) -> name)) context in *)
prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^
string_of_equality ~env current);
(* (CicPp.pp (Inference.term_of_equality current) names));*)
| None, Some (n, p) ->
let nn, np = new' in
if Utils.debug_metas then
- ignore (
- List.map (fun x -> Indexing.check_target context x "simplify1")n;
- List.map (fun x -> Indexing.check_target context x "simplify2")p);
+ (List.iter
+ (fun x -> ignore
+ (Indexing.check_target context x "simplify1"))
+ n;
+ List.iter
+ (fun x -> ignore
+ (Indexing.check_target context x "simplify2"))
+ p);
simplify (nn @ n, np @ p) active passive
| Some (n, p), Some (rn, rp) ->
let nn, np = new' in
in
ParamodulationSuccess (proof, env)
)
+
;;
+let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred"
+
+let given_clause_fullred dbd env goals theorems passive active =
+ profiler0.HExtlib.profile
+ (given_clause_fullred dbd env goals theorems passive) active
+
let rec saturate_equations env goal accept_fun passive active =
elapsed_time := Unix.gettimeofday () -. !start_time;
Indexing.init_index ();
maxdepth := depth;
maxwidth := width;
+(* CicUnification.unif_ty := false;*)
let proof, goal = status in
let goal' = goal in
let uri, metasenv, meta_proof, term_to_prove = proof in
\forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
intros.auto paramodulation.
qed.
-
+*)
theorem bool507:
\forall A:Set.
\forall one:A.
\forall x,y:A. zero = (mult x (mult (inv x) y)).
intros.auto paramodulation.
qed.
-
+(*
theorem bool515:
\forall A:Set.
\forall one:A.
\forall i2: (\forall x:A. (mult x one) = x).
\forall inv1: (\forall x:A. (add x (inv x)) = one).
\forall inv2: (\forall x:A. (mult x (inv x)) = zero).
- (*
- \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
- \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
- \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
- *)
\forall x,y:A.
inv x = (add (inv x) (inv (add y x))).
intros.auto paramodulation.
\forall i2: (\forall x:A. (mult x one) = x).
\forall inv1: (\forall x:A. (add x (inv x)) = one).
\forall inv2: (\forall x:A. (mult x (inv x)) = zero).
- (*
- \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
- \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
- \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
- *)
\forall x,y:A.
inv x = (add (inv (add y x)) (inv x)).
intros.auto paramodulation.
intros;
auto paramodulation.
qed.
-(* 46 sec. *)
theorem bool756:
\forall A:Set.
[auto paramodulation
|auto paramodulation]
qed.
-(* 186 sec *)
-*)
+
theorem bool756full:
\forall A:Set.
\forall one:A.
add x y = add x (add y (mult x z)).
intros;auto paramodulation.
qed.
-(* war=5; active 225, maxmeta 172568 *)
-(* war=4; active 249, maxmeta 223220 *)
-(*
+
theorem bool1164:
\forall A:Set.
\forall one:A.
\forall x,y,z:A.
add x (add y z) = add (add x z) y.
intros.auto paramodulation.
-qed.*)
+qed.
theorem bool381:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 90 *)
theorem bool5hint2:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 41 *)
theorem bool5hint3:
\forall A:Set.
(inv (mult x y)) = (add (inv x) (inv y)).
intros.auto paramodulation.
qed.
-(* 41 *)
theorem bool5:
\forall A:Set.
qed.
*)
+
projects / helm.git / commitdiff