NCic.Const r
;;
+ let eq_refl =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
+ in
+ NCic.Const r
+ ;;
+
let extract lift vl t =
let rec pos i = function
| [] -> raise Not_found
| Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
;;
- let mk_predicate amount ft p vl =
+ let mk_predicate hole_type amount ft p vl =
let rec aux t p =
match p with
| [] -> NCic.Rel 1
in
NCic.Appl l
in
- NCic.Lambda("x", NCic.Implicit `Type, aux ft (List.rev p))
+ NCic.Lambda("x", hole_type, aux ft (List.rev p))
;;
- let mk_proof (bag : NCic.term Terms.bag) steps =
+ let mk_proof (bag : NCic.term Terms.bag) mp steps =
let module Subst = FoSubst in
let position i l =
let rec aux = function
NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
t vl
in
- let rec aux seen = function
+ let close_with_forall vl t =
+ List.fold_left
+ (fun t i ->
+ NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
+ t vl
+ in
+ let rec aux ongoal seen = function
| [] -> NCic.Rel 1
| id :: tl ->
-(* prerr_endline ("Let4 : " ^string_of_int id); *)
let amount = List.length seen in
let _, lit, vl, proof = Terms.M.find id bag in
let lit =
| Terms.Equation (l,r,ty,_) ->
Terms.Node [ Terms.Leaf eqP; ty; l; r]
in
-(* prerr_endline ("X" ^ ppfot lit); *)
+ if not ongoal && id = mp then
+ (assert (vl = []);
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ extract amount vl lit,
+ (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]),
+ aux true ((id,([],lit))::seen) (id::tl)))
+ else
match proof with
+ | Terms.Exact _ when tl=[] -> aux ongoal seen tl
+ | Terms.Step _ when tl=[] -> assert false
| Terms.Exact ft ->
- NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type,
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
close_with_lambdas vl (extract amount vl ft),
- aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
| Terms.Step (_, id1, id2, dir, pos, subst) ->
+ let id, id1 = if ongoal then id1,id else id,id1 in
let proof_of_id id =
- let vars = vars_of id seen in
+ let vars = List.rev (vars_of id seen) in
let args = List.map (Subst.apply_subst subst) vars in
let args = List.map (extract amount vl) args in
NCic.Appl (NCic.Rel (List.length vl + position id seen) :: args)
in
let p_id1 = proof_of_id id1 in
let p_id2 = proof_of_id id2 in
- let pred =
+ let pred, hole_type, l, r =
let id1_ty = ty_of id1 seen in
- mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl
+ let id2_ty,l,r =
+ match ty_of id2 seen with
+ | Terms.Node [ _; t; l; r ] ->
+ extract amount vl (Subst.apply_subst subst t),
+ extract amount vl (Subst.apply_subst subst l),
+ extract amount vl (Subst.apply_subst subst r)
+ | _ -> assert false
+ in
+ mk_predicate
+ id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
+ id2_ty,
+ l,r
+ in
+ let l, r, eq_ind =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ r,l,eq_ind_r
+ else
+ l,r,eq_ind
in
- let eq_ind = if dir=Terms.Left2Right then eq_ind else eq_ind_r in
- NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type,
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
close_with_lambdas vl
- (NCic.Appl [ eq_ind ; NCic.Implicit `Type;
- pred; NCic.Implicit `Term; p_id1;
- NCic.Implicit `Term; p_id2 ]),
- aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
+ aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
in
- aux [] steps
+ aux false [] steps
;;
end
Set.Make(struct type t=int let compare=Pervasives.compare end)
in
let all id =
- let rec traverse acc i =
+ let rec traverse ongoal (accg,acce) i =
match Terms.M.find i bag with
- | (_,_,_,Terms.Exact _) -> acc
+ | (_,_,_,Terms.Exact _) -> accg, acce
| (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
- traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2
+ let accg, acce =
+ if ongoal then C.add i1 accg, acce
+ else accg, C.add i1 acce
+ in
+ let acce = C.add i2 acce in
+ traverse false (traverse ongoal (accg,acce) i1) i2
in
- C.elements (traverse C.empty id)
+ traverse true (C.empty,C.empty) id
in
- S.topological_sort (all i) all
+ let esteps =
+ S.topological_sort (C.elements (snd (all i)))
+ (fun i -> C.elements (snd (all i)))
+ in
+ let gsteps =
+ S.topological_sort (C.elements (fst (all i)))
+ (fun i -> C.elements (fst (all i)))
+ in
+ let gsteps = List.rev gsteps in
+ esteps@gsteps
in
prerr_endline "YES!";
prerr_endline "Proof:";
List.iter (fun x ->
prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
- let proofterm = B.mk_proof bag l in
+ let proofterm = B.mk_proof bag i l in
prerr_endline
(NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
proofterm);
let _metasenv, _subst, _proofterm, _prooftype =
NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
in
+ prerr_endline "REFINED!";
()
| Failure _ -> prerr_endline "FAILURE";
;;
projects / helm.git / commitdiff