+(* 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;;
+type equality =
+ int * (* weight *)
+ proof *
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+
+and proof =
+ | NoProof
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri *
+ (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 string_of_equality ?env =
+ match env with
+ | None -> (
+ function
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
+ (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
+ )
+ | Some (_, context, _) -> (
+ let names = names_of_context context in
+ function
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
+ (CicPp.pp left names) (string_of_comparison o)
+ (CicPp.pp right names)
+ )
+;;
+
+
+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
+ | Cic.Constant (_, _, _, uris, _) ->
+ assert (List.length uris <= List.length termlist);
+ let rec aux = function
+ | [], tl -> [], tl
+ | (uri::uris), (term::tl) ->
+ let ens, args = aux (uris, tl) in
+ (uri, term)::ens, args
+ | _, _ -> assert false
+ in
+ aux (uris, termlist)
+ | _ -> assert false
+;;
+
+
+let build_proof_term proof =
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofGoalBlock (proofbit, proof) ->
+ print_endline "found ProofGoalBlock, going up...";
+ do_build_goal_proof proofbit 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, (pos, eq), eqproof) ->
+ let t' = Cic.Lambda (name, ty, bo) in
+ let proof' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+ let eqproof = do_build_proof eqproof in
+ let _, _, (ty, what, other, _), menv', args' = eq in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+ | SubProof (term, meta_index, proof) ->
+ let proof = do_build_proof proof in
+ let eq i = function
+ | Cic.Meta (j, _) -> i = j
+ | _ -> false
+ in
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
+
+ and do_build_goal_proof proofbit proof =
+ 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, poseq, eqproof) ->
+ let eqproof' = replace_proof newproof eqproof in
+ ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
+ | ProofGoalBlock (pb, p) ->
+ let pb' = replace_proof newproof pb in
+ ProofGoalBlock (pb', p)
+ | BasicProof _ -> newproof
+ | SubProof (term, meta_index, p) ->
+ SubProof (term, meta_index, replace_proof newproof p)
+ | p -> p
+ in
+ do_build_proof proof
+;;
+
+
+let rec metas_of_term = function
+ | Cic.Meta (i, c) -> [i]
+ | Cic.Var (_, ens)
+ | Cic.Const (_, ens)
+ | Cic.MutInd (_, _, ens)
+ | Cic.MutConstruct (_, _, _, ens) ->
+ List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+ | Cic.Cast (s, t)
+ | Cic.Prod (_, s, t)
+ | Cic.Lambda (_, s, t)
+ | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+ | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+ | Cic.MutCase (uri, i, s, t, l) ->
+ (metas_of_term s) @ (metas_of_term t) @
+ (List.flatten (List.map metas_of_term l))
+ | Cic.Fix (i, il) ->
+ List.flatten
+ (List.map (fun (s, i, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | Cic.CoFix (i, il) ->
+ List.flatten
+ (List.map (fun (s, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | _ -> []
+;;
+
+
exception NotMetaConvertible;;
let meta_convertibility_aux table t1 t2 =
let module C = Cic in
- let rec aux table t1 t2 =
+ let print_table t =
+ String.concat ", "
+ (List.map
+ (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+ in
+ let rec aux ((table_l, table_r) as table) t1 t2 =
match t1, t2 with
- | t1, t2 when t1 = t2 -> table
| C.Meta (m1, tl1), C.Meta (m2, tl2) ->
- let m1_binding, table =
- try List.assoc m1 table, table
- with Not_found -> m2, (m1, m2)::table
+ let m1_binding, table_l =
+ try List.assoc m1 table_l, table_l
+ with Not_found -> m2, (m1, m2)::table_l
+ and m2_binding, table_r =
+ try List.assoc m2 table_r, table_r
+ with Not_found -> m1, (m2, m1)::table_r
in
- if m1_binding <> m2 then
+ if (m1_binding <> m2) || (m2_binding <> m1) then
raise NotMetaConvertible
else (
try
| None, Some _ | Some _, None -> raise NotMetaConvertible
| None, None -> res
| Some t1, Some t2 -> (aux res t1 t2))
- table tl1 tl2
+ (table_l, table_r) tl1 tl2
with Invalid_argument _ ->
raise NotMetaConvertible
)
table il1 il2
with Invalid_argument _ -> raise NotMetaConvertible
)
+ | t1, t2 when t1 = t2 -> table
| _, _ -> raise NotMetaConvertible
and aux_ens table ens1 ens2 =
let meta_convertibility_eq eq1 eq2 =
- let _, (ty, left, right), _, _ = eq1
- and _, (ty', left', right'), _, _ = eq2 in
+ let _, _, (ty, left, right, _), _, _ = eq1
+ and _, _, (ty', left', right', _), _, _ = eq2 in
if ty <> ty' then
false
+ else if (left = left') && (right = right') then
+ true
+ else if (left = right') && (right = left') then
+ true
else
- let print_table t w =
- Printf.printf "table %s is:\n" w;
- List.iter
- (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
- t;
- print_newline ();
- in
try
- let table = meta_convertibility_aux [] left left' in
-(* print_table table "before"; *)
+ let table = meta_convertibility_aux ([], []) left left' in
let _ = meta_convertibility_aux table right right' in
-(* print_table table "after"; *)
true
with NotMetaConvertible ->
-(* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
-(* (CicPp.ppterm left) (CicPp.ppterm right) *)
-(* (CicPp.ppterm left') (CicPp.ppterm right'); *)
try
- let table = meta_convertibility_aux [] left right' in
+ let table = meta_convertibility_aux ([], []) left right' in
let _ = meta_convertibility_aux table right left' in
true
with NotMetaConvertible ->
let meta_convertibility t1 t2 =
- try
- let _ = meta_convertibility_aux [] t1 t2 in
+ let f t =
+ String.concat ", "
+ (List.map
+ (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+ in
+ if t1 = t2 then
true
- with NotMetaConvertible ->
- false
+ else
+ try
+ let l, r = meta_convertibility_aux ([], []) t1 t2 in
+ true
+ with NotMetaConvertible ->
+ false
;;
-let beta_expand ?(metas_ok=true) ?(match_only=false)
- what type_of_what where context metasenv ugraph =
- let module S = CicSubstitution in
+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) -> check_irl 1 l
+ | Cic.Rel _ -> true
+ | Cic.Const _ -> true
+ | Cic.MutInd (_, _, []) -> true
+ | Cic.MutConstruct (_, _, _, []) -> true
+ | _ -> false
+;;
+
+
+let lookup_subst meta subst =
+ match meta with
+ | Cic.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+;;
+
+
+let unification_simple metasenv context t1 t2 ugraph =
let module C = Cic 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'
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup = lookup_subst in
+ let rec occurs_check subst what where =
+ match where with
+ | t when what = t -> 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
+ | C.Meta (i, _), C.Meta (j, _) when i > j ->
+ unif subst menv t s
+ | C.Meta _, t when occurs_check subst s t ->
+ raise
+ (U.UnificationFailure (lazy "Inference.unification.unif"))
+ | C.Meta (i, l), t -> (
+ try
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let subst =
+ if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+ else subst
in
- (expansions, C.Const (uri, lifted_ens))
+ 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
+ (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 [] metasenv t1 t2 in
+ let menv =
+ List.filter
+ (fun (m, _, _) ->
+ try let _ = List.find (fun (i, _) -> m = i) subst in false
+ with Not_found -> true)
+ menv
+ in
+ List.rev subst, menv, ugraph
+;;
- | 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))
+let unification metasenv context t1 t2 ugraph =
+ 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)));
+ CicUnification.fo_unif metasenv context t1 t2 ugraph
+ ) else
+ unification_simple metasenv context t1 t2 ugraph
+ in
+ let rec fix_term = function
+ | (Cic.Meta (i, l) as t) ->
+ let t' = lookup_subst t subst in
+ if t <> t' then fix_term t' else t
+ | Cic.Appl l -> Cic.Appl (List.map fix_term l)
+ | t -> t
+ in
+ let rec fix_subst = function
+ | [] -> []
+ | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
+ in
+ fix_subst subst, menv, ug
+;;
- | 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
- | _ ->
- try
- let subst', metasenv', ugraph' =
- 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 term' = CicMetaSubst.apply_subst subst' term in
- if not (meta_convertibility term term') then (
-(* let names = names_of_context context in *)
-(* Printf.printf "\nterm e term' sono diversi!:\n%s\n%s\n\n" *)
-(* (CicPp.pp term names) (CicPp.pp term' names); *)
- res, lifted_term
- )
- else
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- else
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- with _ ->
- 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 ([], [])
+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
+ let module U = CicUnification in
+ let lookup meta subst =
+ match meta with
+ | C.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+ in
+ let rec do_match subst menv s t =
+ match s, t with
+ | s, t when s = t -> subst, menv
+ | s, C.Meta (i, l) ->
+ let filter_menv i menv =
+ List.filter (fun (m, _, _) -> i <> m) menv
+ in
+ let subst, menv =
+ let value = lookup t subst in
+ match value with
+ | value when value = t ->
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ (i, (context, s, ty))::subst, filter_menv i menv
+ | value when value <> s ->
+ raise MatchingFailure
+ | value -> do_match subst menv s value
+ in
+ subst, menv
+ | 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 _ ->
+ raise MatchingFailure
+ )
+ | _, _ ->
+ raise MatchingFailure
in
- let expansions, _ = aux 0 where context metasenv [] ugraph in
- List.map
- (fun (term, subst, metasenv, ugraph) ->
- let term' = C.Lambda (C.Anonymous, type_of_what, term) in
-(* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
-(* (CicPp.ppterm term') (print_subst subst); *)
- (term', subst, metasenv, ugraph))
- expansions
+ let subst, menv = do_match [] metasenv t1 t2 in
+ subst, menv, ugraph
;;
+*)
-type equality =
- Cic.term * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term) * (* right side *)
- Cic.metasenv * (* environment for metas *)
- Cic.term list (* arguments *)
+let matching metasenv context t1 t2 ugraph =
+ try
+ let subst, metasenv, ugraph =
+ unification metasenv context t1 t2 ugraph
+ in
+ let t' = CicMetaSubst.apply_subst subst t1 in
+ if not (meta_convertibility t1 t') then
+ raise MatchingFailure
+ else
+ let metas = metas_of_term t1 in
+ let fix_subst = function
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ (j, (c, Cic.Meta (i, lc), ty))
+ | s -> s
+ in
+ let subst = List.map fix_subst subst in
+ subst, metasenv, ugraph
+ with
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ raise MatchingFailure
;;
-let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
+let find_equalities context proof =
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
+ let eq_uri = LibraryObjects.eq_URI () in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let ok_types ty menv =
+ List.for_all (fun (_, _, mt) -> mt = ty) menv
+ in
let rec aux index newmeta = function
| [] -> [], newmeta
| (Some (_, C.Decl (term)))::tl ->
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, _) =
- PrimitiveTactics.new_metasenv_for_apply newmeta proof
- context (S.lift index term)
- in
- let newmeta =
- List.fold_left
- (fun maxm arg ->
- match arg with
- | C.Meta (i, _) -> (max maxm i)
- | _ -> assert false)
- newmeta args
+ let (head, newmetas, args, newmeta) =
+ ProofEngineHelpers.saturate_term newmeta []
+ context (S.lift index term) 0
in
let p =
if List.length args = 0 then
C.Appl ((C.Rel index)::args)
in (
match head with
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- Printf.printf "OK: %s\n" (CicPp.ppterm term);
- Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
+ debug_print
+ (lazy
+ (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+ Some e, (newmeta+1)
| _ -> None, newmeta
)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- Some (C.Rel index,
- (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when UriManager.eq uri eq_uri ->
+ let t1 = S.lift index t1
+ and t2 = S.lift index t2 in
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
+ Some e, (newmeta+1)
| _ -> None, newmeta
in (
match do_find context term with
| Some p, newmeta ->
let tl, newmeta' = (aux (index+1) newmeta tl) in
- p::tl, max newmeta newmeta'
+ (index, p)::tl, max newmeta newmeta'
| None, _ ->
aux (index+1) newmeta tl
)
| _::tl ->
aux (index+1) newmeta tl
in
- aux 1 newmeta context
+ let il, maxm = aux 1 newmeta context in
+ let indexes, equalities = List.split il in
+ indexes, equalities, maxm
;;
-let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
- let newargs, _ =
- List.fold_right
- (fun t (newargs, index) ->
- match t with
- | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
- | _ -> assert false)
- args ([], newmeta)
- in
- let repl where =
- ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
- ~where
- in
- let menv', _ =
- List.fold_right
- (fun (i, context, term) (menv, index) ->
- ((index, context, term)::menv, index+1))
- menv ([], newmeta)
- in
- (newmeta + (List.length newargs) + 1,
- (repl proof, (repl ty, repl left, repl right), menv', newargs))
+(*
+let equations_blacklist =
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
+ UriManager.UriSet.empty [
+ "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+ "cic:/Coq/Init/Logic/trans_eq.con";
+ "cic:/Coq/Init/Logic/f_equal.con";
+ "cic:/Coq/Init/Logic/f_equal2.con";
+ "cic:/Coq/Init/Logic/f_equal3.con";
+ "cic:/Coq/Init/Logic/f_equal4.con";
+ "cic:/Coq/Init/Logic/f_equal5.con";
+ "cic:/Coq/Init/Logic/sym_eq.con";
+ "cic:/Coq/Init/Logic/eq_ind.con";
+ "cic:/Coq/Init/Logic/eq_ind_r.con";
+ "cic:/Coq/Init/Logic/eq_rec.con";
+ "cic:/Coq/Init/Logic/eq_rec_r.con";
+ "cic:/Coq/Init/Logic/eq_rect.con";
+ "cic:/Coq/Init/Logic/eq_rect_r.con";
+ "cic:/Coq/Logic/Eqdep/UIP.con";
+ "cic:/Coq/Logic/Eqdep/UIP_refl.con";
+ "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
+ "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:/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;;
-exception TermIsNotAnEquality;;
-
-let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
- | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- (proof, (ty, t1, t2), [], [])
- | _ ->
- raise TermIsNotAnEquality
+let find_library_equalities dbd context status maxmeta =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let blacklist =
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add u s)
+ equations_blacklist
+ [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
+ eq_ind_r_URI ()]
+ in
+ let candidates =
+ List.fold_left
+ (fun l uri ->
+ let suri = UriManager.string_of_uri uri in
+ if UriManager.UriSet.mem uri blacklist then
+ l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
+ in
+ (uri, t, ty)::l)
+ []
+ (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 ()
+ and eq_uri2 = LibraryObjects.eq_URI () in
+ let iseq uri =
+ (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
+ in
+ let ok_types ty menv =
+ List.for_all (fun (_, _, mt) -> mt = ty) menv
+ in
+ let rec has_vars = function
+ | C.Meta _ | C.Rel _ | C.Const _ -> false
+ | C.Var _ -> true
+ | C.Appl l -> List.exists has_vars l
+ | C.Prod (_, s, t) | C.Lambda (_, s, t)
+ | C.LetIn (_, s, t) | C.Cast (s, t) ->
+ (has_vars s) || (has_vars t)
+ | _ -> false
+ in
+ let rec aux newmeta = function
+ | [] -> [], newmeta
+ | (uri, term, termty)::tl ->
+ debug_print
+ (lazy
+ (Printf.sprintf "Examining: %s (%s)"
+ (CicPp.ppterm term) (CicPp.ppterm termty)));
+ let res, newmeta =
+ match termty with
+ | C.Prod (name, s, t) when not (has_vars termty) ->
+ let head, newmetas, args, newmeta =
+ ProofEngineHelpers.saturate_term newmeta [] context termty 0
+ in
+ let p =
+ if List.length args = 0 then
+ term
+ else
+ C.Appl (term::args)
+ in (
+ match head with
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when (iseq uri) && (ok_types ty newmetas) ->
+ debug_print
+ (lazy
+ (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ )
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when iseq uri && not (has_vars termty) ->
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ in
+ match res with
+ | Some e ->
+ let tl, newmeta' = aux newmeta tl in
+ (uri, e)::tl, max newmeta newmeta'
+ | None ->
+ aux newmeta tl
+ in
+ let found, maxm = aux maxmeta candidates in
+ let uriset, eqlist =
+ (List.fold_left
+ (fun (s, l) (u, e) ->
+ 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, (u, e)::l))
+ (UriManager.UriSet.empty, []) found)
+ in
+ uriset, eqlist, maxm
;;
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-
-
-let superposition_left (metasenv, context, ugraph) target source =
+let find_library_theorems dbd env status equalities_uris =
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), _, _ = target in
- let eqproof, (ty, t1, t2), newmetas, args = source in
-
- (* ALB: TODO check that ty and eq_ty are indeed equal... *)
- assert (eq_ty = ty);
-
- let where, is_left =
- match nonrec_kbo 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... *)
- )
+ let module T = CicTypeChecker in
+ let blacklist =
+ let refl_equal =
+ UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
+ let s =
+ UriManager.UriSet.remove refl_equal
+ (UriManager.UriSet.union equalities_uris equations_blacklist)
+ in
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add u s)
+ s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
+ eq_ind_r_URI ()]
in
- let metasenv' = newmetas @ metasenv in
- let res1 =
- List.filter
- (fun (t, s, m, ug) ->
- nonrec_kbo (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) ->
- nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
- (beta_expand t2 ty where context metasenv' ugraph)
+ let metasenv, context, ugraph = env in
+ let candidates =
+ List.fold_left
+ (fun l uri ->
+ if UriManager.UriSet.mem uri blacklist then l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
+ (t, ty, [])::l)
+ [] (MetadataQuery.signature_of_goal ~dbd status)
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)
- else (eq_ty, left, newgoal)
- in
- (eqproof, equation, [], [])
+ 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
+ (t, ty, [])
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
+ refl_equal::candidates
;;
-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), newmetas, args = target in
- let eqp', (ty', t1, t2), newm', args' = source in
- let maxmeta = ref newmeta in
-
- (* TODO check if ty and ty' are equal... *)
- assert (eq_ty = ty');
-
-(* 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 = nonrec_kbo (subst what) (subst other) in
- let cmp2 = nonrec_kbo (subst left) (subst right) in
-(* cmp1 = Gt && cmp2 = Gt *)
- cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
-(* && (ok t s other right ug) *)
+let find_context_hypotheses env equalities_indexes =
+ let metasenv, context, ugraph = env in
+ let _, res =
+ List.fold_left
+ (fun (n, l) entry ->
+ match entry with
+ | None -> (n+1, l)
+ | Some _ ->
+ if List.mem n equalities_indexes then
+ (n+1, l)
+ else
+ let t = Cic.Rel n in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' metasenv context t ugraph in
+ (n+1, (t, ty, [])::l))
+ (1, []) context
in
- let metasenv' = metasenv @ newmetas @ newm' in
- let beta_expand = beta_expand ~metas_ok:false in
- let res1 =
- List.filter
- (condition left right t1 t2)
- (beta_expand t1 eq_ty left context metasenv' ugraph)
- and res2 =
- List.filter
- (condition left right t2 t1)
- (beta_expand t2 eq_ty left context metasenv' ugraph)
- and res3 =
- List.filter
- (condition right left t1 t2)
- (beta_expand t1 eq_ty right context metasenv' ugraph)
- and res4 =
+ res
+;;
+
+
+let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+ let table = Hashtbl.create (List.length args) in
+ let newargs, newmeta =
+ List.fold_right
+ (fun t (newargs, index) ->
+ match t with
+ | Cic.Meta (i, l) ->
+ if Hashtbl.mem table i then
+ let idx = Hashtbl.find table i in
+ ((Cic.Meta (idx, l))::newargs, index+1)
+ else
+ let _ = Hashtbl.add table i index in
+ ((Cic.Meta (index, l))::newargs, index+1)
+ | _ -> assert false)
+ args ([], newmeta+1)
+ in
+ let repl where =
+ ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
+ ~where
+ in
+ let menv' =
+ List.fold_right
+ (fun (i, context, term) menv ->
+ try
+ let index = Hashtbl.find table i in
+ (index, context, term)::menv
+ with Not_found ->
+ (i, context, term)::menv)
+ menv []
+ in
+ let ty = repl ty
+ and left = repl left
+ and right = repl right in
+ let metas = (metas_of_term left) @ (metas_of_term right) in
+ let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
+ let newargs =
List.filter
- (condition right left t2 t1)
- (beta_expand t2 eq_ty right context metasenv' ugraph)
+ (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
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
- fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right), newmetas, newargs)
- in
- maxmeta := newmeta;
- newequality
+ 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
+ (function Cic.Meta (i, _) -> i = v | _ -> assert false)
+ newargs) then
+ Hashtbl.replace table k first)
+ (Hashtbl.copy table)
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))
+ let rec fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof term -> BasicProof (repl term)
+ | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
+ let subst' =
+ List.fold_left
+ (fun s arg ->
+ match arg with
+ | Cic.Meta (i, l) -> (
+ try
+ let j = Hashtbl.find table i in
+ if List.mem_assoc i subst then
+ s
+ else
+ let _, context, ty = CicUtil.lookup_meta i menv in
+ (i, (context, Cic.Meta (j, l), ty))::s
+ with Not_found | CicUtil.Meta_not_found _ ->
+ s
+ )
+ | _ -> assert false)
+ [] args
+ in
+ ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
+ | p -> assert false
in
- !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+ let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
+ (newmeta + 1, neweq)
;;
-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 term_is_equality term =
+ let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+ match term with
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+ | _ -> false
+;;
- let proof, (eq_ty, left, right), metas, args = target
- and proof', (ty, t1, t2), metas', args' = source in
- if eq_ty <> ty then
- newmeta, target
- else
- 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
- let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right), 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\n" step; *)
-(* print_newline (); *)
-
- let ok (t, s, m, ug) =
- nonrec_kbo (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
-(* print_endline "res:"; *)
-(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
- 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'' =
- 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),
- 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
- let newmetasenv = metasenv @ metas in
- let newargs = args @ args' in
- fix_metas newmeta
- (newproof, (eq_ty, left, right), newmetasenv, newargs)
- in
-(* Printf.printf *)
-(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
-(* (string_of_equality ~env newtarget) *)
-(* (string_of_equality ~env target); *)
-(* print_newline (); *)
- demodulate newmeta step metasenv newtarget
- in
- demodulate newmeta 3 (metasenv @ metas') target
+exception TermIsNotAnEquality;;
+
+let equality_of_term proof term =
+ let eq_uri = LibraryObjects.eq_URI () in
+ let iseq uri = UriManager.eq uri eq_uri in
+ match term with
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
+ e
+ | _ ->
+ raise TermIsNotAnEquality
;;
-(*
-let demodulation newmeta env target source =
- newmeta, target
-;;
-*)
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+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
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
+;;
projects / helm.git / blobdiff