type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
let eqsig = ref (fun _ -> assert false);;
-let set_sig f = eqsig:=
-f;;
-
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
let default_sig = function
| Eq ->
- let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+ 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 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/peq.ind" in
+ 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";
+ (*prerr_endline "setting default sig";*)
eqsig := default_sig
let set_reference_of_oxuri reference_of_oxuri =
in eqsig:= nsig
;;
-let debug c r = prerr_endline r; c
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
- let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp" ;;
- let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;;
- let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";;
- let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";;
+ 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 =
NCic.Lambda("x", hole_type, aux ft (List.rev p1))
;;
- let mk_proof (bag : NCic.term Terms.bag) mp steps =
+(*
+ let mk_morphism eq amount ft p1 vl =
+ let rec aux t p =
+ match p with
+ | [] -> eq
+ | n::tl ->
+ match t with
+ | Terms.Leaf _
+ | Terms.Var _ -> assert false
+ | Terms.Node l ->
+ let dag,arity = ____ in
+ let l =
+ HExtlib.list_rev_mapi_filter
+ (fun t i ->
+ if i < arity then None
+ else if i = n then Some (aux t tl)
+ else Some (NCic.Appl [refl ...]))
+ l
+ in
+ NCic.Appl (dag::l)
+ in aux ft (List.rev pl)
+ ;;
+*)
+
+ let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
let module Subst = FoSubst in
let position i l =
let rec aux = function
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
- ((*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 = 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=[] ->
| 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),
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
l,r,eq_ind ()
in
- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
+ let body = aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
+ in
+ if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl (NCic.Appl
+ [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
+ body
+ else
+ 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)
+ close_with_lambdas vl (NCic.Appl
+ [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
+ body)
in
- aux false [] steps
+ aux false [] steps, proof_type
;;
projects / helm.git / blobdiff