extract t
;;
-
let mk_predicate status hole_type amount ft p1 vl =
let rec aux t p =
match p with
end)
in
let module Pp = Pp.Pp(NCicBlob) in
- prerr_endline ("term: " ^ Pp.pp_foterm ft);
- prerr_endline ("path: " ^ String.concat ","
+ (* prerr_endline ("term: " ^ Pp.pp_foterm ft);
+ prerr_endline ("path: " ^ String.concat ","
(List.map string_of_int p1));
- prerr_endline ("leading to: " ^ Pp.pp_foterm t);
+ prerr_endline ("leading to: " ^ Pp.pp_foterm t); *)
assert false
| Terms.Node l ->
let l =
let module Pp = Pp.Pp(NCicBlob)
in
let module Subst = FoSubst in
+ let compose subst1 subst2 =
+ let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in
+ let s2 = List.filter (fun (m,_) -> not (List.mem_assoc m s1)) subst2
+ in s1 @ s2
+ in
let position i l =
let rec aux = function
| [] -> assert false
let lit = Subst.apply_subst subst lit in
extract status 0 [] lit in
(* composition of all subst acting on goal *)
- let res_subst =
- let rec rsaux ongoal acc =
- function
- | [] -> acc (* is the final subst for refl *)
- | id::tl when ongoal ->
- let lit,vl,proof = get_literal id in
- (match proof with
- | Terms.Exact _ -> rsaux ongoal acc tl
- | Terms.Step (_, _, _, _, _, s) ->
- rsaux ongoal (s@acc) tl)
- | id::tl ->
- (* subst is the the substitution for refl *)
- rsaux (id=mp) subst tl
- in
- let r = rsaux false [] steps in
- (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
- prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
- r
+ let res_subst = subst
in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1
let refl =
if demod then NCic.Implicit `Term
else mk_refl eq_ty in
- (* prerr_endline ("Reached m point, id=" ^ (string_of_int id));
+ (* prerr_endline ("Reached m point, id=" ^ (string_of_int id));
(NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
aux true ((id,([],lit))::seen) (id::tl))) *)
- NCicSubstitution.subst status
+ let res = NCicSubstitution.subst status
~avoid_beta_redexes:true ~no_implicit:false refl
(aux true ((id,([],lit))::seen) (id::tl))
+ in res
else
match proof with
| Terms.Exact _ when tl=[] ->
- (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
+ (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id)); *)
aux ongoal seen tl
| Terms.Step _ when tl=[] -> assert false
| Terms.Exact ft ->
close_with_lambdas vl (extract status amount vl ft),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- *)
- NCicSubstitution.subst status
+ *)
+ let res = NCicSubstitution.subst status
~avoid_beta_redexes:true ~no_implicit:false
(close_with_lambdas vl (extract status amount vl ft))
(aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ in res
| Terms.Step (_, id1, id2, dir, pos, subst) ->
+ (* prerr_endline (if ongoal then "on goal" else "not on goal");
+ prerr_endline (Pp.pp_substitution subst); *)
+ (* let subst = if ongoal then res_subst else subst in *)
let id, id1,(lit,vl,proof) =
if ongoal then
let lit,vl,proof = get_literal id1 in
- id1,id,(Subst.apply_subst res_subst lit,
- Subst.filter res_subst vl, proof)
+ id1,id,(Subst.apply_subst res_subst lit,
+ Subst.filter res_subst vl, proof)
else id,id1,(lit,vl,proof) in
(* free variables remaining in the goal should not
be abstracted: we do not want to prove a generalization *)
+ (* prerr_endline ("variables = " ^ String.concat ","
+ (List.map string_of_int vl)); *)
let vl = if ongoal then [] else vl in
let proof_of_id id =
let vars = List.rev (vars_of id seen) in
in
let p_id1 = proof_of_id id1 in
let p_id2 = proof_of_id id2 in
-(*
- let morphism, l, r =
- let p =
- if (ongoal=true) = (dir=Terms.Left2Right) then
- p_id2
- else sym p_id2 in
- let id1_ty = ty_of id1 seen in
- let id2_ty,l,r =
- match ty_of id2 seen with
- | Terms.Node [ _; t; l; r ] ->
- extract status amount vl (Subst.apply_subst subst t),
- extract status amount vl (Subst.apply_subst subst l),
- extract status amount vl (Subst.apply_subst subst r)
- | _ -> assert false
- in
- (*prerr_endline "mk_predicate :";
- if ongoal then prerr_endline "ongoal=true"
- else prerr_endline "ongoal=false";
- prerr_endline ("id=" ^ string_of_int id);
- prerr_endline ("id1=" ^ string_of_int id1);
- prerr_endline ("id2=" ^ string_of_int id2);
- prerr_endline ("Positions :" ^
- (String.concat ", "
- (List.map string_of_int pos)));*)
- mk_morphism
- p amount (Subst.apply_subst subst id1_ty) pos vl,
- l,r
- in
- let rewrite_step = iff1 morphism p_id1
- in
-*)
let pred, hole_type, l, r =
let id1_ty = ty_of id1 seen in
let id2_ty,l,r =
extract status amount vl (Subst.apply_subst subst r)
| _ -> assert false
in
- (*
- prerr_endline "mk_predicate :";
- if ongoal then prerr_endline "ongoal=true"
- else prerr_endline "ongoal=false";
- prerr_endline ("id=" ^ string_of_int id);
- prerr_endline ("id1=" ^ string_of_int id1
- ^": " ^ Pp.pp_foterm id1_ty);
- prerr_endline ("id2=" ^ string_of_int id2
- ^ ": " ^ NCicPp.ppterm [][][] id2_ty);
- prerr_endline ("Positions :" ^
- (String.concat ", "
- (List.map string_of_int pos)));*)
- mk_predicate status
+ (* let _ = prerr_endline ("body = " ^(Pp.pp_foterm id1_ty))
+ in *)
+ mk_predicate status
id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
id2_ty,
l,r
bag, maxvar, res
;;
- let rewrite_eq ~unify l r ty vl table =
+ (* rewrite_eq check if in table there an equation matching l=r;
+ used in subsumption and deep_eq. In deep_eq, we need to match
+ several times times w.r.t. the same table, hence we should refresh
+ the retrieved clauses, to avoid clashes of variables *)
+
+ let rewrite_eq ~refresh ~unify maxvar l r ty vl table =
let retrieve = if unify then IDX.DT.retrieve_unifiables
else IDX.DT.retrieve_generalizations in
let lcands = retrieve table l in
let rcands = retrieve table r in
- let f b c =
+ let f b c =
let id, dir, l, r, vl =
match c with
| (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
| [] -> None
| (id2,dir,c,vl1)::tl ->
try
+ let c,maxvar = if refresh then
+ let maxvar,_,r = Utils.relocate maxvar vl1 [] in
+ Subst.apply_subst r c,maxvar
+ else c,maxvar in
let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
- Some (id2, dir, subst)
+ Some (id2, dir, subst, maxvar)
with FoUnif.UnificationFailure _ -> aux tl
in
aux (cands1 @ cands2)
match lit with
| Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,_) ->
- match rewrite_eq ~unify l r ty vl table with
+ match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with
| None -> None
- | Some (id2, dir, subst) ->
+ | Some (id2, dir, subst, maxvar) ->
let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
build_new_clause bag maxvar (fun _ -> true)
Terms.Superposition id_t subst id id2 [2] dir
(* id refers to a clause proving contextl l = contextr r *)
let rec deep_eq ~unify l r ty pos contextl contextr table acc =
+ (* let _ = prerr_endline ("pos = " ^ String.concat ","
+ (List.map string_of_int pos)) in *)
match acc with
| None -> None
| Some(bag,maxvar,(id,lit,vl,p),subst) ->
(* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
+ (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *)
+ (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *)
let l = Subst.apply_subst subst l in
let r = Subst.apply_subst subst r in
+ (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *)
+ (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *)
try
let subst1 = Unif.unification (* vl *) [] l r in
let lit =
match lit with Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,o) ->
- Terms.Equation (FoSubst.apply_subst subst1 l,
- FoSubst.apply_subst subst1 r, ty, o)
+ let l = Subst.apply_subst subst1 l in
+ let r = Subst.apply_subst subst1 r in
+ Terms.Equation (l, r, ty, o)
in
Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst)
with FoUnif.UnificationFailure _ ->
- match rewrite_eq ~unify l r ty vl table with
- | Some (id2, dir, subst1) ->
+ match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with
+ | Some (id2, dir, subst1, maxvar) ->
(* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
- prerr_endline ("old subst = "^Pp.pp_substitution subst);*)
+ prerr_endline ("old subst = "^Pp.pp_substitution subst); *)
let newsubst = Subst.concat subst1 subst in
let id_t =
FoSubst.apply_subst newsubst
(Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r])
in
- (match
+ (match
build_new_clause_reloc bag maxvar (fun _ -> true)
Terms.Superposition id_t
- subst1 id id2 (pos@[2]) dir
- with
+ subst1 id id2 (pos@[2]) dir
+ with
| Some ((bag, maxvar), c), r ->
- (* prerr_endline ("r = "^Pp.pp_substitution r); *)
+ (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *)
+ (* prerr_endline ("r = "^Pp.pp_substitution r); *)
let newsubst = Subst.flat
(Subst.concat r subst) in
Some(bag,maxvar,c,newsubst)
let bag, clause =
if no_demod then bag, clause else demodulate bag clause table
in
- let _ = debug (lazy ("demodulated goal : "
+ let _ = debug(lazy ("demodulated goal : "
^ Pp.pp_unit_clause clause))
in
if List.exists (are_alpha_eq clause) g_actives then None
| None -> Some (bag,clause)
| Some (bag,maxvar,cl,subst) ->
debug (lazy "Goal subsumed");
+ debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst));
raise (Success (bag,maxvar,cl,subst))
(*
match is_subsumed ~unify:true bag maxvar clause table with
| None -> Some (bag, clause)
| Some ((bag,maxvar),c) ->
- prerr_endline "Goal subsumed";
+ debug (lazy "Goal subsumed");
raise (Success (bag,maxvar,c))
*)
;;
projects / helm.git / commitdiff