summaryrefslogtreecommitdiff
path: root/tactics/refine.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/refine.ml')
-rw-r--r--tactics/refine.ml81
1 files changed, 40 insertions, 41 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 4a2fb01b..712e1f81 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refine.ml,v 1.34.2.2 2004/07/16 19:30:54 herbelin Exp $ *)
+(* $Id: refine.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
@@ -66,12 +66,12 @@ and sg_proofs = (term_with_holes option) list
(* pour debugger *)
let rec pp_th (TH(c,mm,sg)) =
- (str"TH=[ " ++ hov 0 (prterm c ++ fnl () ++
+ (str"TH=[ " ++ hov 0 (pr_lconstr c ++ fnl () ++
(* pp_mm mm ++ fnl () ++ *)
pp_sg sg) ++ str "]")
and pp_mm l =
hov 0 (prlist_with_sep (fun _ -> (fnl ()))
- (fun (n,c) -> (int n ++ str" --> " ++ prterm c)) l)
+ (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)
@@ -89,72 +89,71 @@ and pp_sg sg =
* meta_map correspond à celui des buts qui seront engendrés par le refine.
*)
-let replace_by_meta env gmm = function
+let replace_by_meta env = function
| TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
| (TH (c,mm,_)) as th ->
- let n = Clenv.new_meta() in
+ let n = Evarutil.new_meta() in
let m = mkMeta n in
(* quand on introduit une mv on calcule son type *)
let ty = match kind_of_term c with
| Lambda (Name id,c1,c2) when isCast c2 ->
- mkNamedProd id c1 (snd (destCast c2))
+ let _,_,t = destCast c2 in mkNamedProd id c1 t
| Lambda (Anonymous,c1,c2) when isCast c2 ->
- mkArrow c1 (snd (destCast c2))
+ let _,_,t = destCast c2 in mkArrow c1 t
| _ -> (* (App _ | Case _) -> *)
- Retyping.get_type_of_with_meta env Evd.empty (gmm@mm) c
+ Retyping.get_type_of_with_meta env Evd.empty mm c
(*
| Fix ((_,j),(v,_,_)) ->
v.(j) (* en pleine confiance ! *)
| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
*)
in
- mkCast (m,ty),[n,ty],[Some th]
+ mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
exception NoMeta
-let replace_in_array env gmm a =
+let replace_in_array keep_length env a =
if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
raise NoMeta;
let a' = Array.map (function
- | (TH (c,mm,[])) -> c,mm,[]
- | th -> replace_by_meta env gmm th) a
+ | (TH (c,mm,[])) when not keep_length -> c,mm,[]
+ | th -> replace_by_meta env th) a
in
- let v' = Array.map (fun (x,_,_) -> x) a' in
- let mm = Array.fold_left (@) [] (Array.map (fun (_,x,_) -> x) a') in
- let sgp = Array.fold_left (@) [] (Array.map (fun (_,_,x) -> x) 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 "_" in
next_global_ident_away true id (ids_of_named_context (named_context env))
-let rec compute_metamap env gmm c = match kind_of_term c with
+let rec compute_metamap env c = match kind_of_term c with
(* le terme est directement une preuve *)
| (Const _ | Evar _ | Ind _ | Construct _ |
Sort _ | Var _ | Rel _) ->
TH (c,[],[])
+
(* le terme est une mv => un but *)
| Meta n ->
- (*
- Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
- let ty = Retyping.get_type_of_with_meta env Evd.empty lmeta c in
- *)
TH (c,[],[None])
- | Cast (m,ty) when isMeta m ->
+
+ | Cast (m,_, ty) when isMeta m ->
TH (c,[destMeta m,ty],[None])
+
(* abstraction => il faut décomposer si le terme dessous n'est pas pur
* attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
* où x est une variable FRAICHE *)
| Lambda (name,c1,c2) ->
let v = fresh env name in
let env' = push_named (v,None,c1) env in
- begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
+ begin match compute_metamap env' (subst1 (mkVar v) c2) with
(* terme de preuve complet *)
| TH (_,_,[]) -> TH (c,[],[])
(* terme de preuve incomplet *)
| th ->
- let m,mm,sgp = replace_by_meta env' gmm th in
+ let m,mm,sgp = replace_by_meta env' th in
TH (mkLambda (Name v,c1,m), mm, sgp)
end
@@ -163,21 +162,21 @@ let rec compute_metamap env gmm c = match kind_of_term c with
error "Refine: body of let-in cannot contain existentials";
let v = fresh env name in
let env' = push_named (v,Some c1,t1) env in
- begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
+ begin match compute_metamap env' (subst1 (mkVar v) c2) with
(* terme de preuve complet *)
| TH (_,_,[]) -> TH (c,[],[])
(* terme de preuve incomplet *)
| th ->
- let m,mm,sgp = replace_by_meta env' gmm th in
+ let m,mm,sgp = replace_by_meta env' th in
TH (mkLetIn (Name v,c1,t1,m), mm, sgp)
end
(* 4. Application *)
| App (f,v) ->
- let a = Array.map (compute_metamap env gmm) (Array.append [|f|] v) in
+ let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
begin
try
- let v',mm,sgp = replace_in_array env gmm a in
+ let v',mm,sgp = replace_in_array false env a in
let v'' = Array.sub v' 1 (Array.length v) in
TH (mkApp(v'.(0), v''),mm,sgp)
with NoMeta ->
@@ -188,10 +187,10 @@ let rec compute_metamap env gmm c = match kind_of_term c with
(* bof... *)
let nbr = Array.length v in
let v = Array.append [|p;cc|] v in
- let a = Array.map (compute_metamap env gmm) v in
+ let a = Array.map (compute_metamap env) v in
begin
try
- let v',mm,sgp = replace_in_array env gmm a in
+ let v',mm,sgp = replace_in_array false env a in
let v'' = Array.sub v' 2 nbr in
TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
with NoMeta ->
@@ -205,12 +204,12 @@ let rec compute_metamap env gmm c = match kind_of_term c with
let fi' = Array.map (fun id -> Name id) vi in
let env' = push_named_rec_types (fi',ai,v) env in
let a = Array.map
- (compute_metamap env' gmm)
+ (compute_metamap env')
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
- let v',mm,sgp = replace_in_array env' gmm a in
+ let v',mm,sgp = replace_in_array true env' a in
let fix = mkFix ((ni,i),(fi',ai,v')) in
TH (fix,mm,sgp)
with NoMeta ->
@@ -218,7 +217,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
end
(* Cast. Est-ce bien exact ? *)
- | Cast (c,t) -> compute_metamap env gmm c
+ | Cast (c,_,t) -> compute_metamap env c
(*let TH (c',mm,sgp) = compute_metamap sign c in
TH (mkCast (c',t),mm,sgp) *)
@@ -235,12 +234,12 @@ let rec compute_metamap env gmm c = match kind_of_term c with
let fi' = Array.map (fun id -> Name id) vi in
let env' = push_named_rec_types (fi',ai,v) env in
let a = Array.map
- (compute_metamap env' gmm)
+ (compute_metamap env')
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
- let v',mm,sgp = replace_in_array env' gmm a in
+ let v',mm,sgp = replace_in_array true env' a in
let cofix = mkCoFix (i,(fi',ai,v')) in
TH (cofix,mm,sgp)
with NoMeta ->
@@ -253,14 +252,14 @@ let rec compute_metamap env gmm c = match kind_of_term c with
* Réalise le 3. ci-dessus
*)
-let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
+let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let c = substl subst c in
match (kind_of_term c,sgp) with
(* mv => sous-but : on ne fait rien *)
| Meta _ , _ ->
tclIDTAC gl
- | Cast (c,_), _ when isMeta c ->
+ | Cast (c,_,_), _ when isMeta c ->
tclIDTAC gl
(* terme pur => refine *)
@@ -339,8 +338,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
let refine oc gl =
let sigma = project gl in
- let env = pf_env gl in
- let (gmm,c) = Clenv.exist_to_meta sigma oc in
- let th = compute_metamap env gmm c in
- tcc_aux [] th gl
-
+ let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+ (* 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) c in
+ tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 11:26:45 +0000