From 17f33fa8cb65de1f3edcba6ac750bbdb4d061117 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 10:33:10 +0000 Subject: [PATCH] moved hard coded uris to HelmLibraryObjects --- helm/ocaml/tactics/discriminationTactics.ml | 18 ++--- helm/ocaml/tactics/equalityTactics.ml | 9 +-- helm/ocaml/tactics/fourierR.ml | 12 +-- helm/ocaml/tactics/proofEngineHelpers.ml | 30 +------- helm/ocaml/tactics/proofEngineHelpers.mli | 8 +- helm/ocaml/tactics/ring.ml | 82 ++++++++------------- helm/ocaml/tactics/tacticals.ml | 4 +- 7 files changed, 56 insertions(+), 107 deletions(-) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index c413d4694..9e91eeb07 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -23,6 +23,7 @@ * http://cs.unibo.it/helm/. *) +open HelmLibraryObjects let rec injection_tac ~term ~status:((proof, goal) as status) = let module C = Cic in @@ -34,8 +35,8 @@ let rec injection_tac ~term ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) - or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> ( + when (U.eq equri Logic.eq_URI) + or (U.eq equri Logic_Type.eqt_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -86,8 +87,8 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) - or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> ( + when (U.eq equri Logic.eq_URI) or + (U.eq equri Logic_Type.eqt_URI) -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -210,8 +211,7 @@ let discriminate'_tac ~term ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) - or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> ( + when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -275,8 +275,8 @@ prerr_endline ("XXXX nth funzionano ") ; C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[])) - else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[])) + then (C.MutInd(Logic.false_URI,0,[])) + else (C.MutInd(Logic.true_URI,0,[])) in aux red_ty 1 ) constructor_list @@ -285,7 +285,7 @@ prerr_endline ("XXXX nth funzionano ") ; let (proof',goals') = EliminationTactics.elim_type_tac - ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[])) + ~term:(C.MutInd(Logic.false_URI,0,[])) ~status in (match goals' with diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index a66328220..3af6b861d 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -61,9 +61,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = C.Lambda (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'') in - let fresh_meta = ProofEngineHelpers.new_meta proof in - let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in let (proof',goals) = @@ -123,9 +122,9 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = C.Lambda (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'') in - let fresh_meta = ProofEngineHelpers.new_meta proof in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in + CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in let (proof',goals) = diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index a807554c5..537ef3f5d 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -737,9 +737,9 @@ let r = let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let fresh_meta = ProofEngineHelpers.new_meta proof in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in + CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,t)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = @@ -762,9 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)= debug("my_cut di "^CicPp.ppterm c^"\n"); - let fresh_meta = ProofEngineHelpers.new_meta proof in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in + CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,c)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = @@ -901,9 +901,9 @@ debug("inizio EQ\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in - let fresh_meta = ProofEngineHelpers.new_meta proof in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = - ProofEngineHelpers.identity_relocation_list_for_metavariable context in + CicMkImplicit.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))); let (proof,goals) = diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 79304211d..ccac132ef 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -61,36 +61,12 @@ let mk_fresh_name context name ~typ = try_next 1 ;; -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) -(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable canonical_context = - let canonical_context_length = List.length canonical_context in - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (1,canonical_context) - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -let new_meta ~proof = - let (_,metasenv,_,_) = proof in - let rec aux = - function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - 1 + aux (None,metasenv) +let new_meta_of_proof ~proof:(_, metasenv, _, _) = + CicMkImplicit.new_meta metasenv let subst_meta_in_proof proof meta term newmetasenv = let uri,metasenv,bo,ty = proof in - let subst_in = CicUnification.apply_subst [meta,term] in + let subst_in = CicMetaSubst.apply_subst [meta,term] in let metasenv' = newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) in diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 0e2244f43..652776262 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -29,15 +29,9 @@ (* [typ] will be the type of the variable *) val mk_fresh_name : ProofEngineTypes.mk_fresh_name_type -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list *) -(* [Rel 1 ; ... ; Rel n] where n = List.length [canonical_context] *) -val identity_relocation_list_for_metavariable : - 'a option list -> Cic.term option list - (* Returns the first meta whose number is above the *) (* number of the higher meta. *) -val new_meta : proof:ProofEngineTypes.proof -> int +val new_meta_of_proof : proof:ProofEngineTypes.proof -> int val subst_meta_in_proof : ProofEngineTypes.proof -> diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index c7015a755..8e592e61d 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" @@ -216,11 +204,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 +266,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 +299,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 +339,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 +364,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 +374,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 @@ -481,8 +461,8 @@ 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 (t1, t2) = split_eq ty in (* goal like t1 = t2 *) @@ -507,8 +487,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 +525,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 ] ; diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index d499acb9a..57660310b 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -68,8 +68,8 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = e -> match e with (Fail _) - | (CicTypeChecker.TypeCheckerFailure (CicTypeChecker.NotWellTyped _)) - | (CicUnification.UnificationFailed) -> + | (CicTypeChecker.TypeCheckerFailure _) + | (CicUnification.UnificationFailure _) -> warn ( "Tacticals.try_tactics failed with exn: " ^ Printexc.to_string e); -- 2.39.2