From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- tactics/refine.ml | 81 +++++++++++++++++++++++++++---------------------------- 1 file changed, 40 insertions(+), 41 deletions(-) (limited to 'tactics/refine.ml') 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 -- cgit v1.2.3