diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/ftactic.ml | 72 | ||||
-rw-r--r-- | tactics/ftactic.mli | 62 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 259 | ||||
-rw-r--r-- | tactics/tactics.mllib | 1 |
4 files changed, 233 insertions, 161 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml new file mode 100644 index 000000000..fcc385c4e --- /dev/null +++ b/tactics/ftactic.ml @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Proofview.Notations + +(** Focussing tactics *) + +type 'a focus = +| Uniform of 'a +| Depends of 'a list + +(** Type of tactics potentially goal-dependent. If it contains a [Depends], + then the length of the inner list is guaranteed to be the number of + currently focussed goals. Otherwise it means the tactic does not depends + on the current set of focussed goals. *) +type 'a t = 'a focus Proofview.tactic + +let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) + +let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function +| Uniform x -> f x +| Depends l -> + let f arg = f arg >>= function + | Uniform x -> + (** We dispatch the uniform result on each goal under focus, as we know + that the [m] argument was actually dependent. *) + Proofview.Goal.raw_goals >>= fun l -> + let ans = List.map (fun _ -> x) l in + Proofview.tclUNIT ans + | Depends l -> Proofview.tclUNIT l + in + Proofview.tclDISPATCHL (List.map f l) >>= fun l -> + Proofview.tclUNIT (Depends (List.concat l)) + +let enter f = + bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + +let raw_enter f = + bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l)) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + +let lift (type a) (t:a Proofview.tactic) : a t = + Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) + +(** If the tactic returns unit, we can focus on the goals if necessary. *) +let run m k = m >>= function +| Uniform v -> k v +| Depends l -> + let tacs = List.map k l in + Proofview.tclDISPATCH tacs + +let (>>=) = bind + +let (<*>) = fun m n -> bind m (fun () -> n) + +module Self = +struct + type 'a t = 'a focus Proofview.tactic + let return = return + let (>>=) = bind +end + +module Ftac = Monad.Make(Self) +module List = Ftac.List + +let debug_prompt = Tactic_debug.debug_prompt diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli new file mode 100644 index 000000000..16cfca08d --- /dev/null +++ b/tactics/ftactic.mli @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Potentially focussing tactics *) + +type +'a focus + +type +'a t = 'a focus Proofview.tactic +(** The type of focussing tactics. A focussing tactic is like a normal tactic, + except that it is able to remember it have entered a goal. Whenever this is + the case, each subsequent effect of the tactic is dispatched on the + focussed goals. This is a monad. *) + +(** {5 Monadic interface} *) + +val return : 'a -> 'a t +(** The unit of the monad. *) + +val bind : 'a t -> ('a -> 'b t) -> 'b t +(** The bind of the monad. *) + +(** {5 Operations} *) + +val lift : 'a Proofview.tactic -> 'a t +(** Transform a tactic into a focussing tactic. The resulting tactic is not + focussed. *) + +val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic +(** Given a continuation producing a tactic, evaluates the focussing tactic. If + the tactic has not focussed, then the continuation is evaluated once. + Otherwise it is called in each of the currently focussed goals. *) + +(** {5 Focussing} *) + +val enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t +(** Enter a goal. The resulting tactic is focussed. *) + +val raw_enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t +(** Enter a goal, without evar normalization. The resulting tactic is + focussed. *) + +(** {5 Notations} *) + +val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +(** Notation for {!bind}. *) + +val (<*>) : unit t -> 'a t -> 'a t +(** Sequence. *) + +(** {5 List operations} *) + +module List : Monad.ListS with type 'a t := 'a t + +(** {5 Debug} *) + +val debug_prompt : + int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ccea38caa..5b0002d7e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -42,61 +42,6 @@ open Tacintern open Taccoerce open Proofview.Notations -(** Goal-sensitive tactics *) -module GTac = -struct - type 'a garg = - | Uniform of 'a - | Depends of 'a list - - (** Type of tactics potentially goal-dependent. If it contains a [Depends], - then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depends - on the current set of focussed goals. *) - type 'a t = 'a garg Proofview.tactic - - let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) - - let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function - | Uniform x -> f x - | Depends l -> - let f arg = f arg >>= function - | Uniform x -> - (** We dispatch the uniform result on each goal under focus, as we know - that the [m] argument was actually dependent. *) - Proofview.Goal.raw_goals >>= fun l -> - let ans = List.map (fun _ -> x) l in - Proofview.tclUNIT ans - | Depends l -> Proofview.tclUNIT l - in - Proofview.tclDISPATCHL (List.map f l) >>= fun l -> - Proofview.tclUNIT (Depends (List.concat l)) - - let enter f = - bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) - - let raw_enter f = - bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) - - let lift (type a) (t:a Proofview.tactic) : a t = - Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) - - (** If the tactic returns unit, we can focus on the goals if necessary. *) - let run m k = m >>= function - | Uniform v -> k v - | Depends l -> - let tacs = List.map k l in - Proofview.tclDISPATCH tacs - - let (>>=) = bind - -end - -module GTac' = Monad_.Make(GTac) -module GTacList = GTac'.List - let safe_msgnl s = Proofview.NonLogical.catch (Proofview.NonLogical.print (s++fnl())) @@ -768,56 +713,56 @@ let interp_constr_may_eval ist env sigma c = let rec message_of_value v = let v = Value.normalize v in let open Tacmach.New in - let open GTac in + let open Ftactic in if has_type v (topwit wit_tacvalue) then - GTac.return (str "<tactic>") + Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - GTac.enter begin fun gl -> GTac.return (pr_constr_env (pf_env gl) v) end + Ftactic.enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) v) end else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in - GTac.enter begin fun gl -> - GTac.return (pr_constr_under_binders_env (pf_env gl) c) + Ftactic.enter begin fun gl -> + Ftactic.return (pr_constr_under_binders_env (pf_env gl) c) end else if has_type v (topwit wit_unit) then - GTac.return (str "()") + Ftactic.return (str "()") else if has_type v (topwit wit_int) then - GTac.return (int (out_gen (topwit wit_int) v)) + Ftactic.return (int (out_gen (topwit wit_int) v)) else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in let print env c = pr_constr_env env (snd (c env Evd.empty)) in - GTac.enter begin fun gl -> - GTac.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) c) p) + Ftactic.enter begin fun gl -> + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) c) p) end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - GTac.enter begin fun gl -> GTac.return (pr_constr_env (pf_env gl) c) end + Ftactic.enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) c) end else match Value.to_list v with | Some l -> - GTacList.map message_of_value l >>= fun l -> - GTac.return (prlist_with_sep spc (fun x -> x) l) + Ftactic.List.map message_of_value l >>= fun l -> + Ftactic.return (prlist_with_sep spc (fun x -> x) l) | None -> - GTac.return (str "<abstr>") (** TODO *) + Ftactic.return (str "<abstr>") (** TODO *) let interp_message_token ist = function - | MsgString s -> GTac.return (str s) - | MsgInt n -> GTac.return (int n) + | MsgString s -> Ftactic.return (str s) + | MsgInt n -> Ftactic.return (int n) | MsgIdent (loc,id) -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with - | None -> Tacticals.New.tclZEROMSG (pr_id id ++ str" not found.") + | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (pr_id id ++ str" not found.")) | Some v -> message_of_value v let interp_message_nl ist l = - let open GTac in - GTacList.map (interp_message_token ist) l >>= function - | [] -> GTac.return (mt ()) - | l -> GTac.return (prlist_with_sep spc (fun x -> x) l ++ fnl ()) + let open Ftactic in + Ftactic.List.map (interp_message_token ist) l >>= function + | [] -> Ftactic.return (mt ()) + | l -> Ftactic.return (prlist_with_sep spc (fun x -> x) l ++ fnl ()) let interp_message ist l = - let open GTac in - GTacList.map (interp_message_token ist) l >>= fun l -> - GTac.return (prlist_with_sep spc (fun x -> x) l) + let open Ftactic in + Ftactic.List.map (interp_message_token ist) l >>= fun l -> + Ftactic.return (prlist_with_sep spc (fun x -> x) l) let rec interp_intro_pattern ist env sigma = function | loc, IntroAction pat -> @@ -1072,10 +1017,10 @@ let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c let pack_sigma (sigma,c) = {it=c;sigma=sigma;} (* Interprets an l-tac expression into a value *) -let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t = +let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Ftactic.t = let value_interp ist = match tac with | TacFun (it, body) -> - GTac.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, it, body))) + Ftactic.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, it, body))) | TacLetIn (true,l,u) -> interp_letrec ist l u | TacLetIn (false,l,u) -> interp_letin ist l u | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr @@ -1083,7 +1028,7 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t = | TacArg (loc,a) -> interp_tacarg ist a | t -> (** Delayed evaluation *) - GTac.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, [], t))) + Ftactic.return (of_tacvalue (VFun (extract_trace ist, ist.lfun, [], t))) in Control.check_for_interrupt (); match curr_debug ist with @@ -1092,7 +1037,7 @@ let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t = let ist = { ist with extra = TacStore.set ist.extra f_debug v } in value_interp ist in - debug_prompt lev tac eval + Ftactic.debug_prompt lev tac eval | _ -> value_interp ist @@ -1109,12 +1054,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let msg = interp_message_nl ist s in let tac l = Proofview.tclLIFT (Proofview.NonLogical.print (hov 0 l)) in Proofview.tclTHEN - (GTac.run msg tac) + (Ftactic.run msg tac) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> let msg = interp_message ist s in let tac l = Proofview.V82.tactic (fun gl -> tclFAIL (interp_int_or_var ist n) l gl) in - GTac.run msg tac + Ftactic.run msg tac | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin @@ -1166,45 +1111,42 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | ConstrWithBindingsArgType | BindingsArgType | OptArgType _ | PairArgType _ -> (** generic handler *) - GTac.enter begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let goal = Proofview.Goal.goal gl in let (sigma, arg) = interp_genarg ist env sigma concl goal x in - Proofview.V82.tclEVARS sigma <*> GTac.return arg + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return arg) end | _ as tag -> (** Special treatment. TODO: use generic handler *) - GTac.enter begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in match tag with | IntOrVarArgType -> - GTac.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) + Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> - GTac.return (value_of_ident (interp_fresh_ident ist env + Ftactic.return (value_of_ident (interp_fresh_ident ist env (out_gen (glbwit wit_ident) x))) | VarArgType -> - GTac.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x)) + Ftactic.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x)) | GenArgType -> f (out_gen (glbwit wit_genarg) x) | ConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl in - Proofview.V82.tclEVARS sigma <*> - GTac.return v + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) | OpenConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in - Proofview.V82.tclEVARS sigma <*> - GTac.return v + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) | ConstrMayEvalArgType -> let (sigma,c_interp) = interp_constr_may_eval ist env sigma (out_gen (glbwit wit_constr_may_eval) x) in - Proofview.V82.tclEVARS sigma <*> - GTac.return (Value.of_constr c_interp) + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) | ListArgType ConstrArgType -> let wit = glbwit (wit_list wit_constr) in let (sigma,l_interp) = Tacmach.New.of_old begin fun gl -> @@ -1213,62 +1155,60 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (out_gen wit x) (project gl) end gl in - Proofview.V82.tclEVARS sigma <*> - GTac.return (in_gen (topwit (wit_list wit_genarg)) l_interp) + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in - GTac.return ( + Ftactic.return ( let ans = List.map (mk_hyp_value ist env) (out_gen wit x) in in_gen (topwit (wit_list wit_genarg)) ans ) | ListArgType IntOrVarArgType -> let wit = glbwit (wit_list wit_int_or_var) in let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in - GTac.return (in_gen (topwit (wit_list wit_genarg)) ans) + Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType IdentArgType -> let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in let ans = List.map mk_ident (out_gen wit x) in - GTac.return (in_gen (topwit (wit_list wit_genarg)) ans) + Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) | ListArgType t -> - let open GTac in + let open Ftactic in let list_unpacker wit l = let map x = f (in_gen (glbwit wit) x) >>= fun v -> - GTac.return (out_gen (topwit wit) v) + Ftactic.return (out_gen (topwit wit) v) in - GTacList.map map (glb l) >>= fun l -> - GTac.return (in_gen (topwit (wit_list wit)) l) + Ftactic.List.map map (glb l) >>= fun l -> + Ftactic.return (in_gen (topwit (wit_list wit)) l) in list_unpack { list_unpacker } x | ExtraArgType _ -> - let (>>=) = GTac.bind in + let (>>=) = Ftactic.bind in (** Special treatment of tactics *) if has_type x (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) x in val_interp ist tac >>= fun v -> - GTac.return v + Ftactic.return v else let goal = Proofview.Goal.goal gl in let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in - Proofview.V82.tclEVARS newsigma <*> - GTac.return v + Ftactic.(lift (Proofview.V82.tclEVARS newsigma) <*> return v) | _ -> assert false end in - let (>>=) = GTac.bind in + let (>>=) = Ftactic.bind in let addvar (x, v) accu = f v >>= fun v -> - GTac.return (Id.Map.add x v accu) + Ftactic.return (Id.Map.add x v accu) in - let tac = GTacList.fold_right addvar l ist.lfun >>= fun lfun -> + let tac = Ftactic.List.fold_right addvar l ist.lfun >>= fun lfun -> let trace = push_trace (loc,LtacNotationCall s) ist in let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in val_interp ist body in - GTac.run tac (fun v -> tactic_of_value ist v) + Ftactic.run tac (fun v -> tactic_of_value ist v) | TacML (loc,opn,l) when List.for_all global_genarg l -> (* spiwack: a special case for tactics (from TACTIC EXTEND) when @@ -1298,25 +1238,25 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with tac args ist end -and force_vrec ist v : typed_generic_argument GTac.t = +and force_vrec ist v : typed_generic_argument Ftactic.t = let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body - | v -> GTac.return (of_tacvalue v) - else GTac.return v + | v -> Ftactic.return (of_tacvalue v) + else Ftactic.return v -and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument GTac.t = +and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic.t = match r with | ArgVar (loc,id) -> let v = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id in - GTac.bind (force_vrec ist v) begin fun v -> + Ftactic.bind (force_vrec ist v) begin fun v -> let v = propagate_trace ist loc id v in - if mustbetac then GTac.return (coerce_to_tactic loc id v) else GTac.return v + if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in @@ -1326,49 +1266,47 @@ and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument GTac.t = let ist = { lfun = Id.Map.empty; extra = extra; } in val_interp ist (Tacenv.interp_ltac r) -and interp_tacarg ist arg : typed_generic_argument GTac.t = +and interp_tacarg ist arg : typed_generic_argument Ftactic.t = match arg with | TacGeneric arg -> - GTac.enter begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let goal = Proofview.Goal.goal gl in let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in - Proofview.V82.tclEVARS sigma <*> - GTac.return v + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return v) end | Reference r -> interp_ltac_reference dloc false ist r | ConstrMayEval c -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in - Proofview.V82.tclEVARS sigma <*> - GTac.return (Value.of_constr c_interp) + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) end | UConstr c -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in - GTac.return (Value.of_uconstr (interp_uconstr ist env c)) + Ftactic.return (Value.of_uconstr (interp_uconstr ist env c)) end | MetaIdArg (loc,_,id) -> assert false | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist r | TacCall (loc,f,l) -> - let (>>=) = GTac.bind in + let (>>=) = Ftactic.bind in interp_ltac_reference loc true ist f >>= fun fv -> - GTacList.map (fun a -> interp_tacarg ist a) l >>= fun largs -> + Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacExternal (loc,com,req,la) -> - let (>>=) = GTac.bind in - GTacList.map (fun a -> interp_tacarg ist a) la >>= fun la_interp -> + let (>>=) = Ftactic.bind in + Ftactic.List.map (fun a -> interp_tacarg ist a) la >>= fun la_interp -> interp_external loc ist com req la_interp | TacFreshId l -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in - GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) + Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) end | TacPretype c -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let {closure;term} = interp_uconstr ist env c in @@ -1380,11 +1318,10 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = let (sigma,c_interp) = Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term in - Proofview.V82.tclEVARS sigma <*> - GTac.return (Value.of_constr c_interp) + Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp)) end | TacNumgoals -> - GTac.lift begin + Ftactic.lift begin let open Proofview.Notations in Proofview.numgoals >>= fun i -> Proofview.tclUNIT (Value.of_int i) @@ -1395,16 +1332,16 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = if String.equal tg "tactic" then val_interp ist (tactic_out t ist) else if String.equal tg "value" then - GTac.return (value_out t) + Ftactic.return (value_out t) else if String.equal tg "constr" then - GTac.return (Value.of_constr (constr_out t)) + Ftactic.return (Value.of_constr (constr_out t)) else Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">") (* Interprets an application node *) -and interp_app loc ist fv largs : typed_generic_argument GTac.t = - let (>>=) = GTac.bind in +and interp_app loc ist fv largs : typed_generic_argument Ftactic.t = + let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then @@ -1439,9 +1376,9 @@ and interp_app loc ist fv largs : typed_generic_argument GTac.t = (fun () -> str"evaluation returns"++fnl()++pr_value None v) end <*> - if List.is_empty lval then GTac.return v else interp_app loc ist v lval + if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else - GTac.return (of_tacvalue (VFun(trace,newlfun,lvar,body))) + Ftactic.return (of_tacvalue (VFun(trace,newlfun,lvar,body))) | _ -> fail else fail @@ -1463,7 +1400,7 @@ and tactic_of_value ist vle = else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic.")) and eval_value ist tac = - let (>>=) = GTac.bind in + let (>>=) = Ftactic.bind in val_interp ist tac >>= fun v -> if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (trace,lfun,[],t) -> @@ -1472,9 +1409,9 @@ and eval_value ist tac = extra = TacStore.set ist.extra f_trace trace; } in let tac = eval_tactic ist t in let dummy = VFun (extract_trace ist, Id.Map.empty, [], TacId []) in - catch_error_tac trace (tac <*> GTac.return (of_tacvalue dummy)) - | _ -> GTac.return v - else GTac.return v + catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) + | _ -> Ftactic.return v + else Ftactic.return v (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = @@ -1496,7 +1433,7 @@ and interp_letin ist llc u = let ist = { ist with lfun } in val_interp ist u | ((_, id), body) :: defs -> - GTac.bind (interp_tacarg ist body) (fun v -> + Ftactic.bind (interp_tacarg ist body) (fun v -> fold (Id.Map.add id v lfun) defs) in fold ist.lfun llc @@ -1535,7 +1472,7 @@ and interp_match_successes lz ist tac = (* Interprets the Match expressions *) and interp_match ist lz constr lmr = - let (>>=) = GTac.bind in + let (>>=) = Ftactic.bind in begin Proofview.tclORELSE (interp_ltac_constr ist constr) begin function @@ -1545,7 +1482,7 @@ and interp_match ist lz constr lmr = Proofview.tclZERO e end end >>= fun constr -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in @@ -1554,7 +1491,7 @@ and interp_match ist lz constr lmr = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - GTac.enter begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in @@ -1565,7 +1502,7 @@ and interp_match_goal ist lz lr lmr = end and interp_external loc ist com req la = - GTac.enter begin fun gl -> + Ftactic.enter begin fun gl -> let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in let g ch = internalise_tacarg ch in interp_tacarg ist (System.connect f g com) @@ -1689,13 +1626,13 @@ and interp_genarg_var_list ist env x = in_gen (topwit (wit_list wit_var)) lc (* Interprets tactic expressions : returns a "constr" *) -and interp_ltac_constr ist e : constr GTac.t = - let (>>=) = GTac.bind in +and interp_ltac_constr ist e : constr Ftactic.t = + let (>>=) = Ftactic.bind in begin Proofview.tclORELSE (val_interp ist e) begin function | Not_found -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in Proofview.tclLIFT begin debugging_step ist (fun () -> @@ -1707,7 +1644,7 @@ and interp_ltac_constr ist e : constr GTac.t = | e -> Proofview.tclZERO e end end >>= fun result -> - GTac.raw_enter begin fun gl -> + Ftactic.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in let result = Value.normalize result in try @@ -1718,7 +1655,7 @@ and interp_ltac_constr ist e : constr GTac.t = str " has value " ++ fnl() ++ pr_constr_env env cresult) end <*> - GTac.return cresult + Ftactic.return cresult with CannotCoerceTo _ -> let env = Proofview.Goal.env gl in Proofview.tclZERO (UserError ( "", @@ -1730,7 +1667,7 @@ and interp_ltac_constr ist e : constr GTac.t = (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac : unit Proofview.tactic = - GTac.run (val_interp ist tac) (fun v -> tactic_of_value ist v) + Ftactic.run (val_interp ist tac) (fun v -> tactic_of_value ist v) (* Interprets a primitive tactic *) and interp_atomic ist tac : unit Proofview.tactic = @@ -2167,9 +2104,9 @@ let () = (***************************************************************************) (* Other entry points *) -let val_interp ist tac k = GTac.run (val_interp ist tac) k +let val_interp ist tac k = Ftactic.run (val_interp ist tac) k -let interp_ltac_constr ist c k = GTac.run (interp_ltac_constr ist c) k +let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k let interp_redexp env sigma r = let ist = default_ist () in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index d2f02d77f..69836a654 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Ftactic Geninterp Dnet Dn |