(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
-
+
let eqsig = ref (fun _ -> assert false);;
let set_sig f = eqsig:= f;;
let get_sig = fun x -> !eqsig x;;
List.fold_left
(fun (i,acc) t ->
i+1,
- let f = extract amount vl f in
+ let f = extract amount vl f in
if i = n then
let imp = NCic.Implicit `Term in
NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
in aux ft (List.rev pl)
;;
- let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
+ let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
+ let module NCicBlob =
+ NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end)
+ in
+ let module Pp = Pp.Pp(NCicBlob)
+ in
let module Subst = FoSubst in
let position i l =
let rec aux = function
let get_literal id =
let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
let lit =match lit with
- | Terms.Predicate t -> assert false
+ | Terms.Predicate t -> t (* assert false *)
| Terms.Equation (l,r,ty,_) ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
in
let lit,_,_ = get_literal mp in
let lit = Subst.apply_subst subst lit in
extract 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
+ in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1
| id :: tl ->
let amount = List.length seen in
let lit,vl,proof = get_literal id in
if not ongoal && id = mp then
- let lit = Subst.apply_subst subst lit in
+ let lit = Subst.apply_subst subst lit in
let eq_ty = extract amount [] lit in
- let refl = mk_refl eq_ty in
- (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
- (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
+ let refl =
+ if demod then NCic.Implicit `Term
+ else mk_refl eq_ty in
+ (* 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
~avoid_beta_redexes:true ~no_implicit:false refl
aux ongoal seen tl
| Terms.Step _ when tl=[] -> assert false
| Terms.Exact ft ->
- (* prerr_endline ("Exact for " ^ (string_of_int id));*)
- (*
+ (*
+ prerr_endline ("Exact for " ^ (string_of_int id));
NCic.LetIn ("clause_" ^ string_of_int id,
close_with_forall vl (extract amount vl lit),
close_with_lambdas vl (extract amount vl ft),
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
| Terms.Step (_, id1, id2, dir, pos, subst) ->
let id, id1,(lit,vl,proof) =
- if ongoal then id1,id,get_literal id1
- else id,id1,(lit,vl,proof)
- in
- let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
+ 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)
+ 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 *)
+ let vl = if ongoal then [] else vl in
let proof_of_id id =
let vars = List.rev (vars_of id seen) in
let args = List.map (Subst.apply_subst subst) vars in
extract amount vl (Subst.apply_subst subst r)
| _ -> assert false
in
- (*prerr_endline "mk_predicate :";
+ (*
+ 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 ("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)));*)
let body = aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
in
- if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+ let occ= NCicUntrusted.count_occurrences [] 1 body in
+ if occ <= 1 then
NCicSubstitution.subst
~avoid_beta_redexes:true ~no_implicit:false
(close_with_lambdas vl rewrite_step) body