--- /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$ *)
+
+module Index = Equality_indexing.DT (* discrimination tree based indexing *)
+(*
+module Index = Equality_indexing.DT (* path tree based indexing *)
+*)
+
+let debug_print = Utils.debug_print;;
+
+(*
+for debugging
+let check_equation env equation msg =
+ let w, proof, (eq_ty, left, right, order), metas, args = equation in
+ let metasenv, context, ugraph = env
+ let metasenv' = metasenv @ metas in
+ try
+ CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+ 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
+*)
+
+type retrieval_mode = Matching | Unification;;
+
+let string_of_res ?env =
+ function
+ None -> "None"
+ | Some (t, s, m, u, (p,e)) ->
+ Printf.sprintf "Some: (%s, %s, %s)"
+ (Utils.string_of_pos p)
+ (Equality.string_of_equality ?env e)
+ (CicPp.ppterm t)
+;;
+
+let print_res ?env res =
+ prerr_endline
+ (String.concat "\n"
+ (List.map (string_of_res ?env) res))
+;;
+
+let print_candidates ?env mode term res =
+ let _ =
+ match mode with
+ | Matching ->
+ prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
+ | Unification ->
+ prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
+ in
+ prerr_endline
+ (String.concat "\n"
+ (List.map
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Equality.string_of_equality ?env e))
+ res));
+;;
+
+
+let apply_subst = Subst.apply_subst
+
+let index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty
+let init_index = Index.init_index
+
+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 check_for_duplicates metas msg =
+ if List.length metas <>
+ List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
+ begin
+ prerr_endline ("DUPLICATI " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ assert false
+ end
+;;
+
+let check_res res msg =
+ match res with
+ Some (t, subst, menv, ug, eq_found) ->
+ let eqs = Equality.string_of_equality (snd eq_found) in
+ check_disjoint_invariant subst menv msg;
+ check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
+ | None -> ()
+;;
+
+let check_target bag context target msg =
+ let w, proof, (eq_ty, left, right, order), metas,_ =
+ Equality.open_equality target in
+ (* check that metas does not contains duplicates *)
+ let eqs = Equality.string_of_equality target in
+ let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
+ let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
+ let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
+ let _ = if menv <> metas then
+ begin
+ prerr_endline ("extra metas " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ prerr_endline "**********************";
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ prerr_endline ("left: " ^ (CicPp.ppterm left));
+ prerr_endline ("right: " ^ (CicPp.ppterm right));
+ prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
+ assert false
+ end
+ else () in ()
+(*
+ try
+ ignore(CicTypeChecker.type_of_aux'
+ metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
+ with e ->
+ prerr_endline msg;
+ 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
+*)
+
+
+(* returns a list of all the equalities in the tree that are in relation
+ "mode" with the given term, where mode can be either Matching or
+ Unification.
+
+ Format of the return value: list of tuples in the form:
+ (position - Left or Right - of the term that matched the given one in this
+ equality,
+ equality found)
+
+ Note that if equality is "left = right", if the ordering is left > right,
+ the position will always be Left, and if the ordering is left < right,
+ position will be Right.
+*)
+
+let get_candidates ?env mode tree term =
+ let s =
+ match mode with
+ | Matching ->
+ Index.retrieve_generalizations tree term
+ | Unification ->
+ Index.retrieve_unifiables tree term
+
+ in
+ Index.PosEqSet.elements s
+;;
+
+(*
+ finds the first equality in the index that matches "term", of type "termty"
+ termty can be Implicit if it is not needed. The result (one of the sides of
+ the equality, actually) should be not greater (wrt the term ordering) than
+ term
+
+ Format of the return value:
+
+ (term to substitute, [Cic.Rel 1 properly lifted - see the various
+ build_newtarget functions inside the various
+ demodulation_* functions]
+ substitution used for the matching,
+ metasenv,
+ ugraph, [substitution, metasenv and ugraph have the same meaning as those
+ returned by CicUnification.fo_unif]
+ (equality where the matching term was found, [i.e. the equality to use as
+ rewrite rule]
+ uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
+ the equality: this is used to build the proof term, again see one of
+ the build_newtarget functions]
+ ))
+*)
+let rec find_matches bag metasenv context ugraph lift_amount term termty =
+ let module C = Cic in
+ let module U = Utils in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let cmp = !Utils.compare_terms in
+ let check = match termty with C.Implicit None -> false | _ -> true in
+ function
+ | [] -> None
+ | candidate::tl ->
+ let pos, equality = candidate in
+ let (_, proof, (ty, left, right, o), metas,_) =
+ Equality.open_equality equality
+ in
+ if Utils.debug_metas then
+ ignore(check_target bag context (snd candidate) "find_matches");
+ if Utils.debug_res then
+ begin
+ let c="eq = "^(Equality.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(Equality.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;
+ if check && not (fst (CicReduction.are_convertible
+ ~metasenv context termty ty ugraph)) then (
+ find_matches bag metasenv context ugraph lift_amount term termty tl
+ ) else
+ let do_match c =
+ let subst', metasenv', ugraph' =
+ Founif.matching
+ metasenv metas context term (S.lift lift_amount c) ugraph
+ in
+ Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
+ in
+ let c, other =
+ if pos = Utils.Left then left, right
+ else right, left
+ in
+ if o <> U.Incomparable then
+ let res =
+ try
+ do_match c
+ 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");
+ res
+ else
+ let res =
+ try do_match c
+ with Founif.MatchingFailure -> None
+ in
+ if Utils.debug_res then ignore (check_res res "find2");
+ match res with
+ | Some (_, s, _, _, _) ->
+ let c' = apply_subst s c in
+ (*
+ let other' = U.guarded_simpl context (apply_subst s other) in *)
+ let other' = apply_subst s other in
+ let order = cmp c' other' in
+ if order = U.Gt then
+ res
+ else
+ find_matches bag
+ metasenv context ugraph lift_amount term termty tl
+ | None ->
+ find_matches bag metasenv context ugraph lift_amount term termty tl
+;;
+
+let find_matches metasenv context ugraph lift_amount term termty =
+ find_matches metasenv context ugraph lift_amount term termty
+;;
+
+(*
+ as above, but finds all the matching equalities, and the matching condition
+ can be either Founif.matching or Inference.unification
+*)
+(* XXX termty unused *)
+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
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let cmp = !Utils.compare_terms in
+ function
+ | [] -> []
+ | candidate::tl ->
+ let pos, equality = candidate in
+ let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
+ let do_match c =
+ let subst', metasenv', ugraph' =
+ unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
+ in
+ (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
+ in
+ let c, other =
+ if pos = Utils.Left then left, right
+ else right, left
+ in
+ if o <> U.Incomparable then
+ try
+ let res = do_match c in
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl)
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ else
+ try
+ let res = do_match c in
+ match res with
+ | _, s, _, _, _ ->
+ let c' = apply_subst s c
+ and other' = apply_subst s other in
+ let order = cmp c' other' in
+ if order <> U.Lt && order <> U.Le then
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl)
+ else
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term termty tl
+;;
+
+let find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+=
+ find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+ (*prerr_endline "CANDIDATES:";
+ 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));*)
+;;
+(*
+ returns true if target is subsumed by some equality in table
+*)
+(*
+let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Equality.string_of_equality equation)l))
+;;
+*)
+
+let subsumption_aux use_unification env table target =
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+ let _, context, ugraph = env in
+ let metasenv = tmetas in
+ let predicate, unif_fun =
+ if use_unification then
+ Unification, Founif.unification
+ else
+ Matching, Founif.matching
+ in
+ let leftr =
+ match left with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 left ty leftc
+ in
+ let rec ok what leftorright = function
+ | [] -> None
+ | (_, subst, menv, ug, (pos,equation))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+ try
+ let other = if pos = Utils.Left then r else l in
+ let what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
+ let subst', menv', ug' =
+ unif_fun metasenv m context what' other' ugraph
+ in
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok what leftorright tl
+ | Some s -> Some (s, equation, leftorright <> pos ))
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _ -> ok what leftorright tl
+ in
+ match ok right Utils.Left leftr with
+ | Some _ as res -> res
+ | None ->
+ let rightr =
+ match right with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 right ty rightc
+ in
+ ok left Utils.Right rightr
+;;
+
+let subsumption x y z =
+ subsumption_aux false x y z
+;;
+
+let unification x y z =
+ subsumption_aux true x y z
+;;
+
+let subsumption_aux_all use_unification env table target =
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+ let _, context, ugraph = env in
+ let metasenv = tmetas in
+ let predicate, unif_fun =
+ if use_unification then
+ Unification, Founif.unification
+ else
+ Matching, Founif.matching
+ in
+ let leftr =
+ match left with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 left ty leftc
+ in
+ let rightr =
+ match right with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 right ty rightc
+ in
+ let rec ok_all what leftorright = function
+ | [] -> []
+ | (_, subst, menv, ug, (pos,equation))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+ try
+ let other = if pos = Utils.Left then r else l in
+ let what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
+ let subst', menv', ug' =
+ unif_fun metasenv m context what' other' ugraph
+ in
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok_all what leftorright tl
+ | Some s ->
+ (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
+ in
+ (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
+;;
+
+let subsumption_all x y z =
+ subsumption_aux_all false x y z
+;;
+
+let unification_all x y z =
+ subsumption_aux_all true x y z
+;;
+let rec demodulation_aux bag ?from ?(typecheck=false)
+ metasenv context ugraph table lift_amount term =
+(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let candidates =
+ get_candidates
+ ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
+ in
+ let res =
+ match term with
+ | C.Meta _ -> None
+ | term ->
+ let termty, ugraph =
+ if typecheck then
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ else
+ C.Implicit None, ugraph
+ in
+ let res =
+ find_matches bag metasenv context ugraph lift_amount term termty candidates
+ in
+ if Utils.debug_res then ignore(check_res res "demod1");
+ if res <> None then
+ res
+ 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 bag ~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 bag ~from:"2"
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux bag 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 bag
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux bag 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
+
+(** demodulation, when target is an equality *)
+let rec demodulation_equality bag ?from eq_uri newmeta env table target =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let module U = Utils in
+ let metasenv, context, ugraph = env in
+ let w, proof, (eq_ty, left, right, order), metas, id =
+ Equality.open_equality target
+ in
+ (* first, we simplify *)
+(* let right = U.guarded_simpl context right in *)
+(* let left = U.guarded_simpl context left in *)
+(* let order = !Utils.compare_terms left right in *)
+(* let stat = (eq_ty, left, right, order) in *)
+(* let w = Utils.compute_equality_weight stat in*)
+ (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
+ if Utils.debug_metas then
+ ignore(check_target bag context target "demod equalities input");
+ let metasenv' = (* metasenv @ *) metas in
+ let maxmeta = ref newmeta in
+
+ let build_newtarget is_left (t, subst, menv, ug, eq_found) =
+
+ if Utils.debug_metas then
+ begin
+ ignore(check_for_duplicates menv "input1");
+ ignore(check_disjoint_invariant subst menv "input2");
+ let substs = Subst.ppsubst subst in
+ ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
+ end;
+ let pos, equality = eq_found in
+ let (_, proof',
+ (ty, what, other, _), menv',id') = Equality.open_equality equality in
+ let ty =
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ with CicUtil.Meta_not_found _ -> ty
+ in
+ let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newproof =
+ let bo =
+ Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
+ let bo' =
+ let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
+ C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
+ in
+ (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
+ (Cic.Lambda (name, ty, bo'))))))
+ in
+ let newmenv = menv in
+ let left, right = if is_left then newterm, right else left, newterm in
+ let ordering = !Utils.compare_terms left right in
+ let stat = (eq_ty, left, right, ordering) in
+ let res =
+ let w = Utils.compute_equality_weight stat in
+ (Equality.mk_equality bag (w, newproof, stat,newmenv))
+ in
+ if Utils.debug_metas then
+ ignore(check_target bag context res "buildnew_target output");
+ !maxmeta, res
+ in
+
+ let res =
+ demodulation_aux bag ~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
+ (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
+ if (Equality.is_weak_identity newtarget) (* || *)
+ (*Equality.meta_convertibility_eq target newtarget*) then
+ newmeta, newtarget
+ else
+ demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ | None ->
+ let res = demodulation_aux bag 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 (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
+ newmeta, newtarget
+ else
+ demodulation_equality bag ?from eq_uri newmeta env table 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
+ in table.
+*)
+let rec betaexpand_term
+ ?(subterms_only=false) metasenv context ugraph table lift_amount term
+=
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+
+ let res, lifted_term =
+ match term with
+ | C.Meta (i, l) ->
+ let l = [] in
+ let l', lifted_l =
+ List.fold_right
+ (fun arg (res, lifted_tl) ->
+ match arg with
+ | Some arg ->
+ let arg_res, lifted_arg =
+ betaexpand_term metasenv context ugraph table
+ lift_amount arg in
+ let l1 =
+ List.map
+ (fun (t, s, m, ug, eq_found) ->
+ (Some t)::lifted_tl, s, m, ug, eq_found)
+ arg_res
+ in
+ (l1 @
+ (List.map
+ (fun (l, s, m, ug, eq_found) ->
+ (Some lifted_arg)::l, s, m, ug, eq_found)
+ res),
+ (Some lifted_arg)::lifted_tl)
+ | None ->
+ (List.map
+ (fun (r, s, m, ug, eq_found) ->
+ None::r, s, m, ug, eq_found) res,
+ None::lifted_tl)
+ ) l ([], [])
+ in
+ let e =
+ List.map
+ (fun (l, s, m, ug, eq_found) ->
+ (C.Meta (i, l), s, m, ug, eq_found)) l'
+ in
+ e, C.Meta (i, lifted_l)
+
+ | C.Rel m ->
+ [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
+
+ | C.Prod (nn, s, t) ->
+ let l1, lifted_s =
+ betaexpand_term metasenv context ugraph table lift_amount s in
+ let l2, lifted_t =
+ betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug, eq_found) ->
+ C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
+ and l2' =
+ List.map
+ (fun (t, s, m, ug, eq_found) ->
+ C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
+ l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
+
+ | C.Lambda (nn, s, t) ->
+ let l1, lifted_s =
+ betaexpand_term metasenv context ugraph table lift_amount s in
+ let l2, lifted_t =
+ betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t in
+ let l1' =
+ List.map
+ (fun (t, s, m, ug, eq_found) ->
+ C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
+ and l2' =
+ List.map
+ (fun (t, s, m, ug, eq_found) ->
+ C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
+ l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
+
+ | C.Appl l ->
+ let l', lifted_l =
+ List.fold_left
+ (fun (res, lifted_tl) arg ->
+ let arg_res, lifted_arg =
+ betaexpand_term metasenv context ugraph table lift_amount arg
+ in
+ let l1 =
+ List.map
+ (fun (a, s, m, ug, eq_found) ->
+ a::lifted_tl, s, m, ug, eq_found)
+ arg_res
+ in
+ (l1 @
+ (List.map
+ (fun (r, s, m, ug, eq_found) ->
+ lifted_arg::r, s, m, ug, eq_found)
+ res),
+ lifted_arg::lifted_tl)
+ ) ([], []) (List.rev l)
+ in
+ (List.map
+ (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
+ C.Appl lifted_l)
+
+ | t -> [], (S.lift lift_amount t)
+ in
+ match term with
+ | C.Meta (i, l) -> res, lifted_term
+ | term ->
+ let termty, ugraph =
+ C.Implicit None, ugraph
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+ in
+ let candidates = get_candidates Unification table term in
+ let r =
+ if subterms_only then
+ []
+ else
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
+ in
+ r @ res, lifted_term
+;;
+
+(**
+ superposition_right
+ returns a list of new clauses inferred with a right superposition step
+ between the positive equation "target" and one in the "table" "newmeta" is
+ the first free meta index, i.e. the first number above the highest meta
+ index: its updated value is also returned
+*)
+let superposition_right bag
+ ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let module CR = CicReduction in
+ let module U = Utils in
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
+ Equality.open_equality target
+ in
+ if Utils.debug_metas then
+ ignore (check_target bag context target "superpositionright");
+ let metasenv' = newmetas in
+ let maxmeta = ref newmeta in
+ let res1, res2 =
+ match ordering with
+ | U.Gt ->
+ fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
+ | U.Lt ->
+ [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
+ | _ ->
+ let res l r =
+ List.filter
+ (fun (_, subst, _, _, _) ->
+ let subst = apply_subst subst in
+ let o = !Utils.compare_terms (subst l) (subst r) in
+ o <> U.Lt && o <> U.Le)
+ (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
+ in
+ (res left right), (res right left)
+ in
+ let build_new ordering (bo, s, m, ug, eq_found) =
+ if Utils.debug_metas then
+ ignore (check_target bag context (snd eq_found) "buildnew1" );
+
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id') =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+
+ let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
+ let newgoal, newproof =
+ (* qua *)
+ let bo' =
+ Utils.guarded_simpl context (apply_subst s (S.subst other bo))
+ in
+ let name = C.Name "x" in
+ let bo'' =
+ let l, r =
+ if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
+ C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
+ in
+ bo',
+ Equality.Step
+ (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
+ in
+ let newmeta, newequality =
+ let left, right =
+ 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 = (* Founif.filter s *) m in
+ let stat = (eq_ty, left, right, neworder) in
+ let eq' =
+ let w = Utils.compute_equality_weight stat in
+ Equality.mk_equality bag (w, newproof, stat, newmenv) in
+ if Utils.debug_metas then
+ ignore (check_target bag context eq' "buildnew3");
+ let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
+ if Utils.debug_metas then
+ ignore (check_target bag context eq' "buildnew4");
+ newm, eq'
+ in
+ maxmeta := newmeta;
+ if Utils.debug_metas then
+ ignore(check_target bag context newequality "buildnew2");
+ newequality
+ in
+ let new1 = List.map (build_new U.Gt) res1
+ and new2 = List.map (build_new U.Lt) res2 in
+ let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
+ (!maxmeta,
+ (List.filter ok (new1 @ new2)))
+;;
+
+(** demodulation, when the target is a theorem *)
+let rec demodulation_theorem bag newmeta env table theorem =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let metasenv, context, ugraph = env in
+ let maxmeta = ref newmeta in
+ let term, termty, metas = theorem in
+ let metasenv' = metas in
+
+ let build_newtheorem (t, subst, menv, ug, eq_found) =
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newty =
+ let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(* let bo' = apply_subst subst t in *)
+(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
+(*
+ let newproofold =
+ Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+ Equality.BasicProof (Equality.empty_subst,term))
+ in
+ (Equality.build_proof_term_old newproofold, bo)
+*)
+ (* TODO, not ported to the new proofs *)
+ if true then assert false; term, bo
+ in
+ !maxmeta, (newterm, newty, menv)
+ in
+ let res =
+ demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+ in
+ match res with
+ | Some t ->
+ let newmeta, newthm = build_newtheorem t in
+ let newt, newty, _ = newthm in
+ if Equality.meta_convertibility termty newty then
+ newmeta, newthm
+ else
+ demodulation_theorem bag newmeta env table newthm
+ | None ->
+ newmeta, theorem
+;;
+
+(*****************************************************************************)
+(** OPERATIONS ON GOALS **)
+(** **)
+(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
+(*****************************************************************************)
+
+let open_goal g =
+ match g with
+ | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
+ (* assert (LibraryObjects.is_eq_URI uri); *)
+ proof,menv,eq,ty,l,r
+ | _ -> assert false
+;;
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 =
+ Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * C[x] ---> (eq ty unchanged C[x])
+ * [posu] is the side of the [unchanged] term in the original goal
+ *)
+let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
+ let _,_,eq,ty,l,r = open_goal goal in
+ let unchanged = if posu = Utils.Left then l else r in
+ let unchanged = CicSubstitution.lift 1 unchanged in
+ let ty = CicSubstitution.lift 1 ty in
+ let pred =
+ match posu with
+ | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+ | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+ in
+ (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the
+ * expansion builds a new goal *)
+let build_newgoal bag context goal posu rule expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal in
+ let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = apply_subst subst t in
+ let ty = apply_subst subst ty in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Founif.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+(**
+ superposition_left
+ returns a list of new clauses inferred with a left superposition step
+ the negative equation "target" and one of the positive equations in "table"
+*)
+let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
+ let names = Utils.names_of_context context in
+ let proof,menv,eq,ty,l,r = open_goal goal in
+ let c = !Utils.compare_terms l r in
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ *)
+ List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ end
+ else
+ match c with
+ | Utils.Gt -> (* prerr_endline "GT"; *)
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = r,l,Utils.Left in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false
+ in
+ (* rinfresco le meta *)
+ List.fold_right
+ (fun g (max,acc) ->
+ let max,g = Equality.fix_metas_goal max g in max,g::acc)
+ newgoals (maxmeta,[])
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal bag env table goal =
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let _, context, ugraph = env in
+(* let term = Utils.guarded_simpl (~debug:true) context term in*)
+ let do_right () =
+ let resright = demodulation_aux bag menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg =
+ build_newgoal bag context goal Utils.Left Equality.Demodulation t
+ in
+ if goal_metaconvertibility_eq goal newg then
+ false, goal
+ else
+ true, snd (demodulation_goal bag env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
+ match resleft with
+ | Some t ->
+ let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
+ else
+ true, snd (demodulation_goal bag env table newg)
+ | None -> do_right ()
+;;
+
+type next = L | R
+type solved = Yes of Equality.goal | No of Equality.goal list
+
+(* returns all the 1 step demodulations *)
+module C = Cic;;
+module S = CicSubstitution;;
+let rec demodulation_all_aux
+ metasenv context ugraph table lift_amount term
+=
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term
+ in
+ match term with
+ | C.Meta _ -> []
+ | _ ->
+ let termty, ugraph = C.Implicit None, ugraph in
+ let res =
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
+ in
+ match term with
+ | C.Appl l ->
+ let res, _, _ =
+ List.fold_left
+ (fun (res,l,r) t ->
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ (demodulation_all_aux
+ metasenv context ugraph table lift_amount t),
+ l@[List.hd r], List.tl r)
+ (res, [], List.map (S.lift 1) l) l
+ in
+ res
+ | C.Prod (nn, s, t)
+ | C.Lambda (nn, s, t) ->
+ let context = (Some (nn, C.Decl s))::context in
+ let mk s t =
+ match term with
+ | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
+ in
+ res @
+ List.map
+ (fun (rel, subst, m, ug, c) ->
+ mk (S.lift 1 s) rel, subst, m, ug, c)
+ (demodulation_all_aux
+ metasenv context ugraph table (lift_amount+1) t)
+ (* we could demodulate also in s, but then t may be badly
+ * typed... *)
+ | t -> res
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let _, context, ugraph = env in
+ let solved goal res side =
+ let newg = build_newgoal bag context goal side Equality.Demodulation res in
+ match newg with
+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
+ when LibraryObjects.is_eq_URI uri ->
+ (try
+ let _ =
+ Founif.unification m m context left right CicUniv.empty_ugraph
+ in
+ Yes newg
+ with CicUnification.UnificationFailure _ -> No [newg])
+ | _ -> No [newg]
+ in
+ let solved goal res_list side =
+ let newg = List.map (fun x -> solved goal x side) res_list in
+ try
+ List.find (function Yes _ -> true | _ -> false) newg
+ with Not_found ->
+ No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+ in
+ let rec first f l =
+ match l with
+ | [] -> None
+ | x::tl ->
+ match f x with
+ | None -> first f tl
+ | Some x as ok -> ok
+ in
+ let rec aux steps next goal =
+ if steps = 0 then None else
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let do_step t =
+ demodulation_all_aux menv context ugraph table 0 t
+ in
+ match next with
+ | L ->
+ (match do_step left with
+ | _::_ as res ->
+ (match solved goal res Utils.Right with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> aux steps R goal)
+ | Yes newgoal -> Some newgoal)
+ | [] -> aux steps R goal)
+ | R ->
+ (match do_step right with
+ | _::_ as res ->
+ (match solved goal res Utils.Left with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> None)
+ | Yes newgoal -> Some newgoal)
+ | [] -> None)
+ in
+ aux steps L initgoal
+;;
+
+let get_stats () = "" ;;
projects / helm.git / blobdiff