(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
(*
* L'idée est, en quelque sorte, d'avoir de "vraies" métavariables
* dans Coq, c'est-à-dire de donner des preuves incomplètes -- mais
* où les trous sont typés -- et que les sous-buts correspondants
* soient engendrés pour finir la preuve.
*
* Exemple :
* J'ai le but
* forall (x:nat), { y:nat | (minus y x) = x }
* et je donne la preuve incomplète
* 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
*)
(* 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.
* 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
* castées par leur types (celui est connu : soit donné, soit trouvé
* pendant la phase de résolution).
*
* 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 _ (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
* à partir d'une preuve incomplète.
*)
open Pp
open Util
open Names
open Term
open Termops
open Namegen
open Tacmach
open Sign
open Environ
open Reduction
open Typing
open Tactics
open Tacticals
open Printer
type term_with_holes = TH of constr * meta_type_map * sg_proofs
and sg_proofs = (term_with_holes option) list
(* pour debugger *)
let rec pp_th (TH(c,mm,sg)) =
(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" --> " ++ 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
*
* Pour cela, on renvoie une meta_map qui indique pour chaque meta-variable
* si elle correspond à un but (None) ou si elle réduite à son tour
* 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
* 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.
*)
let replace_by_meta env sigma = function
| TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
| (TH (c,mm,_)) as th ->
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 ->
let _,_,t = destCast c2 in mkNamedProd id c1 t
| Lambda (Anonymous,c1,c2) when isCast c2 ->
let _,_,t = destCast c2 in mkArrow c1 t
| _ -> (* (App _ | Case _) -> *)
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)"
*)
in
mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
exception NoMeta
let replace_in_array keep_length env sigma a =
if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
raise NoMeta;
let a' = Array.map (function
| (TH (c,mm,[])) when not keep_length -> c,mm,[]
| 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_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 _) ->
TH (c,[],[])
(* le terme est une mv => un but *)
| Meta n ->
TH (c,[],[None])
| 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' sigma (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' sigma th in
TH (mkLambda (Name v,c1,m), mm, sgp)
end
| LetIn (name, c1, t1, c2) ->
let v = fresh env name in
let th1 = compute_metamap env sigma c1 in
let env' = push_named (v,Some c1,t1) env in
let th2 = compute_metamap env' sigma (subst1 (mkVar v) c2) in
begin match th1,th2 with
(* terme de preuve complet *)
| TH (_,_,[]), TH (_,_,[]) -> TH (c,[],[])
(* terme de preuve incomplet *)
| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
let m1,mm1,sgp1 =
if sgp1=[] then (c1,mm1,[])
else replace_by_meta env sigma th1 in
let m2,mm2,sgp2 =
if sgp2=[] then (c2,mm2,[])
else replace_by_meta env' sigma th2 in
TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
end
(* 4. Application *)
| App (f,v) ->
let a = Array.map (compute_metamap env sigma) (Array.append [|f|] v) in
begin
try
let v',mm,sgp = replace_in_array false env sigma a in
let v'' = Array.sub v' 1 (Array.length v) in
TH (mkApp(v'.(0), v''),mm,sgp)
with NoMeta ->
TH (c,[],[])
end
| Case (ci,p,cc,v) ->
(* bof... *)
let nbr = Array.length v in
let v = Array.append [|p;cc|] v in
let a = Array.map (compute_metamap env sigma) v in
begin
try
let v',mm,sgp = replace_in_array false env sigma a in
let v'' = Array.sub v' 2 nbr in
TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
with NoMeta ->
TH (c,[],[])
end
(* 5. Fix. *)
| Fix ((ni,i),(fi,ai,v)) ->
(* TODO: use a fold *)
let vi = Array.map (fresh env) fi in
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' sigma)
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
let v',mm,sgp = replace_in_array true env' sigma a in
let fix = mkFix ((ni,i),(fi',ai,v')) in
TH (fix,mm,sgp)
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
error "refine: proof term contains metas in a product."
else
TH (c,[],[])
(* Cofix. *)
| CoFix (i,(fi,ai,v)) ->
let vi = Array.map (fresh env) fi in
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' sigma)
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
in
begin
try
let v',mm,sgp = replace_in_array true env' sigma a in
let cofix = mkCoFix (i,(fi',ai,v')) in
TH (cofix,mm,sgp)
with NoMeta ->
TH (c,[],[])
end
(* tcc_aux : term_with_holes -> tactic
*
* Réalise le 3. ci-dessus
*)
let ensure_products n =
let p = ref 0 in
let rec aux n gl =
if n = 0 then tclFAIL 0 (mt()) gl
else
tclTHEN
(tclORELSE intro (fun gl -> incr p; introf gl))
(aux (n-1)) gl in
tclORELSE
(aux n)
(* Now we know how many red are needed *)
(fun gl -> tclDO !p red_in_concl 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 ->
tclIDTAC gl
(* terme pur => refine *)
| _,[] ->
refine c gl
(* abstraction => intro *)
| Lambda (Name id,_,m), _ ->
assert (isMeta (strip_outer_cast m));
begin match sgp with
| [None] -> intro_mustbe_force id gl
| [Some th] ->
tclTHEN (introduction id)
(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 (onLastHypId (fun id -> clear [id])) gl
| [Some th] ->
tclTHEN
intro
(onLastHypId (fun id ->
tclTHEN
(clear [id])
(tcc_aux (mkVar (*dummy*) id::subst) th))) gl
| _ -> assert false
end
(* let in without holes in the body => possibly dependent intro *)
| 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
| [None] -> introduction id
| [Some th] ->
tclTHEN (introduction id)
(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
| None -> tclIDTAC
| 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 *)
onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)
| _ -> assert false)]
gl
(* fix => tactique Fix *)
| Fix ((ni,j),(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
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
(tclTHEN
(ensure_products (succ ni.(j)))
(mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j))
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
(* cofix => tactique CoFix *)
| CoFix (j,(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
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 (out_name fi.(j)) (firsts@List.tl lasts) j)
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
(* sinon on fait refine du terme puis appels rec. sur les sous-buts.
* c'est le cas pour App et MutCase. *)
| _ ->
tclTHENS
(refine c)
(List.map
(function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
gl
(* Et finalement la tactique refine elle-même : *)
let refine (evd,c) gl =
let sigma = project gl in
let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (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
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