+(* 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/.
+ *)
+
open Utils;;
| BasicProof of Cic.term
| ProofBlock of
Cic.substitution * UriManager.uri *
- (Cic.name * Cic.term) * Cic.term *
- (* name, ty, eq_ty, left, right *)
-(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *)
- (Utils.pos * equality) * proof
- | ProofGoalBlock of proof * proof (* equality *)
-(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *)
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * proof
| ProofSymBlock of Cic.term list * proof
| SubProof of Cic.term * int * proof
;;
;;
+let rec string_of_proof = function
+ | NoProof -> "NoProof"
+ | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+ | SubProof (t, i, p) ->
+ Printf.sprintf "SubProof(%s, %s, %s)"
+ (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
+ | ProofSymBlock _ -> "ProofSymBlock"
+ | ProofBlock _ -> "ProofBlock"
+ | ProofGoalBlock (p1, p2) ->
+ Printf.sprintf "ProofGoalBlock(%s, %s)"
+ (string_of_proof p1) (string_of_proof p2)
+;;
+
+
+(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
let build_ens_for_sym_eq sym_eq_URI termlist =
let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
match obj with
in
aux (uris, termlist)
| _ -> assert false
-(* [(UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *)
-(* (UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *)
-(* (UriManager.uri_of_string *)
-(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *)
;;
| ProofGoalBlock (proofbit, proof) ->
print_endline "found ProofGoalBlock, going up...";
do_build_goal_proof proofbit proof
-(* | ProofSymBlock (ens, proof) -> *)
-(* let proof = do_build_proof proof in *)
-(* Cic.Appl [ *)
-(* Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *)
-(* proof *)
-(* ] *)
| ProofSymBlock (termlist, proof) ->
let proof = do_build_proof proof in
let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
- | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
+ | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
let t' = Cic.Lambda (name, ty, bo) in
let proof' =
let _, proof', _, _, _ = eq in
~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
and do_build_goal_proof proofbit proof =
-(* match proofbit with *)
-(* | BasicProof _ -> do_build_proof proof *)
-(* | proofbit -> *)
- match proof with
- | ProofGoalBlock (pb, p(* eq *)) ->
- do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
-(* let _, proof, _, _, _ = eq in *)
-(* let newproof = replace_proof proofbit proof in *)
-(* do_build_proof newproof *)
-
-(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
-(* let eqproof' = replace_proof proofbit eqproof in *)
-(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
- | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+ match proof with
+ | ProofGoalBlock (pb, p) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
+ | _ -> do_build_proof (replace_proof proofbit proof)
and replace_proof newproof = function
- | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
+ | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
let eqproof' = replace_proof newproof eqproof in
- ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
- | ProofGoalBlock (pb, p(* equality *)) ->
+ ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
+ | ProofGoalBlock (pb, p) ->
let pb' = replace_proof newproof pb in
- ProofGoalBlock (pb', p(* equality *))
-(* let w, proof, t, menv, args = equality in *)
-(* let proof' = replace_proof newproof proof in *)
-(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+ ProofGoalBlock (pb', p)
| BasicProof _ -> newproof
| SubProof (term, meta_index, p) ->
SubProof (term, meta_index, replace_proof newproof p)
| p -> p
in
-(* let _, proof, _, _, _ = equality in *)
do_build_proof proof
;;
(fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
in
let rec aux ((table_l, table_r) as table) t1 t2 =
-(* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
-(* (print_table table_l) (print_table table_r); *)
match t1, t2 with
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
let m1_binding, table_l =
try List.assoc m2 table_r, table_r
with Not_found -> m1, (m2, m1)::table_r
in
-(* let m1_binding, m2_binding, table = *)
-(* let m1b, table = *)
-(* try List.assoc m1 table, table *)
-(* with Not_found -> m2, (m1, m2)::table *)
-(* in *)
-(* let m2b, table = *)
-(* try List.assoc m2 table, table *)
-(* with Not_found -> m1, (m2, m1)::table *)
-(* in *)
-(* m1b, m2b, table *)
-(* in *)
-(* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
-(* (print_table table_l) (print_table table_r); *)
if (m1_binding <> m2) || (m2_binding <> m1) then
raise NotMetaConvertible
else (
else
try
let l, r = meta_convertibility_aux ([], []) t1 t2 in
- (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
true
with NotMetaConvertible ->
false
;;
-(*
-let replace_metas (* context *) term =
- let module C = Cic in
- let rec aux = function
- | C.Meta (i, c) ->
-(* let irl = *)
-(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(* in *)
-(* if c = irl then *)
-(* C.Implicit (Some (`MetaIndex i)) *)
-(* else ( *)
-(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
-(* (String.concat "\n" *)
-(* (List.map *)
-(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
-(* C.Meta (i, c) *)
-(* ) *)
- C.Implicit (Some (`MetaInfo (i, c)))
- | C.Var (u, ens) -> C.Var (u, aux_ens ens)
- | C.Const (u, ens) -> C.Const (u, aux_ens ens)
- | C.Cast (s, t) -> C.Cast (aux s, aux t)
- | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
- | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
- | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
- | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
- | C.MutCase (uri, i, s, t, l) ->
- C.MutCase (uri, i, aux s, aux t, List.map aux l)
- | C.Fix (i, il) ->
- let il' =
- List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
- C.Fix (i, il')
- | C.CoFix (i, il) ->
- let il' =
- List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
- C.CoFix (i, il')
- | t -> t
- and aux_ens ens =
- List.map (fun (u, t) -> (u, aux t)) ens
- in
- aux term
-;;
-*)
-
-
-(*
-let restore_metas (* context *) term =
- let module C = Cic in
- let rec aux = function
- | C.Implicit (Some (`MetaInfo (i, c))) ->
-(* let c = *)
-(* CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(* in *)
-(* C.Meta (i, c) *)
-(* let local_context:(C.term option) list = *)
-(* Marshal.from_string mc 0 *)
-(* in *)
-(* C.Meta (i, local_context) *)
- C.Meta (i, c)
- | C.Var (u, ens) -> C.Var (u, aux_ens ens)
- | C.Const (u, ens) -> C.Const (u, aux_ens ens)
- | C.Cast (s, t) -> C.Cast (aux s, aux t)
- | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
- | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
- | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
- | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
- | C.MutCase (uri, i, s, t, l) ->
- C.MutCase (uri, i, aux s, aux t, List.map aux l)
- | C.Fix (i, il) ->
- let il' =
- List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
- C.Fix (i, il')
- | C.CoFix (i, il) ->
- let il' =
- List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
- C.CoFix (i, il')
- | t -> t
- and aux_ens ens =
- List.map (fun (u, t) -> (u, aux t)) ens
- in
- aux term
-;;
-*)
-
-(*
-let rec restore_subst (* context *) subst =
- List.map
- (fun (i, (c, t, ty)) ->
- i, (c, restore_metas (* context *) t, ty))
- subst
-;;
-*)
-
-
let rec check_irl start = function
| [] -> true
| None::tl -> check_irl (start+1) tl
| _ -> false
;;
+
let rec is_simple_term = function
| Cic.Appl ((Cic.Meta _)::_) -> false
| Cic.Appl l -> List.for_all is_simple_term l
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise
- (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
)
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
- raise (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ 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
- (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
)
| _, _ ->
- raise (U.UnificationFailure
- (U.failure_msg_of_string "Inference.unification.unif"))
+ raise (U.UnificationFailure (lazy "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
let menv =
let unification metasenv context t1 t2 ugraph =
-(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
debug_print
| [] -> []
| (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
in
-(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
-(* print_endline "|"; *)
fix_subst subst, menv, ug
;;
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
exception MatchingFailure;;
+(*
let matching_simple metasenv context t1 t2 ugraph =
let module C = Cic in
let module M = CicMetaSubst in
| _ -> assert false
in
let rec do_match subst menv s t =
-(* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
-(* (print_subst subst); *)
-(* print_newline (); *)
-(* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
-(* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
- (* Printf.printf "after apply_subst: %s %s\n%s" *)
- (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
- (* print_newline (); *)
match s, t with
| s, t when s = t -> subst, menv
-(* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
-(* do_match subst menv t s *)
-(* | C.Meta _, t when occurs_check subst s t -> *)
-(* raise MatchingFailure *)
-(* | s, C.Meta _ when occurs_check subst t s -> *)
-(* raise MatchingFailure *)
| s, C.Meta (i, l) ->
let filter_menv i menv =
List.filter (fun (m, _, _) -> i <> m) menv
let subst, menv =
let value = lookup t subst in
match value with
-(* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
-(* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
| value when value = t ->
let _, _, ty = CicUtil.lookup_meta i menv in
(i, (context, s, ty))::subst, filter_menv i menv
| value -> do_match subst menv s value
in
subst, menv
-(* else if value <> s then *)
-(* raise MatchingFailure *)
-(* else subst *)
-(* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
-(* else subst *)
-(* in *)
-(* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
-(* subst, menv *)
-(* | _, C.Meta _ -> do_match subst menv t s *)
-(* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
-(* raise MatchingFailure *)
| C.Appl ls, C.Appl lt -> (
try
List.fold_left2
(fun (subst, menv) s t -> do_match subst menv s t)
(subst, menv) ls lt
with Invalid_argument _ ->
-(* print_endline (Printexc.to_string e); *)
-(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(* print_newline (); *)
raise MatchingFailure
)
| _, _ ->
-(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(* print_newline (); *)
raise MatchingFailure
in
let subst, menv = do_match [] metasenv t1 t2 in
- (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
- (* print_newline (); *)
subst, menv, ugraph
;;
+*)
let matching metasenv context t1 t2 ugraph =
-(* if (is_simple_term t1) && (is_simple_term t2) then *)
-(* let subst, menv, ug = *)
-(* matching_simple metasenv context t1 t2 ugraph in *)
-(* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
-(* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
-(* (\* print_newline (); *\) *)
-(* subst, menv, ug *)
-(* else *)
-(* debug_print *)
-(* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
-(* print_newline (); *)
try
let subst, metasenv, ugraph =
- (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
unification metasenv context t1 t2 ugraph
in
let t' = CicMetaSubst.apply_subst subst t1 in
| s -> s
in
let subst = List.map fix_subst subst in
-
-(* Printf.printf "matching %s %s:\n%s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
-(* print_newline (); *)
-
subst, metasenv, ugraph
with
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
-(* Printf.printf "failed to match %s %s\n" *)
-(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
-(* print_endline (Printexc.to_string e); *)
raise MatchingFailure
;;
-(* let matching = *)
-(* let profile = CicUtil.profile "Inference.matching" in *)
-(* (fun metasenv context t1 t2 ugraph -> *)
-(* profile (matching metasenv context t1 t2) ugraph) *)
-(* ;; *)
-
-
-let beta_expand ?(metas_ok=true) ?(match_only=false)
- what type_of_what where context metasenv ugraph =
- let module S = CicSubstitution in
- let module C = Cic in
-
-(* let _ = *)
-(* let names = names_of_context context in *)
-(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
-(* (CicPp.pp what names) (CicPp.ppterm what) *)
-(* (CicPp.pp where names) (CicPp.ppterm where); *)
-(* print_newline (); *)
-(* in *)
- (*
- return value:
- ((list of all possible beta expansions, subst, metasenv, ugraph),
- lifted term)
- *)
- let rec aux lift_amount term context metasenv subst ugraph =
-(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
- let res, lifted_term =
- match term with
- | C.Rel m ->
- [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
-
- | C.Var (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Var (uri, e), s, m, ug)) ens'
- in
- expansions, C.Var (uri, lifted_ens)
-
- | C.Meta (i, l) ->
- let l', lifted_l =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- match arg with
- | Some arg ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
- arg_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
- res),
- (Some lifted_arg)::lifted_tl)
- | None ->
- (List.map
- (fun (r, s, m, ug) -> None::r, s, m, ug)
- res,
- None::lifted_tl)
- ) l ([], [])
- in
- let e =
- List.map
- (fun (l, s, m, ug) ->
- (C.Meta (i, l), s, m, ug)) l'
- in
- e, C.Meta (i, lifted_l)
-
- | C.Sort _
- | C.Implicit _ as t -> [], t
-
- | C.Cast (s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Cast (lifted_s, lifted_t)
-
- | C.Prod (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Prod (nn, lifted_s, lifted_t)
-
- | C.Lambda (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
-
- | C.LetIn (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
-
- | C.Appl l ->
- let l', lifted_l =
- aux_list lift_amount l context metasenv subst ugraph
- in
- (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
- C.Appl lifted_l)
-
- | C.Const (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Const (uri, e), s, m, ug)) ens'
- in
- (expansions, C.Const (uri, lifted_ens))
-
- | C.MutInd (uri, i ,exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutInd (uri, i, e), s, m, ug)) ens'
- in
- (expansions, C.MutInd (uri, i, lifted_ens))
-
- | C.MutConstruct (uri, i, j, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
- in
- (expansions, C.MutConstruct (uri, i, j, lifted_ens))
-
- | C.MutCase (sp, i, outt, t, pl) ->
- let pl_res, lifted_pl =
- aux_list lift_amount pl context metasenv subst ugraph
- in
- let l1, lifted_outt =
- aux lift_amount outt context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph in
-
- let l1' =
- List.map
- (fun (outt, s, m, ug) ->
- C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
- let l3' =
- List.map
- (fun (pl, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
- in
- (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
-
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, idx, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
- C.Fix (i, lifted_fl))
-
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
- C.CoFix (i, lifted_fl))
- in
- let retval =
- match term with
- | C.Meta _ when (not metas_ok) ->
- res, lifted_term
- | _ ->
-(* let term' = *)
-(* if match_only then replace_metas context term *)
-(* else term *)
-(* in *)
- try
- let subst', metasenv', ugraph' =
-(* Printf.printf "provo a unificare %s e %s\n" *)
-(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
- if match_only then
- matching metasenv context term (S.lift lift_amount what) ugraph
- else
- CicUnification.fo_unif metasenv context
- (S.lift lift_amount what) term ugraph
- in
-(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
-(* (CicPp.ppterm (S.lift lift_amount what)); *)
-(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
-(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
- (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-(* if match_only then *)
-(* let t' = CicMetaSubst.apply_subst subst' term in *)
-(* if not (meta_convertibility term t') then ( *)
-(* res, lifted_term *)
-(* ) else ( *)
-(* let metas = metas_of_term term in *)
-(* let fix_subst = function *)
-(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
-(* (j, (c, C.Meta (i, lc), ty)) *)
-(* | s -> s *)
-(* in *)
-(* let subst' = List.map fix_subst subst' in *)
-(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
-(* lifted_term) *)
-(* ) *)
-(* else *)
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- with
- | MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
- res, lifted_term
- in
-(* Printf.printf "exit aux\n"; *)
- retval
-
- and aux_list lift_amount l context metasenv subst ugraph =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 = List.map
- (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map
- (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
- lifted_arg::lifted_tl)
- ) l ([], [])
-
- and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
- List.fold_right
- (fun (u, arg) (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map (fun (r, s, m, ug) ->
- (u, lifted_arg)::r, s, m, ug) res),
- (u, lifted_arg)::lifted_tl)
- ) exp_named_subst ([], [])
-
- in
- let expansions, _ =
-(* let where = *)
-(* if match_only then replace_metas (\* context *\) where *)
-(* else where *)
-(* in *)
- aux 0 where context metasenv [] ugraph
- in
- let mapfun =
-(* if match_only then *)
-(* (fun (term, subst, metasenv, ugraph) -> *)
-(* let term' = *)
-(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
-(* and subst = restore_subst subst in *)
-(* (term', subst, metasenv, ugraph)) *)
-(* else *)
- (fun (term, subst, metasenv, ugraph) ->
- let term' = C.Lambda (C.Anonymous, type_of_what, term) in
- (term', subst, metasenv, ugraph))
- in
- List.map mapfun expansions
-;;
-
let find_equalities context proof =
let module C = Cic in
let do_find context term =
match term with
| C.Prod (name, s, t) ->
-(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
let (head, newmetas, args, newmeta) =
ProofEngineHelpers.saturate_term newmeta []
context (S.lift index term) 0
debug_print
(lazy
(Printf.sprintf "OK: %s" (CicPp.ppterm term)));
-(* debug_print ( *)
-(* Printf.sprintf "args: %s\n" *)
-(* (String.concat ", " (List.map CicPp.ppterm args)))); *)
-(* debug_print (lazy ( *)
-(* Printf.sprintf "newmetas:\n%s\n" *)
-(* (print_metasenv newmetas))); *)
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
;;
+(*
let equations_blacklist =
List.fold_left
(fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
"cic:/Coq/ZArith/Zcompare/rename.con";
(* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
perche' questo cacchio di teorema rompe le scatole :'( *)
- "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+ "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+
+ "cic:/matita/logic/equality/eq_f.con";
+ "cic:/matita/logic/equality/eq_f2.con";
+ "cic:/matita/logic/equality/eq_rec.con";
+ "cic:/matita/logic/equality/eq_rect.con";
]
- ;;
+;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
let find_library_equalities dbd context status maxmeta =
let module C = Cic in
in
(uri, t, ty)::l)
[]
- (MetadataQuery.equations_for_goal ~dbd status)
+ (let t1 = Unix.gettimeofday () in
+ let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+ let t2 = Unix.gettimeofday () in
+ (debug_print
+ (lazy
+ (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
+ (t2 -. t1))));
+ eqs)
in
- let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *)
- and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *)
+ let eq_uri1 = eq_XURI ()
+ and eq_uri2 = LibraryObjects.eq_URI () in
let iseq uri =
(UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
in
let uriset, eqlist =
(List.fold_left
(fun (s, l) (u, e) ->
- if List.exists (meta_convertibility_eq e) l then (
+ if List.exists (meta_convertibility_eq e) (List.map snd l) then (
debug_print
(lazy
(Printf.sprintf "NO!! %s already there!"
(string_of_equality e)));
(UriManager.UriSet.add u s, l)
- ) else (UriManager.UriSet.add u s, e::l))
+ ) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
in
uriset, eqlist, maxm
else
let t = CicUtil.term_of_uri uri in
let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
- (uri, t, ty, [])::l)
+ (t, ty, [])::l)
[] (MetadataQuery.signature_of_goal ~dbd status)
in
let refl_equal =
let u = eq_XURI () in
let t = CicUtil.term_of_uri u in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- (u, t, ty, [])
+ (t, ty, [])
in
refl_equal::candidates
;;
let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
-(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
let table = Hashtbl.create (List.length args) in
- let is_this_case = ref false in
let newargs, newmeta =
List.fold_right
(fun t (newargs, index) ->
let _ =
if List.length metas > 0 then
let first = List.hd metas in
+ (* this new equality might have less variables than its parents: here
+ we fill the gap with a dummy arg. Example:
+ with (f X Y) = X we can simplify
+ (g X) = (f X Y) in
+ (g X) = X.
+ So the new equation has only one variable, but it still has type like
+ \lambda X,Y:..., so we need to pass a dummy arg for Y
+ (I hope this makes some sense...)
+ *)
Hashtbl.iter
(fun k v ->
if not (List.exists
let rec fix_proof = function
| NoProof -> NoProof
| BasicProof term -> BasicProof (repl term)
- | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
-
-(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
-(* (string_of_equality equality) (print_subst subst); *)
-
-(* debug_print "table is:"; *)
-(* Hashtbl.iter *)
-(* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
-(* table; *)
+ | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
let subst' =
List.fold_left
(fun s arg ->
let _, context, ty = CicUtil.lookup_meta i menv in
(i, (context, Cic.Meta (j, l), ty))::s
with Not_found | CicUtil.Meta_not_found _ ->
-(* debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
s
)
| _ -> assert false)
[] args
in
-
-(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
-(* print_newline (); *)
-
ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
| p -> assert false
in
let w = compute_equality_weight ty t1 t2 in
let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
e
-(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
raise TermIsNotAnEquality
;;
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-(*
-let superposition_left (metasenv, context, ugraph) target source =
- 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
- (* we assume that target is ground (does not contain metavariables): this
- * should always be the case (I hope, at least) *)
- let proof, (eq_ty, left, right, t_order), _, _ = target in
- let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- []
- else
- let where, is_left =
- match t_order (* compare_terms left right *) with
- | Lt -> right, false
- | Gt -> left, true
- | _ -> (
- Printf.printf "????????? %s = %s" (CicPp.ppterm left)
- (CicPp.ppterm right);
- print_newline ();
- assert false (* again, for ground terms this shouldn't happen... *)
- )
- in
- let metasenv' = newmetas @ metasenv in
- let result = s_order (* compare_terms t1 t2 *) in
- let res1, res2 =
- match result with
- | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
- | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
- | _ ->
- let res1 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
- (beta_expand t1 ty where context metasenv' ugraph)
- and res2 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
- (beta_expand t2 ty where context metasenv' ugraph)
- in
- res1, res2
- in
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let build_new what other eq_URI (t, s, m, ug) =
- let newgoal, newgoalproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- let bo' = S.subst (M.apply_subst s other) bo in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []);
- S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
- S.subst (M.apply_subst s other) bo,
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; eqproof])
- | _ -> assert false
- in
- let equation =
- if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
- else (eq_ty, left, newgoal, compare_terms left newgoal)
- in
- (newgoalproof (* eqproof *), equation, [], [])
- in
- let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
- new1 @ new2
-;;
-
-
-let superposition_right newmeta (metasenv, context, ugraph) target source =
- 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 eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
- let eqp', (ty', t1, t2, s_order), newm', args' = source in
- let maxmeta = ref newmeta in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty' then
- newmeta, []
- else
- (* let ok term subst other other_eq_side ugraph = *)
- (* match term with *)
- (* | C.Lambda (nn, ty, bo) -> *)
- (* let bo' = S.subst (M.apply_subst subst other) bo in *)
- (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
- (* not res *)
- (* | _ -> assert false *)
- (* in *)
- let condition left right what other (t, s, m, ug) =
- let subst = M.apply_subst s in
- let cmp1 = compare_terms (subst what) (subst other) in
- let cmp2 = compare_terms (subst left) (subst right) in
- (* cmp1 = Gt && cmp2 = Gt *)
- cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
- (* && (ok t s other right ug) *)
- in
- let metasenv' = metasenv @ newmetas @ newm' in
- let beta_expand = beta_expand ~metas_ok:false in
- let cmp1 = t_order (* compare_terms left right *)
- and cmp2 = s_order (* compare_terms t1 t2 *) in
- let res1, res2, res3, res4 =
- let res l r s t =
- List.filter
- (condition l r s t)
- (beta_expand s eq_ty l context metasenv' ugraph)
- in
- match cmp1, cmp2 with
- | Gt, Gt ->
- (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
- | Gt, Lt ->
- [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
- | Lt, Gt ->
- [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
- | Lt, Lt ->
- [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
- | Gt, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1 in
- res1, res2, [], []
- | Lt, _ ->
- let res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- [], [], res3, res4
- | _, Gt ->
- let res1 = res left right t1 t2
- and res3 = res right left t1 t2 in
- res1, [], res3, []
- | _, Lt ->
- let res2 = res left right t2 t1
- and res4 = res right left t2 t1 in
- [], res2, [], res4
- | _, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1
- and res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- res1, res2, res3, res4
- in
- let newmetas = newmetas @ newm' in
- let newargs = args @ args' in
- let build_new what other is_left eq_URI (t, s, m, ug) =
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let newterm, neweqproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- let bo' = M.apply_subst s (S.subst other bo) in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- eqproof; other; eqp'])
- | _ -> assert false
- in
- let newmeta, newequality =
- let left, right =
- if is_left then (newterm, M.apply_subst s right)
- else (M.apply_subst s left, newterm) in
- let neworder = compare_terms left right in
- fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
- in
- maxmeta := newmeta;
- newequality
- in
- let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
- and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
- and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
- let ok = function
- | _, (_, left, right, _), _, _ ->
- not (fst (CR.are_convertible context left right ugraph))
- in
- (!maxmeta,
- (List.filter ok (new1 @ new2 @ new3 @ new4)))
-;;
-*)
-
-
-let is_identity ((_, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+ | ((_, _, (ty, left, right, _), menv, _) as equality) ->
(left = right ||
- (meta_convertibility left right) ||
- (fst (CicReduction.are_convertible context left right ugraph)))
-;;
-
-
-(*
-let demodulation newmeta (metasenv, context, ugraph) target source =
- 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 proof, (eq_ty, left, right, t_order), metas, args = target
- and proof', (ty, t1, t2, s_order), metas', args' = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- newmeta, target
- else
- let first_step, get_params =
- match s_order (* compare_terms t1 t2 *) with
- | Gt -> 1, (function
- | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
- | _ -> assert false)
- | Lt -> 1, (function
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false)
- | _ ->
- let first_step = 3 in
- let get_params step =
- match step with
- | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false
- in
- first_step, get_params
- in
- let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right, t_order), metas, args = target in
- let is_left, what, other, eq_URI = get_params step in
-
- let env = metasenv, context, ugraph in
- let names = names_of_context context in
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-
- let ok (t, s, m, ug) =
- compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
- in
- let res =
- let r = (beta_expand ~metas_ok:false ~match_only:true
- what ty (if is_left then left else right)
- context (metasenv @ metas) ugraph)
- in
-(* let m' = metas_of_term what *)
-(* and m'' = metas_of_term (if is_left then left else right) in *)
-(* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-(* print_endline "res:"; *)
-(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
-(* print_newline (); *)
-(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(* print_newline (); *)
-(* ); *)
- List.filter ok r
- in
- match res with
- | [] ->
- if step = 0 then newmeta, target
- else demodulate newmeta (step-1) metasenv target
- | (t, s, m, ug)::_ ->
- let newterm, newproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
-(* let bo' = M.apply_subst s (S.subst other bo) in *)
- let bo' = S.subst (M.apply_subst s other) bo in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []);
- S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
-(* M.apply_subst s (S.subst other bo), *)
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; proof'])
- | _ -> assert false
- in
- let newmeta, newtarget =
- let left, right =
-(* if is_left then (newterm, M.apply_subst s right) *)
-(* else (M.apply_subst s left, newterm) in *)
- if is_left then newterm, right
- else left, newterm
- in
- let neworder = compare_terms left right in
-(* let newmetasenv = metasenv @ metas in *)
-(* let newargs = args @ args' in *)
-(* fix_metas newmeta *)
-(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
- let m = (metas_of_term left) @ (metas_of_term right) in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
- and newargs =
- List.filter
- (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
- args
- in
- newmeta,
- (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
- in
-(* Printf.printf *)
-(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
-(* (string_of_equality ~env newtarget) *)
-(* (string_of_equality ~env target); *)
-(* (\* let _, _, newm, newa = newtarget in *\) *)
-(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
-(* (\* (print_metasenv newm) *\) *)
-(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
-(* print_newline (); *)
- if is_identity env newtarget then
- newmeta, newtarget
- else
- demodulate newmeta first_step metasenv newtarget
- in
- demodulate newmeta first_step (metasenv @ metas') target
-;;
-
-
-(*
-let demodulation newmeta env target source =
- newmeta, target
-;;
-*)
-
-
-let subsumption env target source =
- let _, (ty, tl, tr, _), tmetas, _ = target
- and _, (ty', sl, sr, _), smetas, _ = source in
- if ty <> ty' then
- false
- else
- let metasenv, context, ugraph = env in
- let metasenv = metasenv @ tmetas @ smetas in
- let names = names_of_context context in
- let samesubst subst subst' =
-(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
-(* (print_subst subst) (print_subst subst'); *)
-(* print_newline (); *)
- let tbl = Hashtbl.create (List.length subst) in
- List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
- List.for_all
- (fun (m, (c, t1, t2)) ->
- try
- let c', t1', t2' = Hashtbl.find tbl m in
- if (c = c') && (t1 = t1') && (t2 = t2') then true
- else false
- with Not_found ->
- true)
- subst'
- in
- let subsaux left right left' right' =
- try
- let subst, menv, ug = matching metasenv context left left' ugraph
- and subst', menv', ug' = matching metasenv context right right' ugraph
- in
-(* Printf.printf "left = right: %s = %s\n" *)
-(* (CicPp.pp left names) (CicPp.pp right names); *)
-(* Printf.printf "left' = right': %s = %s\n" *)
-(* (CicPp.pp left' names) (CicPp.pp right' names); *)
- samesubst subst subst'
- with e ->
-(* print_endline (Printexc.to_string e); *)
- false
- in
- let res =
- if subsaux tl tr sl sr then true
- else subsaux tl tr sr sl
- in
- if res then (
- Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
- (string_of_equality ~env target) (string_of_equality ~env source);
- print_newline ();
- );
- res
-;;
-*)
-
-
-let extract_differing_subterms t1 t2 =
- let module C = Cic in
- let rec aux t1 t2 =
- match t1, t2 with
- | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
- [(t1, t2)]
- | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
- let res = List.concat (List.map2 aux tl1 tl2) in
- if h1 <> h2 then
- if res = [] then [(h1, h2)] else [(t1, t2)]
- else
- if List.length res > 1 then [(t1, t2)] else res
- | t1, t2 ->
- if t1 <> t2 then [(t1, t2)] else []
- in
- let res = aux t1 t2 in
- match res with
- | hd::[] -> Some hd
- | _ -> None
-;;
-
-
-let rec string_of_proof = function
- | NoProof -> "NoProof"
- | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
- | SubProof (t, i, p) ->
- Printf.sprintf "SubProof(%s, %s, %s)"
- (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
- | ProofSymBlock _ -> "ProofSymBlock"
- | ProofBlock _ -> "ProofBlock"
- | ProofGoalBlock (p1, p2) ->
- Printf.sprintf "ProofGoalBlock(%s, %s)"
- (string_of_proof p1) (string_of_proof p2)
+ (* (meta_convertibility left right) || *)
+ (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
;;
projects / helm.git / blobdiff