(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
- let eqP () =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
- in
- NCic.Const r
- ;;
+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;;
- let eq_ind () =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con")
- in
- NCic.Const r
- ;;
+let default_sig = function
+ | Eq ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+ let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
+ NCic.Const ref
+ | EqInd_l ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
+ NCic.Const ref
+ | EqInd_r ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
+ NCic.Const ref
+ | Refl ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+ let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
+ NCic.Const ref
- let eq_ind_r () =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_elim_r.con")
- in
- NCic.Const r
- ;;
+let set_default_sig () =
+ (*prerr_endline "setting default sig";*)
+ eqsig := default_sig
- 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 set_reference_of_oxuri reference_of_oxuri =
+ prerr_endline "setting oxuri in nCicProof";
+ let nsig = function
+ | Eq ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
+ | EqInd_l ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_ind.con"))
+ | EqInd_r ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_elim_r.con"))
+ | Refl ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
+ in eqsig:= nsig
;;
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
+
+ let eqP() = debug (!eqsig Eq) "eq" ;;
+ let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
+ let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";;
+ let eq_refl() = debug (!eqsig Refl) "refl";;
+
+
let extract lift vl t =
let rec pos i = function
| [] -> raise Not_found
extract t
;;
+
let mk_predicate hole_type amount ft p1 vl =
let rec aux t p =
match p with
match t with
| Terms.Leaf _
| Terms.Var _ ->
-(* prerr_endline ("term: " ^ ppfot ft); *)
+ let module NCicBlob = NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end)
+ in
+ let module Pp = Pp.Pp(NCicBlob) in
+ 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);
assert false
| Terms.Node l ->
let l =
NCic.Lambda("x", hole_type, aux ft (List.rev p1))
;;
- let mk_proof (bag : NCic.term Terms.bag) mp steps =
+ let dag =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in
+ NCic.Const ref
+ ;;
+
+ (*
+ let eq_setoid =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in
+ NCic.Const ref
+ ;;
+ *)
+
+ let sym eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism1 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism2 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; eq; NCic.Implicit `Term];
+ ;;
+
+ let trans eq p =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq]
+ ;;
+
+ let iff1 eq p =
+ let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type;
+ eq; p];
+ ;;
+
+(*
+ let mk_refl = function
+ | NCic.Appl [_; _; x; _] ->
+ let uri= NUri.uri_of_string "cic:/matita/ng/properties/relations/refl.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term(*x*)]
+ | _ -> assert false
+*)
+
+ let mk_refl = function
+ | NCic.Appl [_; ty; l; _]
+ -> NCic.Appl [eq_refl();ty;l]
+ | _ -> assert false
+
+
+ let mk_morphism eq amount ft pl vl =
+ let rec aux t p =
+ match p with
+ | [] -> eq
+ | n::tl ->
+ prerr_endline (string_of_int n);
+ match t with
+ | Terms.Leaf _
+ | Terms.Var _ -> assert false
+ | Terms.Node [] -> assert false
+ | Terms.Node [ Terms.Leaf eqt ; _; l; r ]
+ when (eqP ()) = eqt ->
+ if n=2 then eq_morphism1 (aux l tl)
+ else eq_morphism2 (aux r tl)
+ | Terms.Node (f::l) ->
+ snd (
+ List.fold_left
+ (fun (i,acc) t ->
+ i+1,
+ 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::
+ [aux t tl])
+ else
+ NCicUntrusted.mk_appl acc [extract amount vl t]
+ ) (1,extract amount vl f) l)
+ in aux ft (List.rev pl)
+ ;;
+
+ 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
t vl
in
let get_literal id =
- let (_, lit, vl, proof),_ = Terms.M.find id bag in
+ 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
- lit, vl, proof
+ lit, vl, proof
+ in
+ let proof_type =
+ 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
let amount = List.length seen in
let lit,vl,proof = get_literal id in
if not ongoal && id = mp then
- ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
- NCic.LetIn ("clause_" ^ string_of_int id,
- extract amount [] lit,
- (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
- aux true ((id,([],lit))::seen) (id::tl)))
+ let lit = Subst.apply_subst subst lit in
+ let eq_ty = extract amount [] lit in
+ 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 true ((id,([],lit))::seen) (id::tl))
else
match proof with
| Terms.Exact _ when tl=[] ->
- (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
- aux ongoal seen tl
+ (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
+ 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),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ *)
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl (extract amount vl ft))
+ (aux ongoal
+ ((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
let args = List.map (extract amount vl) args in
- let rel_for_id = NCic.Rel (List.length vl + position id seen) in
- if args = [] then rel_for_id
+ let rel_for_id = NCic.Rel (List.length vl + position id seen) in
+ if args = [] then rel_for_id
else NCic.Appl (rel_for_id::args)
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 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
+ (*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 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)));*)
+ (*
+ 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
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 ()
+ let rewrite_step =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ NCic.Appl
+ [eq_ind_r(); hole_type; r; pred; p_id1; l; p_id2]
+ else
+ NCic.Appl
+ [ eq_ind(); hole_type; l; pred; p_id1; r; p_id2]
+ in
+ let body = aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
+ in
+ 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
else
- l,r,eq_ind ()
- in
- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
- (* NCic.Implicit `Type, *)
- close_with_lambdas vl
- (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)
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
+ (* NCic.Implicit `Type, *)
+ close_with_lambdas vl rewrite_step, body)
in
- aux false [] steps
+ aux false [] steps, proof_type
;;
projects / helm.git / blobdiff