(* $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;;
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
-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 set_default_sig () =
- (*prerr_endline "setting default sig";*)
- eqsig := default_sig
-
-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 eqP () =
+ let r =
+ !reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+ in
+ NCic.Const r
;;
-(* let debug c r = prerr_endline r; c *)
-let debug c _ = c;;
+ let eq_ind () =
+ let r =
+ !reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_ind.con")
+ in
+ NCic.Const r
+ ;;
- 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 eq_ind_r () =
+ let r =
+ !reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_elim_r.con")
+ in
+ NCic.Const r
+ ;;
+ let eq_refl () =
+ let r =
+ !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
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 _ ->
- let module NCicBlob = NCicBlob.NCicBlob(
- struct
- let metasenv = [] let subst = [] let context = []
- end)
- in
- let module Pp = Pp.Pp(NCicBlob) in
+ let module Pp =
+ Pp.Pp(NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end))
+ 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);
+ 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 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 mk_proof (bag : NCic.term Terms.bag) mp steps =
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 -> t (* assert false *)
+ | Terms.Predicate t -> assert false
| Terms.Equation (l,r,ty,_) ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
in
- 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
+ lit, vl, proof
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
- 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))
+ ((*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)))
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
- 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
+ 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
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
- ^": " ^ 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)));*)
+ (*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_predicate
id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
id2_ty,
l,r
in
- 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
+ let l, r, eq_ind =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ r,l,eq_ind_r ()
else
- 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)
+ 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)
in
- aux false [] steps, proof_type
+ aux false [] steps
;;
projects / helm.git / blobdiff