X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=c505807f2ddc24295a060912d90fd3602cb7bfb3;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=ab7bde56f8dfa4049ca0989ccb55e64d3ac7eada;hpb=df0606d3bcbc41272fcde2d013bbe0b1aadf98af;p=helm.git diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index ab7bde56f..c505807f2 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -28,8 +28,6 @@ open PrimitiveTactics open ProofEngineTypes open UriManager -open HelmLibraryObjects - (** DEBUGGING *) (** perform debugging output? *) @@ -192,11 +190,11 @@ exception GoalUnringable *) let ringable = let is_equality = function - | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_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 @@ -254,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 = 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 @@ -287,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 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 @@ -328,20 +326,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 @@ -353,8 +351,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 *) @@ -362,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 Reals.rtheory ; t] + Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t] ) aterms @@ -390,12 +388,13 @@ let elim_type_tac ~term status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) +(* 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"; ProofEngineTypes.apply_tactic - (Tacticals.thens ~start:(E.elim_type_tac ~term) + (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) @@ -466,8 +465,8 @@ let purge_hyps_tac ~count = let ring_tac status = let (proof, goal) = status in warn "in Ring tactic"; - let eqt = mkMutInd (Logic.eq_URI, 0) [] in - let r = Reals.r in + 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 *) @@ -484,7 +483,7 @@ let ring_tac status = try let new_hyps = ref 0 in (* number of new hypotheses created *) ProofEngineTypes.apply_tactic - (Tacticals.try_tactics + (Tacticals.first ~tactics:[ "reflexivity", EqualityTactics.reflexivity_tac ; "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; @@ -492,8 +491,8 @@ let ring_tac status = "exact sym_eqt su t1 ...", exact_tac ~term:( Cic.Appl - [mkConst Logic.sym_eq_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 ] ; @@ -527,15 +526,15 @@ let ring_tac status = in let status'' = ProofEngineTypes.apply_tactic - (Tacticals.try_tactics (* try to solve 1st subgoal *) + (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.sym_eq_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 ] ;