X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=4691239f411eb78362ce68dc29e839450675c6e2;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=8e592e61d842322d4173bc0e0b6dd6420a50abdc;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 8e592e61d..4691239f4 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -49,11 +49,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 +125,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,7 +191,7 @@ 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 Logic.eq_URI) -> true | _ -> false in let is_real = function @@ -390,10 +377,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 = +let elim_type_tac ~term status = warn "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 +389,15 @@ 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 = +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 + 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 +406,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) = +let reflexivity_tac (proof, goal) = warn "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 +427,27 @@ 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)) + (status_of_single_goal_tactic_result + (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) 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,12 +455,14 @@ 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) = + +let ring_tac status = + let (proof, goal) = status in warn "in Ring tactic"; - let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in + let eqt = mkMutInd (Logic.eq_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 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 @@ -478,8 +476,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.try_tactics ~tactics:[ "reflexivity", EqualityTactics.reflexivity_tac ; "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; @@ -487,22 +485,26 @@ let ring_tac ~status:((proof, goal) as status) = "exact sym_eqt su t1 ...", exact_tac ~term:( Cic.Appl - [mkConst Logic_Type.sym_eqt_URI + [mkConst Logic.sym_eq_URI [equality_is_a_congruence_A, 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 + 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 "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 @@ -517,30 +519,36 @@ 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.try_tactics (* 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 + [mkConst Logic.sym_eq_URI [equality_is_a_congruence_A, 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 + 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 "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 @@ -553,12 +561,16 @@ let ring_tac ~status:((proof, goal) as status) = in try (* try to solve main goal *) warn "trying reflexivity ...."; - EqualityTactics.reflexivity_tac ~status:status' + 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')] + ProofEngineTypes.apply_tactic + (purge_hyps_tac ~count:!new_hyps) status')]) + status' in - status'')] + status'')]) + status with (Fail s) -> raise (Fail ("Ring failure: " ^ s)) end @@ -566,9 +578,12 @@ let ring_tac ~status:((proof, goal) as status) = 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") +let ring_tac = ProofEngineTypes.mk_tactic ring_tac +