summaryrefslogtreecommitdiff
path: root/tactics/refine.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/refine.ml')
-rw-r--r--tactics/refine.ml108
1 files changed, 55 insertions, 53 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml
index ff3f0887..cbca38d0 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
+(* $Id$ *)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
@@ -16,19 +16,19 @@
* où les trous sont typés -- et que les sous-buts correspondants
* soient engendrés pour finir la preuve.
*
- * Exemple :
+ * Exemple :
* J'ai le but
- * (x:nat) { y:nat | (minus y x) = x }
+ * forall (x:nat), { y:nat | (minus y x) = x }
* et je donne la preuve incomplète
- * [x:nat](exist nat [y:nat]((minus y x)=x) (plus x x) ?)
+ * fun (x:nat) => exist nat [y:nat]((minus y x)=x) (plus x x) ?
* ce qui engendre le but
- * (minus (plus x x) x)=x
+ * (minus (plus x x) x) = x
*)
(* Pour cela, on procède de la manière suivante :
*
* 1. Un terme de preuve incomplet est un terme contenant des variables
- * existentielles Evar i.e. "?" en syntaxe concrète.
+ * existentielles Evar i.e. "_" en syntaxe concrète.
* La résolution de ces variables n'est plus nécessairement totale
* (ise_resolve called with fail_evar=false) et les variables
* existentielles restantes sont remplacées par des méta-variables
@@ -38,8 +38,10 @@
* 2. On met ensuite le terme "à plat" i.e. on n'autorise des MV qu'au
* permier niveau et pour chacune d'elles, si nécessaire, on donne
* à son tour un terme de preuve incomplet pour la résoudre.
- * Exemple: le terme (f a ? [x:nat](e ?)) donne
- * (f a ?1 ?2) avec ?2 => [x:nat]?3 et ?3 => (e ?4)
+ * Exemple: le terme (f a _ (fun (x:nat) => e _)) donne
+ * (f a ?1 ?2) avec:
+ * - ?2 := fun (x:nat) => ?3
+ * - ?3 := e ?4
* ?1 et ?4 donneront des buts
*
* 3. On écrit ensuite une tactique tcc qui engendre les sous-buts
@@ -51,6 +53,7 @@ open Util
open Names
open Term
open Termops
+open Namegen
open Tacmach
open Sign
open Environ
@@ -60,7 +63,7 @@ open Tactics
open Tacticals
open Printer
-type term_with_holes = TH of constr * metamap * sg_proofs
+type term_with_holes = TH of constr * meta_type_map * sg_proofs
and sg_proofs = (term_with_holes option) list
(* pour debugger *)
@@ -70,12 +73,12 @@ let rec pp_th (TH(c,mm,sg)) =
(* pp_mm mm ++ fnl () ++ *)
pp_sg sg) ++ str "]")
and pp_mm l =
- hov 0 (prlist_with_sep (fun _ -> (fnl ()))
+ hov 0 (prlist_with_sep (fun _ -> (fnl ()))
(fun (n,c) -> (int n ++ str" --> " ++ pr_lconstr c)) l)
and pp_sg sg =
hov 0 (prlist_with_sep (fun _ -> (fnl ()))
(function None -> (str"None") | Some th -> (pp_th th)) sg)
-
+
(* compute_metamap : constr -> 'a evar_map -> term_with_holes
* réalise le 2. ci-dessus
*
@@ -84,7 +87,7 @@ and pp_sg sg =
* par un terme de preuve incomplet (Some c).
*
* On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1"
- * -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y
+ * -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y
* a de meta-variables dans c. On suppose de plus que l'ordre dans la
* meta_map correspond à celui des buts qui seront engendrés par le refine.
*)
@@ -101,11 +104,14 @@ let replace_by_meta env sigma = function
| Lambda (Anonymous,c1,c2) when isCast c2 ->
let _,_,t = destCast c2 in mkArrow c1 t
| _ -> (* (App _ | Case _) -> *)
- Retyping.get_type_of_with_meta env sigma mm c
+ let sigma' =
+ List.fold_right (fun (m,t) sigma -> Evd.meta_declare m t sigma)
+ mm sigma in
+ Retyping.get_type_of env sigma' c
(*
| Fix ((_,j),(v,_,_)) ->
v.(j) (* en pleine confiance ! *)
- | _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
+ | _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
*)
in
if occur_meta ty then
@@ -119,28 +125,28 @@ let replace_in_array keep_length env sigma a =
raise NoMeta;
let a' = Array.map (function
| (TH (c,mm,[])) when not keep_length -> c,mm,[]
- | th -> replace_by_meta env sigma th) a
+ | th -> replace_by_meta env sigma th) a
in
let v' = Array.map pi1 a' in
let mm = Array.fold_left (@) [] (Array.map pi2 a') in
let sgp = Array.fold_left (@) [] (Array.map pi3 a') in
v',mm,sgp
-
+
let fresh env n =
let id = match n with Name x -> x | _ -> id_of_string "_H" in
- next_global_ident_away true id (ids_of_named_context (named_context env))
+ next_ident_away_in_goal id (ids_of_named_context (named_context env))
let rec compute_metamap env sigma c = match kind_of_term c with
(* le terme est directement une preuve *)
| (Const _ | Evar _ | Ind _ | Construct _ |
- Sort _ | Var _ | Rel _) ->
+ Sort _ | Var _ | Rel _) ->
TH (c,[],[])
(* le terme est une mv => un but *)
| Meta n ->
TH (c,[],[None])
- | Cast (m,_, ty) when isMeta m ->
+ | Cast (m,_, ty) when isMeta m ->
TH (c,[destMeta m,ty],[None])
@@ -153,7 +159,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
(* terme de preuve complet *)
| TH (_,_,[]) -> TH (c,[],[])
- (* terme de preuve incomplet *)
+ (* terme de preuve incomplet *)
| th ->
let m,mm,sgp = replace_by_meta env' sigma th in
TH (mkLambda (Name v,c1,m), mm, sgp)
@@ -167,13 +173,13 @@ let rec compute_metamap env sigma c = match kind_of_term c with
begin match th1,th2 with
(* terme de preuve complet *)
| TH (_,_,[]), TH (_,_,[]) -> TH (c,[],[])
- (* terme de preuve incomplet *)
+ (* terme de preuve incomplet *)
| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
let m1,mm1,sgp1 =
- if sgp1=[] then (c1,mm1,[])
+ if sgp1=[] then (c1,mm1,[])
else replace_by_meta env sigma th1 in
let m2,mm2,sgp2 =
- if sgp2=[] then (c2,mm2,[])
+ if sgp2=[] then (c2,mm2,[])
else replace_by_meta env' sigma th2 in
TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
end
@@ -214,7 +220,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
let env' = push_named_rec_types (fi',ai,v) env in
let a = Array.map
(compute_metamap env' sigma)
- (Array.map (substl (List.map mkVar (Array.to_list vi))) v)
+ (Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
@@ -224,12 +230,12 @@ let rec compute_metamap env sigma c = match kind_of_term c with
with NoMeta ->
TH (c,[],[])
end
-
+
(* Cast. Est-ce bien exact ? *)
| Cast (c,_,t) -> compute_metamap env sigma c
(*let TH (c',mm,sgp) = compute_metamap sign c in
TH (mkCast (c',t),mm,sgp) *)
-
+
(* Produit. Est-ce bien exact ? *)
| Prod (_,_,_) ->
if occur_meta c then
@@ -244,7 +250,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
let env' = push_named_rec_types (fi',ai,v) env in
let a = Array.map
(compute_metamap env' sigma)
- (Array.map (substl (List.map mkVar (Array.to_list vi))) v)
+ (Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
@@ -257,7 +263,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
(* tcc_aux : term_with_holes -> tactic
- *
+ *
* Réalise le 3. ci-dessus
*)
@@ -270,11 +276,11 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| Cast (c,_,_), _ when isMeta c ->
tclIDTAC gl
-
+
(* terme pur => refine *)
| _,[] ->
refine c gl
-
+
(* abstraction => intro *)
| Lambda (Name id,_,m), _ ->
assert (isMeta (strip_outer_cast m));
@@ -282,18 +288,18 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| [None] -> intro_mustbe_force id gl
| [Some th] ->
tclTHEN (introduction id)
- (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
+ (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)) gl
| _ -> assert false
end
| Lambda (Anonymous,_,m), _ -> (* if anon vars are allowed in evars *)
assert (isMeta (strip_outer_cast m));
begin match sgp with
- | [None] -> tclTHEN intro (onLastHyp (fun id -> clear [id])) gl
+ | [None] -> tclTHEN intro (onLastHypId (fun id -> clear [id])) gl
| [Some th] ->
tclTHEN
intro
- (onLastHyp (fun id ->
+ (onLastHypId (fun id ->
tclTHEN
(clear [id])
(tcc_aux (mkVar (*dummy*) id::subst) th))) gl
@@ -304,29 +310,29 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
let c = pf_concl gl in
let newc = mkNamedLetIn id c1 t1 c in
- tclTHEN
- (change_in_concl None newc)
- (match sgp with
+ tclTHEN
+ (change_in_concl None newc)
+ (match sgp with
| [None] -> introduction id
| [Some th] ->
tclTHEN (introduction id)
- (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th))
- | _ -> assert false)
+ (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th))
+ | _ -> assert false)
gl
(* let in with holes in the body => unable to handle dependency
because of evars limitation, use non dependent assert instead *)
| LetIn (Name id,c1,t1,c2), _ ->
tclTHENS
- (assert_tac (Name id) t1)
- [(match List.hd sgp with
+ (assert_tac (Name id) t1)
+ [(match List.hd sgp with
| None -> tclIDTAC
- | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th));
- (match List.tl sgp with
+ | Some th -> onLastHypId (fun id -> tcc_aux (mkVar id::subst) th));
+ (match List.tl sgp with
| [] -> refine (subst1 (mkVar id) c2) (* a complete proof *)
| [None] -> tclIDTAC (* a meta *)
| [Some th] -> (* a partial proof *)
- onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)
+ onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)
| _ -> assert false)]
gl
@@ -339,10 +345,9 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
let firsts,lasts = list_chop j (Array.to_list fixes) in
tclTHENS
- (mutual_fix_with_index
- (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
+ (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
(List.map (function
- | None -> tclIDTAC
+ | None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
@@ -355,9 +360,9 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
let firsts,lasts = list_chop j (Array.to_list cofixes) in
tclTHENS
- (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
+ (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
(List.map (function
- | None -> tclIDTAC
+ | None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
@@ -374,13 +379,10 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let refine (evd,c) gl =
let sigma = project gl in
- let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
- ~onlyargs:true ~fail:false (pf_env gl)
- (Evd.create_evar_defs evd))
- in
+ let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
let c = Evarutil.nf_evar evd c in
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
- (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
+ (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
complicated to update meta types when passing through a binder *)
let th = compute_metamap (pf_env gl) evd c in
tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 18:32:54 +0000