summaryrefslogtreecommitdiff
path: root/tactics/refine.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/refine.ml')
-rw-r--r--tactics/refine.ml397
1 files changed, 0 insertions, 397 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml
deleted file mode 100644
index f0a3b352..00000000
--- a/tactics/refine.ml
+++ /dev/null
@@ -1,397 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
-(* \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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 07:56:55 +0000