proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
metadataQuery.cmi: proofEngineTypes.cmi
-paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi
+paramodulation/equality.cmi: paramodulation/utils.cmi
+paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
+ paramodulation/equality.cmi
paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
- paramodulation/inference.cmi
+ paramodulation/equality.cmi
paramodulation/indexing.cmi: paramodulation/utils.cmi \
- paramodulation/inference.cmi paramodulation/equality_indexing.cmi
+ paramodulation/equality_indexing.cmi paramodulation/equality.cmi
paramodulation/saturation.cmi: proofEngineTypes.cmi
variousTactics.cmi: proofEngineTypes.cmi
autoTactic.cmi: proofEngineTypes.cmi
hashtbl_equiv.cmx metadataQuery.cmi
paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi
paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
-paramodulation/inference.cmo: paramodulation/utils.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi metadataQuery.cmi \
+paramodulation/equality.cmo: paramodulation/utils.cmi \
+ proofEngineReduction.cmi paramodulation/equality.cmi
+paramodulation/equality.cmx: paramodulation/utils.cmx \
+ proofEngineReduction.cmx paramodulation/equality.cmi
+paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \
+ metadataQuery.cmi paramodulation/equality.cmi \
paramodulation/inference.cmi
-paramodulation/inference.cmx: paramodulation/utils.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx metadataQuery.cmx \
+paramodulation/inference.cmx: paramodulation/utils.cmx proofEngineHelpers.cmx \
+ metadataQuery.cmx paramodulation/equality.cmx \
paramodulation/inference.cmi
paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
- paramodulation/inference.cmi paramodulation/equality_indexing.cmi
+ paramodulation/equality.cmi paramodulation/equality_indexing.cmi
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
- paramodulation/inference.cmx paramodulation/equality_indexing.cmi
+ paramodulation/equality.cmx paramodulation/equality_indexing.cmi
paramodulation/indexing.cmo: paramodulation/utils.cmi \
paramodulation/inference.cmi paramodulation/equality_indexing.cmi \
- paramodulation/indexing.cmi
+ paramodulation/equality.cmi paramodulation/indexing.cmi
paramodulation/indexing.cmx: paramodulation/utils.cmx \
paramodulation/inference.cmx paramodulation/equality_indexing.cmx \
- paramodulation/indexing.cmi
+ paramodulation/equality.cmx paramodulation/indexing.cmi
paramodulation/saturation.cmo: paramodulation/utils.cmi reductionTactics.cmi \
proofEngineTypes.cmi proofEngineReduction.cmi primitiveTactics.cmi \
paramodulation/inference.cmi paramodulation/indexing.cmi \
- paramodulation/saturation.cmi
+ paramodulation/equality.cmi paramodulation/saturation.cmi
paramodulation/saturation.cmx: paramodulation/utils.cmx reductionTactics.cmx \
proofEngineTypes.cmx proofEngineReduction.cmx primitiveTactics.cmx \
paramodulation/inference.cmx paramodulation/indexing.cmx \
- paramodulation/saturation.cmi
+ paramodulation/equality.cmx paramodulation/saturation.cmi
variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
variousTactics.cmi
variousTactics.cmi
autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \
- paramodulation/inference.cmi autoTactic.cmi
+ paramodulation/equality.cmi autoTactic.cmi
autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
- paramodulation/inference.cmx autoTactic.cmi
+ paramodulation/equality.cmx autoTactic.cmi
introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
introductionTactics.cmi
introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
paramodulation/utils.mli \
+ paramodulation/equality.mli\
paramodulation/inference.mli\
paramodulation/equality_indexing.mli\
paramodulation/indexing.mli \
| Some _ ->
let _, metasenv, _, _ = proof in
let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- full || (Inference.term_is_equality meta_goal)
+ full || (Equality.term_is_equality meta_goal)
in
if paramodulation_ok then (
debug_print (lazy "USO PARAMODULATION...");
--- /dev/null
+(* cOpyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
+
+
+(******* CIC substitution ***************************************************)
+
+type cic_substitution = Cic.substitution
+let cic_apply_subst = CicMetaSubst.apply_subst
+let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
+let cic_ppsubst = CicMetaSubst.ppsubst
+let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
+let cic_flatten_subst subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = (* cic_apply_subst_context subst*) context in
+ let term = cic_apply_subst subst term in
+ let ty = cic_apply_subst subst ty in
+ (i, (context, term, ty))) subst
+let rec cic_lookup_subst meta subst =
+ match meta with
+ | Cic.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
+ in cic_lookup_subst t subst
+ with Not_found -> meta
+ )
+ | _ -> meta
+;;
+
+let cic_merge_subst_if_possible s1 s2 =
+ let already_in = Hashtbl.create 13 in
+ let rec aux acc = function
+ | ((i,_,x) as s)::tl ->
+ (try
+ let x' = Hashtbl.find already_in i in
+ if x = x' then aux acc tl else None
+ with
+ | Not_found ->
+ Hashtbl.add already_in i x;
+ aux (s::acc) tl)
+ | [] -> Some acc
+ in
+ aux [] (s1@s2)
+;;
+
+(******** NAIF substitution **************************************************)
+(*
+ * naif version of apply subst; the local context of metas is ignored;
+ * we assume the substituted term must be lifted according to the nesting
+ * depth of the meta.
+ * Alternatively, we could used implicit instead of metas
+ *)
+
+type naif_substitution = (int * Cic.term) list
+
+let naif_apply_subst subst term =
+ let rec aux k t =
+ match t with
+ Cic.Rel _ -> t
+ | Cic.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+ in
+ Cic.Var (uri, exp_named_subst')
+ | Cic.Meta (i, l) ->
+ (try
+ aux k (CicSubstitution.lift k (List.assoc i subst))
+ with Not_found -> t)
+ | Cic.Sort _
+ | Cic.Implicit _ -> t
+ | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
+ | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
+ | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
+ | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+ | Cic.Appl [] -> assert false
+ | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
+ | Cic.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+ in
+ if exp_named_subst' != exp_named_subst then
+ Cic.Const (uri, exp_named_subst')
+ else
+ t (* TODO: provare a mantenere il piu' possibile sharing *)
+ | Cic.MutInd (uri,typeno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+ in
+ Cic.MutInd (uri,typeno,exp_named_subst')
+ | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+ in
+ Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
+ | Cic.MutCase (sp,i,outty,t,pl) ->
+ let pl' = List.map (aux k) pl in
+ Cic.MutCase (sp, i, aux k outty, aux k t, pl')
+ | Cic.Fix (i, fl) ->
+ let len = List.length fl in
+ let fl' =
+ List.map
+ (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
+ in
+ Cic.Fix (i, fl')
+ | Cic.CoFix (i, fl) ->
+ let len = List.length fl in
+ let fl' =
+ List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
+ in
+ Cic.CoFix (i, fl')
+in
+ aux 0 term
+;;
+
+(* naif version of apply_subst_metasenv: we do not apply the
+substitution to the context *)
+
+let naif_apply_subst_metasenv subst metasenv =
+ List.map
+ (fun (n, context, ty) ->
+ (n, context, naif_apply_subst subst ty))
+ (List.filter
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
+ metasenv)
+
+let naif_ppsubst names subst =
+ "{" ^ String.concat "; "
+ (List.map
+ (fun (idx, t) ->
+ Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
+ subst) ^ "}"
+;;
+
+let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
+
+let naif_flatten_subst subst =
+ List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+;;
+
+let rec naif_lookup_subst meta subst =
+ match meta with
+ | Cic.Meta (i, _) ->
+ (try
+ naif_lookup_subst (List.assoc i subst) subst
+ with
+ Not_found -> meta)
+ | _ -> meta
+;;
+
+let naif_merge_subst_if_possible s1 s2 =
+ let already_in = Hashtbl.create 13 in
+ let rec aux acc = function
+ | ((i,x) as s)::tl ->
+ (try
+ let x' = Hashtbl.find already_in i in
+ if x = x' then aux acc tl else None
+ with
+ | Not_found ->
+ Hashtbl.add already_in i x;
+ aux (s::acc) tl)
+ | [] -> Some acc
+ in
+ aux [] (s1@s2)
+;;
+
+(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
+
+type substitution = naif_substitution
+let apply_subst = naif_apply_subst
+let apply_subst_metasenv = naif_apply_subst_metasenv
+let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
+let buildsubst = naif_buildsubst
+let flatten_subst = naif_flatten_subst
+let lookup_subst = naif_lookup_subst
+
+(* filter out from metasenv the variables in substs *)
+let filter subst metasenv =
+ List.filter
+ (fun (m, _, _) ->
+ try let _ = List.find (fun (i, _) -> m = i) subst in false
+ with Not_found -> true)
+ metasenv
+;;
+
+let is_in_subst i subst = List.mem_assoc i subst;;
+
+let merge_subst_if_possible = naif_merge_subst_if_possible;;
+
+let empty_subst = [];;
+
+(********* EQUALITY **********************************************************)
+
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type uncomparable = int -> int
+type equality =
+ uncomparable * (* trick to break structural equality *)
+ int * (* weight *)
+ proof *
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ int (* id *)
+and proof = new_proof * old_proof
+
+and new_proof =
+ | Exact of Cic.term
+ | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)
+and old_proof =
+ | NoProof (* term is the goal missing a proof *)
+ | BasicProof of substitution * Cic.term
+ | ProofBlock of
+ substitution * UriManager.uri *
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
+ | ProofGoalBlock of old_proof * old_proof
+ | ProofSymBlock of Cic.term list * old_proof
+ | SubProof of Cic.term * int * old_proof
+and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+;;
+
+(* globals *)
+let maxid = ref 0;;
+let id_to_eq = Hashtbl.create 1024;;
+
+let freshid () =
+ incr maxid; !maxid
+;;
+
+let reset () =
+ maxid := 0;
+ Hashtbl.clear id_to_eq
+;;
+
+let uncomparable = fun _ -> 0
+
+let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+ let id = freshid () in
+ let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+ Hashtbl.add id_to_eq id eq;
+ eq
+;;
+
+let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
+ (weight,proof,(ty,l,r,o),m,id)
+
+let string_of_equality ?env eq =
+ match env with
+ | None ->
+ let w, _, (ty, left, right, o), _ , id = open_equality eq in
+ Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
+ id w (CicPp.ppterm ty)
+ (CicPp.ppterm left)
+ (Utils.string_of_comparison o) (CicPp.ppterm right)
+ | Some (_, context, _) ->
+ let names = Utils.names_of_context context in
+ let w, _, (ty, left, right, o), _ , id = open_equality eq in
+ Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
+ id w (CicPp.pp ty names)
+ (CicPp.pp left names) (Utils.string_of_comparison o)
+ (CicPp.pp right names)
+;;
+
+let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
+ Pervasives.compare s1 s2
+;;
+
+let rec string_of_proof_old ?(names=[]) = function
+ | NoProof -> "NoProof "
+ | BasicProof (s, t) -> "BasicProof(" ^
+ ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
+ | SubProof (t, i, p) ->
+ Printf.sprintf "SubProof(%s, %s, %s)"
+ (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
+ | ProofSymBlock (_,p) ->
+ Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
+ | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
+ let _,(_,p),_,_,_ = open_equality eq in
+ "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
+ string_of_proof_old p ^ ")"
+ | ProofGoalBlock (p1, p2) ->
+ Printf.sprintf "ProofGoalBlock(%s, %s)"
+ (string_of_proof_old p1) (string_of_proof_old p2)
+;;
+
+
+let proof_of_id id =
+ try
+ let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+ p,m,l,r
+ with
+ Not_found -> assert false
+
+
+let string_of_proof_new ?(names=[]) p gp =
+ let str_of_rule = function
+ | SuperpositionRight -> "SupR"
+ | SuperpositionLeft -> "SupL"
+ | Demodulation -> "Demod"
+ in
+ let str_of_pos = function
+ | Utils.Left -> "left"
+ | Utils.Right -> "right"
+ in
+ let fst4 (x,_,_,_) = x in
+ let rec aux margin name =
+ let prefix = String.make margin ' ' ^ name ^ ": " in function
+ | Exact t ->
+ Printf.sprintf "%sExact (%s)\n"
+ prefix (CicPp.pp t names)
+ | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
+ Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
+ prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
+ (CicPp.pp pred names)^
+ aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^
+ aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2))
+ in
+ aux 0 "" p ^
+ String.concat "\n"
+ (List.map
+ (fun (pos,i,s,t) ->
+ (Printf.sprintf
+ "GOAL: %s %d %s %s\n"
+ (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
+ aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
+ gp)
+;;
+
+let ppsubst = ppsubst ~names:[]
+
+(* 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_old ?(noproof=Cic.Implicit None) proof =
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+ noproof
+ | BasicProof (s,term) -> apply_subst s 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), (ty, what, other, _), menv',_ = open_equality eq in
+ let proof' = do_build_proof proof in
+ let eqproof = do_build_proof eqproof in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ 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 build_proof_term_new proof =
+ let rec aux extra = function
+ | Exact term -> term, []
+ | Step (subst,(_, id1, (pos,id2), pred)) ->
+ let p,m1,_,_ = proof_of_id id1 in
+ let p1,m2 = aux [] p in
+ let p,m3,l,r = proof_of_id id2 in
+ let p2,m4 = aux [] p in
+ let p1 = apply_subst subst p1 in
+ let p2 = apply_subst subst p2 in
+ let l = apply_subst subst l in
+ let r = apply_subst subst r in
+ let pred = apply_subst subst pred in
+ let ty = (* Cic.Implicit None *)
+ match pred with
+ | Cic.Lambda (_,ty,_) -> ty
+ | _ -> assert false
+ in
+ let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+ if pos = Utils.Left then l,r else r,l
+ in
+ let eq_URI =
+ match pos with
+ | Utils.Left -> Utils.eq_ind_URI ()
+ | Utils.Right -> Utils.eq_ind_r_URI ()
+ in
+ (Cic.Appl [
+ Cic.Const (eq_URI, []);
+ ty; what; pred; p1; other; p2]),
+ (apply_subst_metasenv subst (m1@m2@m3@m4))
+ in
+ aux [] proof
+
+
+let build_goal_proof l (refl,reflmenv) =
+ let proof, menv, subst =
+ List.fold_left
+ (fun (current_proof,current_menv,current_subst) (pos,id,subst,pred) ->
+ let p,m,l,r = proof_of_id id in
+ let p,m1 = build_proof_term_new p in
+ let p = apply_subst subst p in
+ let l = apply_subst subst l in
+ let r = apply_subst subst r in
+ let pred = apply_subst subst pred in
+ let newm = apply_subst_metasenv subst (m@m1) in
+ let ty = (* Cic.Implicit None *)
+ match pred with
+ | Cic.Lambda (_,ty,_) -> ty
+ | _ -> assert false
+ in
+ let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+ if pos = Utils.Right then l,r else r,l
+ in
+ let eq_URI =
+ match pos with
+ | Utils.Left -> Utils.eq_ind_r_URI ()
+ | Utils.Right -> Utils.eq_ind_URI ()
+ in
+ ((Cic.Appl [Cic.Const (eq_URI, []);
+ ty; what; pred; current_proof; other; p]),
+ current_menv @ newm, subst @ current_subst))
+ (refl,reflmenv,[]) l
+ in
+ proof, menv
+;;
+
+let refl_proof ty term =
+ Cic.Appl
+ [Cic.MutConstruct
+ (LibraryObjects.eq_URI (), 0, 1, []);
+ ty; term]
+;;
+
+let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+
+let relocate newmeta menv =
+ let subst, metasenv, newmeta =
+ List.fold_right
+ (fun (i, context, ty) (subst, menv, maxmeta) ->
+ let irl = [] (*
+ CicMkImplicit.identity_relocation_list_for_metavariable context *)
+ in
+ let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
+ let newmeta = maxmeta, context, ty in
+ newsubst, newmeta::menv, maxmeta+1)
+ menv ([], [], newmeta+1)
+ in
+ let metasenv = apply_subst_metasenv subst metasenv in
+ let subst = flatten_subst subst in
+ subst, metasenv, newmeta
+
+
+let fix_metas newmeta eq =
+ let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
+ (* debug
+ let _ , eq =
+ fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
+ prerr_endline (string_of_equality eq); *)
+ let subst, metasenv, newmeta = relocate newmeta menv in
+ let ty = apply_subst subst ty in
+ let left = apply_subst subst left in
+ let right = apply_subst subst right in
+ let fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof (subst',term) -> BasicProof (subst@subst',term)
+ | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
+ (*
+ let newsubst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = apply_subst_context subst context in
+ let term = apply_subst subst term in
+ let ty = apply_subst subst ty in
+ (i, (context, term, ty))) subst' in *)
+ ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
+ | p -> assert false
+ in
+ let fix_new_proof = function
+ | Exact p -> Exact (apply_subst subst p)
+ | Step (s,(r,id1,(pos,id2),pred)) ->
+ Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+ in
+ let new_p = fix_new_proof p1 in
+ let old_p = fix_proof p2 in
+ let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
+ (* debug prerr_endline (string_of_equality eq); *)
+ newmeta+1, eq
+
+exception NotMetaConvertible;;
+
+let meta_convertibility_aux table t1 t2 =
+ let module C = Cic in
+ let rec aux ((table_l, table_r) as table) t1 t2 =
+ match t1, t2 with
+ | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
+ 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) || (m2_binding <> m1) then
+ raise NotMetaConvertible
+ else (
+ try
+ List.fold_left2
+ (fun res t1 t2 ->
+ match t1, t2 with
+ | None, Some _ | Some _, None -> raise NotMetaConvertible
+ | None, None -> res
+ | Some t1, Some t2 -> (aux res t1 t2))
+ (table_l, table_r) tl1 tl2
+ with Invalid_argument _ ->
+ raise NotMetaConvertible
+ )
+ | C.Var (u1, ens1), C.Var (u2, ens2)
+ | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
+ aux_ens table ens1 ens2
+ | C.Cast (s1, t1), C.Cast (s2, t2)
+ | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
+ | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
+ | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+ let table = aux table s1 s2 in
+ aux table t1 t2
+ | C.Appl l1, C.Appl l2 -> (
+ try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
+ when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
+ | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
+ when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
+ aux_ens table ens1 ens2
+ | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
+ when (UriManager.eq u1 u2) && i1 = i2 ->
+ let table = aux table s1 s2 in
+ let table = aux table t1 t2 in (
+ try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
+ try
+ List.fold_left2
+ (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
+ if i1 <> i2 then raise NotMetaConvertible
+ else
+ let res = (aux res s1 s2) in aux res t1 t2)
+ table il1 il2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
+ try
+ List.fold_left2
+ (fun res (n1, s1, t1) (n2, s2, t2) ->
+ let res = aux res s1 s2 in aux res t1 t2)
+ table il1 il2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ )
+ | t1, t2 when t1 = t2 -> table
+ | _, _ -> raise NotMetaConvertible
+
+ and aux_ens table ens1 ens2 =
+ let cmp (u1, t1) (u2, t2) =
+ Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
+ in
+ let ens1 = List.sort cmp ens1
+ and ens2 = List.sort cmp ens2 in
+ try
+ List.fold_left2
+ (fun res (u1, t1) (u2, t2) ->
+ if not (UriManager.eq u1 u2) then raise NotMetaConvertible
+ else aux res t1 t2)
+ table ens1 ens2
+ with Invalid_argument _ -> raise NotMetaConvertible
+ in
+ aux table t1 t2
+;;
+
+
+let meta_convertibility_eq eq1 eq2 =
+ let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
+ let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
+ if ty <> ty' then
+ false
+ else if (left = left') && (right = right') then
+ true
+ else if (left = right') && (right = left') then
+ true
+ else
+ try
+ let table = meta_convertibility_aux ([], []) left left' in
+ let _ = meta_convertibility_aux table right right' in
+ true
+ with NotMetaConvertible ->
+ try
+ let table = meta_convertibility_aux ([], []) left right' in
+ let _ = meta_convertibility_aux table right left' in
+ true
+ with NotMetaConvertible ->
+ false
+;;
+
+
+let meta_convertibility t1 t2 =
+ if t1 = t2 then
+ true
+ else
+ try
+ ignore(meta_convertibility_aux ([], []) t1 t2);
+ true
+ with NotMetaConvertible ->
+ false
+;;
+
+exception TermIsNotAnEquality;;
+
+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 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 stat = (ty,t1,t2,o) in
+ let w = Utils.compute_equality_weight stat in
+ let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
+ e
+ | _ ->
+ raise TermIsNotAnEquality
+;;
+
+let is_weak_identity eq =
+ let _,_,(_,left, right,_),_,_ = open_equality eq in
+ left = right || meta_convertibility left right
+;;
+
+let is_identity (_, context, ugraph) eq =
+ let _,_,(ty,left,right,_),menv,_ = open_equality eq in
+ left = right ||
+ (* (meta_convertibility left right)) *)
+ fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+;;
+
+
+let term_of_equality equality =
+ let _, _, (ty, left, right, _), menv, _= open_equality equality in
+ let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
+ let argsno = List.length menv in
+ let t =
+ CicSubstitution.lift argsno
+ (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+ in
+ snd (
+ List.fold_right
+ (fun (i,_,ty) (n, t) ->
+ let name = Cic.Name ("X" ^ (string_of_int n)) in
+ let ty = CicSubstitution.lift (n-1) ty in
+ let t =
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[i]
+ ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+ in
+ (n-1, Cic.Prod (name, ty, t)))
+ menv (argsno, t))
+;;
+
--- /dev/null
+(* Copyright (C) 2006, 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://helm.cs.unibo.it/
+ *)
+
+type substitution
+
+type rule = SuperpositionRight | SuperpositionLeft |Demodulation
+
+type equality
+
+and proof = new_proof * old_proof
+
+and new_proof =
+ Exact of Cic.term
+ | Step of substitution * (rule * int * (Utils.pos * int) * Cic.term)
+
+and old_proof =
+ NoProof
+ | BasicProof of substitution * Cic.term
+ | ProofBlock of substitution * UriManager.uri * (Cic.name * Cic.term) *
+ Cic.term * (Utils.pos * equality) * old_proof
+ | ProofGoalBlock of old_proof * old_proof
+ | ProofSymBlock of Cic.term list * old_proof
+ | SubProof of Cic.term * int * old_proof
+
+and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+
+
+val empty_subst : substitution
+val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst : substitution -> string
+val buildsubst :
+ int -> Cic.context -> Cic.term -> Cic.term -> substitution ->
+ substitution
+val flatten_subst : substitution -> substitution
+val lookup_subst : Cic.term -> substitution -> Cic.term
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
+val is_in_subst : int -> substitution -> bool
+val merge_subst_if_possible:
+ substitution -> substitution ->
+ substitution option
+
+val reset : unit -> unit
+
+val mk_equality :
+ int * proof *
+ (Cic.term * Cic.term * Cic.term * Utils.comparison) *
+ Cic.metasenv ->
+ equality
+
+val open_equality :
+ equality ->
+ int * proof *
+ (Cic.term * Cic.term * Cic.term * Utils.comparison) *
+ Cic.metasenv * int
+val compare : equality -> equality -> int
+val string_of_equality : ?env:Utils.environment -> equality -> string
+val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
+val string_of_proof_new :
+ ?names:(Cic.name option)list -> new_proof -> goal_proof -> string
+val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv
+val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
+val build_goal_proof:
+ goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv
+val refl_proof: Cic.term -> Cic.term -> Cic.term
+(** ensures that metavariables in equality are unique *)
+val fix_metas: int -> equality -> int * equality
+val metas_of_proof: proof -> int list
+
+exception TermIsNotAnEquality;;
+
+(**
+ raises TermIsNotAnEquality if term is not an equation.
+ The first Cic.term is a proof of the equation
+*)
+val equality_of_term: Cic.term -> Cic.term -> equality
+
+(**
+ Re-builds the term corresponding to this equality
+*)
+val term_of_equality: equality -> Cic.term
+val term_is_equality: Cic.term -> bool
+
+(** tests a sort of alpha-convertibility between the two terms, but on the
+ metavariables *)
+val meta_convertibility: Cic.term -> Cic.term -> bool
+
+(** meta convertibility between two equations *)
+val meta_convertibility_eq: equality -> equality -> bool
+
+val is_weak_identity: equality -> bool
+val is_identity: Utils.environment -> equality -> bool
+
module type EqualityIndex =
sig
- module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+ module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
val arities : (Cic.term, int) Hashtbl.t
type key = Cic.term
type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
val retrieve_generalizations : t -> key -> PosEqSet.t
val retrieve_unifiables : t -> key -> PosEqSet.t
val init_index : unit -> unit
- val remove_index : t -> Inference.equality -> t
- val index : t -> Inference.equality -> t
- val in_index : t -> Inference.equality -> bool
+ val remove_index : t -> Equality.equality -> t
+ val index : t -> Equality.equality -> t
+ val in_index : t -> Equality.equality -> bool
end
module DT =
struct
module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
- let compare = Pervasives.compare
+ type t = Utils.pos * Equality.equality
+ let compare (p1,e1) (p2,e2) =
+ let rc = Pervasives.compare p1 p2 in
+ if rc = 0 then Equality.compare e1 e2 else rc
end
module PosEqSet = Set.Make(OrderedPosEquality);;
;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
let meta_convertibility (pos,equality') =
- Inference.meta_convertibility_eq equality equality'
+ Equality.meta_convertibility_eq equality equality'
in
in_index tree l meta_convertibility || in_index tree r meta_convertibility
module PT =
struct
module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
- let compare = Pervasives.compare
+ type t = Utils.pos * Equality.equality
+ let compare (p1,e1) (p2,e2) =
+ let rc = Pervasives.compare p1 p2 in
+ if rc = 0 then Equality.compare e1 e2 else rc
end
module PosEqSet = Set.Make(OrderedPosEquality);;
;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
let meta_convertibility (pos,equality') =
- Inference.meta_convertibility_eq equality equality'
+ Equality.meta_convertibility_eq equality equality'
in
in_index tree l meta_convertibility || in_index tree r meta_convertibility
end
module type EqualityIndex =
sig
- module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+ module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
val arities : (Cic.term, int) Hashtbl.t
type key = Cic.term
type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
val retrieve_generalizations : t -> key -> PosEqSet.t
val retrieve_unifiables : t -> key -> PosEqSet.t
val init_index : unit -> unit
- val remove_index : t -> Inference.equality -> t
- val index : t -> Inference.equality -> t
- val in_index : t -> Inference.equality -> bool
+ val remove_index : t -> Equality.equality -> t
+ val index : t -> Equality.equality -> t
+ val in_index : t -> Equality.equality -> bool
end
module DT : EqualityIndex
| Some (t, s, m, u, ((p,e), eq_URI)) ->
Printf.sprintf "Some: (%s, %s, %s)"
(Utils.string_of_pos p)
- (Inference.string_of_equality ?env e)
+ (Equality.string_of_equality ?env e)
(CicPp.ppterm t)
;;
(List.map
(fun (p, e) ->
Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality ?env e))
+ (Equality.string_of_equality ?env e))
res));
;;
let indexing_retrieval_time = ref 0.;;
-let apply_subst = Inference.apply_subst
+let apply_subst = Equality.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
let check_res res msg =
match res with
Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
- let eqs = Inference.string_of_equality (snd eq_found) in
+ let eqs = Equality.string_of_equality (snd eq_found) in
check_disjoint_invariant subst menv msg;
check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
;;
let check_target context target msg =
- let w, proof, (eq_ty, left, right, order), metas = target in
+ let w, proof, (eq_ty, left, right, order), metas,_ =
+ Equality.open_equality target in
(* check that metas does not contains duplicates *)
- let eqs = Inference.string_of_equality target in
+ let eqs = Equality.string_of_equality target in
let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
- let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
- @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
+ let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
the position will always be Left, and if the ordering is left < right,
position will be Right.
*)
-let local_max = ref 100;;
-
-let make_variant (p,eq) =
- let maxmeta, eq = Inference.fix_metas !local_max eq in
- local_max := maxmeta;
- p, eq
-;;
let get_candidates ?env mode tree term =
let t1 = Unix.gettimeofday () in
function
| [] -> None
| candidate::tl ->
- let pos, (_, proof, (ty, left, right, o), metas) = candidate in
+ let pos, equality = candidate in
+ let (_, proof, (ty, left, right, o), metas,_) =
+ Equality.open_equality equality in
if Utils.debug_metas then
ignore(check_target context (snd candidate) "find_matches");
if Utils.debug_res then
begin
- let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
- let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
- let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
- let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
+ let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
+ let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
+ let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+ let p="proof = "^
+ (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n"
+ in
check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+ check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
function
| [] -> []
| candidate::tl ->
- let pos, (_, _, (ty, left, right, o), metas) = candidate in
+ let pos, equality = candidate in
+ let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
let do_match c eq_URI =
let subst', metasenv', ugraph' =
let t1 = Unix.gettimeofday () in
((pos,equation),_)) -> Inference.string_of_equality equation)l))
in
*)
- let _, _, (ty, left, right, _), tmetas = target in
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let metasenv, context, ugraph = env in
let metasenv = tmetas in
- let merge_if_possible s1 s2 =
- let already_in = Hashtbl.create 13 in
- let rec aux acc = function
- | ((i,x) as s)::tl ->
- (try
- let x' = Hashtbl.find already_in i in
- if x = x' then aux acc tl else None
- with
- | Not_found ->
- Hashtbl.add already_in i x;
- aux (s::acc) tl)
- | [] -> Some acc
- in
- aux [] (s1@s2)
- in
let leftr =
match left with
| Cic.Meta _ -> []
let rec ok what = function
| [] -> None
| (_, subst, menv, ug, ((pos,equation),_))::tl ->
- let _, _, (_, l, r, o), m = equation in
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
try
let other = if pos = Utils.Left then r else l in
let subst', menv', ug' =
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
- (match merge_if_possible subst subst' with
+ (match Equality.merge_subst_if_possible subst subst' with
| None -> ok what tl
| Some s -> Some (s, equation))
with Inference.MatchingFailure ->
if List.exists (fun (i,_,_) -> i = 2840) metasenv
then
(prerr_endline ("term: " ^(CicPp.ppterm term));
- List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality x))
+ List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
candidates;
prerr_endline ("-------");
prerr_endline ("+++++++"));
-(* let candidates = List.map make_variant candidates in *)
let res =
match term with
| C.Meta _ -> None
let module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, proof, (eq_ty, left, right, order), metas = target in
+ let w, ((proof_new, proof_old) as proof),
+ (eq_ty, left, right, order), metas, id =
+ Equality.open_equality target in
(* first, we simplify *)
let right = U.guarded_simpl context right in
let left = U.guarded_simpl context left in
let order = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, order) in
let w = Utils.compute_equality_weight stat in
- let target = w, proof, stat, metas in
+ let target = Equality.mk_equality (w, proof, stat, metas) in
if Utils.debug_metas then
ignore(check_target context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
begin
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
- let substs = Inference.ppsubst subst in
+ let substs = Equality.ppsubst subst in
ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, (proof'_new,proof'_old),
+ (ty, what, other, _), menv',id') = Equality.open_equality equality in
let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
- let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
+ let bo =
+ Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
incr demod_counter;
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
in
if sign = Utils.Positive then
(bo,
- Inference.ProofBlock (
- subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+ (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+ (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
+ Equality.ProofBlock (
+ subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
else
+ assert false
+(*
begin
prerr_endline "***************************************negative";
let metaproof =
incr maxmeta;
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
+(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(* print_newline (); *)
C.Meta (!maxmeta, irl)
in
let eq_found =
- let proof' =
+ let proof'_old' =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof'_old)
in
+ let proof'_new' = assert false (* not implemented *) in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
+ pos,
+ Equality.mk_equality
+ (0, (proof'_new',proof'_old'),
+ (ty, other, what, Utils.Incomparable),menv')
in
let target_proof =
let pb =
- Inference.ProofBlock
+ Equality.ProofBlock
(subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof ([],metaproof))
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
- match proof with
- | Inference.BasicProof _ ->
+ assert false, (* not implemented *)
+ (match snd proof with
+ | Equality.BasicProof _ ->
(* print_endline "replacing a BasicProof"; *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* print_endline "replacing another ProofGoalBlock"; *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if is_left then right else left]
in
(bo,
- Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
- end
+ (assert false, (* not implemented *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
+ end
+*)
in
let newmenv = (* Inference.filter subst *) menv in
let _ =
if Utils.debug_metas then
try ignore(CicTypeChecker.type_of_aux'
- newmenv context (Inference.build_proof_term newproof) ugraph);
+ newmenv context
+ (Equality.build_proof_term_old (snd newproof)) ugraph);
()
with exc ->
prerr_endline "sempre lui";
- prerr_endline (Inference.ppsubst subst);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+ prerr_endline (Equality.ppsubst subst);
+ prerr_endline (CicPp.ppterm
+ (Equality.build_proof_term_old (snd newproof)));
prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+ prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
newmenv));
raise exc;
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let res =
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat,newmenv) in
+ Equality.mk_equality (w, newproof, stat,newmenv)
+ in
if Utils.debug_metas then
ignore(check_target context res "buildnew_target output");
!maxmeta, res
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
+ if (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
demodulation_equality newmeta env table sign newtarget
match res with
| Some t ->
let newmeta, newtarget = build_newtarget false t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
+ if (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
demodulation_equality newmeta env table sign newtarget
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
+let superposition_left newmeta (metasenv, context, ugraph) table target =
+ assert false
+(*
let superposition_left newmeta (metasenv, context, ugraph) table target =
let module C = Cic in
let module S = CicSubstitution in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let weight, proof, (eq_ty, left, right, ordering), menv = target in
+ let weight, proof, (eq_ty, left, right, ordering), menv, id =
+ Equality.open_equality target
+ in
if Utils.debug_metas then
ignore(check_target context target "superpositionleft");
let expansions, _ =
let term = if ordering = U.Gt then left else right in
- begin
- let t1 = Unix.gettimeofday () in
- let res = betaexpand_term metasenv context ugraph table 0 term in
- let t2 = Unix.gettimeofday () in
- beta_expand_time := !beta_expand_time +. (t2 -. t1);
- res
- end
+ betaexpand_term metasenv context ugraph table 0 term
in
let maxmeta = ref newmeta in
let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
let time1 = Unix.gettimeofday () in
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
+ let proof'_new, proof'_old = proof' in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ proof'_new, (* MAH????? *)
+ Equality.ProofSymBlock (termlist, proof'_old)
in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+ pos,
+ Equality.mk_equality
+ (0, proof', (ty, other, what, Utils.Incomparable), menv')
in
- let target_proof =
+ let target_proof = assert false (*
let pb =
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
- Inference.BasicProof ([],metaproof))
+ Equality.ProofBlock
+ (s, eq_URI, (name, ty), bo'', eq_found,
+ Equality.BasicProof (Equality.empty_subst,metaproof))
in
match proof with
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false*)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
- Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+ (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
+ assert false), (* il predicato della beta expand non viene tenuto? *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv)
+ Equality.mk_equality (w, newproof, stat, newmenv)
in
!maxmeta, List.map build_new expansions
;;
-
+*)
let sup_r_counter = ref 1;;
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
+ let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ Equality.open_equality target
+ in
if Utils.debug_metas then
ignore (check_target context target "superpositionright");
let metasenv' = newmetas in
ignore (check_target context (snd eq_found) "buildnew1" );
let time1 = Unix.gettimeofday () in
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id') =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
(* qua *)
let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
- let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+ let name = C.Name "x" in
incr sup_r_counter;
let bo'' =
let l, r =
S.lift 1 eq_ty; l; r]
in
bo',
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
+ ( Equality.Step (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
+ Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+
in
let newmeta, newequality =
let left, right =
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv) in
+ Equality.mk_equality (w, newproof, stat, newmenv) in
if Utils.debug_metas then
ignore (check_target context eq' "buildnew3");
- let newm, eq' = Inference.fix_metas !maxmeta eq' in
+ let newm, eq' = Equality.fix_metas !maxmeta eq' in
if Utils.debug_metas then
ignore (check_target context eq' "buildnew4");
newm, eq'
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
- let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
+ let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let proof, metas, term = goal in
+ let (cicproof,proof), metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = proof, metas, term in
+ let goal = (cicproof,proof), metas, term in
let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
- let newterm, newproof =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+ let newterm, newproof, newcicproof =
+ let bo =
+ Utils.guarded_simpl context (apply_subst subst(S.subst other t))
+ in
let bo' = apply_subst subst t in
- let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
+(* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
incr demod_counter;
let metaproof =
incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let irl = [] (*
+ CicMkImplicit.identity_relocation_list_for_metavariable context *) in
(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
C.Meta (!maxmeta, irl)
in
let eq_found =
- let proof' =
+ let eq_found_proof =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+ pos,
+ Equality.mk_equality
+ (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
in
let goal_proof =
let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof ([],metaproof))
+ Equality.ProofBlock
+ (subst, eq_URI, (name, ty), bo',
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
let rec repl = function
- | Inference.NoProof ->
+ | Equality.NoProof ->
(* debug_print (lazy "replacing a NoProof"); *)
pb
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | Inference.SubProof (term, meta_index, p) ->
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | Equality.SubProof (term, meta_index, p) ->
prerr_endline "subproof!";
- Inference.SubProof (term, meta_index, repl p)
+ Equality.SubProof (term, meta_index, repl p)
| _ -> assert false
in repl proof
in
- bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+ let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
+ (newcicproofstep::cicproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, (newproof, newmetasenv, newterm)
+ !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
in
let res =
demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
| Some t ->
let newmeta, newgoal = build_newgoal t in
let _, _, newg = newgoal in
- if Inference.meta_convertibility term newg then
- newmeta, newgoal
+ if Equality.meta_convertibility term newg then
+ true, newmeta, newgoal
else
demodulation_goal newmeta env table newgoal
| None ->
- newmeta, goal
+ false, newmeta, goal
;;
(** demodulation, when the target is a theorem *)
let metasenv' = metas in
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newty =
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
let bo' = apply_subst subst t in
let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
- let newproof =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
- Inference.BasicProof ([],term))
+ let newproofold =
+ Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+ Equality.BasicProof (Equality.empty_subst,term))
in
- (Inference.build_proof_term newproof, bo)
+ (Equality.build_proof_term_old newproofold, bo)
in
!maxmeta, (newterm, newty, menv)
in
| Some t ->
let newmeta, newthm = build_newtheorem t in
let newt, newty, _ = newthm in
- if Inference.meta_convertibility termty newty then
+ if Equality.meta_convertibility termty newty then
newmeta, newthm
else
demodulation_theorem newmeta env table newthm
(* $Id$ *)
-val beta_expand_time : float ref
-
module Index :
sig
module PosEqSet : Set.S
- with type elt = Utils.pos * Inference.equality
+ with type elt = Utils.pos * Equality.equality
and type t = Equality_indexing.DT.PosEqSet.t
type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
type key = Cic.term
end
-val index : Index.t -> Inference.equality -> Index.t
-val remove_index : Index.t -> Inference.equality -> Index.t
-val in_index : Index.t -> Inference.equality -> bool
+val index : Index.t -> Equality.equality -> Index.t
+val remove_index : Index.t -> Equality.equality -> Index.t
+val in_index : Index.t -> Equality.equality -> bool
val empty : Index.t
val match_unif_time_ok : float ref
val match_unif_time_no : float ref
val subsumption :
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Inference.equality ->
- (Inference.substitution * Inference.equality) option
+ Equality.equality ->
+ (Equality.substitution * Equality.equality) option
val superposition_left :
int ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Inference.equality ->
- int * Inference.equality list
+ Equality.equality ->
+ int * Equality.equality list
val superposition_right :
int ->
'a * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Inference.equality ->
- int * Inference.equality list
+ Equality.equality ->
+ int * Equality.equality list
val demodulation_equality :
?from:string ->
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Utils.equality_sign -> Inference.equality -> int * Inference.equality
+ Utils.equality_sign -> Equality.equality -> int * Equality.equality
val demodulation_goal :
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Inference.proof * Cic.metasenv * Index.key ->
- int * (Inference.proof * Cic.metasenv * Index.key)
+ (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key ->
+ bool * int *
+ ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key)
val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
'a * (Cic.term * Index.key * Cic.metasenv)
val check_target:
Cic.context ->
- Inference.equality -> string -> unit
+ Equality.equality -> string -> unit
-(* maxmeta for relocate *)
-val local_max : int ref
open Utils;;
open Printf;;
-let metas_of_proof_time = ref 0.;;
-let metas_of_term_time = ref 0.;;
-(*
-type substitution = Cic.substitution
-let apply_subst = CicMetaSubst.apply_subst
-let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
-let ppsubst = CicMetaSubst.ppsubst
-let buildsubst n context t ty = (n,(context,t,ty))
-let flatten_subst subst =
- List.map
- (fun (i, (context, term, ty)) ->
- let context = (*` apply_subst_context subst*) context in
- let term = apply_subst subst term in
- let ty = apply_subst subst ty in
- (i, (context, term, ty))) subst
-let rec lookup_subst meta subst =
- match meta with
- | Cic.Meta (i, _) -> (
- try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
- in lookup_subst t subst
- with Not_found -> meta
- )
- | _ -> meta
-;;
-*)
-
-(* naif version of apply subst; the local context of metas is ignored;
-we assume the substituted term must be lifted according to the nesting
-depth of the meta. Alternatively, ee could used implicit instead of
-metas *)
-
-
-type substitution = (int * Cic.term) list
-
-let apply_subst subst term =
- let rec aux k t =
- match t with
- Cic.Rel _ -> t
- | Cic.Var (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.Var (uri, exp_named_subst')
- | Cic.Meta (i, l) ->
- (try
- aux k (CicSubstitution.lift k (List.assoc i subst))
- with Not_found -> t)
- | Cic.Sort _
- | Cic.Implicit _ -> t
- | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
- | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
- | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
- | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
- | Cic.Appl [] -> assert false
- | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
- | Cic.Const (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- if exp_named_subst' != exp_named_subst then
- Cic.Const (uri, exp_named_subst')
- else
- t (* TODO: provare a mantenere il piu' possibile sharing *)
- | Cic.MutInd (uri,typeno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.MutInd (uri,typeno,exp_named_subst')
- | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
- | Cic.MutCase (sp,i,outty,t,pl) ->
- let pl' = List.map (aux k) pl in
- Cic.MutCase (sp, i, aux k outty, aux k t, pl')
- | Cic.Fix (i, fl) ->
- let len = List.length fl in
- let fl' =
- List.map
- (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
- in
- Cic.Fix (i, fl')
- | Cic.CoFix (i, fl) ->
- let len = List.length fl in
- let fl' =
- List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
- in
- Cic.CoFix (i, fl')
-in
- aux 0 term
-;;
-
-(* naif version of apply_subst_metasenv: we do not apply the
-substitution to the context *)
-
-let apply_subst_metasenv subst metasenv =
- List.map
- (fun (n, context, ty) ->
- (n, context, apply_subst subst ty))
- (List.filter
- (fun (i, _, _) -> not (List.mem_assoc i subst))
- metasenv)
-
-let ppsubst subst =
- String.concat "\n"
- (List.map
- (fun (idx, t) ->
- sprintf "%d:= %s" idx (CicPp.ppterm t))
- subst)
-;;
-
-let buildsubst n context t ty = (n,t) ;;
-
-let flatten_subst subst =
- List.map (fun (i,t) -> i, apply_subst subst t ) subst
-;;
-
-let rec lookup_subst meta subst =
- match meta with
- | Cic.Meta (i, _) ->
- (try
- lookup_subst (List.assoc i subst) subst
- with
- Not_found -> meta)
- | _ -> meta
-;;
-
-type equality =
- int * (* weight *)
- proof *
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term * (* right side *)
- Utils.comparison) * (* ordering *)
- Cic.metasenv (* environment for metas *)
-
-and proof =
- | NoProof (* term is the goal missing a proof *)
- | BasicProof of substitution * Cic.term
- | ProofBlock of
- 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 (s, t) -> "BasicProof " ^
- (CicPp.ppterm (apply_subst s 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 (subst, _, _, _ ,_,_) ->
- "ProofBlock" ^ (ppsubst subst)
- | ProofGoalBlock (p1, p2) ->
- Printf.sprintf "ProofGoalBlock(%s, %s)"
- (string_of_proof p1) (string_of_proof p2)
-;;
-
-
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
end
;;
-(* filter out from metasenv the variables in substs *)
-let filter subst metasenv =
- List.filter
- (fun (m, _, _) ->
- try let _ = List.find (fun (i, _) -> m = i) subst in false
- with Not_found -> true)
- metasenv
-;;
-
-(* 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 ?(noproof=Cic.Implicit None) proof =
- let rec do_build_proof proof =
- match proof with
- | NoProof ->
- Printf.fprintf stderr "WARNING: no proof!\n";
- noproof
- | BasicProof (s,term) -> apply_subst s 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' = eq in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- 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)
- | _ -> []
-;;
-
-let rec metas_of_proof p =
- if Utils.debug then
- let t1 = Unix.gettimeofday () in
- let res = metas_of_term (build_proof_term p) in
- let t2 = Unix.gettimeofday () in
- metas_of_proof_time := !metas_of_proof_time +. (t2 -. t1);
- res
- else
- metas_of_term (build_proof_term p)
-;;
-
-
-exception NotMetaConvertible;;
-
-let meta_convertibility_aux table t1 t2 =
- let module C = Cic in
- let rec aux ((table_l, table_r) as table) t1 t2 =
- match t1, t2 with
- | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
- 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) || (m2_binding <> m1) then
- raise NotMetaConvertible
- else (
- try
- List.fold_left2
- (fun res t1 t2 ->
- match t1, t2 with
- | None, Some _ | Some _, None -> raise NotMetaConvertible
- | None, None -> res
- | Some t1, Some t2 -> (aux res t1 t2))
- (table_l, table_r) tl1 tl2
- with Invalid_argument _ ->
- raise NotMetaConvertible
- )
- | C.Var (u1, ens1), C.Var (u2, ens2)
- | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
- aux_ens table ens1 ens2
- | C.Cast (s1, t1), C.Cast (s2, t2)
- | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
- | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
- | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
- let table = aux table s1 s2 in
- aux table t1 t2
- | C.Appl l1, C.Appl l2 -> (
- try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
- with Invalid_argument _ -> raise NotMetaConvertible
- )
- | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
- when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
- | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
- when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
- aux_ens table ens1 ens2
- | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
- when (UriManager.eq u1 u2) && i1 = i2 ->
- let table = aux table s1 s2 in
- let table = aux table t1 t2 in (
- try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
- with Invalid_argument _ -> raise NotMetaConvertible
- )
- | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
- try
- List.fold_left2
- (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
- if i1 <> i2 then raise NotMetaConvertible
- else
- let res = (aux res s1 s2) in aux res t1 t2)
- table il1 il2
- with Invalid_argument _ -> raise NotMetaConvertible
- )
- | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
- try
- List.fold_left2
- (fun res (n1, s1, t1) (n2, s2, t2) ->
- let res = aux res s1 s2 in aux res t1 t2)
- table il1 il2
- with Invalid_argument _ -> raise NotMetaConvertible
- )
- | t1, t2 when t1 = t2 -> table
- | _, _ -> raise NotMetaConvertible
-
- and aux_ens table ens1 ens2 =
- let cmp (u1, t1) (u2, t2) =
- compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
- in
- let ens1 = List.sort cmp ens1
- and ens2 = List.sort cmp ens2 in
- try
- List.fold_left2
- (fun res (u1, t1) (u2, t2) ->
- if not (UriManager.eq u1 u2) then raise NotMetaConvertible
- else aux res t1 t2)
- table ens1 ens2
- with Invalid_argument _ -> raise NotMetaConvertible
- in
- aux table t1 t2
-;;
-
-
-let meta_convertibility_eq eq1 eq2 =
- 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
- try
- let table = meta_convertibility_aux ([], []) left left' in
- let _ = meta_convertibility_aux table right right' in
- true
- with NotMetaConvertible ->
- try
- let table = meta_convertibility_aux ([], []) left right' in
- let _ = meta_convertibility_aux table right left' in
- true
- with NotMetaConvertible ->
- false
-;;
-
-
-let meta_convertibility t1 t2 =
- if t1 = t2 then
- true
- else
- try
- ignore(meta_convertibility_aux ([], []) t1 t2);
- true
- with NotMetaConvertible ->
- false
-;;
-
-
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
;;
let unification_simple locked_menv metasenv context t1 t2 ugraph =
- let debug_print x = prerr_endline (Lazy.force x) in
let module C = Cic in
let module M = CicMetaSubst in
let module U = CicUnification in
- let lookup = lookup_subst in
+ let lookup = Equality.lookup_subst in
let rec occurs_check subst what where =
match where with
| t when what = t -> true
match s, t with
| s, t when s = t -> subst, menv
| C.Meta (i, _), C.Meta (j, _)
- when (locked locked_menv i) &&(locked locked_menv j) ->
- raise
+ when (locked locked_menv i) &&(locked locked_menv j) ->
+ raise
(U.UnificationFailure (lazy "Inference.unification.unif"))
- | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
- unif subst menv t s
+ | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
+ unif subst menv t s
| C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise
(U.UnificationFailure (lazy "Inference.unification.unif"))
| C.Meta (i, l), t when (locked locked_menv i) ->
- raise
+ raise
(U.UnificationFailure (lazy "Inference.unification.unif"))
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
- assert (not (List.mem_assoc i subst));
- let subst = (buildsubst i context t ty)::subst in
+ assert (not (Equality.is_in_subst i subst));
+ let subst = Equality.buildsubst i context t ty subst in
let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
subst, menv
with CicUtil.Meta_not_found m ->
| _, _ ->
raise (U.UnificationFailure (lazy "Inference.unification.unif"))
in
- let subst, menv = unif [] metasenv t1 t2 in
- let menv = filter subst menv in
- List.rev subst, menv, ugraph
+ let subst, menv = unif Equality.empty_subst metasenv t1 t2 in
+ let menv = Equality.filter subst menv in
+ subst, menv, ugraph
;;
let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
) else
if b then
- (* full unification *)
- unification_simple [] metasenv context t1 t2 ugraph
+ (* full unification *)
+ unification_simple [] metasenv context t1 t2 ugraph
else
- (* matching: metasenv1 is locked *)
- unification_simple metasenv1 metasenv context t1 t2 ugraph
+ (* matching: metasenv1 is locked *)
+ unification_simple metasenv1 metasenv context t1 t2 ugraph
in
if Utils.debug_res then
- ignore(check_disjoint_invariant subst menv "unif");
+ ignore(check_disjoint_invariant subst menv "unif");
(* let flatten subst =
List.map
(fun (i, (context, term, ty)) ->
- let context = apply_subst_context subst context in
- let term = apply_subst subst term in
- let ty = apply_subst subst ty in
- (i, (context, term, ty))) subst
+ let context = apply_subst_context subst context in
+ let term = apply_subst subst term in
+ let ty = apply_subst subst ty in
+ (i, (context, term, ty))) subst
in
let flatten subst = profiler.HExtlib.profile flatten subst in
let subst = flatten subst in *)
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = compute_equality_weight stat in
- let proof = BasicProof ([],p) in
- let e = (w, proof, stat, newmetas) in
+ let proof_old =
+ Equality.BasicProof (Equality.empty_subst,p) in
+ let proof_new = Equality.Exact p in
+ let proof = proof_new , proof_old in
+ let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)
| _ -> None, newmeta
)
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = compute_equality_weight stat in
- let e = (w, BasicProof ([],(C.Rel index)), stat, []) in
+ let p = C.Rel index in
+ let proof_old = Equality.BasicProof (Equality.empty_subst,p) in
+ let proof_new = Equality.Exact p in
+ let proof = proof_new, proof_old in
+ let e = Equality.mk_equality (w, proof,stat,[]) 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
- if newmeta' < newmeta then
- prerr_endline "big trouble";
+ if newmeta' < newmeta then
+ prerr_endline "big trouble";
(index, p)::tl, newmeta' (* max???? *)
| None, _ ->
aux (index+1) newmeta tl
in
let il, maxm = aux 1 newmeta context in
let indexes, equalities = List.split il in
- ignore (List.iter (check_eq context "find") equalities);
+ (* ignore (List.iter (check_eq context "find") equalities); *)
indexes, equalities, maxm
;;
else
C.Appl (term::args)
in (
- match head with
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
- when (iseq uri) && (ok_types ty newmetas) ->
+ 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 stat = (ty,t1,t2,o) in
let w = compute_equality_weight stat in
- let proof = BasicProof ([],p) in
- let e = (w, proof, stat, newmetas) in
+ let proof_old =
+ Equality.BasicProof (Equality.empty_subst,p) in
+ let proof_new = Equality.Exact p in
+ let proof = proof_new, proof_old in
+ let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)
| _ -> None, newmeta
)
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = compute_equality_weight stat in
- let e = (w, BasicProof ([],term), stat, []) in
+ let old_proof = Equality.BasicProof (Equality.empty_subst,term) in
+ let new_proof = Equality.Exact term in
+ let proof = new_proof, old_proof in
+ let e = Equality.mk_equality (w, proof, stat, []) in
Some e, (newmeta+1)
| _ -> None, newmeta
in
match res with
| Some e ->
let tl, newmeta' = aux newmeta tl in
- if newmeta' < newmeta then
- prerr_endline "big trouble";
+ if newmeta' < newmeta then
+ prerr_endline "big trouble";
(uri, e)::tl, newmeta' (* max???? *)
| None ->
aux newmeta tl
in
let found, maxm = aux maxmeta candidates in
let uriset, eqlist =
+ let mceq = Equality.meta_convertibility_eq in
(List.fold_left
(fun (s, l) (u, e) ->
- if List.exists (meta_convertibility_eq e) (List.map snd l) then (
+ if List.exists (mceq e) (List.map snd l) then (
debug_print
(lazy
(Printf.sprintf "NO!! %s already there!"
- (string_of_equality e)));
+ (Equality.string_of_equality e)));
(UriManager.UriSet.add u s, l)
) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
res
;;
-(*
-let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
- 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) @
- (metas_of_term ty) @ (metas_of_proof p) in
- 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
- 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 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
- let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
- (newmeta +1, neweq)
-;;
-*)
-
-let relocate newmeta menv =
- let subst, metasenv, newmeta =
- List.fold_right
- (fun (i, context, ty) (subst, menv, maxmeta) ->
- let irl = [] (*
- CicMkImplicit.identity_relocation_list_for_metavariable context *)
- in
- let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
- let newmeta = maxmeta, context, ty in
- newsubst::subst, newmeta::menv, maxmeta+1)
- menv ([], [], newmeta+1)
- in
- let metasenv = apply_subst_metasenv subst metasenv in
- let subst = flatten_subst subst in
- subst, metasenv, newmeta
-
-
-let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
- (*
- let metas = (metas_of_term left)@(metas_of_term right)
- @(metas_of_term ty)@(metas_of_proof p) in
- let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
- *)
- (* debug
- let _ , eq =
- fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
- prerr_endline (string_of_equality eq); *)
- let subst, metasenv, newmeta = relocate newmeta menv in
-(*
- if newmeta > 2839 then
- begin
- prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
- prerr_endline (CicMetaSubst.ppsubst subst);
- prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
- assert false;
- end;
-*)
- let ty = apply_subst subst ty in
- let left = apply_subst subst left in
- let right = apply_subst subst right in
- let fix_proof = function
- | NoProof -> NoProof
- | BasicProof (subst',term) -> BasicProof (subst@subst',term)
- | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
- (*
- let newsubst =
- List.map
- (fun (i, (context, term, ty)) ->
- let context = apply_subst_context subst context in
- let term = apply_subst subst term in
- let ty = apply_subst subst ty in
- (i, (context, term, ty))) subst' in *)
- ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
- | p -> assert false
- in
- let p = fix_proof p in
- (*
- let metas = (metas_of_term left)@(metas_of_term right)
- @(metas_of_term ty)@(metas_of_proof p) in
- let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
- *)
- let eq = (w, p, (ty, left, right, o), metasenv) in
- (* debug prerr_endline (string_of_equality eq); *)
- newmeta+1, eq
-
-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
-;;
-
-
-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 stat = (ty,t1,t2,o) in
- let w = compute_equality_weight stat in
- let e = (w, BasicProof ([],proof), stat, []) in
- e
- | _ ->
- raise TermIsNotAnEquality
-;;
-
-
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-
-let is_weak_identity (metasenv, context, ugraph) = function
- | (_, _, (ty, left, right, _), menv) ->
- (left = right ||
- (meta_convertibility left right))
- (* the test below is not a good idea since it stops
- demodulation too early *)
- (* (fst (CicReduction.are_convertible
- ~metasenv:(metasenv @ menv) context left right ugraph)))*)
-;;
-
-let is_identity (metasenv, context, ugraph) = function
- | (_, _, (ty, left, right, _), menv) ->
- (left = right ||
- (* (meta_convertibility left right)) *)
- (fst (CicReduction.are_convertible
- ~metasenv:(metasenv @ menv) context left right ugraph)))
-;;
-
-
-let term_of_equality equality =
- let _, _, (ty, left, right, _), menv = equality in
- let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
- let argsno = List.length menv in
- let t =
- CicSubstitution.lift argsno
- (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
- in
- snd (
- List.fold_right
- (fun (i,_,ty) (n, t) ->
- let name = Cic.Name ("X" ^ (string_of_int n)) in
- let ty = CicSubstitution.lift (n-1) ty in
- let t =
- ProofEngineReduction.replace
- ~equality:eq ~what:[i]
- ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
- in
- (n-1, Cic.Prod (name, ty, t)))
- menv (argsno, t))
-;;
* http://cs.unibo.it/helm/.
*)
-val metas_of_proof_time : float ref
-
-(* type substitution = Cic.substitution *)
-type substitution = (int * Cic.term) list
-
-type equality =
- int * (* weight *)
- proof * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term * (* right side *)
- Utils.comparison) * (* ordering *)
- Cic.metasenv (* environment for metas *)
-
-and proof =
- | NoProof (* no proof *)
- | BasicProof of substitution * Cic.term (* already a proof of a goal *)
- | ProofBlock of (* proof of a rewrite step *)
- substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
- (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
- | ProofGoalBlock of proof * proof
- (* proof of the new meta, proof of the goal from which this comes *)
- | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *)
- | SubProof of Cic.term * int * proof
- (* parent proof, subgoal, proof of the subgoal *)
-
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
-
-(** builds the Cic.term encoded by proof *)
-val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
-
-val string_of_proof: proof -> string
-
-val filter : substitution -> Cic.metasenv -> Cic.metasenv
-
exception MatchingFailure
(** matching between two terms. Can raise MatchingFailure *)
val matching:
- Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context ->
+ Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- substitution * Cic.metasenv * CicUniv.universe_graph
+ Equality.substitution * Cic.metasenv * CicUniv.universe_graph
(**
special unification that checks if the two terms are "simple", and in
such case should be significantly faster than CicUnification.fo_unif
*)
val unification:
- Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context ->
+ Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- substitution * Cic.metasenv * CicUniv.universe_graph
+ Equality.substitution * Cic.metasenv * CicUniv.universe_graph
(**
fresh metas...
*)
val find_equalities:
- Cic.context -> ProofEngineTypes.proof -> int list * equality list * int
+ Cic.context -> ProofEngineTypes.proof ->
+ int list * Equality.equality list * int
(**
searches the library for equalities that can be applied to the current goal
*)
val find_library_equalities:
HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
- UriManager.UriSet.t * (UriManager.uri * equality) list * int
+ UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
(**
searches the library for theorems that are not equalities (returned by the
function above)
*)
val find_library_theorems:
- HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
- (Cic.term * Cic.term * Cic.metasenv) list
+ HMysql.dbd -> Utils.environment -> ProofEngineTypes.status ->
+ UriManager.UriSet.t ->
+ (Cic.term * Cic.term * Cic.metasenv) list
(**
searches the context for hypotheses that are not equalities
*)
val find_context_hypotheses:
- environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
-
-
-exception TermIsNotAnEquality;;
-
-(**
- raises TermIsNotAnEquality if term is not an equation.
- The first Cic.term is a proof of the equation
-*)
-val equality_of_term: Cic.term -> Cic.term -> equality
-
-(**
- Re-builds the term corresponding to this equality
-*)
-val term_of_equality: equality -> Cic.term
-
-val term_is_equality: Cic.term -> bool
-
-(** tests a sort of alpha-convertibility between the two terms, but on the
- metavariables *)
-val meta_convertibility: Cic.term -> Cic.term -> bool
-
-(** meta convertibility between two equations *)
-val meta_convertibility_eq: equality -> equality -> bool
-
-val is_weak_identity: environment -> equality -> bool
-val is_identity: environment -> equality -> bool
-
-val string_of_equality: ?env:environment -> equality -> string
-
-
-val metas_of_term: Cic.term -> int list
-val metas_of_proof: proof -> int list
-
-(** ensures that metavariables in equality are unique *)
-val fix_metas: int -> equality -> int * equality
+ Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
-val apply_subst: substitution -> Cic.term -> Cic.term
-val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
-val ppsubst: substitution -> string
let maxdepth = ref 3;;
let maxwidth = ref 3;;
+type new_proof =
+ Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv
+type old_proof = Equality.old_proof * Cic.metasenv
type result =
| ParamodulationFailure
- | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option
+ | ParamodulationSuccess of (new_proof * old_proof) option
;;
-type goal = proof * Cic.metasenv * Cic.term;;
+type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;;
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-let symbols_of_equality (_, _, (_, left, right, _), _) =
+let symbols_of_equality equality =
+ let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
let m1 = symbols_of_term left in
let m =
TermMap.fold
(* griggio *)
module OrderedEquality = struct
- type t = Inference.equality
+ type t = Equality.equality
let compare eq1 eq2 =
- match meta_convertibility_eq eq1 eq2 with
+ match Equality.meta_convertibility_eq eq1 eq2 with
| true -> 0
| false ->
- let w1, _, (ty, left, right, _), m1 = eq1
- and w2, _, (ty', left', right', _), m2 = eq2 in
+ let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
+ let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
match Pervasives.compare w1 w2 with
| 0 ->
let res = (List.length m1) - (List.length m2) in
match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
in
let (pos_list, pos_set), passive_table = passive in
- let remove eq l = List.filter (fun e -> e <> eq) l in
+ let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
if !weight_age_ratio > 0 then
weight_age_counter := !weight_age_counter - 1;
match !weight_age_counter with
let passive_table =
Indexing.remove_index passive_table current
in
- current,
+ current,
((remove current pos_list, EqualitySet.remove current pos_set),
passive_table))
| _ ->
and in_age = round (howmany /. (ratio +. 1.)) in
debug_print
(lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
- let symbols, card = None, 0
- in
let counter = ref !symbols_ratio in
let rec pickw w ps =
if w > 0 then
let _ =
counter := !counter - 1;
if !counter = 0 then counter := !symbols_ratio in
- let e = EqualitySet.min_elt ps in
+ let e = EqualitySet.min_elt ps in
let ps' = pickw (w-1) (EqualitySet.remove e ps) in
EqualitySet.add e ps'
else
(** inference of new equalities between current and some in active *)
-let infer env current ((active_list:Inference.equality list), active_table) =
+let infer env current (active_list, active_table) =
let (_,c,_) = env in
if Utils.debug_metas then
(ignore(Indexing.check_target c current "infer1");
(function current ->
Indexing.check_target c current "sup2") res);
let pos = infer_positive table tl in
- res @ pos
+ res @ pos
in
- let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+ let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
maxmeta := maxm;
let curr_table = Indexing.index Indexing.empty current in
let pos = infer_positive curr_table (copy_of_current::active_list)
ignore(List.map
(function current ->
Indexing.check_target c current "sup3") pos);
- res @ pos
+ res @ pos
in
derived_clauses := !derived_clauses + (List.length new_pos);
match !maximal_retained_equality with
let newmeta, newcurrent =
Indexing.demodulation_equality !maxmeta env table sign current in
maxmeta := newmeta;
- if is_identity env newcurrent then
+ if Equality.is_identity env newcurrent then
(* debug_print *)
(* (lazy *)
(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
match demodulate passive_table newcurrent with
| None -> None
| Some newnewcurrent ->
- if newcurrent <> newnewcurrent then
+ if Equality.compare newcurrent newnewcurrent <> 0 then
demod newnewcurrent
else Some newnewcurrent
in
match res with
| None -> None
| Some c ->
+ (* immagino non funzioni piu'... *)
if Indexing.in_index active_table c then
None
else
let new_pos_set =
List.fold_left
(fun s e ->
- if not (Inference.is_identity env e) then
+ if not (Equality.is_identity env e) then
if EqualitySet.mem e s then s
else EqualitySet.add e s
else s)
| None -> None
| Some ((_, _), pt) -> Some pt
in
-
let demodulate table goal =
- let newmeta, newgoal =
+ let changed, newmeta, newgoal =
Indexing.demodulation_goal !maxmeta env table goal in
maxmeta := newmeta;
- goal <> newgoal, newgoal
+ changed, newgoal
in
let changed, goal =
match passive_table with
let active_list, newa =
List.fold_right
(fun equality (res, newn) ->
- let ew, _, _, _ = equality in
+ let ew, _, _, _,_ = Equality.open_equality equality in
if ew < min_weight then
equality::res, newn
else
match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with
| None -> res, newn
| Some e ->
- if equality = e then
+ if Equality.compare equality e = 0 then
e::res, newn
else
res, e::newn)
active_list ([], [])
in
let find eq1 where =
- List.exists (meta_convertibility_eq eq1) where
+ List.exists (Equality.meta_convertibility_eq eq1) where
in
let active, newa =
List.fold_right
(fun eq (res, tbl) ->
if List.mem eq res then
res, tbl
- else if (is_identity env eq) || (find eq res) then (
+ else if (Equality.is_identity env eq) || (find eq res) then (
res, tbl
)
else
active_list ([], Indexing.empty),
List.fold_right
(fun eq p ->
- if (is_identity env eq) then p
- else eq::p)
+ if (Equality.is_identity env eq) then p
+ else eq::p)
newa []
in
match newa with
let backward_simplify_passive env new_pos new_table min_weight passive =
let (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
- let ew, _, _, _ = equality in
+ let ew, _, _, _ , _ = Equality.open_equality equality in
if ew < min_weight then
equality::resl, ress, newn
else
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _ = e in
+ let ew, _, _, _ , _ = Equality.open_equality e in
e::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) new'
in
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _ = e in
+ let ew, _, _, _ , _ = Equality.open_equality e in
e::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) (snd new')
in
;;
let is_commutative_law eq =
- let w, proof, (eq_ty, left, right, order), metas = eq in
+ let w, proof, (eq_ty, left, right, order), metas , _ =
+ Equality.open_equality eq
+ in
match left,right with
Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
(Printf.sprintf "symmetric:\n%s\n"
(String.concat "\n"
(List.map
- (fun e -> string_of_equality ~env e)
+ (fun e -> Equality.string_of_equality ~env e)
given)))) in
close env new' given
;;
(lazy
(Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality equalities))));
+ (List.map Equality.string_of_equality equalities))));
debug_print (lazy "SIMPLYFYING EQUALITIES...");
match equalities with
| [] -> []
(lazy
(Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
- (List.map string_of_equality res))));
+ (List.map Equality.string_of_equality res))));
res
;;
Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
;;
-let check_if_goal_is_subsumed env (proof,menv,ty) table =
+let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
- (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
- match Indexing.subsumption env table goal_equation with
- | Some (subst, (_,p,_,m)) ->
- let p = Inference.apply_subst subst (Inference.build_proof_term p) in
- let newp =
- let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
- | Inference.NoProof -> Inference.BasicProof ([],p)
- | Inference.BasicProof _ -> Inference.BasicProof ([],p)
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
- | _ -> assert false
- in
- repl proof
- in
- Some (newp,Inference.apply_subst_metasenv subst m @ menv)
- | None -> None)
+ (let goal_equation =
+ Equality.mk_equality
+ (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv)
+ in
+ match Indexing.subsumption env table goal_equation with
+ | Some (subst, equality ) ->
+ let (_,(np,p),(ty,l,r,_),m,id) =
+ Equality.open_equality equality in
+ let p = Equality.apply_subst subst
+ (Equality.build_proof_term_old p) in
+ let newp =
+ let rec repl = function
+ | Equality.ProofGoalBlock (_, gp) ->
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,p), gp)
+ | Equality.NoProof ->
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.BasicProof _ ->
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.SubProof (t, i, p2) ->
+ Equality.SubProof (t, i, repl p2)
+ | _ -> assert false
+ in
+ repl proof
+ in
+ let newcicp,np,subst,cicmenv =
+ cicproof,np, subst, (m @ menv)
+ in
+ Some
+ ((newcicp,np,subst,cicmenv),
+ (newp, Equality.apply_subst_metasenv subst m @ menv ))
+ | None -> None)
| _ -> None
;;
in
let newp =
let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
- | Inference.NoProof -> Inference.BasicProof ([],p)
- | Inference.BasicProof _ -> Inference.BasicProof ([],p)
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
+ | Equality.ProofGoalBlock (_, gp) ->
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,p), gp)
+ | Equality.NoProof ->
+
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.BasicProof _ ->
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.SubProof (t, i, p2) ->
+ Equality.SubProof (t, i, repl p2)
| _ -> assert false
in
- repl proof
- in true, Some (newp,m)
+ repl (snd proof)
+ in
+ let reflproof = Equality.refl_proof eq_ty left in
+ true,
+ Some ((fst proof,Equality.Exact reflproof,
+ Equality.empty_subst,m),
+ (newp,m))
| (_, [proof,m,ty])::_ ->
(match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with
| None -> false,None
- | Some (newproof,m) ->
+ | Some p ->
prerr_endline "Proof found by subsumption!";
- true, Some (newproof,m))
+ true, Some p)
| _ -> false, None
in
if ok then
and given_clause_fullred_aux dbd env goals theorems passive active =
prerr_endline (string_of_int !counter ^
" MAXMETA: " ^ string_of_int !maxmeta ^
- " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
" #ACTIVES: " ^ string_of_int (size_of_active active) ^
" #PASSIVES: " ^ string_of_int (size_of_passive passive));
incr counter;
| false ->
let current, passive = select env (fst goals) passive in
prerr_endline
- ("Selected = " ^ string_of_equality ~env current);
+ ("Selected = " ^ Equality.string_of_equality ~env current);
(* ^
(let w,p,(t,l,r,o),m = current in
" size w: " ^ string_of_int (HExtlib.estimate_size w)^
(* weight_age_counter := !weight_age_counter + 1; *)
given_clause_fullred dbd env goals theorems passive active
| Some current ->
- debug_print (lazy (Printf.sprintf "selected: %s"
- (string_of_equality ~env current)));
+ prerr_endline (Printf.sprintf "selected sipl: %s"
+ (Equality.string_of_equality ~env current));
let t1 = Unix.gettimeofday () in
let new' = infer env current active in
let _ =
(String.concat "\n"
(List.map
(fun e -> "Positive " ^
- (string_of_equality ~env e)) new'))))
+ (Equality.string_of_equality ~env e)) new'))))
in
let t2 = Unix.gettimeofday () in
infer_time := !infer_time +. (t2 -. t1);
let active =
- if is_identity env current then active
+ if Equality.is_identity env current then active
else
let al, tbl = active in
al @ [current], Indexing.index tbl current
| None, None -> active, passive, new'
| Some p, None
| None, Some p ->
- let np = new' in
- if Utils.debug_metas then
- begin
- List.iter
- (fun x->Indexing.check_target context x "simplify1")
- p;
- end;
- simplify (new' @ p) active passive
+ if Utils.debug_metas then
+ begin
+ List.iter
+ (fun x->Indexing.check_target context x "simplify1")
+ p;
+ end;
+ simplify (new' @ p) active passive
| Some p, Some rp ->
simplify (new' @ p @ rp) active passive
in
(Printf.sprintf "active:\n%s\n"
(String.concat "\n"
((List.map
- (fun e -> (string_of_equality ~env e))
+ (fun e -> (Equality.string_of_equality ~env e))
(fst active))))))
in
let _ =
(String.concat "\n"
((List.map
(fun e -> "Negative " ^
- (string_of_equality ~env e)) new')))))
+ (Equality.string_of_equality ~env e)) new')))))
in
let passive = add_to_passive passive new' in
given_clause_fullred dbd env goals theorems passive active
saturate_equations env goal accept_fun passive active
| Some current ->
debug_print (lazy (Printf.sprintf "selected: %s"
- (string_of_equality ~env current)));
+ (Equality.string_of_equality ~env current)));
let new' = infer env current active in
let active =
- if is_identity env current then active
+ if Equality.is_identity env current then active
else
let al, tbl = active in
al @ [current], Indexing.index tbl current
(Printf.sprintf "active:\n%s\n"
(String.concat "\n"
(List.map
- (fun e -> string_of_equality ~env e)
+ (fun e -> Equality.string_of_equality ~env e)
(fst active)))))
in
- let _ =
+ let _ =
debug_print
(lazy
(Printf.sprintf "new':\n%s\n"
(String.concat "\n"
(List.map
(fun e -> "Negative " ^
- (string_of_equality ~env e)) new'))))
+ (Equality.string_of_equality ~env e)) new'))))
in
let new' = List.filter accept_fun new' in
let passive = add_to_passive passive new' in
saturate_equations env goal accept_fun passive active
;;
-
+let main dbd full term metasenv ugraph = ()
+(*
let main dbd full term metasenv ugraph =
let module C = Cic in
let module T = CicTypeChecker in
(fst theorems)))))
in
(*try*)
- let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+ let goal =
+ ([],Equality.BasicProof (Equality.empty_subst ,new_meta_goal)), [], goal
+ in
let equalities = simplify_equalities env
(equalities@library_equalities) in
let active = make_active () in
Printf.printf "\nequalities:\n%s\n"
(String.concat "\n"
(List.map
- (string_of_equality ~env) equalities));
+ (Equality.string_of_equality ~env) equalities));
(* (equalities @ library_equalities))); *)
print_endline "--------------------------------------------------";
let start = Unix.gettimeofday () in
match res with
| ParamodulationFailure ->
Printf.printf "NO proof found! :-(\n\n"
- | ParamodulationSuccess (Some (proof, env)) ->
- let proof = Inference.build_proof_term proof in
+ | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) ->
Printf.printf "OK, found a proof!\n";
+ let oldproof = Equation.build_proof_term proof in
+ let newproof,_,newenv,_ =
+ CicRefine.type_of_aux'
+ cicmenv context cicproof CicUniv.empty_ugraph
+ in
(* REMEMBER: we have to instantiate meta_proof, we should use
apply the "apply" tactic to proof and status
*)
let names = names_of_context context in
+ prerr_endline "OLD PROOF";
print_endline (PP.pp proof names);
+ prerr_endline "NEW PROOF";
+ print_endline (PP.pp newproof names);
let newmetasenv =
List.fold_left
- (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
+ (fun m eq ->
+ let (_, _, _, menv,_) = Equality.open_equality eq in
+ m @ menv)
+ metasenv equalities
in
let _ =
(*try*)
"backward_simpl_time: %.9f\n")
!infer_time !forward_simpl_time !forward_simpl_new_time
!backward_simpl_time) ^
- (Printf.sprintf "beta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
(Printf.sprintf "passive_maintainance_time: %.9f\n"
!passive_maintainance_time) ^
(Printf.sprintf " successful unification/matching time: %.9f\n"
raise exc
*)
;;
-
+*)
let default_depth = !maxdepth
and default_width = !maxwidth;;
let reset_refs () =
maxmeta := 0;
- Indexing.local_max := 100;
symbols_counter := 0;
weight_age_counter := !weight_age_ratio;
processed_clauses := 0;
passive_maintainance_time := 0.;
derived_clauses := 0;
kept_clauses := 0;
- Indexing.beta_expand_time := 0.;
- Inference.metas_of_proof_time := 0.;
+ Equality.reset ();
+;;
+
+let interactive_comparison context t1 t2 =
+ let rc = ref [] in
+ let module P = Printf in
+ let rec aux n context t1 t2 =
+(* let names = names_of_context context in*)
+ let pp t1 t2 = () (*
+ P.eprintf "%s%s === %s\n" (String.make n ' ')
+ (CicPp.pp t1 names) (CicPp.pp t2 names) *)
+ in
+ match t1,t2 with
+ | _, Cic.Appl [Cic.Const(uri,_);t2] when
+ UriManager.eq uri (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2
+ | Cic.Implicit _, _ -> pp t1 t2
+ | Cic.Meta (n,_), _ ->
+ rc := (n,t2,context) :: !rc;
+ pp (Cic.Meta(n,[])) t2
+ | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2
+ | Cic.Appl l1,Cic.Appl l2 ->
+ if List.length l1 <> List.length l2 then
+ begin
+ prerr_endline "ERROR: application with diff num of args";
+ pp t1 t2
+ end
+ else
+ List.iter2 (aux (n+1) context) l1 l2
+ | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) ->
+ let context = (Some (name,(Cic.Decl s)))::context in
+ aux (n+1) context t1 t2
+ | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 ->
+ pp t1 t2
+ | _,_ -> pp t1 t2
+ in
+ aux 0 context t1 t2;
+ List.iter (fun (n,t,ctx) ->
+ let names = names_of_context ctx in
+ Printf.eprintf "%d := %s\n" n (CicPp.pp t names))
+ (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc))
;;
+
let saturate
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
let goal' = goal in
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
- prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context));
let eq_indexes, equalities, maxm = find_equalities context proof in
let new_meta_goal, metasenv, type_of_goal =
let irl =
in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
- let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+ let goal =
+ ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal
+ in
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
(res, finish -. start)
in
match res with
- | ParamodulationSuccess (Some (proof, proof_menv)) ->
+ | ParamodulationSuccess
+ (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) ->
prerr_endline "OK, found a proof!";
- debug_print (lazy "OK, found a proof!");
- let proof = Inference.build_proof_term proof in
+ prerr_endline (Equality.string_of_proof_old proof);
+
+ let cic_proof = Equality.build_proof_term_old proof in
+
+ let cic_proof_new,cic_proof_new_menv =
+ Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof)
+ in
+ let newproof_menv =
+ Equality.apply_subst_metasenv subsumption_subst
+ (newproof_menv @ cic_proof_new_menv)
+ in
+ let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in
+
let equality_for_replace i t1 =
match t1 with
| C.Meta (n, _) -> n = i
| _ -> false
in
- prerr_endline "replacing metas";
+ let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
+ prerr_endline "replacing metas (old)";
let proof_menv, what, with_what =
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
+ let irl = mkirl context in
List.fold_left
(fun (acc1,acc2,acc3) (i,_,ty) ->
(i,context,ty)::acc1,
(Cic.Meta(i,irl)) ::acc3)
([],[],[]) proof_menv
in
- let proof = ProofEngineReduction.replace_lifting
+ let cic_proof = ProofEngineReduction.replace_lifting
+ ~equality:(=)
+ ~what ~with_what
+ ~where:cic_proof
+ in
+ prerr_endline "replacing metas (new)";
+ let newproof_menv, what, with_what =
+ let irl = mkirl context in
+ List.fold_left
+ (fun (acc1,acc2,acc3) (i,_,ty) ->
+ (i,context,ty)::acc1,
+ (Cic.Meta(i,[]))::acc2,
+ (Cic.Meta(i,irl)) ::acc3)
+ ([],[],[]) newproof_menv
+ in
+ let cic_proof_new = ProofEngineReduction.replace_lifting
~equality:(=)
~what ~with_what
- ~where:proof
+ ~where:cic_proof_new
in
- (* prerr_endline (CicPp.ppterm proof); *)
let names = names_of_context context in
+ prerr_endline "OLDPROOF";
+ prerr_endline (Equality.string_of_proof_old proof);
+ prerr_endline "OLDPROOFCIC";
+ prerr_endline (CicPp.pp cic_proof names);
+ prerr_endline "NEWPROOF";
+ prerr_endline (Equality.string_of_proof_new ~names newproof goalproof);
+ prerr_endline "NEWPROOFCIC";
+ prerr_endline (CicPp.pp cic_proof_new names);
let newmetasenv =
let i1 =
match new_meta_goal with
List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
in
let newmetasenv = newmetasenv@proof_menv in
+ let newmetasenv_new = newmetasenv@newproof_menv in
let newstatus =
try
- let ty, ug =
- prerr_endline "type checking ... ";
- CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+ let cic_proof,newmetasenv,proof_menv,ty, ug =
+ prerr_endline "type checking ... (old) ";
+(* let old_ty, oldug = *)
+(* CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *)
+(* in*)
+ let cic_proof_new,new_ty,newmetasenv_new,newug =
+ try
+ (*
+ prerr_endline "refining ... (new) ";
+ CicRefine.type_of_aux'
+ newmetasenv_new context cic_proof_new ugraph*)
+ let ty,ug =
+ prerr_endline "typechecking ... (new) ";
+ CicTypeChecker.type_of_aux'
+ newmetasenv_new context cic_proof_new ugraph
+ in
+ cic_proof_new, ty, newmetasenv_new, ug
+ with
+ | CicTypeChecker.TypeCheckerFailure s ->
+ prerr_endline "FAILURE IN TYPECHECKING";
+ prerr_endline (Lazy.force s);
+ assert false
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s ->
+ prerr_endline "FAILURE IN REFINE";
+ prerr_endline (Lazy.force s);
+ interactive_comparison context cic_proof_new cic_proof;
+ assert false
+ in
+(*
+ prerr_endline "check unif ... (old vs new) ";
+ (try
+ ignore(CicUnification.fo_unif
+ newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph)
+ with CicUnification.UnificationFailure _ ->
+ prerr_endline "WARNING, new and old proofs are not unifiable");
+ prerr_endline "unif ... (new) ";
+ let subst, newmetasenv_new, newug =
+ CicUnification.fo_unif
+ newmetasenv_new context new_ty type_of_goal newug
+ in
+ if subst <> [] then
+ prerr_endline "UNIF SERVE ################################";
+*)
+ let subst = [] in
+ if List.length newmetasenv_new <> 0 then
+ prerr_endline
+ ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
+ [] newmetasenv_new);
+ (CicMetaSubst.apply_subst subst cic_proof_new),
+ newmetasenv_new,
+ (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new),
+ (CicMetaSubst.apply_subst subst new_ty),
+ newug
+(* cic_proof,newmetasenv,proof_menv,oldty,oldug*)
in
- prerr_endline (CicPp.pp proof [](* names *));
+ prerr_endline "FINAL PROOF";
+ prerr_endline (CicPp.pp cic_proof names);
+ prerr_endline "ENDOFPROOFS";
+
debug_print
(lazy
(Printf.sprintf
let real_proof =
ProofEngineReduction.replace
~equality:equality_for_replace
- ~what:[goal'] ~with_what:[proof]
+ ~what:[goal'] ~with_what:[cic_proof]
~where:meta_proof
in
debug_print
List.map (fun (i,_,_) -> i) proof_menv)
with CicTypeChecker.TypeCheckerFailure _ ->
debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
- debug_print (lazy (CicPp.pp proof names));
+ debug_print (lazy (CicPp.pp cic_proof names));
raise (ProofEngineTypes.Fail
(lazy "Found a proof, but it doesn't typecheck"))
in
(Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
(Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
(Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
- (Printf.sprintf "\nbeta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "\nmetas_of_proof: %.9f\n"
- !Inference.metas_of_proof_time) ^
(Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
(Printf.sprintf "\nforward_simpl_new_times: %.9f"
!forward_simpl_new_time) ^
(fun (u, e) ->
Printf.sprintf "%s: %s"
(UriManager.string_of_uri u)
- (string_of_equality e)
+ (Equality.string_of_equality e)
)
res))));
res in
in
let env = (metasenv, context, ugraph) in
(*try*)
- let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+ let goal =
+ ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal
+ in
let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive equalities in
Printf.printf "\nequalities:\n%s\n"
(String.concat "\n"
(List.map
- (string_of_equality ~env) equalities));
+ (Equality.string_of_equality ~env) equalities));
print_endline "--------------------------------------------------";
print_endline "GO!";
start_time := Unix.gettimeofday ();
EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
in
Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
- (String.concat "\n" (List.map (string_of_equality ~env) active))
+ (String.concat "\n" (List.map (Equality.string_of_equality ~env) active))
(* (String.concat "\n"
(List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
(String.concat "\n"
- (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
+ (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive));
print_newline ();
(*
with e ->
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof ([],goalterm), [], ty in
+ let initgoal =
+ ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty
+ in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let equalities = simplify_equalities env (equalities@library_equalities) in
let table =
(fun tbl eq -> Indexing.index tbl eq)
Indexing.empty equalities
in
- let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal
- maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
+ let _, newmeta,(newproof,newmetasenv, newty) =
+ Indexing.demodulation_goal
+ maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
in
if newmeta != maxm then
begin
let opengoal = Cic.Meta(maxm,irl) in
let proofterm =
- Inference.build_proof_term ~noproof:opengoal newproof in
+ Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in
let extended_metasenv = (maxm,context,newty)::metasenv in
let extended_status =
(curi,extended_metasenv,pbo,pty),goal in
| Eq -> "="
| Incomparable -> "I"
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
module OrderedTerm =
struct
type t = Cic.term
module IntSet = Set.Make(OrderedInt)
let compute_equality_weight (ty,left,right,o) =
- let factor = 1 in
+ let factor = 2 in
match o with
| Lt ->
let w, m = (weight_of_term
let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+
+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)
+ | _ -> []
+;;
+
type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
val print_metasenv: Cic.metasenv -> string
val print_subst: ?prefix:string -> Cic.substitution -> string
val sym_eq_URI: unit -> UriManager.uri
val eq_XURI: unit -> UriManager.uri
val trans_eq_URI: unit -> UriManager.uri
+
+val metas_of_term: Cic.term -> int list
+
projects / helm.git / commitdiff