- Equality.ml splittend in to subst.ml and equality.ml, the former only for substs
- patch to kill passive generated from an active that is dropped
- fixed deep subsumption
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
metadataQuery.cmi: proofEngineTypes.cmi
-paramodulation/equality.cmi: paramodulation/utils.cmi
+paramodulation/equality.cmi: paramodulation/utils.cmi \
+ paramodulation/subst.cmi
paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
paramodulation/equality.cmi
paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
hashtbl_equiv.cmx metadataQuery.cmi
paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi
paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
+paramodulation/subst.cmo: paramodulation/subst.cmi
+paramodulation/subst.cmx: paramodulation/subst.cmi
paramodulation/equality.cmo: paramodulation/utils.cmi \
- proofEngineReduction.cmi paramodulation/equality.cmi
+ paramodulation/subst.cmi proofEngineReduction.cmi \
+ paramodulation/equality.cmi
paramodulation/equality.cmx: paramodulation/utils.cmx \
- proofEngineReduction.cmx paramodulation/equality.cmi
+ paramodulation/subst.cmx proofEngineReduction.cmx \
+ paramodulation/equality.cmi
paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \
metadataQuery.cmi paramodulation/equality.cmi \
paramodulation/inference.cmi
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
paramodulation/utils.mli \
+ paramodulation/subst.mli\
paramodulation/equality.mli\
paramodulation/inference.mli\
paramodulation/equality_indexing.mli\
(* $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 =
Utils.comparison) * (* ordering *)
Cic.metasenv * (* environment for metas *)
int (* id *)
-and proof = new_proof * old_proof
-
-and new_proof =
+and 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
+ | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term)
+ (* subst, (rule,eq1, eq2,predicate) *)
+and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
;;
(* globals *)
let uncomparable = fun _ -> 0
-let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+let mk_equality (weight,p,(ty,l,r,o),m) =
let id = freshid () in
- let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+ let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
Hashtbl.add id_to_eq id eq;
eq
;;
let mk_tmp_equality (weight,(ty,l,r,o),m) =
let id = -1 in
- uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+ uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
;;
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,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
p,l,r
with
Not_found -> assert false
-let string_of_proof_new ?(names=[]) p gp =
+let string_of_proof ?(names=[]) p gp =
let str_of_rule = function
| SuperpositionRight -> "SupR"
| SuperpositionLeft -> "SupL"
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)
+ prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
(CicPp.pp pred names)^
aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
(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)) ^
+ (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^
aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
gp)
;;
let rec depend eq id =
- let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
+ let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
if id = ideq then true else
match p with
Exact _ -> false
| Step (_,(_,id1,(_,id2),_)) ->
- let eq1 = Hashtbl.find id_to_eq id1 in
- let eq2 = Hashtbl.find id_to_eq id2 in
- depend eq1 id || depend eq1 id2
+ let eq1 = Hashtbl.find id_to_eq id1 in
+ let eq2 = Hashtbl.find id_to_eq id2 in
+ depend eq1 id || depend eq2 id2
;;
-
-let ppsubst = ppsubst ~names:[]
+
+let ppsubst = Subst.ppsubst ~names:[];;
(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
let build_ens uri 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 (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 mk_sym uri ty t1 t2 p =
let ens, args = build_ens uri [ty;t1;t2;p] in
Cic.Appl (Cic.Const(uri, ens) :: args)
| _ -> assert false
;;
+let open_eq_ind args =
+ match args with
+ | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
+ | _ -> assert false
+;;
+
+let open_pred pred =
+ match pred with
+ | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r]))
+ when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
+ | _ -> prerr_endline (CicPp.ppterm pred); assert false
+;;
+
+let is_not_fixed t =
+ CicSubstitution.subst (Cic.Implicit None) t <>
+ CicSubstitution.subst (Cic.Rel 1) t
+;;
+
+
let canonical t =
let rec remove_refl t =
match t with
| Cic.Appl l -> Cic.Appl (List.map canonical l)
| _ -> t
in
- remove_refl (canonical t)
+ remove_refl (canonical t)
+;;
+
+let ty_of_lambda = function
+ | Cic.Lambda (_,ty,_) -> ty
+ | _ -> assert false
+;;
+
+let compose_contexts ctx1 ctx2 =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
+;;
+
+let mk_eq uri ty l r =
+ Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+;;
+
+let mk_refl uri ty t =
+ Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+;;
+
+let open_eq = function
+ | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
+ uri, ty, l ,r
+ | _ -> assert false
+;;
+
+let contextualize uri ty left right t =
+ (* aux [uri] [ty] [left] [right] [ctx] [t]
+ *
+ * the parameters validate this invariant
+ * t: eq(uri) ty left right
+ * that is used only by the base case
+ *
+ * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
+ *)
+ let rec aux uri ty left right ctx_d = function
+ | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+ let ty2,eq,lp,rp = open_pred pred in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let is_not_fixed_lp = is_not_fixed lp in
+ let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
+ (* extract the context and the fixed term from the predicate *)
+ let m, ctx_c =
+ let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
+ (* they were under a lambda *)
+ let m = CicSubstitution.subst (Cic.Implicit None) m in
+ let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
+ m, ctx_c
+ in
+ (* create the compound context and put the terms under it *)
+ let ctx_dc = compose_contexts ctx_d ctx_c in
+ let dc_what = put_in_ctx ctx_dc what in
+ let dc_other = put_in_ctx ctx_dc other in
+ (* m is already in ctx_c so it is put in ctx_d only *)
+ let d_m = put_in_ctx ctx_d m in
+ (* we also need what in ctx_c *)
+ let c_what = put_in_ctx ctx_c what in
+ (* now put the proofs in the compound context *)
+ let p1 = (* p1: dc_what = d_m *)
+ if is_not_fixed_lp then
+ aux uri ty1 c_what m ctx_d p1
+ else
+ mk_sym uri_sym ty d_m dc_what
+ (aux uri ty1 m c_what ctx_d p1)
+ in
+ let p2 = (* p2: dc_other = dc_what *)
+ if avoid_eq_ind then
+ mk_sym uri_sym ty dc_what dc_other
+ (aux uri ty1 what other ctx_dc p2)
+ else
+ aux uri ty1 other what ctx_dc p2
+ in
+ (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
+ if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
+ let a,b,c,paeqb,pbeqc =
+ if is_not_fixed_lp then
+ dc_other,dc_what,d_m,p2,p1
+ else
+ d_m,dc_what,dc_other,
+ (mk_sym uri_sym ty dc_what d_m p1),
+ (mk_sym uri_sym ty dc_other dc_what p2)
+ in
+ mk_trans uri_trans ty a b c paeqb pbeqc
+ | t ->
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+ let pred =
+ (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
+ let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
+ let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
+ let l = ctx_d in
+ let lty = CicSubstitution.lift 1 ty in
+ Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
+ in
+ let d_left = put_in_ctx ctx_d left in
+ let d_right = put_in_ctx ctx_d right in
+ let refl_eq = mk_refl uri ty d_left in
+ mk_sym uri_sym ty d_right d_left
+ (mk_eq_ind uri_ind ty left pred refl_eq right t)
+ in
+ let empty_context = Cic.Rel 1 in
+ aux uri ty left right empty_context t
;;
+let contextualize_rewrites t ty =
+ let eq,ty,l,r = open_eq ty in
+ contextualize eq ty l r t
+;;
+
let build_proof_step subst p1 p2 pos l r pred =
- 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,body = (* Cic.Implicit None *)
+ let p1 = Subst.apply_subst subst p1 in
+ let p2 = Subst.apply_subst subst p2 in
+ let l = Subst.apply_subst subst l in
+ let r = Subst.apply_subst subst r in
+ let pred = Subst.apply_subst subst pred in
+ let ty,body =
match pred with
| Cic.Lambda (_,ty,body) -> ty,body
| _ -> assert false
in
- let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+ let what, other =
if pos = Utils.Left then l,r else r,l
in
- let is_not_fixed t =
- CicSubstitution.subst (Cic.Implicit None) t <>
- CicSubstitution.subst (Cic.Rel 1) t
- in
- match body,pos with
-(*
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty other what third
- (mk_sym uri_sym ty what other p2) p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty other what third p2 p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1 p2
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1
- (mk_sym uri_sym ty other what p2)
- | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr) (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other =
- CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr)
- (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr))
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
-*)
- | _, Utils.Left ->
+ match pos with
+ | Utils.Left ->
mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
- | _, Utils.Right ->
+ | Utils.Right ->
mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
;;
-let build_proof_term_new proof =
+let build_proof_term proof =
let rec aux = function
| Exact term -> term
| Step (subst,(_, id1, (pos,id2), pred)) ->
let string_of_id names id =
try
- let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
match p with
| Exact t ->
Printf.sprintf "%d = %s: %s = %s" id
((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
;;
-let build_goal_proof l initial =
+let build_goal_proof l initial ty =
let proof =
List.fold_left
(fun current_proof (pos,id,subst,pred) ->
let p,l,r = proof_of_id id in
- let p = build_proof_term_new p in
+ let p = build_proof_term p in
let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
build_proof_step subst current_proof p pos l r pred)
initial l
in
- canonical proof
+ canonical (contextualize_rewrites proof ty)
;;
let refl_proof ty term =
ty; term]
;;
-let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+let metas_of_proof p =
+ Utils.metas_of_term (build_proof_term p)
+;;
let relocate newmeta menv =
let subst, metasenv, newmeta =
let irl = [] (*
CicMkImplicit.identity_relocation_list_for_metavariable context *)
in
- let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
+ let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
let newmeta = maxmeta, context, ty in
newsubst, newmeta::menv, maxmeta+1)
- menv ([], [], newmeta+1)
+ menv (Subst.empty_subst, [], newmeta+1)
in
- let metasenv = apply_subst_metasenv subst metasenv in
- let subst = flatten_subst subst in
+ let metasenv = Subst.apply_subst_metasenv subst metasenv in
+ let subst = 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
+ let w, p, (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 ty = Subst.apply_subst subst ty in
+ let left = Subst.apply_subst subst left in
+ let right = Subst.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)
+ | Exact p -> Exact (Subst.apply_subst subst p)
| Step (s,(r,id1,(pos,id2),pred)) ->
- Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+ Step (Subst.concat_substs s subst,(r,id1,(pos,id2), 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
+ let p = fix_proof p in
+ let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
(* debug prerr_endline (string_of_equality eq); *)
newmeta+1, eq
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
+ let e = mk_equality (w, Exact proof, stat,[]) in
e
| _ ->
raise TermIsNotAnEquality
* http://helm.cs.unibo.it/
*)
-type substitution
-
-type rule = SuperpositionRight | SuperpositionLeft |Demodulation
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
type equality
-and proof = new_proof * old_proof
-
-and new_proof =
+and 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
+ | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term)
-and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
-val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
-
-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 pp_proof: (Cic.name option) list -> goal_proof -> proof -> string
val reset : unit -> unit
int * proof *
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
Cic.metasenv * int
+val depend : equality -> int -> bool
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
-val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
-val build_goal_proof: goal_proof -> Cic.term -> Cic.term
+val string_of_proof :
+ ?names:(Cic.name option)list -> proof -> goal_proof -> string
+val build_proof_term: proof -> Cic.term
+(* build_goal_proof [goal_proof] [initial_proof] [ty]
+ * [ty] is the type of the goal *)
+val build_goal_proof: goal_proof -> Cic.term -> Cic.term-> Cic.term
val refl_proof: Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality
val is_weak_identity: equality -> bool
val is_identity: Utils.environment -> equality -> bool
-
let indexing_retrieval_time = ref 0.;;
-let apply_subst = Equality.apply_subst
+let apply_subst = Subst.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+ (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
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"
+ (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
in
check_for_duplicates metas "gia nella metas";
check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
- (match Equality.merge_subst_if_possible subst subst' with
+ (match Subst.merge_subst_if_possible subst subst' with
| None -> ok what tl
| Some s -> Some (s, equation))
with Inference.MatchingFailure ->
let module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, ((proof_new, proof_old) (*as proof*)),
- (eq_ty, left, right, order), metas, id =
- Equality.open_equality target in
+ let w, proof, (eq_ty, left, right, order), metas, id =
+ Equality.open_equality target
+ in
(* first, we simplify *)
(* let right = U.guarded_simpl context right in *)
(* let left = U.guarded_simpl context left in *)
begin
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
- let substs = Equality.ppsubst subst in
+ let substs = Subst.ppsubst subst in
ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
- let (_, (proof'_new,proof'_old),
+ let (_, proof',
(ty, what, other, _), menv',id') = Equality.open_equality equality in
let ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
- (bo,
- (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)))
+ (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
+ (Cic.Lambda (name, ty, bo'))))))
else
assert false
(*
if Utils.debug_metas then
try ignore(CicTypeChecker.type_of_aux'
newmenv context
- (Equality.build_proof_term_old (snd newproof)) ugraph);
+ (Equality.build_proof_term newproof) ugraph);
()
with exc ->
prerr_endline "sempre lui";
- prerr_endline (Equality.ppsubst subst);
+ prerr_endline (Subst.ppsubst subst);
prerr_endline (CicPp.ppterm
- (Equality.build_proof_term_old (snd newproof)));
+ (Equality.build_proof_term newproof));
prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
+ prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
newmenv));
raise exc;
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
Equality.open_equality target
in
if Utils.debug_metas then
S.lift 1 eq_ty; l; r]
in
bo',
- (Equality.Step
- (s,(Equality.SuperpositionRight,
- id,(pos,id'),(Cic.Lambda(name,ty,bo'')))),
- Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
-
+ Equality.Step
+ (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
in
let newmeta, newequality =
let left, right =
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let (cicproof,proof), metas, term = goal in
+ let goalproof, metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = (cicproof,proof), metas, term in
+ let goal = goalproof, metas, term in
let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, equality = eq_found in
- let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
+ let (_, proof', (ty, what, other, _), menv',id) =
Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
- let newterm, newproof, newcicproof =
+ let newterm, newgoalproof =
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 bo' = (*apply_subst subst*) t in
let name = C.Name "x" in
incr demod_counter;
- let metaproof =
- incr maxmeta;
- 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 eq_found_proof =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof')
- in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
- in
- let goal_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- let rec repl = function
- | Equality.NoProof ->
-(* debug_print (lazy "replacing a NoProof"); *)
- pb
- | Equality.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
-(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | Equality.SubProof (term, meta_index, p) ->
- prerr_endline "subproof!";
- Equality.SubProof (term, meta_index, repl p)
- | _ -> assert false
- in repl proof
- in
- let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
- bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
- (newcicproofstep::cicproof)
+ let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
+ !maxmeta, (newgoalproof, newmetasenv, newterm)
in
let res =
demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newty =
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
- let bo' = apply_subst subst t in
- let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
+(* let bo' = apply_subst subst t in *)
+(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
incr demod_counter;
+(*
let newproofold =
Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
Equality.BasicProof (Equality.empty_subst,term))
in
(Equality.build_proof_term_old newproofold, bo)
+*)
+ (* TODO, not ported to the new proofs *)
+ if true then assert false; term, bo
in
!maxmeta, (newterm, newty, menv)
in
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.equality ->
- (Equality.substitution * Equality.equality) option
+ (Subst.substitution * Equality.equality) option
val superposition_left :
int ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key ->
+ Equality.goal_proof * Cic.metasenv * Index.key ->
bool * int *
- ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key)
+ (Equality.goal_proof * Cic.metasenv * Index.key)
val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+ (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
let module C = Cic in
let module M = CicMetaSubst in
let module U = CicUnification in
- let lookup = Equality.lookup_subst in
+ let lookup = Subst.lookup_subst in
let rec occurs_check subst what where =
match where with
| t when what = t -> true
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
- assert (not (Equality.is_in_subst i subst));
- let subst = Equality.buildsubst i context t ty subst in
+ assert (not (Subst.is_in_subst i subst));
+ let subst = Subst.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 Equality.empty_subst metasenv t1 t2 in
- let menv = Equality.filter subst menv in
+ let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
+ let menv = Subst.filter subst menv in
subst, menv, ugraph
;;
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = compute_equality_weight stat 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 proof = Equality.Exact p in
let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)
| _ -> None, newmeta
let stat = (ty,t1,t2,o) in
let w = compute_equality_weight 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 proof = Equality.Exact p in
let e = Equality.mk_equality (w, proof,stat,[]) 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 proof_old =
- Equality.BasicProof (Equality.empty_subst,p) in
- let proof_new = Equality.Exact p in
- let proof = proof_new, proof_old in
+ let proof = Equality.Exact p 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 old_proof = Equality.BasicProof (Equality.empty_subst,term) in
- let new_proof = Equality.Exact term in
- let proof = new_proof, old_proof in
+ let proof = Equality.Exact term in
let e = Equality.mk_equality (w, proof, stat, []) in
Some e, (newmeta+1)
| _ -> None, newmeta
Cic.metasenv -> Cic.metasenv -> Cic.context ->
Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
(**
special unification that checks if the two terms are "simple", and in
Cic.metasenv -> Cic.metasenv -> Cic.context ->
Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
(**
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
+ Equality.goal_proof * Equality.proof * Subst.substitution * Cic.metasenv
type result =
| ParamodulationFailure
- | ParamodulationSuccess of (new_proof * old_proof) option
+ | ParamodulationSuccess of new_proof option
;;
-type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;;
+type goal = Equality.goal_proof * Cic.metasenv * Cic.term;;
type theorem = Cic.term * Cic.term * Cic.metasenv;;
match !weight_age_counter with
| 0 -> (
weight_age_counter := !weight_age_ratio;
- match pos_list with
- | (hd:EqualitySet.elt)::tl ->
- let passive_table =
- Indexing.remove_index passive_table hd
- in hd, ((tl, EqualitySet.remove hd pos_set), passive_table)
- | _ -> assert false)
+ let rec skip_giant pos_list pos_set passive_table =
+ match pos_list with
+ | (hd:EqualitySet.elt)::tl ->
+ let w,_,_,_,_ = Equality.open_equality hd in
+ let passive_table =
+ Indexing.remove_index passive_table hd
+ in
+ let pos_set = EqualitySet.remove hd pos_set in
+ if w < 50 then
+ hd, ((tl, pos_set), passive_table)
+ else
+ (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n");
+ skip_giant tl pos_set passive_table)
+ | _ -> assert false
+ in
+ skip_giant pos_list pos_set passive_table)
| _ when (!symbols_counter > 0) ->
(symbols_counter := !symbols_counter - 1;
let cardinality map =
passive_table)
;;
+let filter_dependent passive id =
+ prerr_endline ("+++++++++++++++passives "^
+ ( string_of_int (size_of_passive passive)));
+ let (pos_list, pos_set), passive_table = passive in
+ let passive =
+ List.fold_right
+ (fun eq ((list,set),table) ->
+ if Equality.depend eq id then
+ (let _,_,_,_,id_eq = Equality.open_equality eq in
+ if id_eq = 9228 then
+ prerr_endline ("\n\n--------filtering "^(string_of_int id_eq));
+ ((list,
+ EqualitySet.remove eq set),
+ Indexing.remove_index table eq))
+ else ((eq::list, set),table))
+ pos_list (([],pos_set),passive_table) in
+ prerr_endline ("+++++++++++++++passives "^
+ ( string_of_int (size_of_passive passive)));
+ passive
+;;
+
(* initializes the passive set of equalities *)
let make_passive pos =
match t1,t2 with
| t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
| t1, t2 when subsumption_used -> t1 = t2, subsumption_used
+(* VERSIONE ERRATA
| Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
let rc = check_subsumed b t1 t1 in
if rc then
true, true
+ else if h1 = h2 then
+ (try
+ List.fold_left2
+ (fun (ok_so_far, subsumption_used) t t' ->
+ aux true (ok_so_far, subsumption_used) t t')
+ (ok_so_far, subsumption_used) l l'
+ with Invalid_argument _ -> false,subsumption_used)
else
+ false, subsumption_used
+ | _ -> false, subsumption_used *)
+ | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
+ let rc = check_subsumed b t1 t2 in
+ if rc then
+ true, true
+ else if h1 = h2 then
(try
List.fold_left2
(fun (ok_so_far, subsumption_used) t t' ->
aux true (ok_so_far, subsumption_used) t t')
(ok_so_far, subsumption_used) l l'
with Invalid_argument _ -> false,subsumption_used)
- | _ -> false, subsumption_used
+ else
+ false, subsumption_used
+ | _ -> false, subsumption_used
in
fst (aux false (true,false) left right)
;;
(* if Indexing.subsumption env active_table c = None then*)
(match Indexing.subsumption env passive_table c with
| None -> res
- | Some (_,c') -> None (*Some c'*))
+ | Some (_,c') ->
+ None
+ (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
+ Some c'*))
(*
else
None
let find eq1 where =
List.exists (Equality.meta_convertibility_eq eq1) where
in
- let active, newa =
+ let id_of_eq eq =
+ let _, _, _, _,id = Equality.open_equality eq in id
+ in
+ let ((active1,pruned),tbl), newa =
List.fold_right
- (fun eq (res, tbl) ->
+ (fun eq ((res,pruned), tbl) ->
if List.mem eq res then
- res, tbl
+ (res, (id_of_eq eq)::pruned),tbl
else if (Equality.is_identity env eq) || (find eq res) then (
- res, tbl
+ (res, (id_of_eq eq)::pruned),tbl
)
else
- eq::res, Indexing.index tbl eq)
- active_list ([], Indexing.empty),
+ (eq::res,pruned), Indexing.index tbl eq)
+ active_list (([],pruned), Indexing.empty),
List.fold_right
(fun eq p ->
if (Equality.is_identity env eq) then p
else eq::p)
newa []
in
+ if List.length active1 <> List.length (fst active) then
+ prerr_endline "\n\n\nMANCAVANO DELLE PRUNED!!!!\n\n\n";
match newa with
- | [] -> active, None
- | _ -> active, Some newa
+ | [] -> (active1,tbl), None, pruned
+ | _ -> (active1,tbl), Some newa, pruned
;;
([], Indexing.empty, 1000000) new'
in
*)
- let active, newa =
+ let active, newa, pruned =
backward_simplify_active env new_pos new_table min_weight active in
match passive with
| None ->
- active, (make_passive []), newa, None
+ active, (make_passive []), newa, None, pruned
| Some passive ->
- active, passive, newa, None
+ active, passive, newa, None, pruned
(* prova
let passive, newp =
backward_simplify_passive env new_pos new_table min_weight passive in
Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
;;
-let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
+let check_if_goal_is_subsumed env (goalproof,menv,ty) table =
prerr_endline "check_goal_subsumed";
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
(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
- prerr_endline "1";
- let p = Equality.apply_subst subst
- (Equality.build_proof_term_old p) in
- prerr_endline "2";
- 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
- prerr_endline "3";
- let newcicp,np,subst,cicmenv =
- cicproof,np, subst,
- Equality.apply_subst_metasenv subst (m @ menv)
- in
- prerr_endline ".";
- Some
- ((newcicp,np,subst,cicmenv),
- (newp, Equality.apply_subst_metasenv subst m @ menv ))
- | None -> None)
+ (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv)
+ in
+ match Indexing.subsumption env table goal_equation with
+ | Some (subst, equality ) ->
+ let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
+ let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+ Some (goalproof, p, subst, cicmenv)
+ | None -> None)
| _ -> None
;;
(* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
match (fst goals) with
- | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_
+ | (_,[goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_
when left = right && iseq uri ->
- let p =
- Cic.Appl [Cic.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
- 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 (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
+ let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+ true, Some (goalproof, reflproof, Subst.empty_subst,m)
+ | (_, [goal])::_ ->
+ (match check_if_goal_is_subsumed env goal (snd active) with
| None -> false,None
| Some p ->
prerr_endline "Proof found by subsumption!";
forward_simpl_new_time :=
!forward_simpl_new_time +. (t2 -. t1);
let t1 = Unix.gettimeofday () in
- let active, passive, newa, retained =
+ let active, passive, newa, retained, pruned =
backward_simplify env new' ~passive active in
+ let passive =
+ List.fold_left filter_dependent passive pruned in
let t2 = Unix.gettimeofday () in
backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
match newa, retained with
| Some p, Some rp ->
simplify (new' @ p @ rp) active passive
in
- let active, _, new' = simplify new' active passive in
+ let active, passive, new' = simplify new' active passive in
let goals =
let a,b,_ = build_table new' in
simplify_goals env goals ~passive (a,b)
in
let rec simplify new' active passive =
let new' = forward_simplify_new env new' ~passive active in
- let active, passive, newa, retained =
+ let active, passive, newa, retained, pruned =
backward_simplify env new' ~passive active in
+ let passive =
+ List.fold_left filter_dependent passive pruned in
match newa, retained with
| None, None -> active, passive, new'
| Some p, None
in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
- let goal =
- ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal
- in
+ let goal = [], [], goal in
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
in
match res with
| ParamodulationSuccess
- (Some
- ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *)
- (proof, proof_menv))) (* OLD *)
+ (Some (goalproof,newproof,subsumption_subst, proof_menv))
->
prerr_endline "OK, found a proof!";
* goalproof);*)
prerr_endline (Equality.pp_proof names goalproof newproof);
- (* generation of the old proof *)
- let cic_proof = Equality.build_proof_term_old proof in
-
- (* generation of the new proof *)
+ (* generation of the proof *)
let cic_proof_new =
Equality.build_goal_proof
- goalproof (Equality.build_proof_term_new newproof)
+ goalproof (Equality.build_proof_term newproof) type_of_goal
in
let cic_proof_new =
- Equality.apply_subst subsumption_subst cic_proof_new
+ Subst.apply_subst subsumption_subst cic_proof_new
in
(* replacing fake mets with real ones *)
| _ -> false
in
let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
- prerr_endline "replacing metas (old)";
- let proof_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)
- ([],[],[]) proof_menv
- in
- 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
(i,context,ty)::acc1,
(Cic.Meta(i,[]))::acc2,
(Cic.Meta(i,irl)) ::acc3)
- ([],[],[]) newproof_menv
+ ([],[],[]) proof_menv
in
let cic_proof_new = ProofEngineReduction.replace_lifting
~equality:(=)
in
(* pp new/old proof *)
-(* prerr_endline "OLDPROOF";*)
-(* prerr_endline (Equality.string_of_proof_old proof);*)
-(* prerr_endline "OLDPROOFCIC";*)
-(* prerr_endline (CicPp.pp cic_proof names); *)
(* prerr_endline "NEWPROOFCIC";*)
(* prerr_endline (CicPp.pp cic_proof_new names); *)
List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
in
let newmetasenv_new = newmetasenv@newproof_menv in
- let newmetasenv = newmetasenv@proof_menv in
(* check/refine/... build the new proof *)
let newstatus =
let cic_proof,newmetasenv,proof_menv,ty, ug =
- prerr_endline "type checking ... (old) ";
- let _old_ty, _oldug =
- try
- CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph
- with
- CicTypeChecker.TypeCheckerFailure s ->
- prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!";
- prerr_endline (Lazy.force s);
- Cic.Implicit None, CicUniv.empty_ugraph
- in
let cic_proof_new,new_ty,newmetasenv_new,newug =
try
(*
in
let env = (metasenv, context, ugraph) in
(*try*)
- let goal =
- ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal
+ let goal = [], [], goal
in
let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
if library_equalities = [] then prerr_endline "VUOTA!!!";
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 =
- ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty
- in
+ let initgoal = [], [], ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let equalities = simplify_equalities env (equalities@library_equalities) in
let table =
begin
let opengoal = Cic.Meta(maxm,irl) in
let proofterm =
- Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in
+ Equality.build_goal_proof newproof opengoal ty in
let extended_metasenv = (maxm,context,newty)::metasenv in
let extended_status =
(curi,extended_metasenv,pbo,pty),goal in
--- /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 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 = [];;
+
+let concat_substs x y = x @ y;;
+
--- /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
+
+val empty_subst : substitution
+val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst : ?names:(Cic.name option list) -> 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 concat_substs: substitution -> substitution -> substitution
+
projects / helm.git / commitdiff