aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/omega/coq_omega.ml81
-rw-r--r--proofs/clenv.ml119
-rw-r--r--proofs/clenv.mli9
-rw-r--r--tactics/tactics.ml19
-rw-r--r--tactics/tactics.mli2
5 files changed, 50 insertions, 180 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 0d2a2f8f1..6df04bd37 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -70,91 +70,12 @@ let new_identifier_var =
let rec mk_then =
function [t] -> t | (t::l) -> (tclTHEN (t) (mk_then l)) | [] -> tclIDTAC
-let collect_com lbind =
- map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind
-
-(*** EST-CE QUE CES FONCTIONS NE SONT PAS AILLEURS DANS LE CODE ?? *)
-
-let make_clenv_binding_apply wc (c,t) lbind =
- let largs = collect_com lbind in
- let lcomargs = List.length largs in
- if lcomargs = List.length lbind then
- let clause = mk_clenv_from wc (c,t) in
- clenv_constrain_missing_args largs clause
- else if lcomargs = 0 then
- let clause = mk_clenv_rename_from wc (c,t) in
- clenv_match_args lbind clause
- else
- errorlabstrm "make_clenv_bindings"
- (str "Cannot mix bindings and free associations")
-
-let resolve_with_bindings_tac (c,lbind) gl =
- let (wc,kONT) = startWalk gl in
- let t = w_hnf_constr wc (w_type_of wc c) in
- let clause = make_clenv_binding_apply wc (c,t) lbind in
- res_pf kONT clause gl
-
-(*
-let pf_one_step_reduce = pf_reduce Tacred.one_step_reduce
-
-let reduce_to_mind gl t =
- let rec elimrec t l =
- let c, args = whd_stack t in
- match kind_of_term c, args with
- | (Ind ind,_) -> (ind,Environ.it_mkProd_or_LetIn t l)
- | (Const _,_) ->
- (try
- let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
- with e when catchable_exception e ->
- errorlabstrm "tactics__reduce_to_mind"
- (str"Not an inductive product"))
- | (Case _,_) ->
- (try
- let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
- with e when catchable_exception e ->
- errorlabstrm "tactics__reduce_to_mind"
- (str"Not an inductive product"))
- | (Cast (c,_),[]) -> elimrec c l
- | (Prod (n,ty,t'),[]) ->
- let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
- elimrec t' ((n,None,ty')::l)
- | (LetIn (n,b,ty,t'),[]) ->
- let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
- elimrec t' ((n,Some b,ty')::l)
- | _ -> error "Not an inductive product"
- in
- elimrec t []
-*)
-
-let reduce_to_mind = pf_reduce_to_quantified_ind
-
-let constructor_tac nconstropt i lbind gl =
- let cl = pf_concl gl in
- let (mind, redcl) = reduce_to_mind gl cl in
- let (mib,mip) = Global.lookup_inductive mind in
- let nconstr = Array.length mip.mind_consnames
- and sigma = project gl in
- (match nconstropt with
- | Some expnconstr ->
- if expnconstr <> nconstr then
- error "Not the expected number of constructors"
- | _ -> ());
- if i > nconstr then error "Not enough Constructors";
- let c = mkConstruct (ith_constructor_of_inductive mind i) in
- let resolve_tac = resolve_with_bindings_tac (c,lbind) in
- (tclTHEN (tclTHEN (change_in_concl redcl) intros) resolve_tac) gl
-
-let exists_tac c= constructor_tac (Some 1) 1 [Com,c]
-
+let exists_tac c = constructor_tac (Some 1) 1 [Com,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 [[], Lazy.force s]
-(*** fin de EST-CE QUE CES FONCTIONS NE SONT PAS AILLEURS DANS LE CODE ?? *)
-(****************************************************************)
-
let rev_assoc k =
let rec loop = function
| [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 831267087..6db3cfcac 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -336,7 +336,7 @@ let mk_clenv wc cty =
let clenv_environments bound c =
let rec clrec (ne,e,metas) n c =
match n, kind_of_term c with
- | (0, _) -> (ne, e, List.rev metas, c)
+ | (Some 0, _) -> (ne, e, List.rev metas, c)
| (n, Cast (c,_)) -> clrec (ne,e,metas) n c
| (n, Prod (na,c1,c2)) ->
let mv = new_meta () in
@@ -356,9 +356,10 @@ let clenv_environments bound c =
ne
in
let e' = Intmap.add mv (Cltyp (mk_freelisted c1)) e in
- clrec (ne',e', (mkMeta mv)::metas) (n-1)
+ clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) c2) else c2)
- | (n, LetIn (na,b,_,c)) -> clrec (ne,e,metas) (n-1) (subst1 b c)
+ | (n, LetIn (na,b,_,c)) ->
+ clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c)
| (n, _) -> (ne, e, List.rev metas, c)
in
clrec (Intmap.empty,Intmap.empty,[]) bound c
@@ -371,13 +372,7 @@ let mk_clenv_from_n wc n (c,cty) =
env = env;
hook = wc }
-let mk_clenv_from wc (c,cty) =
- let (namenv,env,args,concl) = clenv_environments (-1) cty in
- { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
- templtyp = mk_freelisted concl;
- namenv = namenv;
- env = env;
- hook = wc }
+let mk_clenv_from wc = mk_clenv_from_n wc None
let connect_clenv wc clenv =
{ templval = clenv.templval;
@@ -412,8 +407,6 @@ let mk_clenv_rename_hnf_constr_type_of wc t =
let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
-let mk_clenv_printable_type_of = mk_clenv_type_of
-
let clenv_assign mv rhs clenv =
let rhs_fls = mk_freelisted rhs in
if intset_exists (mentions clenv mv) rhs_fls.freemetas then
@@ -891,12 +884,13 @@ let clenv_metavars clenv mv =
let clenv_template_metavars clenv = clenv.templval.freemetas
-(* [clenv_dependent clenv cval ctyp]
- * returns a list of the metavariables which appear in the term cval,
+(* [clenv_dependent hyps_only clenv]
+ * returns a list of the metavars which appear in the template of clenv,
* and which are dependent, This is computed by taking the metavars in cval,
* in right-to-left order, and collecting the metavars which appear
- * in their types, and adding in all the metavars appearing in ctyp, the
- * type of cval. *)
+ * in their types, and adding in all the metavars appearing in the
+ * type of clenv.
+ * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
let dependent_metas clenv mvs conclmetas =
List.fold_right
@@ -904,12 +898,15 @@ let dependent_metas clenv mvs conclmetas =
Intset.union deps (clenv_metavars clenv mv))
mvs conclmetas
-let clenv_dependent clenv =
+let clenv_dependent hyps_only clenv =
let mvs = collect_metas (clenv_instance_template clenv) in
let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
let deps = dependent_metas clenv mvs ctyp_mvs in
- List.filter (fun mv -> Intset.mem mv deps) mvs
+ List.filter
+ (fun mv -> Intset.mem mv deps && not (hyps_only && Intset.mem mv ctyp_mvs))
+ mvs
+let clenv_missing c = clenv_dependent true c
(* [clenv_independent clenv]
* returns a list of metavariables which appear in the term cval,
@@ -923,57 +920,17 @@ let clenv_independent clenv =
let deps = dependent_metas clenv mvs ctyp_mvs in
List.filter (fun mv -> not (Intset.mem mv deps)) mvs
-
-(* [clenv_missing clenv]
- * returns a list of the metavariables which appear in the term cval,
- * and which are dependent, and do NOT appear in ctyp. *)
-
-let clenv_missing clenv =
- let mvs = collect_metas (clenv_instance_template clenv) in
- let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
- let deps = dependent_metas clenv mvs ctyp_mvs in
- List.filter
- (fun n -> Intset.mem n deps && not (Intset.mem n ctyp_mvs))
- mvs
-
-let clenv_constrain_missing_args mlist clause =
- if mlist = [] then
- clause
- else
- let occlist = clenv_missing clause in
- if List.length occlist = List.length mlist then
- List.fold_left2
- (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv)
- clause occlist mlist
- else
- error ("Not the right number of missing arguments (expected "
- ^(string_of_int (List.length occlist))^")")
-
-let clenv_constrain_dep_args mlist clause =
- if mlist = [] then
- clause
- else
- let occlist = clenv_dependent clause in
- if List.length occlist = List.length mlist then
- List.fold_left2
- (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv)
- clause occlist mlist
- else
- error ("Not the right number of missing arguments (expected "
- ^(string_of_int (List.length occlist))^")")
-
-let clenv_constrain_dep_args_of mv mlist clause =
- if mlist = [] then
- clause
- else
- let occlist = clenv_dependent clause in
- if List.length occlist = List.length mlist then
- List.fold_left2
- (fun clenv occ m -> clenv_unify true CONV (mkMeta occ) m clenv)
- clause occlist mlist
- else
- error ("clenv_constrain_dep_args_of: Not the right number " ^
- "of dependent arguments")
+let clenv_constrain_dep_args hyps_only clause = function
+ | [] -> clause
+ | mlist ->
+ let occlist = clenv_dependent hyps_only clause in
+ if List.length occlist = List.length mlist then
+ List.fold_left2
+ (fun clenv k c -> clenv_unify true CONV (mkMeta k) c clenv)
+ clause occlist mlist
+ else
+ error ("Not the right number of missing arguments (expected "
+ ^(string_of_int (List.length occlist))^")")
let clenv_lookup_name clenv id =
match intmap_inv clenv.namenv id with
@@ -1011,8 +968,8 @@ let clenv_match_args s clause =
in
let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
and c_typ = w_hnf_constr clause.hook (w_type_of clause.hook c) in
- matchrec
- (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
+ matchrec
+ (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
in
matchrec clause s
@@ -1024,7 +981,7 @@ let clenv_match_args s clause =
* metas. *)
let clenv_pose_dependent_evars clenv =
- let dep_mvs = clenv_dependent clenv in
+ let dep_mvs = clenv_dependent false clenv in
List.fold_left
(fun clenv mv ->
let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
@@ -1066,12 +1023,12 @@ let e_res_pf kONT clenv gls =
let collect_com lbind =
map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind
-let make_clenv_binding_apply wc n (c,t) lbind =
+let make_clenv_binding_gen n wc (c,t) lbind =
let largs = collect_com lbind in
let lcomargs = List.length largs in
if lcomargs = List.length lbind then
let clause = mk_clenv_from_n wc n (c,t) in
- clenv_constrain_missing_args largs clause
+ clenv_constrain_dep_args (n <> None) clause largs
else if lcomargs = 0 then
let clause = mk_clenv_rename_from_n wc n (c,t) in
clenv_match_args lbind clause
@@ -1079,18 +1036,8 @@ let make_clenv_binding_apply wc n (c,t) lbind =
errorlabstrm "make_clenv_bindings"
(str "Cannot mix bindings and free associations")
-let make_clenv_binding wc (c,t) lbind =
- let largs = collect_com lbind in
- let lcomargs = List.length largs in
- if lcomargs = List.length lbind then
- let clause = mk_clenv_from wc (c,t) in
- clenv_constrain_dep_args largs clause
- else if lcomargs = 0 then
- let clause = mk_clenv_rename_from wc (c,t) in
- clenv_match_args lbind clause
- else
- errorlabstrm "make_clenv_bindings"
- (str "Cannot mix bindings and free associations")
+let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
+let make_clenv_binding = make_clenv_binding_gen None
open Printer
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e83d8d7d7..623890538 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -61,11 +61,10 @@ val unify_0 :
val collect_metas : constr -> int list
val mk_clenv : 'a -> constr -> 'a clausenv
val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_from_n : 'a -> int -> constr * constr -> 'a clausenv
+val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
-val mk_clenv_rename_from_n : wc -> int -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
-val mk_clenv_printable_type_of : wc -> constr -> wc clausenv
val mk_clenv_type_of : wc -> constr -> wc clausenv
val connect_clenv : wc -> 'a clausenv -> wc clausenv
@@ -88,8 +87,10 @@ val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
val clenv_independent : wc clausenv -> int list
val clenv_missing : 'a clausenv -> int list
+(*
val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
+*)
val clenv_lookup_name : 'a clausenv -> identifier -> int
val clenv_match_args : (bindOcc * constr) list -> wc clausenv -> wc clausenv
val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
@@ -108,8 +109,10 @@ val unify_to_subterm :
wc clausenv -> constr * constr -> wc clausenv * constr
val unify_to_subterm_list :
bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
+(*
val clenv_constrain_dep_args_of :
int -> constr list -> wc clausenv -> wc clausenv
+*)
val clenv_typed_unify :
Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef9222a30..2285850c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -929,11 +929,10 @@ let rec intros_clearing = function
(* Adding new hypotheses *)
-let new_hyp mopt c blist g =
+let new_hyp mopt c lbind g =
let (wc,kONT) = startWalk g in
- let clause = mk_clenv_printable_type_of wc c in
- let clause' = clenv_match_args blist clause in
- let (thd,tstack) = whd_stack (clenv_instance_template clause') in
+ let clause = make_clenv_binding wc (c,w_type_of wc c) lbind in
+ let (thd,tstack) = whd_stack (clenv_instance_template clause) in
let nargs = List.length tstack in
let cut_pf =
applist(thd,
@@ -983,7 +982,7 @@ let dyn_rename = function
(* Introduction tactics *)
(************************)
-let constructor_checking_bound boundopt i lbind gl =
+let constructor_tac boundopt i lbind gl =
let cl = pf_concl gl in
let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
let nconstr =
@@ -1001,7 +1000,7 @@ let constructor_checking_bound boundopt i lbind gl =
let apply_tac = apply_with_bindings (cons,lbind) in
(tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl
-let one_constructor i = (constructor_checking_bound None i)
+let one_constructor i = constructor_tac None i
let any_constructor gl =
let cl = pf_concl gl in
@@ -1036,7 +1035,7 @@ let dyn_constructor = function
| l -> bad_tactic_args "constructor" l
-let left = (constructor_checking_bound (Some 2) 1)
+let left = constructor_tac (Some 2) 1
let simplest_left = left []
let dyn_left = function
@@ -1044,7 +1043,7 @@ let dyn_left = function
| [Bindings binds] -> tactic_bind_list left binds
| l -> bad_tactic_args "left" l
-let right = (constructor_checking_bound (Some 2) 2)
+let right = constructor_tac (Some 2) 2
let simplest_right = right []
let dyn_right = function
@@ -1053,7 +1052,7 @@ let dyn_right = function
| l -> bad_tactic_args "right" l
-let split = (constructor_checking_bound (Some 1) 1)
+let split = constructor_tac (Some 1) 1
let simplest_split = split []
let dyn_split = function
@@ -1137,7 +1136,7 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
let hyp = mkVar id in
let hyp_typ = clenv_type_of elimclause' hyp in
let hypclause =
- mk_clenv_from_n elimclause'.hook 0 (hyp, hyp_typ) in
+ mk_clenv_from_n elimclause'.hook (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain hypmv elimclause' hypclause in
let new_hyp_prf = clenv_instance_template elimclause'' in
let new_hyp_typ = clenv_instance_template_type elimclause'' in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a1c961400..76a21ba83 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -229,7 +229,7 @@ val dorE : bool -> clause ->tactic
(*s Introduction tactics. *)
-val constructor_checking_bound : int option -> int ->
+val constructor_tac : int option -> int ->
constr substitution -> tactic
val one_constructor : int -> constr substitution -> tactic
val any_constructor : tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 19:03:20 +0000