let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
- let eq_ind_r,ty,t1,t2 =
+
+ prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n");
+ let eq_ind_r,ty,t1,t2 =
match CicTypeChecker.type_of_aux' metasenv context equality with
C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
(proof',[fresh_meta])
;;
+(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*)
+
let simpl_tac ~status:(proof,goal) =
*)
let ineq1_of_term (h,t) =
+ debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
match t with (* match t *)
Cic.Appl (t1::next) ->
let arg1= List.hd next in
|_->assert false)(* match u *)
| Cic.MutInd (u,i,o) ->
(match UriManager.string_of_uri u with
- "cic:/Coq/Init/Logic_Type/eqT.con" ->
- let t0= arg1 in
+ "cic:/Coq/Init/Logic_Type/eqT.ind" ->
+ debug("Ho trovato una ==\n");
+ let t0= arg1 in
let arg1= arg2 in
let arg2= List.hd(List.tl (List.tl next)) in
(match t0 with
Cic.Const (u,boh) ->
(match UriManager.string_of_uri u with
"cic:/Coq/Reals/Rdefinitions/R.con"->
+
[{hname=h;
htype="eqTLR";
hleft=arg1;
hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
hstrict=false}]
- |_-> assert false)
- |_-> assert false)
- |_-> assert false)
- |_-> assert false)(* match t1 *)
- |_-> assert false (* match t *)
+ |_-> debug("eqT deve essere applicato a const R\n");assert false)
+ |_-> debug("eqT deve essere appl a const\n");assert false)
+ |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false)
+ |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *)
+ |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *)
;;
(* coq wrapper
let ineq1_of_constr = ineq1_of_term;;
fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
- debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
- ^ CicPp.ppterm ty ^"\n");
+ debug("!!!!!!!!1:unify "^CicPp.ppterm _Rle_not_lt^" with "
+ ^ CicPp.ppterm ty ^" fails\n");
let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
debug("!!!!!!!!!2\n");
r
(* preuve que 0<=(-n)*(1/d) => False
*)
-let tac_zero_infeq_false gl (n,d) ~status=
-debug("stat tac_zero_infeq_false");
-let r =
- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+debug("stat tac_zero_infeq_false\n");
+(*let r =
+ (
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+ Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
~continuation:(tac_zero_inf_pos (-n,d))) ~status in
- debug("stat tac_zero_infeq_false");
- r
+ debug("end tac_zero_infeq_false\n");
+ r*)
+ Ring.id_tac ~status
;;
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
-debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
+debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n");
let (proof,goals) =
rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
~status:((curi,metasenv',pbo,pty),goal)
(* transform hyps into inequations *)
List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
- with _-> ())
+ with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
hyps;
let tac=ref Ring.id_tac in
if res=[] then
(print_string "Tactic Fourier fails.\n";flush stdout;
- failwith "fourier_tac fails")
+ failwith "fourier can't proove it")
else
(
match res with (*match res*)
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal)
metasenv in
+
+ debug("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n");
+
PrimitiveTactics.change_tac ~what:ty
~with_what:(Cic.Appl [ _not; ineq]) ~status)
~continuation:(Tacticals.then_
r)
~continuations:[(Tacticals.thens
~start:(
- fun ~status ->
+ fun ~status:(proof,goals as status) ->
+
let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
(match r with (p,gl) ->
debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
let metano,context,ty = List.find (function (m,_,_) -> m=
goal) metasenv in
debug("ty = "^CicPp.ppterm ty^"\n");
- let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
+ let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
~status in
debug("fine ECCOCI\n");
r)
r)
; "id", Ring.id_tac]
])
-(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
- ;tac2]))
- ;!tac1]);(*end tac:=*)
+ ;Tacticals.then_
+ ~start:
+ (
+ fun ~status:(proof,goal as status) ->
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=
+ goal) metasenv in
+ (* check if ty is of type *)
+ let w1 =
+ debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
+ (match ty with
+ (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
+ Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a])
+ |_ -> assert false)
+ in
+ let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
+ debug("fine MY_CHNGE\n");
+ r
+ )
+ ~continuation:Ring.id_tac(*tac2*)]))
+ ;Ring.id_tac(*!tac1*)]);(*end tac:=*)
tac:=(Tacticals.thens
~start:(PrimitiveTactics.cut_tac ~term:_False)
~continuations:[Tacticals.then_
projects / helm.git / blobdiff