diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 940 |
1 files changed, 412 insertions, 528 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 54adbd937..1112da4a0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -40,29 +40,49 @@ open Misctypes open Locus open Tacintern open Taccoerce +open Sigma.Notations open Proofview.Notations +let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> + let Val.Dyn (t, _) = v in + match Val.eq t (val_tag wit) with + | None -> false + | Some Refl -> true + +let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> None + | Some Refl -> Some x + +let in_gen wit v = Val.Dyn (val_tag wit, v) +let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x + +let val_tag wit = val_tag (topwit wit) + +let pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Val.repr tag + let safe_msgnl s = Proofview.NonLogical.catch (Proofview.NonLogical.print_debug (s++fnl())) (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) -type value = tlevel generic_argument +type value = Val.t (** Abstract application, to print ltac functions *) type appl = | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.kernel_name * typed_generic_argument list) list + | GlbAppl of (Names.kernel_name * Val.t list) list (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) -let pr_generic arg = - let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in - try - Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg - with e when Errors.noncritical e -> str"<generic>" +let pr_generic arg = (** FIXME *) + let Val.Dyn (tag, _) = arg in + str"<" ++ Val.repr tag ++ str ">" let pr_appl h vs = Pptactic.pr_ltac_constant h ++ spc () ++ Pp.prlist_with_sep spc pr_generic vs @@ -85,7 +105,7 @@ type tacvalue = Id.t option list * glob_tactic_expr | VRec of value Id.Map.t ref * glob_tactic_expr -let (wit_tacvalue : (Empty.t, Empty.t, tacvalue) Genarg.genarg_type) = +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = Genarg.create_arg None "tacvalue" let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -124,8 +144,59 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure + let cast_error wit v = + let pr_v = mt () in (** FIXME *) + let Val.Dyn (tag, _) = v in + let tag = Val.repr tag in + errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag + ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.") + + let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> None + | Some Refl -> Some x + + let try_prj wit v = match prj (val_tag wit) v with + | None -> cast_error wit v + | Some x -> x + + let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c = + fun wit v -> match wit with + | ExtraArg _ -> try_prj wit v + | ListArg t -> + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.List tag -> + let map x = val_cast t (Val.Dyn (tag, x)) in + List.map map v + | _ -> cast_error wit (Val.Dyn (tag, v)) + end + | OptArg t -> + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.Opt tag -> + let map x = val_cast t (Val.Dyn (tag, x)) in + Option.map map v + | _ -> cast_error wit (Val.Dyn (tag, v)) + end + | PairArg (t1, t2) -> + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.Pair (tag1, tag2) -> + let (v1, v2) = v in + let v1 = Val.Dyn (tag1, v1) in + let v2 = Val.Dyn (tag2, v2) in + (val_cast t1 v1, val_cast t2 v2) + | _ -> cast_error wit (Val.Dyn (tag, v)) + end + + let cast (Topwit wit) v = val_cast wit v + end +let print_top_val env v = mt () (** FIXME *) + let dloc = Loc.ghost let catching_error call_trace fail (e, info) = @@ -177,13 +248,13 @@ let pr_value env v = | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c | _ -> str "a term" else - str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v) + str "a value of type" ++ spc () ++ pr_argument_type v let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in let pr_iarg (id, arg) = - let arg = pr_argument_type (genarg_tag arg) in + let arg = pr_argument_type arg in hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg) in let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in @@ -200,7 +271,7 @@ let pr_inspect env expr result = | VRec (ist, body) -> str "a recursive closure" ++ fnl () ++ pr_closure env !ist body else - let pp_type = pr_argument_type (genarg_tag result) in + let pp_type = pr_argument_type result in str "an object of type" ++ spc () ++ pp_type in pp_expr ++ fnl() ++ str "this is " ++ pp_result @@ -209,17 +280,6 @@ let pr_inspect env expr result = let constr_of_id env id = Term.mkVar (let _ = Environ.lookup_named id env in id) -(* To embed tactics *) - -let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), - (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = - Dyn.create "tactic" - -let ((value_in : value -> Dyn.t), - (value_out : Dyn.t -> value)) = Dyn.create "value" - -let valueIn t = TacDynamic (Loc.ghost, value_in t) - (** Generic arguments : table of interpretation functions *) let push_trace call ist = match TacStore.get ist.extra f_trace with @@ -260,9 +320,9 @@ let coerce_to_tactic loc id v = | _ -> fail () else fail () +let intro_pattern_of_ident id = (Loc.ghost, IntroNaming (IntroIdentifier id)) let value_of_ident id = - in_gen (topwit wit_intro_pattern) - (Loc.ghost, IntroNaming (IntroIdentifier id)) + in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id) let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 @@ -337,10 +397,6 @@ let interp_intro_pattern_naming_var loc ist env sigma id = try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id) with Not_found -> IntroIdentifier id -let interp_hint_base ist s = - try try_interp_ltac_var coerce_to_hint_base ist None (dloc,Id.of_string s) - with Not_found -> s - let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> @@ -455,7 +511,9 @@ let extract_ltac_constr_values ist env = (* Extract the identifier list from lfun: join all branches (what to do else?)*) let rec intropattern_ids (loc,pat) = match pat with | IntroNaming (IntroIdentifier id) -> [id] - | IntroAction (IntroOrAndPattern ll) -> + | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> + List.flatten (List.map intropattern_ids l) + | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) -> List.flatten (List.map intropattern_ids (List.flatten ll)) | IntroAction (IntroInjection l) -> List.flatten (List.map intropattern_ids l) @@ -633,10 +691,10 @@ let pf_interp_constr ist gl = let new_interp_constr ist c k = let open Proofview in - Proofview.Goal.enter begin fun gl -> - let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c) - end + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let (sigma, c) = interp_constr ist (Goal.env gl) (Tacmach.New.project gl) c in + Sigma.Unsafe.of_pair (k c, sigma) + end } let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = @@ -659,14 +717,28 @@ let interp_constr_list ist env sigma c = let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr -let interp_auto_lemmas ist env sigma lems = - let local_sigma, lems = interp_open_constr_list ist env sigma lems in - List.map (fun lem -> (local_sigma,lem)) lems - (* Interprets a type expression *) let pf_interp_type ist gl = interp_type ist (pf_env gl) (project gl) +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = constr_flags) + ?(expected_type = WithoutTypeConstraint) ist c = + { delayed = begin fun env sigma -> + let open Pretyping in + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = ist.lfun; + } in + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_ltac flags env sigma vars expected_type term in + Sigma.Unsafe.of_pair (c, sigma) + end } + + (* Interprets a reduction expression *) let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid) @@ -791,37 +863,37 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end + Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project 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 - Ftactic.nf_enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c) - end + Ftactic.nf_enter { enter = begin fun gl -> + Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Tacmach.New.project gl) c) + end } else if has_type v (topwit wit_unit) then Ftactic.return (str "()") else if has_type v (topwit wit_int) then 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 sigma c = pr_constr_env env sigma (snd (c env Evd.empty)) in - Ftactic.nf_enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p) - end + let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in + Ftactic.nf_enter { enter = begin fun gl -> + Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Tacmach.New.project gl) c) p) + end } else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end + Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) c) end } else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in - Ftactic.nf_enter begin fun gl -> + Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_closed_glob_env (pf_env gl) - (Proofview.Goal.sigma gl) c) - end + (Tacmach.New.project gl) c) + end } else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> Ftactic.return (prlist_with_sep spc (fun x -> x) l) | None -> - let tag = pr_argument_type (genarg_tag v) in + let tag = pr_argument_type v in Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) let interp_message_token ist = function @@ -838,11 +910,6 @@ let interp_message ist l = Ftactic.List.map (interp_message_token ist) l >>= fun l -> Ftactic.return (prlist_with_sep spc (fun x -> x) l) -let interp_message ist 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 -> let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in @@ -866,13 +933,22 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn (c,ipat) -> - let c = fun env sigma -> interp_open_constr ist env sigma c in + let c = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn (c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x -and interp_or_and_intro_pattern ist env sigma = - List.fold_map (interp_intro_pattern_list_as_list ist env) sigma +and interp_or_and_intro_pattern ist env sigma = function + | IntroAndPattern l -> + let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in + sigma, IntroAndPattern l + | IntroOrPattern ll -> + let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in + sigma, IntroOrPattern ll and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> @@ -947,19 +1023,11 @@ let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, c = interp_open_constr ist env sigma c in sigma, (c,bl) -let interp_constr_with_bindings_arg ist env sigma (keep,c) = - let sigma, c = interp_constr_with_bindings ist env sigma c in - sigma, (keep,c) - let interp_open_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in let sigma, c = interp_open_constr ist env sigma c in sigma, (c, bl) -let interp_open_constr_with_bindings_arg ist env sigma (keep,c) = - let sigma, c = interp_open_constr_with_bindings ist env sigma c in - sigma,(keep,c) - let loc_of_bindings = function | NoBindings -> Loc.ghost | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) @@ -969,13 +1037,21 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in - let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in + Sigma.Unsafe.of_pair (c, sigma) + } in (loc,f) let interp_induction_arg ist gl arg = match arg with | keep,ElimOnConstr c -> - keep,ElimOnConstr (fun env sigma -> interp_constr_with_bindings ist env sigma c) + keep,ElimOnConstr { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr_with_bindings ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err_loc (loc, "", @@ -985,11 +1061,13 @@ let interp_induction_arg ist gl arg = let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') - else keep, ElimOnConstr (fun env sigma -> - try sigma, (constr_of_id env id', NoBindings) + else + (keep, ElimOnConstr { delayed = begin fun env sigma -> + try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> user_err_loc (loc, "interp_induction_arg", - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")) + pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") + end }) in try (** FIXME: should be moved to taccoerce *) @@ -1007,16 +1085,18 @@ let interp_induction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr (fun env sigma -> sigma,(c,NoBindings)) + | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in - let f env sigma = + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in - sigma,(c,NoBindings) in + Sigma.Unsafe.of_pair ((c,NoBindings), sigma) + } in keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and @@ -1081,20 +1161,17 @@ let rec read_match_rule lfun ist env sigma = function (* misc *) -let mk_constr_value ist gl c = - let (sigma,c_interp) = pf_interp_constr ist gl c in - sigma, Value.of_constr c_interp -let mk_open_constr_value ist gl c = - let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in - sigma, Value.of_constr c_interp -let mk_hyp_value ist env sigma c = - Value.of_constr (mkVar (interp_hyp ist env sigma c)) -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;} +let interp_focussed wit f v = + Ftactic.nf_enter { enter = begin fun gl -> + let v = Genarg.out_gen (glbwit wit) v in + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let v = in_gen (topwit wit) (f env sigma v) in + Ftactic.return v + end } (* Interprets an l-tac expression into a value *) -let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : typed_generic_argument Ftactic.t = +let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t = (* The name [appl] of applied top-level Ltac names is ignored in [value_interp]. It is installed in the second step by a call to [name_vfun], because it gives more opportunities to detect a @@ -1159,9 +1236,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end | TacAbstract (tac,ido) -> - Proofview.Goal.nf_enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT (Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac) - end + end } | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1204,102 +1281,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac (* For extensions *) | TacAlias (loc,s,l) -> - let body = Tacenv.interp_alias s in - let rec f x = match genarg_tag x with - | QuantHypArgType | RedExprArgType - | ConstrWithBindingsArgType - | BindingsArgType - | OptArgType _ | PairArgType _ -> (** generic handler *) - Ftactic.nf_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 - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return arg) - end - | _ as tag -> (** Special treatment. TODO: use generic handler *) - Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - match tag with - | IntOrVarArgType -> - Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) - | IdentArgType -> - Ftactic.return (value_of_ident (interp_ident ist env sigma - (out_gen (glbwit wit_ident) x))) - | VarArgType -> - Ftactic.return (mk_hyp_value ist env sigma (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 - Ftactic.(lift (Proofview.Unsafe.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 - Ftactic.(lift (Proofview.Unsafe.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 - Ftactic.(lift (Proofview.Unsafe.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 -> - Evd.MonadR.List.map_right - (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c) - (out_gen wit x) - (project gl) - end gl in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (in_gen (topwit (wit_list wit_genarg)) l_interp)) - | ListArgType VarArgType -> - let wit = glbwit (wit_list wit_var) in - Ftactic.return ( - let ans = List.map (mk_hyp_value ist env sigma) (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 - 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_ident ist env sigma x) in - let ans = List.map mk_ident (out_gen wit x) in - Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) - | ListArgType t -> - let open Ftactic in - let list_unpacker wit l = - let map x = - f (in_gen (glbwit wit) x) >>= fun v -> - Ftactic.return (out_gen (topwit wit) v) - in - Ftactic.List.map map (glb l) >>= fun l -> - Ftactic.return (in_gen (topwit (wit_list wit)) l) - in - list_unpack { list_unpacker } x - | ExtraArgType _ -> - (** 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 - else - let goal = Proofview.Goal.goal gl in - let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in - Ftactic.(lift (Proofview.Unsafe.tclEVARS newsigma) <*> return v) - | _ -> assert false - end - in + let (ids, body) = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in - let interp_vars = - Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l - in - let addvar (x, v) accu = Id.Map.add x v accu in + let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = - let lfun = List.fold_right addvar l ist.lfun in + let addvar x v accu = Id.Map.add x v accu in + let lfun = List.fold_right2 addvar ids l ist.lfun in let trace = push_trace (loc,LtacNotationCall s) ist in let ist = { lfun = lfun; @@ -1308,52 +1295,35 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.lift (tactic_of_value ist v) in let tac = - Ftactic.with_env interp_vars >>= fun (env,l) -> - let name () = Pptactic.pr_tactic env (TacAlias(loc,s,l)) in - Proofview.Trace.name_tactic name (tac l) + Ftactic.with_env interp_vars >>= fun (env, lr) -> + let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in + Proofview.Trace.name_tactic name (tac lr) (* spiwack: this use of name_tactic is not robust to a change of implementation of [Ftactic]. In such a situation, some more elaborate solution will have to be used. *) in + let tac = + let len1 = List.length ids in + let len2 = List.length l in + if len1 = len2 then tac + else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ + expected " ++ int len1 ++ str ", found " ++ int len2) + in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) - | TacML (loc,opn,l) when List.for_all global_genarg l -> - let trace = push_trace (loc,LtacMLCall tac) ist in - let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in - (* spiwack: a special case for tactics (from TACTIC EXTEND) when - every argument can be interpreted without a - [Proofview.Goal.nf_enter]. *) - let tac = Tacenv.interp_ml_tactic opn in - (* dummy values, will be ignored *) - let env = Environ.empty_env in - let sigma = Evd.empty in - let concl = Term.mkRel (-1) in - let goal = Evar.unsafe_of_int (-1) in - (* /dummy values *) - let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in - let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in - Proofview.Trace.name_tactic name - (catch_error_tac trace (tac args ist)) | TacML (loc,opn,l) -> + let open Ftactic.Notations in let trace = push_trace (loc,LtacMLCall tac) ist in let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let goal_sigma = Proofview.Goal.sigma gl in - let concl = Proofview.Goal.concl gl in - let goal = Proofview.Goal.goal gl in - let tac = Tacenv.interp_ml_tactic opn in - let (sigma,args) = - Evd.MonadR.List.map_right - (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma - in - Proofview.Unsafe.tclEVARS sigma <*> - let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in - Proofview.Trace.name_tactic name - (catch_error_tac trace (tac args ist)) - end + let tac = Tacenv.interp_ml_tactic opn in + let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in + let tac args = + let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in + Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) + in + Ftactic.run args tac -and force_vrec ist v : typed_generic_argument Ftactic.t = +and force_vrec ist v : Val.t Ftactic.t = let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in @@ -1362,7 +1332,7 @@ and force_vrec ist v : typed_generic_argument Ftactic.t = | v -> Ftactic.return (of_tacvalue v) else Ftactic.return v -and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic.t = +and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = match r with | ArgVar (loc,id) -> let v = @@ -1382,28 +1352,22 @@ and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic. let appl = GlbAppl[r,[]] in val_interp ~appl ist (Tacenv.interp_ltac r) -and interp_tacarg ist arg : typed_generic_argument Ftactic.t = +and interp_tacarg ist arg : Val.t Ftactic.t = match arg with - | TacGeneric arg -> - Ftactic.nf_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 - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) - end + | TacGeneric arg -> interp_genarg ist arg | Reference r -> interp_ltac_reference dloc false ist r | ConstrMayEval c -> - Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Ftactic.s_enter { s_enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) - end + Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) + end } | UConstr c -> - Ftactic.enter begin fun gl -> + Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in Ftactic.return (Value.of_uconstr (interp_uconstr ist env c)) - end + end } | MetaIdArg (loc,_,id) -> assert false | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist r @@ -1413,26 +1377,18 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacFreshId l -> - Ftactic.enter begin fun gl -> - let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in + Ftactic.enter { enter = begin fun gl -> + let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Tacmach.New.project gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id))) - end + end } | TacPretype c -> - Ftactic.enter begin fun gl -> + Ftactic.s_enter { s_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 - let vars = { - Pretyping.ltac_constrs = closure.typed; - Pretyping.ltac_uconstrs = closure.untyped; - Pretyping.ltac_idents = closure.idents; - Pretyping.ltac_genargs = ist.lfun; - } in - let (sigma,c_interp) = - Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term - in - Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) - end + let c = interp_uconstr ist env c in + let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in + Sigma (Ftactic.return (Value.of_constr c), sigma, p) + end } | TacNumgoals -> Ftactic.lift begin let open Proofview.Notations in @@ -1440,20 +1396,9 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = Proofview.tclUNIT (Value.of_int i) end | Tacexp t -> val_interp ist t - | TacDynamic(_,t) -> - let tg = (Dyn.tag t) in - if String.equal tg "tactic" then - val_interp ist (tactic_out t ist) - else if String.equal tg "value" then - Ftactic.return (value_out t) - else if String.equal tg "constr" then - 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 Ftactic.t = +and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in let fv = Value.normalize fv in @@ -1597,141 +1542,84 @@ and interp_match ist lz constr lmr = Proofview.tclZERO ~info e end end >>= fun constr -> - Ftactic.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Ftactic.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project 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 interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) - end + end } (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Ftactic.nf_enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Ftactic.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in let hyps = if lr then List.rev hyps else hyps in let concl = Proofview.Goal.concl gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) - end + end } (* Interprets extended tactic generic arguments *) -(* spiwack: interp_genarg has an argument [concl] for the case of - "casted open constr". And [gl] for [Geninterp]. I haven't changed - the interface for geninterp yet as it is used by ARGUMENT EXTEND - (in turn used by plugins). At the time I'm writing this comment - though, the only concerned plugins are the declarative mode (which - needs the [extra] field of goals to interprete rules) and ssreflect - (a handful of time). I believe we'd need to address "casted open - constr" and the declarative mode rules to provide a reasonable - interface. *) -and interp_genarg ist env sigma concl gl x = - let evdref = ref sigma in - let rec interp_genarg x = - match genarg_tag x with - | IntOrVarArgType -> - in_gen (topwit wit_int_or_var) - (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) - | IdentArgType -> - in_gen (topwit wit_ident) - (interp_ident ist env sigma (out_gen (glbwit wit_ident) x)) - | VarArgType -> - in_gen (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x)) - | GenArgType -> - in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x)) - | ConstrArgType -> - let (sigma,c_interp) = - interp_constr ist env !evdref (out_gen (glbwit wit_constr) x) - in - evdref := sigma; - in_gen (topwit wit_constr) c_interp - | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (out_gen (glbwit wit_constr_may_eval) x) in - evdref := sigma; - in_gen (topwit wit_constr_may_eval) c_interp - | QuantHypArgType -> - in_gen (topwit wit_quant_hyp) - (interp_declared_or_quantified_hypothesis ist env sigma - (out_gen (glbwit wit_quant_hyp) x)) - | RedExprArgType -> - let (sigma,r_interp) = - interp_red_expr ist env !evdref (out_gen (glbwit wit_red_expr) x) - in - evdref := sigma; - in_gen (topwit wit_red_expr) r_interp - | OpenConstrArgType -> - let expected_type = WithoutTypeConstraint in - in_gen (topwit wit_open_constr) - (interp_open_constr ~expected_type - ist env !evdref - (snd (out_gen (glbwit wit_open_constr) x))) - | ConstrWithBindingsArgType -> - in_gen (topwit wit_constr_with_bindings) - (pack_sigma (interp_constr_with_bindings ist env !evdref - (out_gen (glbwit wit_constr_with_bindings) x))) - | BindingsArgType -> - in_gen (topwit wit_bindings) - (pack_sigma (interp_bindings ist env !evdref (out_gen (glbwit wit_bindings) x))) - | ListArgType ConstrArgType -> - let (sigma,v) = interp_genarg_constr_list ist env !evdref x in - evdref := sigma; - v - | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x - | ListArgType _ -> - let list_unpacker wit l = - let map x = - out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) - in - in_gen (topwit (wit_list wit)) (List.map map (glb l)) +and interp_genarg ist x : Val.t Ftactic.t = + let open Ftactic.Notations in + (** Ad-hoc handling of some types. *) + let tag = genarg_tag x in + if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then + interp_genarg_var_list ist x + else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then + interp_genarg_constr_list ist x + else + let GenArg (Glbwit wit, x) = x in + match wit with + | ListArg wit -> + let map x = + interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> + Ftactic.return (Value.cast (topwit wit) x) in - list_unpack { list_unpacker } x - | OptArgType _ -> - let opt_unpacker wit o = match glb o with - | None -> in_gen (topwit (wit_opt wit)) None + Ftactic.List.map map x >>= fun l -> + Ftactic.return (Value.of_list (val_tag wit) l) + | OptArg wit -> + let ans = match x with + | None -> Ftactic.return (Value.of_option (val_tag wit) None) | Some x -> - let x = out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) in - in_gen (topwit (wit_opt wit)) (Some x) + interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> + let x = Value.cast (topwit wit) x in + Ftactic.return (Value.of_option (val_tag wit) (Some x)) in - opt_unpack { opt_unpacker } x - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let (p, q) = glb o in - let p = out_gen (topwit wit1) (interp_genarg (in_gen (glbwit wit1) p)) in - let q = out_gen (topwit wit2) (interp_genarg (in_gen (glbwit wit2) q)) in - in_gen (topwit (wit_pair wit1 wit2)) (p, q) - in - pair_unpack { pair_unpacker } x - | ExtraArgType s -> - let (sigma,v) = Geninterp.generic_interp ist { Evd.it=gl;sigma=(!evdref) } x in - evdref:=sigma; - v - in - let v = interp_genarg x in - !evdref , v - + ans + | PairArg (wit1, wit2) -> + let (p, q) = x in + interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p -> + interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q -> + let p = Value.cast (topwit wit1) p in + let q = Value.cast (topwit wit2) q in + Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q))) + | ExtraArg s -> + Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x) (** returns [true] for genargs which have the same meaning independently of goals. *) -and global_genarg = - let rec global_tag = function - | IntOrVarArgType | GenArgType -> true - | ListArgType t | OptArgType t -> global_tag t - | PairArgType (t1,t2) -> global_tag t1 && global_tag t2 - | _ -> false - in - fun x -> global_tag (genarg_tag x) - -and interp_genarg_constr_list ist env sigma x = - let lc = out_gen (glbwit (wit_list wit_constr)) x in +and interp_genarg_constr_list ist x = + Ftactic.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in - sigma , in_gen (topwit (wit_list wit_constr)) lc + let lc = Value.of_list (val_tag wit_constr) lc in + Sigma.Unsafe.of_pair (Ftactic.return lc, sigma) + end } -and interp_genarg_var_list ist env sigma x = - let lc = out_gen (glbwit (wit_list wit_var)) x in +and interp_genarg_var_list ist x = + Ftactic.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in - in_gen (topwit (wit_list wit_var)) lc + Ftactic.return (Value.of_list (val_tag wit_var) lc) + end } (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : constr Ftactic.t = @@ -1740,7 +1628,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = (val_interp ist e) begin function (err, info) -> match err with | Not_found -> - Ftactic.enter begin fun gl -> + Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in Proofview.tclLIFT begin debugging_step ist (fun () -> @@ -1748,13 +1636,13 @@ and interp_ltac_constr ist e : constr Ftactic.t = Pptactic.pr_glob_tactic env e) end <*> Proofview.tclZERO Not_found - end + end } | err -> Proofview.tclZERO ~info err end end >>= fun result -> - Ftactic.enter begin fun gl -> + Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in @@ -1769,7 +1657,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = let env = Proofview.Goal.env gl in Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ str "offending expression: " ++ fnl() ++ pr_inspect env e result) - end + end } (* Interprets tactic expressions : returns a "tactic" *) @@ -1790,27 +1678,27 @@ and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) - (Tactics.intros_patterns l')) sigma - end + (Tactics.intro_patterns l')) sigma + end } | TacIntroMove (ido,hto) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let mloc = interp_move_location ist env sigma hto in let ido = Option.map (interp_ident ist env sigma) ido in name_atomic ~env (TacIntroMove(ido,mloc)) (Tactics.intro_move ido mloc) - end + end } | TacExact c -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin @@ -1825,9 +1713,9 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in (k,(loc,f))) cb @@ -1838,12 +1726,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in sigma, Tactics.apply_delayed_in a ev id l cl in Tacticals.New.tclWITHHOLES ev tac sigma - end + end } end | TacElim (ev,(keep,cb),cbo) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1851,10 +1739,10 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacCase (ev,(keep,cb)) -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let named_tac = @@ -1862,16 +1750,16 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacCase(ev,(keep,cb))) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } | TacFix (idopt,n) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacFix(idopt,n)) (Proofview.V82.tactic (Tactics.fix idopt n)) - end + end } | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin @@ -1890,14 +1778,14 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacCofix idopt -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let idopt = Option.map (interp_ident ist env sigma) idopt in name_atomic ~env (TacCofix (idopt)) (Proofview.V82.tactic (Tactics.cofix idopt)) - end + end } | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin @@ -1916,9 +1804,9 @@ and interp_atomic ist tac : unit Proofview.tactic = end end | TacAssert (b,t,ipat,c) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in @@ -1928,17 +1816,17 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacAssert(b,t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma - end + end } | TacGeneralize cl -> - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma - end + (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma + end } | TacGeneralizeDep c -> (new_interp_constr ist c) (fun c -> name_atomic (* spiwack: probably needs a goal environment *) @@ -1947,9 +1835,9 @@ and interp_atomic ist tac : unit Proofview.tactic = ) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in if Locusops.is_nowhere clp then @@ -1980,58 +1868,22 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) ((sigma,sigma'),c) clp eqpat) sigma') - end - - (* Automation tactics *) - | TacTrivial (debug,lems,l) -> - begin if debug == Tacexpr.Info then - msg_warning - (strbrk"The \"info_trivial\" tactic" ++ spc () - ++strbrk"does not print traces anymore." ++ spc() - ++strbrk"Use \"Info 1 trivial\", instead.") - end; - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let lems = interp_auto_lemmas ist env sigma lems in - name_atomic ~env - (TacTrivial(debug,List.map snd lems,l)) - (Auto.h_trivial ~debug - lems - (Option.map (List.map (interp_hint_base ist)) l)) - end - | TacAuto (debug,n,lems,l) -> - begin if debug == Tacexpr.Info then - msg_warning - (strbrk"The \"info_auto\" tactic" ++ spc () - ++strbrk"does not print traces anymore." ++ spc() - ++strbrk"Use \"Info 1 auto\", instead.") - end; - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let lems = interp_auto_lemmas ist env sigma lems in - name_atomic ~env - (TacAuto(debug,n,List.map snd lems,l)) - (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) - lems - (Option.map (List.map (interp_hint_base ist)) l)) - end + end } (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) Proofview.V82.nf_evar_goals <*> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma,l = List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) (* spiwack: the [*p] variants are for printing *) let cp = c in - let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in + let c = interp_induction_arg ist gl c in let ipato = interp_intro_pattern_naming_option ist env sigma ipato in let ipatsp = ipats in let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in @@ -2042,12 +1894,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let l,lp = List.split l in let sigma,el = Option.fold_map (interp_constr_with_bindings ist env) sigma el in - name_atomic ~env + let tac = name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) - (Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) - (Tactics.induction_destruct isrec ev (l,el))) - end + (Tactics.induction_destruct isrec ev (l,el)) + in + Sigma.Unsafe.of_pair (tac, sigma) + end } | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2056,25 +1908,25 @@ and interp_atomic ist tac : unit Proofview.tactic = (Elim.h_double_induction h1 h2) (* Context management *) | TacClear (b,l) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) else (* spiwack: until the tactic is in the monad *) let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac - end + end } | TacClearBody l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = interp_hyp_list ist env sigma l in name_atomic ~env (TacClearBody l) (Tactics.clear_body l) - end + end } | TacMove (id1,id2) -> Proofview.V82.tactic begin fun gl -> Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) @@ -2082,9 +1934,9 @@ and interp_atomic ist tac : unit Proofview.tactic = gl end | TacRename l -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let l = List.map (fun (id1,id2) -> interp_hyp ist env sigma id1, @@ -2093,20 +1945,20 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacRename l) (Tactics.rename_hyp l) - end + end } (* Constructors *) | TacSplit (ev,bll) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in let named_tac = let tac = Tactics.split_with_bindings ev bll in name_atomic ~env (TacSplit (ev, bll)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end + end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) @@ -2132,16 +1984,20 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in + let sigma = Sigma.to_evar_map sigma in let ist = { ist with lfun = lfun' } in - if is_onhyps && is_onconcl - then interp_type ist (pf_env gl) sigma c - else interp_constr ist (pf_env gl) sigma c - in + let (sigma, c) = + if is_onhyps && is_onconcl + then interp_type ist (pf_env gl) sigma c + else interp_constr ist (pf_env gl) sigma c + in + Sigma.Unsafe.of_pair (c, sigma) + end } in (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) gl end @@ -2150,47 +2006,54 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin Proofview.V82.nf_evar_goals <*> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in Proofview.V82.tactic begin fun gl -> let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let c_interp patvars sigma = + let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in - try interp_constr ist env sigma c + try + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - in + end } in (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) gl end - end + end } end (* Equivalence relations *) | TacSymmetry c -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma c in name_atomic ~env (TacSymmetry cl) (Tactics.intros_symmetry cl) - end + end } (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let l' = List.map (fun (b,m,(keep,c)) -> - let f env sigma = interp_open_constr_with_bindings ist env sigma c in + let f = { delayed = fun env sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + } in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let cl = interp_clause ist env sigma cl in name_atomic ~env (TacRewrite (ev,l,cl,by)) @@ -2198,11 +2061,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)) - end + end } | TacInversion (DepInversion (k,c,ids),hyp) -> - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c_interp) = match c with | None -> sigma , None @@ -2218,11 +2081,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) (Inv.dinv k c_interp ids_interp dqhyps)) sigma - end + end } | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let hyps = interp_hyp_list ist env sigma idl in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in @@ -2230,19 +2093,20 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) (Inv.inv_clause k ids_interp hyps dqhyps)) sigma - end + end } | TacInversion (InversionUsing (c,idl),hyp) -> - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let (sigma,c_interp) = interp_constr ist env sigma c in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in - Proofview.Unsafe.tclEVARS sigma <*> - name_atomic ~env + let tac = name_atomic ~env (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) (Leminv.lemInv_clause dqhyps c_interp hyps) - end + in + Sigma.Unsafe.of_pair (tac, sigma) + end } (* Initial call for interpretation *) @@ -2263,7 +2127,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in @@ -2272,7 +2136,7 @@ let interp_tac_gen lfun avoid_ids debug t = interp_tactic ist (intern_pure_tactic { ltacvars; genv = env } t) - end + end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t let _ = Proof_global.set_interp_tac interp @@ -2292,16 +2156,16 @@ let hide_interp global t ot = Proofview.tclENV >>= fun env -> hide_interp env else - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> hide_interp (Proofview.Goal.env gl) - end + end } (***************************************************************************) (** Register standard arguments *) let def_intern ist x = (ist, x) let def_subst _ x = x -let def_interp ist gl x = (project gl, x) +let def_interp ist x = Ftactic.return x let declare_uniform t = Genintern.register_intern0 t def_intern; @@ -2323,27 +2187,58 @@ let () = let () = declare_uniform wit_pre_ident +let lift f = (); fun ist x -> Ftactic.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + Ftactic.return (f ist env sigma x) +end } + +let lifts f = (); fun ist x -> Ftactic.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let (sigma, v) = f ist env sigma x in + Sigma.Unsafe.of_pair (Ftactic.return v, sigma) +end } + +let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma -> + let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in + Sigma.Unsafe.of_pair (bl, sigma) + } + +let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> + let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in + Sigma.Unsafe.of_pair (c, sigma) + } + let () = - let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) (project gl) ref) in - Geninterp.register_interp0 wit_ref interp; - let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in - Geninterp.register_interp0 wit_intro_pattern interp; - let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) (project gl) pat) in - Geninterp.register_interp0 wit_clause_dft_concl interp; - let interp ist gl s = interp_sort (project gl) s in - Geninterp.register_interp0 wit_sort interp + Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + Geninterp.register_interp0 wit_ref (lift interp_reference); + Geninterp.register_interp0 wit_ident (lift interp_ident); + Geninterp.register_interp0 wit_var (lift interp_hyp); + Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern); + Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause); + Geninterp.register_interp0 wit_constr (lifts interp_constr); + Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); + Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); + Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr); + Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); + Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr); + Geninterp.register_interp0 wit_bindings interp_bindings'; + Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval); + () let () = - let interp ist gl tac = + let interp ist tac = let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in - (project gl, TacArg (dloc, valueIn (of_tacvalue f))) + Ftactic.return (TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f))) in Geninterp.register_interp0 wit_tactic interp let () = - Geninterp.register_interp0 wit_uconstr (fun ist gl c -> - project gl , interp_uconstr ist (pf_env gl) c - ) + Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl -> + Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c) + end }) (***************************************************************************) (* Other entry points *) @@ -2358,24 +2253,13 @@ let interp_redexp env sigma r = interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) -(* Embed tactics in raw or glob tactic expr *) - -let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) -let tacticIn t = - globTacticIn (fun ist -> - try glob_tactic (t ist) - with e when Errors.noncritical e -> anomaly ~label:"tacticIn" - (str "Incorrect tactic expression. Received exception is:" ++ - Errors.print e)) - -(***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = let eval ty env sigma lfun arg = let ist = { lfun = lfun; extra = TacStore.empty; } in - if has_type arg (glbwit wit_tactic) then - let tac = out_gen (glbwit wit_tactic) arg in + if Genarg.has_type arg (glbwit wit_tactic) then + let tac = Genarg.out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in Pfedit.refine_by_tactic env sigma ty tac else @@ -2394,9 +2278,9 @@ let _ = Hook.set Auto.extern_interp let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> + let tac _ ist = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let map = function | None -> None | Some id -> @@ -2407,5 +2291,5 @@ let lift_constr_tac_to_ml_tac vars tac = in let args = List.map_filter map vars in tac args ist - end in + end } in tac |