paramodulation/subst.cmi
paramodulation/equality_retrieval.cmi: proofEngineTypes.cmi \
paramodulation/equality.cmi autoTypes.cmi autoCache.cmi
-paramodulation/inference.cmi: paramodulation/subst.cmi
+paramodulation/founif.cmi: paramodulation/subst.cmi
paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
paramodulation/equality.cmi
paramodulation/indexing.cmi: paramodulation/utils.cmi \
proofEngineTypes.cmx proofEngineHelpers.cmx metadataQuery.cmx \
paramodulation/equality.cmx autoTypes.cmx autoCache.cmx \
paramodulation/equality_retrieval.cmi
-paramodulation/inference.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi paramodulation/inference.cmi
-paramodulation/inference.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx paramodulation/inference.cmi
+paramodulation/founif.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \
+ paramodulation/founif.cmi
+paramodulation/founif.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \
+ paramodulation/founif.cmi
paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
paramodulation/equality.cmi paramodulation/equality_indexing.cmi
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
paramodulation/equality.cmx paramodulation/equality_indexing.cmi
paramodulation/indexing.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi paramodulation/inference.cmi \
+ paramodulation/subst.cmi paramodulation/founif.cmi \
paramodulation/equality_indexing.cmi paramodulation/equality.cmi \
paramodulation/indexing.cmi
paramodulation/indexing.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx paramodulation/inference.cmx \
+ paramodulation/subst.cmx paramodulation/founif.cmx \
paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
paramodulation/indexing.cmi
paramodulation/saturation.cmo: paramodulation/utils.cmi \
paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
- proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \
- paramodulation/indexing.cmi paramodulation/equality_retrieval.cmi \
+ proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/indexing.cmi \
+ paramodulation/founif.cmi paramodulation/equality_retrieval.cmi \
paramodulation/equality.cmi autoCache.cmi paramodulation/saturation.cmi
paramodulation/saturation.cmx: paramodulation/utils.cmx \
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
- proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \
- paramodulation/indexing.cmx paramodulation/equality_retrieval.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/indexing.cmx \
+ paramodulation/founif.cmx paramodulation/equality_retrieval.cmx \
paramodulation/equality.cmx autoCache.cmx paramodulation/saturation.cmi
variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
paramodulation/subst.mli\
paramodulation/equality.mli\
paramodulation/equality_retrieval.mli\
- paramodulation/inference.mli\
+ paramodulation/founif.mli\
paramodulation/equality_indexing.mli\
paramodulation/indexing.mli \
paramodulation/saturation.mli \
--- /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/.
+ *)
+
+(* let _profiler = <:profiler<_profiler>>;; *)
+
+(* $Id$ *)
+
+open Utils;;
+open Printf;;
+
+let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
+
+let check_disjoint_invariant subst metasenv msg =
+ if (List.exists
+ (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
+ then
+ begin
+ prerr_endline ("not disjoint: " ^ msg);
+ assert false
+ end
+;;
+
+let rec check_irl start = function
+ | [] -> true
+ | None::tl -> check_irl (start+1) tl
+ | (Some (Cic.Rel x))::tl ->
+ if x = start then check_irl (start+1) tl else false
+ | _ -> false
+;;
+
+let rec is_simple_term = function
+ | Cic.Appl ((Cic.Meta _)::_) -> false
+ | Cic.Appl l -> List.for_all is_simple_term l
+ | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
+ | Cic.Rel _ -> true
+ | Cic.Const _ -> true
+ | Cic.MutInd (_, _, []) -> true
+ | Cic.MutConstruct (_, _, _, []) -> true
+ | _ -> false
+;;
+
+let locked menv i =
+ List.exists (fun (j,_,_) -> i = j) menv
+;;
+
+let unification_simple locked_menv metasenv context t1 t2 ugraph =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup = Subst.lookup_subst in
+ let rec occurs_check subst what where =
+ match where with
+ | Cic.Meta(i,_) when i = what -> true
+ | C.Appl l -> List.exists (occurs_check subst what) l
+ | C.Meta _ ->
+ let t = lookup where subst in
+ if t <> where then occurs_check subst what t else false
+ | _ -> false
+ in
+ let rec unif subst menv s t =
+ let s = match s with C.Meta _ -> lookup s subst | _ -> s
+ and t = match t with C.Meta _ -> lookup t subst | _ -> t
+
+ in
+ match s, t with
+ | s, t when s = t -> subst, menv
+ (* sometimes the same meta has different local contexts; this
+ could create "cyclic" substitutions *)
+ | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv
+ | C.Meta (i, _), C.Meta (j, _)
+ when (locked locked_menv i) &&(locked locked_menv j) ->
+ raise
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
+ | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
+ unif subst menv t s
+ | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
+ unif subst menv t s
+ | C.Meta (i,_), t when occurs_check subst i t ->
+ raise
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
+ | C.Meta (i, l), t when (locked locked_menv i) ->
+ raise
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
+ | C.Meta (i, l), t -> (
+ try
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ assert (not (Subst.is_in_subst i subst));
+ let subst = Subst.buildsubst i context t ty subst in
+ let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
+ subst, menv
+ with CicUtil.Meta_not_found m ->
+ let names = names_of_context context in
+ (*debug_print
+ (lazy*) prerr_endline
+ (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+ (CicPp.pp t1 names) (CicPp.pp t2 names)
+ (print_metasenv menv) (print_metasenv metasenv));
+ assert false
+ )
+ | _, C.Meta _ -> unif subst menv t s
+ | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
+ | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
+ try
+ List.fold_left2
+ (fun (subst', menv) s t -> unif subst' menv s t)
+ (subst, menv) tls tlt
+ with Invalid_argument _ ->
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
+ in
+ let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
+ let menv = Subst.filter subst menv in
+ subst, menv, ugraph
+;;
+
+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 =
+ HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
+ (* metasenv1 @ metasenv2 *)
+ in
+ let subst, menv, ug =
+ if not (is_simple_term t1) || not (is_simple_term t2) then (
+ debug_print
+ (lazy
+ (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+ (CicPp.ppterm t1) (CicPp.ppterm t2)));
+ raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
+ ) else
+ if b then
+ (* full unification *)
+ unification_simple [] metasenv context t1 t2 ugraph
+ else
+ (* matching: metasenv1 is locked *)
+ unification_simple metasenv1 metasenv context t1 t2 ugraph
+ in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst menv "unif");
+ (* let flatten subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = apply_subst_context subst context in
+ let term = apply_subst subst term in
+ let ty = 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 *)
+ subst, menv, ug
+;;
+
+exception MatchingFailure;;
+
+(** matching takes in input the _disjoint_ metasenv of t1 and t2;
+it perform unification in the union metasenv, then check that
+the first metasenv has not changed *)
+let matching metasenv1 metasenv2 context t1 t2 ugraph =
+ try
+ unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
+ with
+ CicUnification.UnificationFailure _ ->
+ raise MatchingFailure
+;;
+
+let unification m1 m2 c t1 t2 ug =
+ try
+ unification_aux true m1 m2 c t1 t2 ug
+ with exn ->
+ raise exn
+;;
+
+let get_stats () = "" (*<:show<Inference.>>*) ;;
--- /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/.
+ *)
+
+exception MatchingFailure
+
+(** matching between two terms. Can raise MatchingFailure *)
+val matching:
+ Cic.metasenv -> Cic.metasenv -> Cic.context ->
+ Cic.term -> Cic.term ->
+ CicUniv.universe_graph ->
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
+
+(**
+ special unification that checks if the two terms are "simple", and in
+ such case should be significantly faster than CicUnification.fo_unif
+*)
+val unification:
+ Cic.metasenv -> Cic.metasenv -> Cic.context ->
+ Cic.term -> Cic.term ->
+ CicUniv.universe_graph ->
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
+
+val get_stats: unit -> string
(*
try
ignore(CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
+ metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
with e ->
prerr_endline msg;
- prerr_endline (Inference.string_of_proof proof);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
+ prerr_endline (Founif.string_of_proof proof);
+ prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
raise e
) else
let do_match c =
let subst', metasenv', ugraph' =
- Inference.matching
+ Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
let res =
try
do_match c
- with Inference.MatchingFailure ->
+ with Founif.MatchingFailure ->
find_matches bag metasenv context ugraph lift_amount term termty tl
in
if Utils.debug_res then ignore (check_res res "find1");
else
let res =
try do_match c
- with Inference.MatchingFailure -> None
+ with Founif.MatchingFailure -> None
in
if Utils.debug_res then ignore (check_res res "find2");
match res with
(*
as above, but finds all the matching equalities, and the matching condition
- can be either Inference.matching or Inference.unification
+ can be either Founif.matching or Inference.unification
*)
-let rec find_all_matches ?(unif_fun=Inference.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches
?unif_fun metasenv context ugraph lift_amount term termty l
(*prerr_endline "CANDIDATES:";
- List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+ List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
(List.length rc));*)
;;
let metasenv = tmetas in
let predicate, unif_fun =
if use_unification then
- Unification, Inference.unification
+ Unification, Founif.unification
else
- Matching, Inference.matching
+ Matching, Founif.matching
in
let leftr =
match left with
| None -> ok what leftorright tl
| Some s -> Some (s, equation, leftorright <> pos ))
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _ -> ok what leftorright tl
in
match ok right Utils.Left leftr with
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right in
- let newmenv = (* Inference.filter s *) m in
+ let newmenv = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
bo, (newgoalproofstep::goalproof)
in
- let newmetasenv = (* Inference.filter subst *) menv in
+ let newmetasenv = (* Founif.filter subst *) menv in
(newgoalproof, newmetasenv, newterm)
;;
+++ /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/.
- *)
-
-(* let _profiler = <:profiler<_profiler>>;; *)
-
-(* $Id$ *)
-
-open Utils;;
-open Printf;;
-
-let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
-
-let check_disjoint_invariant subst metasenv msg =
- if (List.exists
- (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
- then
- begin
- prerr_endline ("not disjoint: " ^ msg);
- assert false
- end
-;;
-
-let rec check_irl start = function
- | [] -> true
- | None::tl -> check_irl (start+1) tl
- | (Some (Cic.Rel x))::tl ->
- if x = start then check_irl (start+1) tl else false
- | _ -> false
-;;
-
-let rec is_simple_term = function
- | Cic.Appl ((Cic.Meta _)::_) -> false
- | Cic.Appl l -> List.for_all is_simple_term l
- | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
- | Cic.Rel _ -> true
- | Cic.Const _ -> true
- | Cic.MutInd (_, _, []) -> true
- | Cic.MutConstruct (_, _, _, []) -> true
- | _ -> false
-;;
-
-let locked menv i =
- List.exists (fun (j,_,_) -> i = j) menv
-;;
-
-let unification_simple locked_menv metasenv context t1 t2 ugraph =
- let module C = Cic in
- let module M = CicMetaSubst in
- let module U = CicUnification in
- let lookup = Subst.lookup_subst in
- let rec occurs_check subst what where =
- match where with
- | Cic.Meta(i,_) when i = what -> true
- | C.Appl l -> List.exists (occurs_check subst what) l
- | C.Meta _ ->
- let t = lookup where subst in
- if t <> where then occurs_check subst what t else false
- | _ -> false
- in
- let rec unif subst menv s t =
- let s = match s with C.Meta _ -> lookup s subst | _ -> s
- and t = match t with C.Meta _ -> lookup t subst | _ -> t
-
- in
- match s, t with
- | s, t when s = t -> subst, menv
- (* sometimes the same meta has different local contexts; this
- could create "cyclic" substitutions *)
- | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv
- | C.Meta (i, _), C.Meta (j, _)
- when (locked locked_menv i) &&(locked locked_menv j) ->
- raise
- (U.UnificationFailure (lazy "Inference.unification.unif"))
- | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
- unif subst menv t s
- | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
- unif subst menv t s
- | C.Meta (i,_), t when occurs_check subst i t ->
- raise
- (U.UnificationFailure (lazy "Inference.unification.unif"))
- | C.Meta (i, l), t when (locked locked_menv i) ->
- raise
- (U.UnificationFailure (lazy "Inference.unification.unif"))
- | C.Meta (i, l), t -> (
- try
- let _, _, ty = CicUtil.lookup_meta i menv in
- assert (not (Subst.is_in_subst i subst));
- let subst = Subst.buildsubst i context t ty subst in
- let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
- subst, menv
- with CicUtil.Meta_not_found m ->
- let names = names_of_context context in
- (*debug_print
- (lazy*) prerr_endline
- (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
- (CicPp.pp t1 names) (CicPp.pp t2 names)
- (print_metasenv menv) (print_metasenv metasenv));
- assert false
- )
- | _, C.Meta _ -> unif subst menv t s
- | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
- raise (U.UnificationFailure (lazy "Inference.unification.unif"))
- | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
- try
- List.fold_left2
- (fun (subst', menv) s t -> unif subst' menv s t)
- (subst, menv) tls tlt
- with Invalid_argument _ ->
- raise (U.UnificationFailure (lazy "Inference.unification.unif"))
- )
- | _, _ ->
- raise (U.UnificationFailure (lazy "Inference.unification.unif"))
- in
- let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
- let menv = Subst.filter subst menv in
- subst, menv, ugraph
-;;
-
-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 =
- HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
- (* metasenv1 @ metasenv2 *)
- in
- let subst, menv, ug =
- if not (is_simple_term t1) || not (is_simple_term t2) then (
- debug_print
- (lazy
- (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
- (CicPp.ppterm t1) (CicPp.ppterm t2)));
- raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
- ) else
- if b then
- (* full unification *)
- unification_simple [] metasenv context t1 t2 ugraph
- else
- (* matching: metasenv1 is locked *)
- unification_simple metasenv1 metasenv context t1 t2 ugraph
- in
- if Utils.debug_res then
- ignore(check_disjoint_invariant subst menv "unif");
- (* let flatten subst =
- List.map
- (fun (i, (context, term, ty)) ->
- let context = apply_subst_context subst context in
- let term = apply_subst subst term in
- let ty = 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 *)
- subst, menv, ug
-;;
-
-exception MatchingFailure;;
-
-(** matching takes in input the _disjoint_ metasenv of t1 and t2;
-it perform unification in the union metasenv, then check that
-the first metasenv has not changed *)
-let matching metasenv1 metasenv2 context t1 t2 ugraph =
- try
- unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
- with
- CicUnification.UnificationFailure _ ->
- raise MatchingFailure
-;;
-
-let unification m1 m2 c t1 t2 ug =
- try
- unification_aux true m1 m2 c t1 t2 ug
- with exn ->
- raise exn
-;;
-
-let get_stats () = "" (*<:show<Inference.>>*) ;;
+++ /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/.
- *)
-
-exception MatchingFailure
-
-(** matching between two terms. Can raise MatchingFailure *)
-val matching:
- Cic.metasenv -> Cic.metasenv -> Cic.context ->
- Cic.term -> Cic.term ->
- CicUniv.universe_graph ->
- Subst.substitution * Cic.metasenv * CicUniv.universe_graph
-
-(**
- special unification that checks if the two terms are "simple", and in
- such case should be significantly faster than CicUnification.fo_unif
-*)
-val unification:
- Cic.metasenv -> Cic.metasenv -> Cic.context ->
- Cic.term -> Cic.term ->
- CicUniv.universe_graph ->
- Subst.substitution * Cic.metasenv * CicUniv.universe_graph
-
-val get_stats: unit -> string
(let _,context,_ = env in
try
let s,m,_ =
- Inference.unification m m context left right CicUniv.empty_ugraph
+ Founif.unification m m context left right CicUniv.empty_ugraph
in
let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
let m = Subst.apply_subst_metasenv s m in
let get_stats () = ""
(*
- <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+ <:show<Saturation.>> ^ Indexing.get_stats () ^ Founif.get_stats () ^
Equality.get_stats ()
;;
*)
projects / helm.git / commitdiff