diff options
author | 2012-05-29 11:08:37 +0000 | |
---|---|---|
committer | 2012-05-29 11:08:37 +0000 | |
commit | 5fa47f1258408541150e2e4c26d60ff694e7c1bc (patch) | |
tree | 9e7aee1ea714cebdccc50dbd85735948d8baeaf0 /plugins | |
parent | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (diff) |
locus.mli for occurrences+clauses, misctypes.mli for various little things
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 10 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 8 | ||||
-rw-r--r-- | plugins/firstorder/instances.ml | 5 | ||||
-rw-r--r-- | plugins/firstorder/rules.ml | 5 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 40 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.mli | 8 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 13 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 42 | ||||
-rw-r--r-- | plugins/funind/glob_termops.mli | 1 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 15 | ||||
-rw-r--r-- | plugins/funind/indfun.mli | 5 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 49 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 1 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 21 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.ml4 | 1 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 5 | ||||
-rw-r--r-- | plugins/ring/ring.ml | 4 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 3 |
20 files changed, 129 insertions, 114 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a1e968668..58111f597 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -19,6 +19,8 @@ open Glob_term open Term open Pp open Compat +open Decl_kinds +open Misctypes (* INTERN *) @@ -194,7 +196,7 @@ let abstract_one_hyp inject h glob = let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let glob_prop = GSort (dummy_loc,GProp Null) +let glob_prop = GSort (dummy_loc,GProp) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -345,13 +347,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null) + Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Glob_term.GSort(dummy_loc,GProp Null) + Glob_term.GSort(dummy_loc,GProp) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps glob_prop in let loc_ids,npatt = @@ -361,7 +363,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let term2 = GLetIn(dummy_loc,Anonymous, GCast(dummy_loc,glob_of_pat npatt, - CastConv (DEFAULTcast,app_ind)),term1) in + CastConv app_ind),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 2870e8f7e..956a561aa 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,7 +29,7 @@ open Termops open Namegen open Reductionops open Goptions - +open Misctypes (* Strictness option *) @@ -237,7 +237,7 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) + tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere) (thin_body [id]) gls in tclMAP add_aux items gls @@ -750,7 +750,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) + (forward None (Some (dummy_loc, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls @@ -781,7 +781,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac None (Name id) t None Tacexpr.nowhere gls + letin_tac None (Name id) t None Locusops.nowhere gls (* tactics for reconsider *) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 8d580d235..a45d3075f 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -25,6 +25,7 @@ open Formula open Sequent open Names open Libnames +open Misctypes let compare_instance inst1 inst2= match inst1,inst2 with @@ -181,12 +182,12 @@ let right_instance_tac inst continue seq= [tclTHENLIST [introf; (fun gls-> - split (Glob_term.ImplicitBindings + split (ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Glob_term.ImplicitBindings [t])) + (tclTHEN (split (ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b56fe4e50..a226cc455 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -18,6 +18,7 @@ open Declarations open Formula open Sequent open Libnames +open Locus type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -203,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [all_occurrences,EvalConstRef (destConst (constant "not")); - all_occurrences,EvalConstRef (destConst (constant "iff"))] + [AllOccurrences,EvalConstRef (destConst (constant "not")); + AllOccurrences,EvalConstRef (destConst (constant "iff"))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4d5cbe223..5bf772fc5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -15,6 +15,7 @@ open Tacticals open Tactics open Indfun_common open Libnames +open Misctypes let msgnl = Pp.msgnl @@ -441,13 +442,8 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = decompose_prod_n_assum (List.length context) reduced_type_of_hyp in tclTHENLIST - [ - h_reduce_with_zeta - (Tacticals.onHyp hyp_id) - ; - scan_type new_context new_typ_of_hyp - - ] + [ h_reduce_with_zeta (Locusops.onHyp hyp_id); + scan_type new_context new_typ_of_hyp ] else if isProd type_of_hyp then begin @@ -688,13 +684,13 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id if args_id = [] then tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; do_prove hyps ] else tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; tclMAP instanciate_one_hyp hyps; (fun g -> let all_g_hyps_id = @@ -732,7 +728,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [(false,[1]),t] None; + pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( tclTHENSEQ [h_simplest_case t; (fun g' -> @@ -818,9 +814,10 @@ let build_proof tclTHENLIST [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + (fun hyp_id -> + h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g @@ -850,9 +847,9 @@ let build_proof tclTHENLIST [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; + h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g | Rel _ -> anomaly "Free var in goal conclusion !" @@ -1010,7 +1007,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings)); intros_reflexivity] g ) ] @@ -1346,7 +1343,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)]; + [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1442,12 +1439,12 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let build_clause eqs = { - Tacexpr.onhyps = + Locus.onhyps = Some (List.map - (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp) + (fun id -> (Locus.AllOccurrences, id), Locus.InHyp) eqs ); - Tacexpr.concl_occs = Glob_term.no_occurrences_expr + Locus.concl_occs = Locus.NoOccurrences } let rec rewrite_eqs_in_eqs eqs = @@ -1460,7 +1457,8 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences + true (* dep proofs also: *) true id (mkVar eq) false)) gl ) eqs @@ -1482,7 +1480,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 0f776ee6e..b38503cb9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -15,6 +15,7 @@ open Tacticals open Tactics open Indfun_common open Functional_principles_proofs +open Misctypes exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -504,7 +505,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in let funs = List.map fst fas in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 1c02c16ec..00d130d28 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,6 +1,6 @@ open Names open Term - +open Misctypes val generate_functional_principle : (* do we accept interactive proving *) @@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found -val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list +val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list -val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit -val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit +val build_scheme : (identifier*Libnames.reference*glob_sort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e8fec0dd8..aed71c3ae 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -17,19 +17,20 @@ open Genarg open Pcoq open Tacticals open Constr +open Misctypes let pr_binding prc = function - | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function - | Glob_term.ImplicitBindings l -> + | ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence prc l - | Glob_term.ExplicitBindings l -> + | ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Glob_term.NoBindings -> mt () + | NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) @@ -308,7 +309,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = let typ = Tacmach.pf_type_of gl cstr in tclTHEN - (Tactics.letin_tac None (Name idunsafe) cstr None allHypsAndConcl) + (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl) (tclTHENFIRST (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 954e389a4..f18309d04 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -8,6 +8,7 @@ open Indfun_common open Errors open Util open Glob_termops +open Misctypes let observe strm = if do_observe () @@ -1258,7 +1259,8 @@ let rec rebuild_return_type rt = Topconstr.CProdN(loc,n,rebuild_return_type t') | Topconstr.CLetIn(loc,na,t,t') -> Topconstr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],Topconstr.Default Glob_term.Explicit,rt], + | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], + Topconstr.Default Decl_kinds.Explicit,rt], Topconstr.CSort(dummy_loc,GType None)) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b14197891..6433fe37c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -3,6 +3,9 @@ open Glob_term open Errors open Util open Names +open Decl_kinds +open Misctypes + (* Ocaml 3.06 Map.S does not handle is_empty *) let idmap_is_empty m = m = Idmap.empty @@ -19,7 +22,7 @@ let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(dummy_loc,s) let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous) -let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) +let mkGCast(b,t) = GCast(dummy_loc,b,CastConv t) (* Some basic functions to decompose glob_constrs @@ -180,10 +183,9 @@ let change_vars = | GRec _ -> error "Local (co)fixes are not supported" | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv (k,t)) -> - GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,change_vars mapping b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,change_vars mapping b, + Miscops.map_cast_type (change_vars mapping) c) and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in if idmap_is_empty new_mapping @@ -360,10 +362,9 @@ let rec alpha_rt excluded rt = | GRec _ -> error "Not handled GRec" | GSort _ -> rt | GHole _ -> rt - | GCast (loc,b,CastConv (k,t)) -> - GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) - | GCast (loc,b,CastCoerce) -> - GCast(loc,alpha_rt excluded b,CastCoerce) + | GCast (loc,b,c) -> + GCast(loc,alpha_rt excluded b, + Miscops.map_cast_type (alpha_rt excluded) c) | GApp(loc,f,args) -> GApp(loc, alpha_rt excluded f, @@ -411,7 +412,7 @@ let is_free_in id = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | GCast (_,b,(CastConv t|CastVM t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -507,10 +508,9 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,replace_var_by_pattern b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,replace_var_by_pattern b, + Miscops.map_cast_type replace_var_by_pattern c) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl then br @@ -593,7 +593,7 @@ let ids_of_glob_constr c = | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,(CastConv t|CastVM t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc | GLetTuple (_,nal,(na,po),b,c) -> @@ -661,10 +661,9 @@ let zeta_normalize = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt - | GCast(loc,b,CastConv(k,t)) -> - GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) - | GCast(loc,b,CastCoerce) -> - GCast(loc,zeta_normalize_term b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,zeta_normalize_term b, + Miscops.map_cast_type zeta_normalize_term c) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -702,8 +701,9 @@ let expand_as = GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" - | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) - | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) + | GCast(loc,b,c) -> + GCast(loc,expand_as map b, + Miscops.map_cast_type (expand_as map) c) | GCases(loc,sty,po,el,brl) -> GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 80a8811f1..761337b07 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,4 +1,5 @@ open Glob_term +open Misctypes (* Ocaml 3.06 Map.S does not handle is_empty *) val idmap_is_empty : 'a Names.Idmap.t -> bool diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 42df294a0..96bde6f1b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -7,6 +7,8 @@ open Indfun_common open Libnames open Glob_term open Declarations +open Misctypes +open Decl_kinds let is_rec_info scheme_info = let test_branche min acc (_,_,br) = @@ -64,7 +66,7 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ) + (princ,NoBindings, Tacmach.pf_type_of g princ) | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> @@ -109,7 +111,7 @@ let functional_induction with_clean c princl pat = in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl ) - (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) + (Hiddentac.h_reduce flag Locusops.allHypsAndConcl) g else Tacticals.tclIDTAC g in @@ -480,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let b = Names.id_of_string "___b" in Topconstr.mkLambdaC( [dummy_loc,Name a;dummy_loc,Name b], - Topconstr.Default Lib.Explicit, + Topconstr.Default Explicit, wf_arg_type, Topconstr.mkAppC(wf_rel_expr, [ @@ -744,10 +746,9 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,CastConv(ck,b2)) -> - CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) - | CCast(loc,b1,CastCoerce) -> - CCast(loc,add_args id new_args b1,CastCoerce) + | CCast(loc,b1,b2) -> + CCast(loc,add_args id new_args b1, + Miscops.map_cast_type (add_args id new_args) b2) | CRecord (loc, w, pars) -> CRecord (loc, (match w with Some w -> Some (add_args id new_args w) | _ -> None), diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index faa5f2e46..c0b72f0b3 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -7,6 +7,7 @@ open Indfun_common open Libnames open Glob_term open Declarations +open Misctypes val do_generate_principle : bool -> @@ -17,8 +18,8 @@ val do_generate_principle : val functional_induction : bool -> Term.constr -> - (Term.constr * Term.constr Glob_term.bindings) option -> - Genarg.intro_pattern_expr Pp.located option -> + (Term.constr * Term.constr bindings) option -> + intro_pattern_expr Pp.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b92a8daf3..667be89d0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,22 +19,23 @@ open Indfun_common open Tacmach open Sign open Hiddentac +open Misctypes (* Some pretty printing function for debugging purpose *) let pr_binding prc = function - | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function - | Glob_term.ImplicitBindings l -> + | ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence prc l - | Glob_term.ExplicitBindings l -> + | ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Glob_term.NoBindings -> mt () + | NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -272,7 +273,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.map (fun (_,_,br_type) -> List.map - (fun id -> dummy_loc, Genarg.IntroIdentifier id) + (fun id -> dummy_loc, IntroIdentifier id) (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches @@ -319,7 +320,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem match b with | None -> pre_tac | Some b -> - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac else pre_tac ) (pf_hyps g) @@ -330,7 +331,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_right (fun (_,pat) acc -> match pat with - | Genarg.IntroIdentifier id -> id::acc + | IntroIdentifier id -> id::acc | _ -> anomaly "Not an identifier" ) (List.nth intro_pats (pred i)) @@ -420,7 +421,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Glob_term.rConst = [] } ) - onConcl; + Locusops.onConcl; observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -571,7 +572,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) ) @@ -754,15 +755,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Termops.InHyp) )) + unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; + tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Termops.InHyp) )) + unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; + tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -797,7 +798,7 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Glob_term.NoBindings); + h_case false (v,NoBindings); intros_with_rewrite ] g | LetIn _ -> @@ -807,7 +808,7 @@ and intros_with_rewrite_aux : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; intros_with_rewrite ] g @@ -822,7 +823,7 @@ and intros_with_rewrite_aux : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; intros_with_rewrite ] g @@ -834,7 +835,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,Glob_term.NoBindings); + h_case false (v,NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -961,12 +962,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = {Glob_term.all_flags with Glob_term.rDelta = false; }) - onConcl + Locusops.onConcl ; h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))] + else unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in @@ -1004,7 +1005,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -1056,7 +1057,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs)) + (make_scheme (array_map_to_list (fun const -> const,GType None) funs)) ) in let proving_tac = @@ -1209,7 +1210,7 @@ let functional_inversion kn hid fconst f_correct : tactic = let pre_tac,f_args,res = match kind_of_term args.(1),kind_of_term args.(2) with | App(f,f_args),_ when eq_constr f fconst -> - ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2)) + ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2)) |_,App(f,f_args) when eq_constr f fconst -> ((fun hid -> tclIDTAC),f_args,args.(1)) | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) @@ -1219,7 +1220,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; h_intro hid; - Inv.inv FullInversion None (Glob_term.NamedHyp hid); + Inv.inv FullInversion None (NamedHyp hid); (fun g -> let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3ea9c3d3e..0ec5f7bce 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -23,6 +23,7 @@ open Declarations open Environ open Glob_term open Glob_termops +open Decl_kinds (** {1 Utilities} *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8eb7d0e8f..d11909043 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -44,7 +44,7 @@ open Equality open Auto open Eauto -open Genarg +open Misctypes open Indfun_common @@ -288,7 +288,7 @@ let tclUSER tac is_mes l g = if is_mes then tclTHENLIST [ - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]; tac ] @@ -566,9 +566,9 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = tclTHENLIST[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; - observe_tac (str "simple_iter") (simpl_iter onConcl); + observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") - (unfold_in_concl[((true,[1]), + (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)]); observe_tac (str "test" ) ( tclTHENLIST[ @@ -685,7 +685,7 @@ let mkDestructEq : [h_generalize new_hyps; (fun g2 -> change_in_concl None - (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case expr], to_revert @@ -857,7 +857,7 @@ let rec make_rewrite_list expr_info max = function let def_na,_,_ = destProd t in Nameops.out_name k_na,Nameops.out_name def_na in - general_rewrite_bindings false Termops.all_occurrences + general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[dummy_loc,NamedHyp def, @@ -883,7 +883,8 @@ let make_rewrite expr_info l hp max = let def_na,_,_ = destProd t in Nameops.out_name k_na,Nameops.out_name def_na in - observe_tac (str "general_rewrite_bindings") (general_rewrite_bindings false Termops.all_occurrences + observe_tac (str "general_rewrite_bindings") + (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[dummy_loc,NamedHyp def, @@ -892,9 +893,9 @@ let make_rewrite expr_info l hp max = [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (tclTHENLIST[ - simpl_iter onConcl; + simpl_iter Locusops.onConcl; observe_tac (str "unfold functional") - (unfold_in_concl[((true,[1]), + (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)]); (list_rewrite true @@ -1413,7 +1414,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; - unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)]; + unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; observe_tac (str "simplest_case") (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))); diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 9deeb6066..cd87e93ec 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -21,6 +21,7 @@ open Ring open Mutils open Glob_term open Errors +open Misctypes let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 1057c646f..2c82bab7b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -34,6 +34,7 @@ open Logic open Libnames open Nametab open Contradiction +open Misctypes module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -129,12 +130,12 @@ let intern_id,unintern_id = let mk_then = tclTHENLIST -let exists_tac c = constructor_tac false (Some 1) 1 (Glob_term.ImplicitBindings [c]) +let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) -let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s] +let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = let rec loop = function diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index b3151f26c..4bf08912a 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -827,9 +827,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences true false c'i_eq_c''i) + Locus.AllOccurrences true false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences true false c'i_eq_c''i)) + Locus.AllOccurrences true false c'i_eq_c''i)) [tac])) else (tclORELSE diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index e834650ac..a74666fdd 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -33,6 +33,7 @@ open Printer open Declare open Decl_kinds open Entries +open Misctypes (****************************************************************************) (* controlled reduction *) @@ -102,7 +103,7 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));; TACTIC EXTEND protect_fv |