X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=bd9c1513661ba61d6abc8561cbb1ced948e7594e;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=c7015a7558042869f8dbb14d4707a6fd19086057;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index c7015a755..bd9c15136 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -28,6 +28,8 @@ open PrimitiveTactics open ProofEngineTypes open UriManager +open HelmLibraryObjects + (** DEBUGGING *) (** perform debugging output? *) @@ -46,26 +48,12 @@ let warn s = uniformity of invocation of "mkXXX" functions. *) -let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" -let refl_eqt_uri = (eqt_uri, 0, 1) let equality_is_a_congruence_A = uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var" let equality_is_a_congruence_x = uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var" let equality_is_a_congruence_y = uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var" -let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con" -let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" -let true_uri = (bool_uri, 0, 1) -let false_uri = (bool_uri, 0, 2) - -let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con" -let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" -let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con" -let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con" -let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" -let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" -let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" let apolynomial_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" @@ -137,20 +125,6 @@ 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 @@ -165,7 +139,7 @@ let metasenv_of_status ~status:((_,m,_,_), _) = m *) 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, _ = CicUtil.lookup_meta goal metasenv in context (** CIC TERM CONSTRUCTORS *) @@ -216,11 +190,11 @@ exception GoalUnringable *) let ringable = let is_equality = function - | Cic.MutInd (uri, 0, []) when (eq uri eqt_uri) -> true + | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true | _ -> false in let is_real = function - | Cic.Const (uri, _) when (eq uri r_uri) -> true + | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true | _ -> false in function @@ -278,7 +252,7 @@ let path_of_int n = @return a cic term representing the variable map containing vars variables *) let btree_of_array ~vars = - let r = mkConst r_uri [] in (* cic objects *) + let r = 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 @@ -311,17 +285,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 rplus_uri) bop) -> (* +. *) + when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *) Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] | Cic.Appl (bop::t1::t2::[]) - when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) + when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *) Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] | Cic.Appl (uop::t::[]) - when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) + when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *) Cic.Appl [mkCtor apopp_uri []; aux t] - | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) + | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *) mkCtor ap0_uri [] - | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) + | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *) mkCtor ap1_uri [] | t -> (* variable *) try @@ -351,27 +325,21 @@ let abstract_poly ~terms = at is the abstract term built from t, t is a single member of aterms *) let build_segments ~terms = - let r = mkConst r_uri [] in (* cic objects *) - let rplus = mkConst rplus_uri [] in - let rmult = mkConst rmult_uri [] in - let ropp = mkConst ropp_uri [] in - let r1 = mkConst r1_uri [] in - let r0 = mkConst r0_uri [] in let theory_args_subst varmap = - [abstract_rings_A_uri, r ; - abstract_rings_Aplus_uri, rplus ; - abstract_rings_Amult_uri, rmult ; - abstract_rings_Aone_uri, r1 ; - abstract_rings_Azero_uri, r0 ; - abstract_rings_Aopp_uri, ropp ; + [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_vm_uri, varmap] in let theory_args_subst' eq varmap t = - [abstract_rings_A_uri, r ; - abstract_rings_Aplus_uri, rplus ; - abstract_rings_Amult_uri, rmult ; - abstract_rings_Aone_uri, r1 ; - abstract_rings_Azero_uri, r0 ; - abstract_rings_Aopp_uri, ropp ; + [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_Aeq_uri, eq ; abstract_rings_vm_uri, varmap ; abstract_rings_T_uri, t] in @@ -382,11 +350,9 @@ let build_segments ~terms = let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in let apolynomial_normalize_ok eq varmap t = mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in - let rtheory = mkConst rtheory_uri [] in let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) - Cic.Lambda (Cic.Anonymous, r, - Cic.Lambda (Cic.Anonymous, r, - mkCtor false_uri [])) + Cic.Lambda (Cic.Anonymous, Reals.r, + Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb)) in let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) List.map (* build ring segments *) @@ -394,7 +360,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 rtheory ; t] + Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t] ) aterms @@ -468,7 +434,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as 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'] @@ -481,10 +447,10 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = *) let ring_tac ~status:((proof, goal) as status) = warn "in Ring tactic"; - let eqt = mkMutInd (eqt_uri, 0) [] in - let r = mkConst r_uri [] in + 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 (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 @@ -507,8 +473,8 @@ let ring_tac ~status:((proof, goal) as status) = "exact sym_eqt su t1 ...", exact_tac ~term:( Cic.Appl - [mkConst sym_eqt_uri - [equality_is_a_congruence_A, mkConst r_uri [] ; + [mkConst Logic_Type.sym_eqt_URI + [equality_is_a_congruence_A, Reals.r; equality_is_a_congruence_x, t1'' ; equality_is_a_congruence_y, t1 ] ; @@ -545,8 +511,8 @@ let ring_tac ~status:((proof, goal) as status) = exact_tac ~term:( Cic.Appl - [mkConst sym_eqt_uri - [equality_is_a_congruence_A, mkConst r_uri [] ; + [mkConst Logic_Type.sym_eqt_URI + [equality_is_a_congruence_A, Reals.r; equality_is_a_congruence_x, t2'' ; equality_is_a_congruence_y, t2 ] ;