X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=1d7cc10e6bfad0a0a16fe9b7ad2b74bc0dc6d078;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8e592e61d842322d4173bc0e0b6dd6420a50abdc;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git
diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 8e592e61d..1d7cc10e6 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -28,17 +28,14 @@ open PrimitiveTactics
open ProofEngineTypes
open UriManager
-open HelmLibraryObjects
-
(** DEBUGGING *)
(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
-let warn s =
- if debug then
- prerr_endline ("RING WARNING: " ^ s)
+let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s)))
(** CIC URIS *)
@@ -49,11 +46,11 @@ let warn s =
*)
let equality_is_a_congruence_A =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
let equality_is_a_congruence_x =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
let equality_is_a_congruence_y =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
let apolynomial_uri =
uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
@@ -125,35 +122,22 @@ let cic_is_const ?(uri: uri option = None) term =
*)
let uri_of_proof ~proof:(uri, _, _, _) = uri
- (**
- @param metano meta list index
- @param metasenv meta list (environment)
- @raise Failure if metano is not found in metasenv
- @return conjecture corresponding to metano in metasenv
- *)
-let conj_of_metano metano =
- try
- List.find (function (m, _, _) -> m = metano)
- with Not_found ->
- failwith (
- "Ring.conj_of_metano: " ^
- (string_of_int metano) ^ " no such meta")
-
(**
@param status current proof engine status
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ~status:((_,m,_,_), _) = m
+let metasenv_of_status ((_,m,_,_), _) = m
(**
@param status a proof engine status
@raise Failure when proof or goal are None
@return context corresponding to current goal
*)
-let context_of_status ~status:(proof, goal as status) =
- let metasenv = metasenv_of_status ~status:status in
- let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+let context_of_status status =
+ let (proof, goal) = status in
+ let metasenv = metasenv_of_status status in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
context
(** CIC TERM CONSTRUCTORS *)
@@ -204,19 +188,19 @@ exception GoalUnringable
*)
let ringable =
let is_equality = function
- | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true
| _ -> false
in
let is_real = function
- | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
+ | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true
| _ -> false
in
function
| Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
- warn "Goal Ringable!";
+ warn (lazy "Goal Ringable!");
true
| _ ->
- warn "Goal Not Ringable :-((";
+ warn (lazy "Goal Not Ringable :-((");
false
(**
@@ -228,8 +212,8 @@ let ringable =
*)
let split_eq = function
| (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
- warn ("" ^ (CicPp.ppterm t1) ^ "");
- warn ("" ^ (CicPp.ppterm t2) ^ "");
+ warn (lazy ("" ^ (CicPp.ppterm t1) ^ ""));
+ warn (lazy ("" ^ (CicPp.ppterm t2) ^ ""));
(t1, t2)
| _ -> raise GoalUnringable
@@ -266,7 +250,7 @@ let path_of_int n =
@return a cic term representing the variable map containing vars variables
*)
let btree_of_array ~vars =
- let r = Reals.r in
+ let r = HelmLibraryObjects.Reals.r in
let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
let size = Array.length vars in
@@ -299,17 +283,17 @@ let abstract_poly ~terms =
let rec aux = function (* TODO not tail recursive *)
(* "bop" -> binary operator | "uop" -> unary operator *)
| Cic.Appl (bop::t1::t2::[])
- when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *)
+ when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rplus_URI) bop) -> (* +. *)
Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
| Cic.Appl (bop::t1::t2::[])
- when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
+ when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rmult_URI) bop) -> (* *. *)
Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
| Cic.Appl (uop::t::[])
- when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
+ when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.ropp_URI) uop) -> (* ~-. *)
Cic.Appl [mkCtor apopp_uri []; aux t]
- | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
+ | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *)
mkCtor ap0_uri []
- | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
+ | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *)
mkCtor ap1_uri []
| t -> (* variable *)
try
@@ -340,20 +324,20 @@ let abstract_poly ~terms =
*)
let build_segments ~terms =
let theory_args_subst varmap =
- [abstract_rings_A_uri, Reals.r ;
- abstract_rings_Aplus_uri, Reals.rplus ;
- abstract_rings_Amult_uri, Reals.rmult ;
- abstract_rings_Aone_uri, Reals.r1 ;
- abstract_rings_Azero_uri, Reals.r0 ;
- abstract_rings_Aopp_uri, Reals.ropp ;
+ [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
+ abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
+ abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
+ abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
+ abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
+ abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
abstract_rings_vm_uri, varmap] in
let theory_args_subst' eq varmap t =
- [abstract_rings_A_uri, Reals.r ;
- abstract_rings_Aplus_uri, Reals.rplus ;
- abstract_rings_Amult_uri, Reals.rmult ;
- abstract_rings_Aone_uri, Reals.r1 ;
- abstract_rings_Azero_uri, Reals.r0 ;
- abstract_rings_Aopp_uri, Reals.ropp ;
+ [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
+ abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
+ abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
+ abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
+ abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
+ abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
abstract_rings_Aeq_uri, eq ;
abstract_rings_vm_uri, varmap ;
abstract_rings_T_uri, t] in
@@ -365,8 +349,8 @@ let build_segments ~terms =
let apolynomial_normalize_ok eq varmap t =
mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
- Cic.Lambda (Cic.Anonymous, Reals.r,
- Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb))
+ Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r,
+ Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, HelmLibraryObjects.Datatypes.falseb))
in
let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
List.map (* build ring segments *)
@@ -374,7 +358,7 @@ let build_segments ~terms =
Cic.Appl [interp_ap varmap ; t],
Cic.Appl (
[interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
- Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t]
+ Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t]
) aterms
@@ -382,7 +366,7 @@ let status_of_single_goal_tactic_result =
function
proof,[goal] -> proof,goal
| _ ->
- raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
+ raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal"))
(* Galla: spostata in variousTactics.ml
(**
@@ -390,10 +374,10 @@ let status_of_single_goal_tactic_result =
@param status current proof engine status
@param term term to cut
*)
-let elim_type_tac ~term ~status =
- warn "in Ring.elim_type_tac";
+let elim_type_tac ~term status =
+ warn (lazy "in Ring.elim_type_tac");
Tacticals.thens ~start:(cut_tac ~term)
- ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
+ ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
*)
(**
@@ -402,11 +386,16 @@ let elim_type_tac ~term ~status =
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
-let elim_type2_tac ~term ~proof ~status =
+(* FG: METTERE I NOMI ANCHE QUI? *)
+let elim_type2_tac ~term ~proof =
+ let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
- warn "in Ring.elim_type2";
- Tacticals.thens ~start:(E.elim_type_tac ~term)
- ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
+ warn (lazy "in Ring.elim_type2");
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens ~start:(E.elim_type_tac term)
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
+ in
+ ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
(* Galla: spostata in variousTactics.ml
(**
@@ -415,11 +404,11 @@ let elim_type2_tac ~term ~proof ~status =
only refl_eqT, coq's one also try "refl_equal"
@param status current proof engine status
*)
-let reflexivity_tac ~status:(proof, goal) =
- warn "in Ring.reflexivity_tac";
+let reflexivity_tac (proof, goal) =
+ warn (lazy "in Ring.reflexivity_tac");
let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
try
- apply_tac ~status:(proof, goal) ~term:refl_eqt
+ apply_tac (proof, goal) ~term:refl_eqt
with (Fail _) as e ->
let e_str = Printexc.to_string e in
raise (Fail ("Reflexivity failed with exception: " ^ e_str))
@@ -436,22 +425,33 @@ let lift ~n (a,b,c,d,e,f,g,h) =
@param count number of hypotheses to remove
@param status current proof engine status
*)
-let purge_hyps_tac ~count ~status:(proof, goal as status) =
+let purge_hyps_tac ~count =
+ let purge_hyps_tac ~count status =
let module S = ProofEngineStructuralRules in
+ let (proof, goal) = status in
let rec aux n context status =
assert(n>=0);
match (n, context) with
| (0, _) -> status
| (n, hd::tl) ->
- aux (n-1) tl
- (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
+ let name_of_hyp =
+ match hd with
+ None
+ | Some (Cic.Anonymous,_) -> assert false
+ | Some (Cic.Name name,_) -> name
+ in
+ aux (n-1) tl
+ (status_of_single_goal_tactic_result
+ (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
- let (_, context, _) = conj_of_metano goal metasenv in
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;
proof',[goal']
+ in
+ ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
(** THE TACTIC! *)
@@ -459,18 +459,21 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) =
Ring tactic, does associative and commutative rewritings in Reals ring
@param status current proof engine status
*)
-let ring_tac ~status:((proof, goal) as status) =
- warn "in Ring tactic";
- let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in
- let r = Reals.r in
- let metasenv = metasenv_of_status ~status in
- let (metano, context, ty) = conj_of_metano goal metasenv in
+
+let ring_tac status =
+ let (proof, goal) = status in
+ warn (lazy "in Ring tactic");
+ let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in
+ let r = HelmLibraryObjects.Reals.r in
+ let metasenv = metasenv_of_status status in
+ let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
+ if debug then
List.iter (* debugging, feel free to remove *)
(fun (descr, term) ->
- warn (descr ^ " " ^ (CicPp.ppterm term)))
+ warn (lazy (descr ^ " " ^ (CicPp.ppterm term))))
(List.combine
["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
"t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
@@ -478,8 +481,8 @@ let ring_tac ~status:((proof, goal) as status) =
t2; t2'; t2''; t2'_eq_t2'']);
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
- Tacticals.try_tactics
- ~status
+ ProofEngineTypes.apply_tactic
+ (Tacticals.first
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -487,29 +490,33 @@ let ring_tac ~status:((proof, goal) as status) =
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_URI
- [equality_is_a_congruence_A, Reals.r;
+ [mkConst HelmLibraryObjects.Logic.sym_eq_URI
+ [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
equality_is_a_congruence_x, t1'' ;
equality_is_a_congruence_y, t1
] ;
t1'_eq_t1''
]) ;
- "elim_type eqt su t1 ...", (fun ~status ->
+ "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
- let context = context_of_status ~status in
- if not (are_convertible context t1'' t1) then begin
- warn "t1'' and t1 are NOT CONVERTIBLE";
+ let context = context_of_status status in
+ let b,_ = (*TASSI : FIXME*)
+ are_convertible context t1'' t1 CicUniv.empty_ugraph in
+ if not b then begin
+ warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
let newstatus =
- elim_type2_tac (* 1st elim_type use *)
- ~status ~proof:t1'_eq_t1''
- ~term:(Cic.Appl [eqt; r; t1''; t1])
+ ProofEngineTypes.apply_tactic
+ (elim_type2_tac (* 1st elim_type use *)
+ ~proof:t1'_eq_t1''
+ ~term:(Cic.Appl [eqt; r; t1''; t1]))
+ status
in
incr new_hyps; (* elim_type add an hyp *)
match newstatus with
(proof,[goal]) -> proof,goal
| _ -> assert false
end else begin
- warn "t1'' and t1 are CONVERTIBLE";
+ warn (lazy "t1'' and t1 are CONVERTIBLE");
status
end
in
@@ -517,58 +524,71 @@ let ring_tac ~status:((proof, goal) as status) =
lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
in
let status'' =
- Tacticals.try_tactics (* try to solve 1st subgoal *)
- ~status:status'
+ ProofEngineTypes.apply_tactic
+ (Tacticals.first (* try to solve 1st subgoal *)
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",
exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_URI
- [equality_is_a_congruence_A, Reals.r;
+ [mkConst HelmLibraryObjects.Logic.sym_eq_URI
+ [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
equality_is_a_congruence_x, t2'' ;
equality_is_a_congruence_y, t2
] ;
t2'_eq_t2''
]) ;
- "elim_type eqt su t2 ...", (fun ~status ->
+ "elim_type eqt su t2 ...",
+ ProofEngineTypes.mk_tactic (fun status ->
let status' =
- let context = context_of_status ~status in
- if not (are_convertible context t2'' t2) then begin
- warn "t2'' and t2 are NOT CONVERTIBLE";
+ let context = context_of_status status in
+ let b,_ = (* TASSI:FIXME *)
+ are_convertible context t2'' t2 CicUniv.empty_ugraph
+ in
+ if not b then begin
+ warn (lazy "t2'' and t2 are NOT CONVERTIBLE");
let newstatus =
- elim_type2_tac (* 2nd elim_type use *)
- ~status ~proof:t2'_eq_t2''
- ~term:(Cic.Appl [eqt; r; t2''; t2])
+ ProofEngineTypes.apply_tactic
+ (elim_type2_tac (* 2nd elim_type use *)
+ ~proof:t2'_eq_t2''
+ ~term:(Cic.Appl [eqt; r; t2''; t2]))
+ status
in
incr new_hyps; (* elim_type add an hyp *)
match newstatus with
(proof,[goal]) -> proof,goal
| _ -> assert false
end else begin
- warn "t2'' and t2 are CONVERTIBLE";
+ warn (lazy "t2'' and t2 are CONVERTIBLE");
status
end
in
try (* try to solve main goal *)
- warn "trying reflexivity ....";
- EqualityTactics.reflexivity_tac ~status:status'
+ warn (lazy "trying reflexivity ....");
+ ProofEngineTypes.apply_tactic
+ EqualityTactics.reflexivity_tac status'
with (Fail _) -> (* leave conclusion to the user *)
- warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps_tac ~count:!new_hyps ~status:status')]
+ warn (lazy "reflexivity failed, solution's left as an ex :-)");
+ ProofEngineTypes.apply_tactic
+ (purge_hyps_tac ~count:!new_hyps) status')])
+ status'
in
- status'')]
+ status'')])
+ status
with (Fail s) ->
- raise (Fail ("Ring failure: " ^ s))
+ raise (Fail (lazy ("Ring failure: " ^ Lazy.force s)))
end
| _ -> (* impossible: we are applying ring exacty to 2 terms *)
assert false
(* wrap ring_tac catching GoalUnringable and raising Fail *)
-let ring_tac ~status =
+
+let ring_tac status =
try
- ring_tac ~status
+ ring_tac status
with GoalUnringable ->
- raise (Fail "goal unringable")
+ raise (Fail (lazy "goal unringable"))
+
+let ring_tac = ProofEngineTypes.mk_tactic ring_tac