type equality =
- Cic.term * (* proof *)
+ 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 *)
-;;
-
-type proof =
+and proof =
+ | NoProof
| BasicProof of Cic.term
| ProofBlock of
- Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
- equality
- | NoProof
+ 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
;;
match env with
| None -> (
function
- | _, (ty, left, right, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+ | 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
- | _, (ty, left, right, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+ | 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 prooftable = Hashtbl.create 2001;;
+let build_proof_term equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
-let store_proof equality proof =
- if not (Hashtbl.mem prooftable equality) then
- Hashtbl.add prooftable equality proof
-;;
+ let indent = ref 0 in
+
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+(* (string_of_equality equality); *)
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofGoalBlock (proofbit, proof (* equality *)) ->
+ print_endline "found ProofGoalBlock, going up...";
+(* let _, proof, _, _, _ = equality in *)
+ do_build_goal_proof proofbit proof
+ | ProofSymBlock (ens, proof) ->
+ let proof = do_build_proof proof in
+ Cic.Appl [
+ Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
+ proof
+ ]
+ | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
+(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
+(* print_newline (); *)
+(* let name, ty, eq_ty, left, right = t' in *)
+(* let bo = *)
+(* Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); *)
+(* eq_ty; left; right] *)
+(* in *)
+ let t' = Cic.Lambda (name, ty, bo) in
+ (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+ (* (string_of_equality eq) (string_of_equality eq'); *)
+ (* print_newline (); *)
-let delete_proof equality =
-(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
-(* print_newline (); *)
- Hashtbl.remove prooftable equality
-;;
+(* let s = String.make !indent ' ' in *)
+(* incr indent; *)
+
+(* print_endline (s ^ "build proof'------------"); *)
+
+ let proof' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+(* print_endline (s ^ "END proof'"); *)
+(* print_endline (s ^ "build eqproof-----------"); *)
-let rec build_term_proof equality =
-(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
-(* print_newline (); *)
- let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
- match proof with
- | NoProof ->
- Printf.fprintf stderr "WARNING: no proof for %s\n"
- (string_of_equality equality);
- Cic.Implicit None
- | BasicProof term -> term
- | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
-(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
-(* (string_of_equality eq) (string_of_equality eq'); *)
-(* print_newline (); *)
- let proof' = build_term_proof eq in
- let eqproof = build_term_proof eq' 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'])
+ let eqproof = do_build_proof eqproof in
+
+(* print_endline (s ^ "END eqproof"); *)
+(* decr indent; *)
+
+
+ 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'])
+
+ 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 *)
+
+ and replace_proof newproof = function
+ | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
+ let eqproof' = replace_proof newproof eqproof in
+ ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
+ | ProofGoalBlock (pb, p(* equality *)) ->
+ 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)) *)
+ | BasicProof _ -> newproof
+ | p -> p
+ in
+ let _, proof, _, _, _ = equality in
+ do_build_proof proof
;;
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
;;
+(*
let replace_metas (* context *) term =
let module C = Cic in
let rec aux = function
in
aux term
;;
+*)
+(*
let restore_metas (* context *) term =
let module C = Cic in
let rec aux = function
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
| 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 module U = CicUnification in
let lookup = lookup_subst in
let rec occurs_check subst what where =
- (* Printf.printf "occurs_check %s %s" *)
- (* (CicPp.ppterm what) (CicPp.ppterm where); *)
- (* print_newline (); *)
match where with
| t when what = t -> true
| C.Appl l -> List.exists (occurs_check subst what) l
| _ -> false
in
let rec unif subst menv s t =
-(* Printf.printf "unif %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
and 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 ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
- raise (U.UnificationFailure "Inference.unification.unif")
-(* | C.Meta (i, l), C.Meta (j, l') -> *)
-(* let _, _, ty = CicUtil.lookup_meta i menv in *)
-(* let _, _, ty' = CicUtil.lookup_meta j menv in *)
-(* let binding1 = lookup s subst in *)
-(* let binding2 = lookup t subst in *)
-(* let subst, menv = *)
-(* if binding1 != s then *)
-(* if binding2 != t then *)
-(* unif subst menv binding1 binding2 *)
-(* else *)
-(* if binding1 = t then *)
-(* subst, menv *)
-(* else *)
-(* ((j, (context, binding1, ty'))::subst, *)
-(* List.filter (fun (m, _, _) -> j <> m) menv) *)
-(* else *)
-(* if binding2 != t then *)
-(* if s = binding2 then *)
-(* subst, menv *)
-(* else *)
-(* ((i, (context, binding2, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* else *)
-(* ((i, (context, t, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* in *)
-(* subst, menv *)
-
- | C.Meta (i, l), t ->
- 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
- let menv = List.filter (fun (m, _, _) -> i <> m) menv in
- subst, menv
+ raise (U.UnificationFailure (U.failure_msg_of_string "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
+ 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 "Inference.unification.unif")
+ raise (U.UnificationFailure (U.failure_msg_of_string "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 e ->
- raise (U.UnificationFailure "Inference.unification.unif")
+ with Invalid_argument _ ->
+ raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
)
- | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+ | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
- (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
- (* print_newline (); *)
-(* let rec fix_term = function *)
-(* | (C.Meta (i, l) as t) -> *)
-(* lookup t subst *)
-(* | C.Appl l -> C.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 *)
-(* List.rev (fix_subst subst), menv, ugraph *)
+ 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
;;
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
+ 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
+ ) else
unification_simple metasenv context t1 t2 ugraph
in
let rec fix_term = function
in
(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
(* print_endline "|"; *)
- (* fix_subst *) subst, menv, ug
+ fix_subst subst, menv, ug
;;
+
(* let unification = CicUnification.fo_unif;; *)
exception MatchingFailure;;
List.fold_left2
(fun (subst, menv) s t -> do_match subst menv s t)
(subst, menv) ls lt
- with e ->
+ with Invalid_argument _ ->
(* print_endline (Printexc.to_string e); *)
(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
(* print_newline (); *)
(* (\* print_newline (); *\) *)
(* subst, menv, ug *)
(* else *)
+(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+(* print_newline (); *)
try
let subst, metasenv, ugraph =
(* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
(* print_newline (); *)
subst, metasenv, ugraph
- with e ->
+ 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 module S = CicSubstitution in
let module C = Cic in
- let print_info = false in
-
(* let _ = *)
(* let names = names_of_context context in *)
(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
(* else *)
((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
lifted_term)
- with e ->
- if print_info then (
- print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
- );
- res, lifted_term
+ with
+ | MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ res, lifted_term
in
(* Printf.printf "exit aux\n"; *)
retval
(* if match_only then replace_metas (\* context *\) where *)
(* else where *)
(* in *)
- if print_info then (
- Printf.printf "searching %s inside %s\n"
- (CicPp.ppterm what) (CicPp.ppterm where);
- );
aux 0 where context metasenv [] ugraph
in
let mapfun =
let module S = CicSubstitution in
let module T = CicTypeChecker 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 ->
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);
+ | 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)));
+(* debug_print (lazy ( *)
+(* 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 e = (p, (ty, t1, t2, o), newmetas, args) in
- store_proof e (BasicProof p);
+ 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 ->
+ | 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 e = (C.Rel index, (ty, t1, t2, o), [], []) in
- store_proof e (BasicProof (C.Rel index));
+ 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 (
;;
-let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
+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/sym_eq.con";
+(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
+(* "cic:/Coq/Init/Peano/mult_n_Sm.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";
+ ]
+ ;;
+
+let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let candidates =
+ List.fold_left
+ (fun l uri ->
+ let suri = UriManager.string_of_uri uri in
+ if UriManager.UriSet.mem uri equations_blacklist then
+ l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
+ in
+ (t, ty)::l)
+ []
+ (MetadataQuery.equations_for_goal ~dbd status)
+ in
+ let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
+ and eq_uri2 = HelmLibraryObjects.Logic.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 aux newmeta = function
+ | [] -> [], newmeta
+ | (term, termty)::tl ->
+ debug_print (lazy (
+ Printf.sprintf "Examining: %s (%s)"
+ (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
+ let res, newmeta =
+ match termty with
+ | C.Prod (name, s, t) ->
+ 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 ->
+ 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
+ e::tl, max newmeta newmeta'
+ | None ->
+ aux newmeta tl
+ in
+ let found, maxm = aux maxmeta candidates in
+ (List.fold_left
+ (fun l e ->
+ if List.exists (meta_convertibility_eq e) l then (
+ debug_print (lazy (
+ Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
+ l
+ )
+ else e::l)
+ [] found), maxm
+;;
+
+
+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 newargs, _ =
+ let is_this_case = ref false in
+ let newargs, newmeta =
List.fold_right
(fun t (newargs, index) ->
match t with
| Cic.Meta (i, l) ->
- Hashtbl.add table i index;
- ((Cic.Meta (index, l))::newargs, index+1)
+ 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)
+ args ([], newmeta+1)
in
let repl where =
ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
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'
- and newargs =
+ let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
+ let newargs =
List.filter
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
- (newmeta + (List.length newargs) + 1,
- (repl proof, (ty, left, right, o), menv', newargs))
+ let table' = Hashtbl.copy table in
+ let first = List.hd metas in
+ let _ =
+ Hashtbl.iter
+ (fun k v ->
+ if not (List.exists
+ (function Cic.Meta (i, _) -> i = v | _ -> assert false)
+ newargs) then
+ Hashtbl.replace table k first)
+ table'
+ in
+(* debug_print *)
+(* (Printf.sprintf "args: %s\nnewargs: %s\n" *)
+(* (String.concat "; " (List.map CicPp.ppterm args)) *)
+(* (String.concat "; " (List.map CicPp.ppterm newargs))); *)
+
+ let rec fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof term ->
+(* let term' = repl term in *)
+(* debug_print *)
+(* (Printf.sprintf "term was: %s\nterm' is: %s\n" *)
+(* (CicPp.ppterm term) (CicPp.ppterm 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; *)
+ 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 ->
+(* 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 neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
+ (newmeta + 1, neweq)
+;;
+
+
+let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
+ let iseq uri = UriManager.eq uri eq_uri in
+ match term with
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+ | _ -> false
;;
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 ->
+let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
+ 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 e = (proof, (ty, t1, t2, o), [], []) in
- store_proof e (BasicProof proof);
+ 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), [], []) *)
| _ ->
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
(!maxmeta,
(List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
+*)
let is_identity ((_, context, ugraph) as env) = function
- | ((_, (ty, left, right, _), _, _) as equality) ->
- let res =
- (left = right ||
- (fst (CicReduction.are_convertible context left right ugraph)))
- in
-(* if res then ( *)
-(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(* print_newline (); *)
-(* ); *)
- res
+ | ((_, _, (ty, left, right, _), _, _) 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
);
res
;;
+*)
let extract_differing_subterms t1 t2 =
| hd::[] -> Some hd
| _ -> None
;;
+
+