let default_sig = function
| Eq ->
- let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+ let uri = NUri.uri_of_string "cic:/matita/basics/logic/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 uri = NUri.uri_of_string "cic:/matita/basics/logic/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 uri = NUri.uri_of_string "cic:/matita/basics/logic/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 uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
NCic.Const ref
let eq_refl() = debug (!eqsig Refl) "refl";;
- let extract lift vl t =
+ let extract status lift vl t =
let rec pos i = function
| [] -> raise Not_found
| j :: tl when j <> i -> 1+ pos i tl
in
let vl_len = List.length vl in
let rec extract = function
- | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
+ | Terms.Leaf x -> NCicSubstitution.lift status (vl_len+lift) x
| Terms.Var j ->
(try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
| Terms.Node l -> NCic.Appl (List.map extract l)
extract t
;;
-
- let mk_predicate hole_type amount ft p1 vl =
+ let mk_predicate status hole_type amount ft p1 vl =
let rec aux t p =
match p with
| [] -> NCic.Rel 1
match t with
| Terms.Leaf _
| Terms.Var _ ->
- let module NCicBlob = NCicBlob.NCicBlob(
+ (*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 ","
+ 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);
+ prerr_endline ("leading to: " ^ Pp.pp_foterm t); *)
assert false
| Terms.Node l ->
let l =
HExtlib.list_mapi
(fun t i ->
if i = n then aux t tl
- else extract amount (0::vl) t)
+ else extract status amount (0::vl) t)
l
in
NCic.Appl l
NCic.Implicit `Term; eq; NCic.Implicit `Term];
;;
- let trans eq p =
+ 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;
| _ -> assert false
- let mk_morphism eq amount ft pl vl =
+ let mk_morphism status eq amount ft pl vl =
let rec aux t p =
match p with
| [] -> eq
List.fold_left
(fun (i,acc) t ->
i+1,
- let f = extract amount vl f in
+ let _f = extract status 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)
+ NCicUntrusted.mk_appl acc [extract status amount vl t]
+ ) (1,extract status 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 =
+ let mk_proof status ?(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 Pp = Pp.Pp(NCicBlob) in*)
let module Subst = FoSubst in
+ (*let compose subst1 subst2 =
+ let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in
+ let s2 = List.filter (fun (m,_) -> not (List.mem_assoc m s1)) subst2
+ in s1 @ s2
+ in*)
let position i l =
let rec aux = function
| [] -> assert false
- | (j,_) :: tl when i = j -> 1
+ | (j,_) :: _ when i = j -> 1
| _ :: tl -> 1 + aux tl
in
aux l
let lit =match lit with
| Terms.Predicate t -> t (* assert false *)
| Terms.Equation (l,r,ty,_) ->
- Terms.Node [ Terms.Leaf eqP(); ty; l; r]
+ 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
+ extract status 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
+ let res_subst = subst
in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1
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 eq_ty = extract status 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));
+ (* 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
+ let res = NCicSubstitution.subst status
~avoid_beta_redexes:true ~no_implicit:false refl
(aux true ((id,([],lit))::seen) (id::tl))
+ in res
else
match proof with
| Terms.Exact _ when tl=[] ->
- (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
+ (* 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));
NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
- close_with_lambdas vl (extract amount vl ft),
+ close_with_forall vl (extract status amount vl lit),
+ close_with_lambdas vl (extract status amount vl ft),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- *)
- NCicSubstitution.subst
+ *)
+ let res = NCicSubstitution.subst status
~avoid_beta_redexes:true ~no_implicit:false
- (close_with_lambdas vl (extract amount vl ft))
+ (close_with_lambdas vl (extract status amount vl ft))
(aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ in res
| Terms.Step (_, id1, id2, dir, pos, subst) ->
- let id, id1,(lit,vl,proof) =
+ (* prerr_endline (if ongoal then "on goal" else "not on goal");
+ prerr_endline (Pp.pp_substitution subst); *)
+ (* let subst = if ongoal then res_subst else subst in *)
+ 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)
+ 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 *)
+ (* prerr_endline ("variables = " ^ String.concat ","
+ (List.map string_of_int vl)); *)
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 args = List.map (extract status amount vl) args in
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 =
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)
+ extract status amount vl (Subst.apply_subst subst t),
+ extract status amount vl (Subst.apply_subst subst l),
+ extract status 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)));*)
- mk_predicate
+ (* let _ = prerr_endline ("body = " ^(Pp.pp_foterm id1_ty))
+ in *)
+ mk_predicate status
id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
id2_ty,
l,r
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
+ let occ =
+ NCicUntrusted.count_occurrences status [] 1 body in
if occ <= 1 then
- NCicSubstitution.subst
+ NCicSubstitution.subst status
~avoid_beta_redexes:true ~no_implicit:false
(close_with_lambdas vl rewrite_step) body
else
NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
+ close_with_forall vl (extract status amount vl lit),
(* NCic.Implicit `Type, *)
close_with_lambdas vl rewrite_step, body)
in
projects / helm.git / blobdiff