(* $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 eq_ind () =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con")
- in
- NCic.Const r
- ;;
+let eqsig = ref (fun _ -> assert false);;
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
- 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 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_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_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 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
match t with
| Terms.Leaf _
| Terms.Var _ ->
-(* prerr_endline ("term: " ^ ppfot ft); *)
+ 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);
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 mk_proof (bag : NCic.term Terms.bag) mp subst steps =
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.Equation (l,r,ty,_) ->
in
lit, vl, proof
in
+ let mk_refl = function
+ | NCic.Appl [_; ty; l; _]
+ -> NCic.Appl [eq_refl();ty;l]
+ | _ -> assert false
+ in
+ let proof_type =
+ let lit,_,_ = get_literal mp in
+ let lit = Subst.apply_subst subst lit in
+ extract 0 [] lit 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 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,
- extract amount [] lit,
- (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
+ NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
aux true ((id,([],lit))::seen) (id::tl)))
else
match proof with
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 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
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
in
- aux false [] steps
+ aux false [] steps, proof_type
;;
projects / helm.git / blobdiff