diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 1363 |
1 files changed, 796 insertions, 567 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0e0ccac2e..04624e1a1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -43,6 +43,7 @@ open Miscops open Locus open Tacintern open Taccoerce +open Proofview.Notations let safe_msgnl s = let _ = @@ -55,8 +56,7 @@ type value = tlevel generic_argument (* Values for interpretation *) type tacvalue = - | VRTactic of (goal list sigma) (* For Match results *) - (* Not a true tacvalue *) + | VRTactic (* variant of unit returned by match. For historical reasons. *) | VFun of ltac_trace * value Id.Map.t * Id.t option list * glob_tactic_expr | VRec of value Id.Map.t ref * glob_tactic_expr @@ -71,19 +71,18 @@ module Value = Taccoerce.Value let dloc = Loc.ghost -let catch_error call_trace tac g = - try tac g with e when Errors.noncritical e -> +let catching_error call_trace fail e = let e = Errors.push e in let inner_trace, e = match Exninfo.get e ltac_trace_info with | Some inner_trace -> inner_trace, e | None -> [], e in - if List.is_empty call_trace && List.is_empty inner_trace then raise e + if List.is_empty call_trace & List.is_empty inner_trace then fail e else begin assert (Errors.noncritical e); (* preserved invariant *) let new_trace = inner_trace @ call_trace in let located_exc = Exninfo.add e ltac_trace_info new_trace in - raise located_exc + fail located_exc end module TacStore = Geninterp.TacStore @@ -93,6 +92,13 @@ let f_avoid_ids : Id.t list TacStore.field = TacStore.field () let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () +let catch_error call_trace f x = + try f x with e when Errors.noncritical e -> catching_error call_trace raise e +let catch_error_tac call_trace tac = + Proofview.tclORELSE + tac + (catching_error call_trace Proofview.tclZERO) + (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; @@ -107,7 +113,7 @@ let check_is_value v = if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with - | VRTactic _ -> (* These are goals produced by Match *) + | VRTactic -> (* These are goals produced by Match *) error "Immediate match producing tactics not allowed in local definitions." | _ -> () else () @@ -248,7 +254,7 @@ let coerce_to_tactic loc id v = if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with - | VFun _ | VRTactic _ -> v + | VFun _ | VRTactic -> v | _ -> fail () else fail () @@ -966,7 +972,17 @@ let verify_metas_coherence gl (ln1,lcm) (ln,lm) = let adjust (l, lc) = (l, Id.Map.map (fun c -> [], c) lc) -type 'a extended_matching_result = + +(* spiwack: a small wrapper around the [Matching] module *) + +type 'a _matching_result = + { s_sub : bound_ident_map * patvar_map ; + s_ctx : 'a ; + s_nxt : 'a matching_result } +and 'a matching_result = 'a _matching_result Goal.sensitive Proofview.tactic + + +type 'a _extended_matching_result = { e_ctx : 'a; e_sub : bound_ident_map * extended_patvar_map; } @@ -1051,168 +1067,156 @@ let extend_gl_hyps { it=gl ; sigma=sigma } sign = Goal.V82.new_goal_with sigma gl sign (* Interprets an l-tac expression into a value *) -let rec val_interp ist gl (tac:glob_tactic_expr) : Evd.evar_map * typed_generic_argument = +let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Goal.sensitive Proofview.tactic = let value_interp ist = match tac with (* Immediate evaluation *) | TacFun (it,body) -> let v = VFun (extract_trace ist,ist.lfun,it,body) in - project gl, of_tacvalue v - | TacLetIn (true,l,u) -> interp_letrec ist gl l u - | TacLetIn (false,l,u) -> interp_letin ist gl l u - | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr - | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr - | TacArg (loc,a) -> interp_tacarg ist gl a + Proofview.tclUNIT (Goal.return (of_tacvalue v)) + | 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 + | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr + | TacArg (loc,a) -> interp_tacarg ist a (* Delayed evaluation *) | t -> let v = VFun (extract_trace ist,ist.lfun,[],t) in - project gl, of_tacvalue v - + Proofview.tclUNIT (Goal.return (of_tacvalue v)) in check_for_interrupt (); - match curr_debug ist with - | DebugOn lev -> - let eval v = - let ist = { ist with extra = TacStore.set ist.extra f_debug v } in - value_interp ist - in - debug_prompt lev gl tac eval - | _ -> value_interp ist + match curr_debug ist with + (* arnaud: todo: debug + | DebugOn lev -> + debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v}) + *) + | _ -> value_interp ist + and eval_tactic ist = function | TacAtom (loc,t) -> - fun gl -> - let call = LtacAtomCall t in - let tac = (* catch error in the interpretation *) - catch_error (push_trace(dloc,call)ist) - (interp_atomic ist gl) t in - (* catch error in the evaluation *) - catch_error (push_trace(loc,call)ist) tac gl + let call = LtacAtomCall t in + catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t) | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false - | TacId s -> fun gl -> - let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in - db_breakpoint (curr_debug ist) s; res - | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl - | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) - | TacShowHyps tac -> tclSHOWHYPS (interp_tactic ist tac) + | TacId s -> Proofview.V82.tactic begin fun gl -> + let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in + db_breakpoint (curr_debug ist) s; res + end + | TacFail (n,s) -> + Proofview.V82.tactic begin fun gl -> + tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl + end + | TacProgress tac -> Proofview.tclPROGRESS (interp_tactic ist tac) + | TacShowHyps tac -> + (* arnaud: todo: + tclSHOWHYPS (interp_tactic ist tac)*) + assert false | TacAbstract (tac,ido) -> - fun gl -> Tactics.tclABSTRACT + Proofview.V82.tactic begin fun gl -> Tactics.tclABSTRACT (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl + end | TacThen (t1,tf,t,tl) -> - tclTHENS3PARTS (interp_tactic ist t1) + Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1) (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) - | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) - | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac) - | TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) - | TacTry tac -> tclTRY (interp_tactic ist tac) - | TacRepeat tac -> tclREPEAT (interp_tactic ist tac) + | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) + | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTimeout (n,tac) -> Proofview.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) + | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> - tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) - | TacFirst l -> tclFIRST (List.map (interp_tactic ist) l) - | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l) - | TacComplete tac -> tclCOMPLETE (interp_tactic ist tac) + Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) + | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) + | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> msg_warning (strbrk "The general \"info\" tactic is currently not working." ++ fnl () ++ - strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto."); + strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto."); eval_tactic ist tac -and force_vrec ist gl v = +and force_vrec ist v = 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} gl body - | v -> project gl , of_tacvalue v - else project gl, v + | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} body + | v -> Proofview.tclUNIT (Goal.return (of_tacvalue v)) + else Proofview.tclUNIT (Goal.return v) -and interp_ltac_reference loc' mustbetac ist gl = function +and interp_ltac_reference loc' mustbetac ist = function | ArgVar (loc,id) -> let v = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id in - let (sigma,v) = force_vrec ist gl v in + force_vrec ist v >>== fun v -> let v = propagate_trace ist loc id v in - sigma , if mustbetac then coerce_to_tactic loc id v else v + if mustbetac then Proofview.tclUNIT (Goal.return (coerce_to_tactic loc id v)) else Proofview.tclUNIT (Goal.return v) | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in let extra = TacStore.set extra f_trace (push_trace loc_info ist) in let ist = { lfun = Id.Map.empty; extra = extra; } in - val_interp ist gl (lookup_ltacref r) + val_interp ist (lookup_ltacref r) -and interp_tacarg ist gl arg = - let evdref = ref (project gl) in - let v = match arg with - | TacGeneric arg -> - let gl = { gl with sigma = !evdref } in - let (sigma, v) = Geninterp.generic_interp ist gl arg in - evdref := sigma; - v - | Reference r -> - let (sigma,v) = interp_ltac_reference dloc false ist gl r in - evdref := sigma; - v - | ConstrMayEval c -> - let (sigma,c_interp) = interp_constr_may_eval ist gl c in - evdref := sigma; - Value.of_constr c_interp - | MetaIdArg (loc,_,id) -> assert false - | TacCall (loc,r,[]) -> - let (sigma,v) = interp_ltac_reference loc true ist gl r in - evdref := sigma; - v - | TacCall (loc,f,l) -> - let (sigma,fv) = interp_ltac_reference loc true ist gl f in - let (sigma,largs) = - List.fold_right begin fun a (sigma',acc) -> - let (sigma', a_interp) = interp_tacarg ist gl a in - sigma' , a_interp::acc - end l (sigma,[]) - in - List.iter check_is_value largs; - let (sigma,v) = interp_app loc ist { gl with sigma=sigma } fv largs in - evdref:= sigma; - v - | TacExternal (loc,com,req,la) -> - let (sigma,la_interp) = - List.fold_right begin fun a (sigma,acc) -> - let (sigma,a_interp) = interp_tacarg ist {gl with sigma=sigma} a in - sigma , a_interp::acc - end la (project gl,[]) - in - let (sigma,v) = interp_external loc ist { gl with sigma=sigma } com req la_interp in - evdref := sigma; - v - | TacFreshId l -> - let id = pf_interp_fresh_id ist gl l in - in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id) - | Tacexp t -> - let (sigma,v) = val_interp ist gl t in - evdref := sigma; - v - | TacDynamic(_,t) -> - let tg = (Dyn.tag t) in - if String.equal tg "tactic" then - let (sigma,v) = val_interp ist gl (tactic_out t ist) in - evdref := sigma; - v - else if String.equal tg "value" then - value_out t - else if String.equal tg "constr" then - Value.of_constr (constr_out t) - else - anomaly ~loc:dloc ~label:"Tacinterp.val_interp" - (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">") +and interp_tacarg ist arg = + let tac_of_old f = + Tacmach.New.of_old f >>-- fun (sigma,v) -> + Proofview.V82.tactic (tclEVARS sigma) <*> + Proofview.tclUNIT (Goal.return v) in - !evdref , v + match arg with + | TacGeneric arg -> + Goal.defs >>-- fun sigma -> + tac_of_old (fun gl -> + Geninterp.generic_interp ist { gl with sigma = sigma } arg) + | Reference r -> interp_ltac_reference dloc false ist r + | ConstrMayEval c -> + tac_of_old (fun gl -> interp_constr_may_eval ist gl c) >>== fun c_interp -> + Proofview.tclUNIT (Goal.return (Value.of_constr c_interp)) + | MetaIdArg (loc,_,id) -> assert false + | TacCall (loc,r,[]) -> + interp_ltac_reference loc true ist r + | TacCall (loc,f,l) -> + interp_ltac_reference loc true ist f >>== fun fv -> + Proofview.tclEVARMAP >= fun sigma -> + List.fold_right begin fun a acc -> + interp_tacarg ist a >>== fun a_interp -> + acc >>== fun acc -> Proofview.tclUNIT (Goal.return (a_interp::acc)) + end l (Proofview.tclUNIT (Goal.return [])) >>== fun largs -> + interp_app loc ist fv largs + | TacExternal (loc,com,req,la) -> + List.fold_right begin fun a acc -> + interp_tacarg ist a >>== fun a_interp -> + acc >>== fun acc -> Proofview.tclUNIT (Goal.return (a_interp::acc)) + end la (Proofview.tclUNIT (Goal.return [])) >>== fun la_interp -> + tac_of_old (fun gl -> interp_external loc ist { gl with sigma=project gl } com req la_interp) + | TacFreshId l -> + Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) >>-- fun id -> + Proofview.tclUNIT (Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id))) + | 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 + Proofview.tclUNIT (Goal.return (value_out t)) + else if String.equal tg "constr" then + Proofview.tclUNIT (Goal.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 gl fv largs = - let fail () = user_err_loc (loc, "Tacinterp.interp_app", - (str"Illegal tactic application.")) in +and interp_app loc ist fv largs = + let fail = + (* spiwack: quick hack, can be inlined. *) + try + user_err_loc (loc, "Tacinterp.interp_app", + (str"Illegal tactic application.")) + with e -> Proofview.tclZERO e + in let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with @@ -1226,72 +1230,78 @@ and interp_app loc ist gl fv largs = let (extfun,lvar,lval)=head_with_value (var,largs) in let fold accu (id, v) = Id.Map.add id v accu in let newlfun = List.fold_left fold olfun extfun in - if List.is_empty lvar then - (* Check evaluation and report problems with current trace *) - let (sigma,v) = - try + if List.is_empty lvar then + begin Proofview.tclORELSE + begin let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error trace (val_interp ist gl) body - with reraise -> - let reraise = Errors.push reraise in - debugging_exception_step ist false reraise - (fun () -> str "evaluation"); - raise reraise - in + catch_error_tac trace (val_interp ist body) + end + begin fun e -> + (* spiwack: [Errors.push] here is unlikely to do what + it's intended to, or anything meaningful for that + matter. *) + let e = Errors.push e in + (* arnaud: todo: debugging: debugging_exception_step ist false e (fun () -> str "evaluation"); *) + Proofview.tclZERO e + end + end >>== fun v -> + (* arnaud: todo: debugging: (* No errors happened, we propagate the trace *) let v = append_trace trace v in - - let gl = { gl with sigma=sigma } in - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v); - if List.is_empty lval then sigma,v else interp_app loc ist gl v lval - else - project gl , of_tacvalue (VFun(trace,newlfun,lvar,body)) - | _ -> fail () - else fail () + debugging_step ist + (fun () -> + str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v); + *) + if List.is_empty lval then Proofview.tclUNIT (Goal.return v) else interp_app loc ist v lval + else + Proofview.tclUNIT (Goal.return (of_tacvalue (VFun(trace,newlfun,lvar,body)))) + | _ -> fail + else fail (* Gives the tactic corresponding to the tactic value *) -and tactic_of_value ist vle g = +and tactic_of_value ist vle = let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with - | VRTactic res -> res + | VRTactic -> Proofview.tclUNIT () | VFun (trace,lfun,[],t) -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace []; } in let tac = eval_tactic ist t in - catch_error trace tac g - | (VFun _|VRec _) -> error "A fully applied tactic is expected." - else errorlabstrm "" (str"Expression does not evaluate to a tactic.") + catch_error_tac trace tac + | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected.")) + else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic.")) (* Evaluation with FailError catching *) -and eval_with_fail ist is_lazy goal tac = - try - let (sigma,v) = val_interp ist goal tac in - let v = Value.normalize v in - sigma , - (if has_type v (topwit wit_tacvalue) then match to_tacvalue v with - | VFun (trace,lfun,[],t) when not is_lazy -> - let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in - let tac = eval_tactic ist t in - of_tacvalue (VRTactic (catch_error trace tac { goal with sigma=sigma })) - | _ -> v - else v) - with - (** FIXME: Should we add [Errors.push]? *) - | FailError (0,s) -> - raise (Eval_fail (Lazy.force s)) - | FailError (lvl,s) as e -> - raise (Exninfo.copy e (FailError (lvl - 1, s))) +and eval_with_fail ist is_lazy tac = + Proofview.tclORELSE + begin + val_interp ist tac >>== fun v -> + (if has_type v (topwit wit_tacvalue) then match to_tacvalue v with + | VFun (trace,lfun,[],t) when not is_lazy -> + let ist = { + lfun = lfun; + extra = TacStore.set ist.extra f_trace trace; } in + let tac = eval_tactic ist t in + catch_error_tac trace (tac <*> Proofview.tclUNIT (Goal.return (of_tacvalue VRTactic))) + | _ -> Proofview.tclUNIT (Goal.return v) + else Proofview.tclUNIT (Goal.return v)) + end + begin function + (** FIXME: Should we add [Errors.push]? *) + | FailError (0,s) -> + Proofview.tclZERO (Eval_fail (Lazy.force s)) + | FailError (lvl,s) as e -> + Proofview.tclZERO (Exninfo.copy e (FailError (lvl - 1, s))) + | e -> Proofview.tclZERO e + end (* Interprets the clauses of a recursive LetIn *) -and interp_letrec ist gl llc u = +and interp_letrec ist llc u = + Proofview.tclUNIT () >= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in let fold accu ((_, id), b) = let v = of_tacvalue (VRec (lref, TacArg (dloc, b))) in @@ -1300,83 +1310,115 @@ and interp_letrec ist gl llc u = let lfun = List.fold_left fold ist.lfun llc in let () = lref := lfun in let ist = { ist with lfun } in - val_interp ist gl u + val_interp ist u (* Interprets the clauses of a LetIn *) -and interp_letin ist gl llc u = - let fold ((_, id), body) (sigma, acc) = - let (sigma, v) = interp_tacarg ist { gl with sigma } body in +and interp_letin ist llc u = + let fold ((_, id), body) acc = + interp_tacarg ist body >>== fun v -> + acc >>== fun acc -> let () = check_is_value v in - sigma, Id.Map.add id v acc + Proofview.tclUNIT (Goal.return (Id.Map.add id v acc)) in - let (sigma, lfun) = List.fold_right fold llc (project gl, ist.lfun) in + List.fold_right fold llc (Proofview.tclUNIT (Goal.return ist.lfun)) >>== fun lfun -> let ist = { ist with lfun } in - val_interp ist { gl with sigma } u + val_interp ist u (* Interprets the Match Context expressions *) -and interp_match_goal ist goal lz lr lmr = +and interp_match_goal ist lz lr lmr = + (* arnaud: on va prier pour que je n'ai pas besoin de faire ça, + sinon, je fais un truc ad-hoc let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in let goal = { it = gl ; sigma = sigma; } in - let hyps = pf_hyps goal in + *) + Goal.hyps >>-- fun hyps -> + let hyps = Environ.named_context_of_val hyps in let hyps = if lr then List.rev hyps else hyps in - let concl = pf_concl goal in - let env = pf_env goal in - let apply_goal_sub app ist (id,c) csr mt mhyps hyps = - let matches = match_subterm_gen app c csr in + Goal.concl >>-- fun concl -> + Goal.env >>-- fun env -> + let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps = let rec match_next_pattern next = match IStream.peek next with - | None -> raise PatternMatchingFailure + | None -> Proofview.tclZERO PatternMatchingFailure | Some ({ m_sub=lgoal; m_ctx=ctxt }, next) -> let lctxt = give_context ctxt id in - try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps - with e when is_match_catchable e -> match_next_pattern next in - match_next_pattern matches - in - let rec apply_match_goal ist env goal nrs lex lpt = + Proofview.tclORELSE + (apply_hyps_context ist env lz mt lctxt (adjust lgoal) mhyps hyps) + begin function + | e when is_match_catchable e -> match_next_pattern next + | e -> Proofview.tclZERO e + end + in + match_next_pattern (match_subterm_gen app c csr) in + let rec apply_match_goal ist env nrs lex lpt = begin let () = match lex with | r :: _ -> db_pattern_rule (curr_debug ist) nrs r | _ -> () in match lpt with - | (All t)::tl -> - begin - db_mc_pattern_success (curr_debug ist); - try eval_with_fail ist lz goal t - with e when is_match_catchable e -> - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl - end - | (Pat (mhyps,mgoal,mt))::tl -> - let mhyps = List.rev mhyps (* Sens naturel *) in - (match mgoal with - | Term mg -> - (try - let lmatch = extended_matches mg concl in - db_matched_concl (curr_debug ist) env concl; - apply_hyps_context ist env lz goal mt Id.Map.empty lmatch mhyps hyps - with e when is_match_catchable e -> - (match e with - | PatternMatchingFailure -> db_matching_failure (curr_debug ist) - | Eval_fail s -> db_eval_failure (curr_debug ist) s - | _ -> db_logic_failure (curr_debug ist) e); - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl) - | Subterm (b,id,mg) -> - (try apply_goal_sub b ist (id,mg) concl mt mhyps hyps - with - | PatternMatchingFailure -> - apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)) - | _ -> - errorlabstrm "Tacinterp.apply_match_goal" - (v 0 (str "No matching clauses for match goal" ++ - (if (curr_debug ist) == DebugOff then - fnl() ++ str "(use \"Set Ltac Debug\" for more info)" - else mt()) ++ str".")) + | (All t)::tl -> + begin + db_mc_pattern_success (curr_debug ist); + Proofview.tclORELSE (eval_with_fail ist lz t) + begin function + | e when is_match_catchable e -> + apply_match_goal ist env (nrs+1) (List.tl lex) tl + | e -> Proofview.tclZERO e + end + end + | (Pat (mhyps,mgoal,mt))::tl -> + let mhyps = List.rev mhyps (* Sens naturel *) in + begin match mgoal with + | Term mg -> + let matches = + try Some (extended_matches mg concl) + with PatternMatchingFailure -> None + in + begin match matches with + | None -> + db_matching_failure (curr_debug ist); + apply_match_goal ist env (nrs+1) (List.tl lex) tl + | Some lmatch -> + Proofview.tclORELSE + begin + db_matched_concl (curr_debug ist) env concl; + apply_hyps_context ist env lz mt Id.Map.empty lmatch mhyps hyps + end + begin function + | e when is_match_catchable e -> + ((match e with + | PatternMatchingFailure -> db_matching_failure (curr_debug ist) + | Eval_fail s -> db_eval_failure (curr_debug ist) s + | _ -> db_logic_failure (curr_debug ist) e); + apply_match_goal ist env (nrs+1) (List.tl lex) tl) + | e -> Proofview.tclZERO e + end + end + | Subterm (b,id,mg) -> + Proofview.tclORELSE (apply_goal_sub b ist (id,mg) concl mt mhyps hyps) + begin function + | PatternMatchingFailure -> + apply_match_goal ist env (nrs+1) (List.tl lex) tl + | e -> Proofview.tclZERO e + end + end + | _ -> + Proofview.tclZERO (UserError ( + "Tacinterp.apply_match_goal" , + (v 0 (str "No matching clauses for match goal" ++ + (if curr_debug ist==DebugOff then + fnl() ++ str "(use \"Set Ltac Debug\" for more info)" + else mt()) ++ str".")) + )) end in - apply_match_goal ist env goal 0 lmr - (read_match_rule (extract_ltac_constr_values ist env) - ist env (project goal) lmr) + Proofview.tclEVARMAP >= fun sigma -> + apply_match_goal ist env 0 lmr + (read_match_rule (extract_ltac_constr_values ist env) + ist env sigma lmr) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = +and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps = + Goal.env >>-- fun env -> let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function | hyp_pat::tl -> let (hypname, _, pat as hyp_pat) = @@ -1387,34 +1429,43 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = let rec match_next_pattern next = match IStream.peek next with | None -> db_hyp_pattern_failure (curr_debug ist) env (hypname, pat); - raise PatternMatchingFailure + Proofview.tclZERO PatternMatchingFailure | Some (s, next) -> - let lids,hyp_match = s.e_ctx in - db_matched_hyp (curr_debug ist) (pf_env goal) hyp_match hypname; - try - let id_match = pi1 hyp_match in - let select_match (id,_,_) = Id.equal id id_match in - let nextlhyps = List.remove_first select_match lhyps_rest in - let lfun = lfun +++ lids in - apply_hyps_context_rec lfun s.e_sub nextlhyps tl - with e when is_match_catchable e -> - match_next_pattern next in - let init_match_pattern = apply_one_mhyp_context goal lmatch hyp_pat lhyps_rest in - match_next_pattern init_match_pattern + let lids, hyp_match = s.e_ctx in + db_matched_hyp (curr_debug ist) env hyp_match hypname; + Proofview.tclORELSE + begin + let id_match = pi1 hyp_match in + let select_match (id,_,_) = Id.equal id id_match in + let nextlhyps = List.remove_first select_match lhyps_rest in + let lfun = lfun +++ lids in + apply_hyps_context_rec lfun s.e_sub nextlhyps tl + end + begin function + | e when is_match_catchable e -> + match_next_pattern next + | e -> Proofview.tclZERO e + end + in + let init_match_pattern = Tacmach.New.of_old (fun gl -> + apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) in + init_match_pattern >>-- match_next_pattern | [] -> let lfun = lfun +++ ist.lfun in let lfun = extend_values_with_bindings lmatch lfun in db_mc_pattern_success (curr_debug ist); - eval_with_fail { ist with lfun } lz goal mt + eval_with_fail {ist with lfun } lz mt in apply_hyps_context_rec lctxt lgmatch hyps mhyps -and interp_external loc ist gl com req la = +and interp_external loc ist gl com req la = assert false +(* arnaud: todo let f ch = extern_request ch req gl la in let g ch = internalise_tacarg ch in - interp_tacarg ist gl (System.connect f g com) + interp_tacarg ist (System.connect f g com) +*) - (* Interprets extended tactic generic arguments *) +(* Interprets extended tactic generic arguments *) and interp_genarg ist gl x = let evdref = ref (project gl) in let rec interp_genarg ist gl x = @@ -1489,206 +1540,293 @@ and interp_genarg_var_list ist gl x = in_gen (topwit (wit_list wit_var)) lc (* Interprets the Match expressions *) -and interp_match ist g lz constr lmr = +and interp_match ist lz constr lmr = let apply_match_subterm app ist (id,c) csr mt = let rec match_next_pattern next = match IStream.peek next with - | None -> raise PatternMatchingFailure + | None -> Proofview.tclZERO PatternMatchingFailure | Some ({ m_sub=lmatch; m_ctx=ctxt; }, next) -> let lctxt = give_context ctxt id in let lfun = extend_values_with_bindings (adjust lmatch) (lctxt +++ ist.lfun) in - try eval_with_fail {ist with lfun=lfun} lz g mt - with e when is_match_catchable e -> match_next_pattern next in + Proofview.tclORELSE + (eval_with_fail {ist with lfun=lfun} lz mt) + begin function + | e when is_match_catchable e -> + match_next_pattern next + | e -> Proofview.tclZERO e + end + in match_next_pattern (match_subterm_gen app c csr) in - let rec apply_match ist sigma csr = let g = { g with sigma=sigma } in function + + let rec apply_match ist csr = function | (All t)::tl -> - (try eval_with_fail ist lz g t - with e when is_match_catchable e -> apply_match ist sigma csr tl) + Proofview.tclORELSE + (eval_with_fail ist lz t) + begin function + | e when is_match_catchable e -> apply_match ist csr tl + | e -> Proofview.tclZERO e + end | (Pat ([],Term c,mt))::tl -> - (try - let lmatch = - try extended_matches c csr - with reraise -> - let reraise = Errors.push reraise in - debugging_exception_step ist false reraise (fun () -> - str "matching with pattern" ++ fnl () ++ - pr_constr_pattern_env (pf_env g) c); - raise reraise - in - try - let lfun = extend_values_with_bindings lmatch ist.lfun in - eval_with_fail { ist with lfun=lfun } lz g mt - with reraise -> - let reraise = Errors.push reraise in - debugging_exception_step ist false reraise (fun () -> - str "rule body for pattern" ++ - pr_constr_pattern_env (pf_env g) c); - raise reraise - with e when is_match_catchable e -> - debugging_step ist (fun () -> str "switching to the next rule"); - apply_match ist sigma csr tl) + let matches = + try Some (extended_matches c csr) + with PatternMatchingFailure -> None + in + Proofview.tclORELSE begin match matches with + | None -> Proofview.tclZERO PatternMatchingFailure + | Some lmatch -> + Proofview.tclORELSE + begin + let lfun = extend_values_with_bindings lmatch ist.lfun in + eval_with_fail { ist with lfun=lfun } lz mt + end + begin function + | e -> + (* arnaud: todo: debugging + debugging_exception_step ist false e (fun () -> + str "rule body for pattern" ++ + pr_constr_pattern_env (pf_env g) c);*) + Proofview.tclZERO e + end + end + begin function + | e when is_match_catchable e -> + debugging_step ist (fun () -> str "switching to the next rule"); + apply_match ist csr tl + | e -> Proofview.tclZERO e + end | (Pat ([],Subterm (b,id,c),mt))::tl -> - (try apply_match_subterm b ist (id,c) csr mt - with PatternMatchingFailure -> apply_match ist sigma csr tl) + Proofview.tclORELSE + (apply_match_subterm b ist (id,c) csr mt) + begin function + | PatternMatchingFailure -> apply_match ist csr tl + | e -> Proofview.tclZERO e + end | _ -> - errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for match.") in - let (sigma,csr) = - try interp_ltac_constr ist g constr - with reraise -> - let reraise = Errors.push reraise in - debugging_exception_step ist true reraise - (fun () -> str "evaluation of the matched expression"); - raise reraise - in - let ilr = read_match_rule (extract_ltac_constr_values ist (pf_env g)) ist (pf_env g) sigma lmr in - let res = - try apply_match ist sigma csr ilr - with reraise -> - let reraise = Errors.push reraise in - debugging_exception_step ist true reraise - (fun () -> str "match expression"); - raise reraise - in + Proofview.tclZERO (UserError ("Tacinterp.apply_match" , str + "No matching clauses for match.")) in + begin Proofview.tclORELSE + (interp_ltac_constr ist constr) + begin function + | e -> + (* spiwack: [Errors.push] here is unlikely to do what + it's intended to, or anything meaningful for that + matter. *) + let e = Errors.push e in + debugging_exception_step ist true e + (fun () -> str "evaluation of the matched expression"); + Proofview.tclZERO e + end + end >>== fun csr -> + Goal.env >>-- fun env -> + Proofview.tclEVARMAP >= fun sigma -> + let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in + Proofview.tclORELSE + (apply_match ist csr ilr) + begin function + | e -> + debugging_exception_step ist true e (fun () -> str "match expression"); + Proofview.tclZERO e + end >>== fun res -> debugging_step ist (fun () -> - str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res)); - res + str "match expression returns " ++ pr_value (Some env) res); + Proofview.tclUNIT (Goal.return res) (* Interprets tactic expressions : returns a "constr" *) -and interp_ltac_constr ist gl e = - let (sigma, result) = - try val_interp ist gl e with Not_found -> - debugging_step ist (fun () -> - str "evaluation failed for" ++ fnl() ++ - Pptactic.pr_glob_tactic (pf_env gl) e); - raise Not_found in +and interp_ltac_constr ist e = + begin Proofview.tclORELSE + (val_interp ist e) + begin function + | Not_found -> + (* arnaud: todo: debugging + debugging_step ist (fun () -> + str "evaluation failed for" ++ fnl() ++ + Pptactic.pr_glob_tactic (pf_env gl) e); + *) + Proofview.tclZERO Not_found + | e -> Proofview.tclZERO e + end + end >>== fun result -> + Goal.env >>-- fun env -> let result = Value.normalize result in try - let cresult = coerce_to_closed_constr (pf_env gl) result in + let cresult = coerce_to_closed_constr env result in debugging_step ist (fun () -> - Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ - str " has value " ++ fnl() ++ - pr_constr_env (pf_env gl) cresult); - sigma, cresult + Pptactic.pr_glob_tactic env e ++ fnl() ++ + str " has value " ++ fnl() ++ + pr_constr_env env cresult); + Proofview.tclUNIT (Goal.return cresult) with CannotCoerceTo _ -> - errorlabstrm "" + Goal.env >>-- fun env -> + Proofview.tclZERO (UserError ( "", + errorlabstrm "" (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ pr_inspect (pf_env gl) e result) + str "offending expression: " ++ fnl() ++ pr_inspect env e result))) (* Interprets tactic expressions : returns a "tactic" *) -and interp_tactic ist tac gl = - let (sigma,v) = val_interp ist gl tac in - tactic_of_value ist v { gl with sigma=sigma } +and interp_tactic ist tac = + val_interp ist tac >>= fun v -> + tactic_of_value ist v (* Interprets a primitive tactic *) -and interp_atomic ist gl tac = - let env = pf_env gl and sigma = project gl in +and interp_atomic ist tac = match tac with (* Basic tactics *) | TacIntroPattern l -> - h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) + Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) >>- fun patterns -> + h_intro_patterns patterns | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> - h_intro_move (Option.map (interp_fresh_ident ist env) ido) - (interp_move_location ist gl hto) - | TacAssumption -> h_assumption + Goal.env >>- fun env -> + Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>- fun mloc -> + h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc + | TacAssumption -> Proofview.V82.tactic h_assumption | TacExact c -> - let (sigma,c_interp) = pf_interp_casted_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_exact c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_casted_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (h_exact c_interp) + gl + end | TacExactNoCheck c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_exact_no_check c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (h_exact_no_check c_interp) + gl + end | TacVmCastNoCheck c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_vm_cast_no_check c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (h_vm_cast_no_check c_interp) + gl + end | TacApply (a,ev,cb,cl) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, l = List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb in let tac = match cl with - | None -> h_apply a ev + | None -> fun l -> Proofview.V82.tactic (h_apply a ev l) | Some cl -> - (fun l -> h_apply_in a ev l (interp_in_hyp_as ist gl cl)) in - tclWITHHOLES ev tac sigma l + (fun l -> + Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>- fun cl -> + h_apply_in a ev l cl) in + Tacticals.New.tclWITHHOLES ev tac sigma l | TacElim (ev,cb,cbo) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> 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 - tclWITHHOLES ev (h_elim ev cb) sigma cbo + Tacticals.New.tclWITHHOLES ev (h_elim ev cb) sigma cbo | TacElimType c -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_elim_type c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_type ist gl c in + tclTHEN + (tclEVARS sigma) + (h_elim_type c_interp) + gl + end | TacCase (ev,cb) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, cb = interp_constr_with_bindings ist env sigma cb in - tclWITHHOLES ev (h_case ev) sigma cb + Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb | TacCaseType c -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_case_type c_interp) - | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_type ist gl c in + tclTHEN + (tclEVARS sigma) + (h_case_type c_interp) + gl + end + | TacFix (idopt,n) -> + Goal.env >>- fun env -> + Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n) | TacMutualFix (id,n,l) -> - let f sigma (id,n,c) = - let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,n,c_interp) in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = f sigma c in - sigma , c_interp::acc - end l (project gl,[]) - in - tclTHEN - (tclEVARS sigma) - (h_mutual_fix (interp_fresh_ident ist env id) n l_interp) - | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt) + Goal.env >>- fun env -> + Proofview.V82.tactic begin fun gl -> + let f sigma (id,n,c) = + let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in + sigma , (interp_fresh_ident ist env id,n,c_interp) in + let (sigma,l_interp) = + List.fold_right begin fun c (sigma,acc) -> + let (sigma,c_interp) = f sigma c in + sigma , c_interp::acc + end l (project gl,[]) + in + tclTHEN + (tclEVARS sigma) + (h_mutual_fix (interp_fresh_ident ist env id) n l_interp) + gl + end + | TacCofix idopt -> + Goal.env >>- fun env -> + Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt)) | TacMutualCofix (id,l) -> - let f sigma (id,c) = - let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in - sigma , (interp_fresh_ident ist env id,c_interp) in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = f sigma c in - sigma , c_interp::acc - end l (project gl,[]) - in - tclTHEN - (tclEVARS sigma) - (h_mutual_cofix (interp_fresh_ident ist env id) l_interp) + Goal.env >>- fun env -> + Proofview.V82.tactic begin fun gl -> + let f sigma (id,c) = + let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in + sigma , (interp_fresh_ident ist env id,c_interp) in + let (sigma,l_interp) = + List.fold_right begin fun c (sigma,acc) -> + let (sigma,c_interp) = f sigma c in + sigma , c_interp::acc + end l (project gl,[]) + in + tclTHEN + (tclEVARS sigma) + (h_mutual_cofix (interp_fresh_ident ist env id) l_interp) + gl + end | TacCut c -> - let (sigma,c_interp) = pf_interp_type ist gl c in - tclTHEN - (tclEVARS sigma) - (h_cut c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_type ist gl c in + tclTHEN + (tclEVARS sigma) + (h_cut c_interp) + gl + end | TacAssert (t,ipat,c) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in - tclTHEN - (tclEVARS sigma) + Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>- fun patt -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) (Tactics.forward (Option.map (interp_tactic ist) t) - (Option.map (interp_intro_pattern ist gl) ipat) c) + (Option.map patt ipat) c) | TacGeneralize cl -> - let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - tclWITHHOLES false (h_generalize_gen) sigma cl + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> + Proofview.V82.tactic begin fun gl -> + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + tclWITHHOLES false (h_generalize_gen) sigma cl gl + end | TacGeneralizeDep c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_generalize_dep c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (h_generalize_dep c_interp) + gl + end | TacLetTac (na,c,clp,b,eqpat) -> - let clp = interp_clause ist gl clp in - let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> + Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>- fun clp -> + Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>- fun eqpat -> if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat) else (* We try to keep the pattern structure as much as possible *) @@ -1697,10 +1835,14 @@ and interp_atomic ist gl tac = (* Automation tactics *) | TacTrivial (debug,lems,l) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> Auto.h_trivial ~debug (interp_auto_lemmas ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (debug,n,lems,l) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) (interp_auto_lemmas ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) @@ -1709,241 +1851,321 @@ and interp_atomic ist gl tac = | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) | TacInductionDestruct (isrec,ev,(l,el,cls)) -> - let sigma, l = - List.fold_map (fun sigma (c,(ipato,ipats)) -> - let c = interp_induction_arg ist gl c in - (sigma,(c, - (Option.map (interp_intro_pattern ist gl) ipato, - Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + Goal.env >>- fun env -> + let l = + Goal.sensitive_list_map begin fun (c,(ipato,ipats)) -> + Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) >- fun c -> + Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern -> + Goal.return begin + c, + (Option.map interp_intro_pattern ipato, + Option.map interp_intro_pattern ipats) + end + end l + in + l >>- fun l -> + Goal.defs >>- fun sigma -> let sigma,el = Option.fold_map (interp_constr_with_bindings ist env) sigma el in - let cls = Option.map (interp_clause ist gl) cls in - tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) + Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>- fun interp_clause -> + let cls = Option.map interp_clause cls in + Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in Elim.h_double_induction h1 h2 | TacDecomposeAnd c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) (Elim.h_decompose_and c_interp) | TacDecomposeOr c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) (Elim.h_decompose_or c_interp) | TacDecompose (l,c) -> let l = List.map (interp_inductive ist) l in - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) (Elim.h_decompose l c_interp) | TacSpecialize (n,cb) -> - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - tclWITHHOLES false (h_specialize n) sigma cb + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> + Proofview.V82.tactic begin fun gl -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES false (h_specialize n) sigma cb gl + end | TacLApply c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_lapply c_interp) + Proofview.V82.tactic begin fun gl -> + let (sigma,c_interp) = pf_interp_constr ist gl c in + tclTHEN + (tclEVARS sigma) + (h_lapply c_interp) + gl + end (* Context management *) - | TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l) - | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l) + | TacClear (b,l) -> + Proofview.V82.tactic begin fun gl -> + h_clear b (interp_hyp_list ist gl l) gl + end + | TacClearBody l -> + Proofview.V82.tactic begin fun gl -> + h_clear_body (interp_hyp_list ist gl l) gl + end | TacMove (dep,id1,id2) -> - h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) + Proofview.V82.tactic begin fun gl -> + h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl + end | TacRename l -> - h_rename (List.map (fun (id1,id2) -> - interp_hyp ist gl id1, - interp_fresh_ident ist env (snd id2)) l) - | TacRevert l -> h_revert (interp_hyp_list ist gl l) + Goal.env >>- fun env -> + Proofview.V82.tactic begin fun gl -> + h_rename (List.map (fun (id1,id2) -> + interp_hyp ist gl id1, + interp_fresh_ident ist env (snd id2)) l) + gl + end + | TacRevert l -> + Proofview.V82.tactic begin fun gl -> + h_revert (interp_hyp_list ist gl l) gl + end (* Constructors *) | TacLeft (ev,bl) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, bl = interp_bindings ist env sigma bl in - tclWITHHOLES ev (h_left ev) sigma bl + Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl | TacRight (ev,bl) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, bl = interp_bindings ist env sigma bl in - tclWITHHOLES ev (h_right ev) sigma bl + Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl | TacSplit (ev,_,bll) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - tclWITHHOLES ev (h_split ev) sigma bll + Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll | TacAnyConstructor (ev,t) -> Tactics.any_constructor ev (Option.map (interp_tactic ist) t) | TacConstructor (ev,n,bl) -> + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let sigma, bl = interp_bindings ist env sigma bl in - tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl + Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl (* Conversion *) | TacReduce (r,cl) -> - let (sigma,r_interp) = pf_interp_red_expr ist gl r in - tclTHEN - (tclEVARS sigma) - (h_reduce r_interp (interp_clause ist gl cl)) + Proofview.V82.tactic begin fun gl -> + let (sigma,r_interp) = pf_interp_red_expr ist gl r in + tclTHEN + (tclEVARS sigma) + (h_reduce r_interp (interp_clause ist gl cl)) + gl + end | TacChange (None,c,cl) -> - let is_onhyps = match cl.onhyps with - | None | Some [] -> true - | _ -> false - in - let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true - | _ -> false - in - let (sigma,c_interp) = - if is_onhyps && is_onconcl - then pf_interp_type ist gl c - else pf_interp_constr ist gl c - in - tclTHEN - (tclEVARS sigma) - (h_change None c_interp (interp_clause ist gl cl)) + Proofview.V82.tactic begin fun gl -> + let is_onhyps = match cl.onhyps with + | None | Some [] -> true + | _ -> false + in + let is_onconcl = match cl.concl_occs with + | AllOccurrences | NoOccurrences -> true + | _ -> false + in + let (sigma,c_interp) = + if is_onhyps && is_onconcl + then pf_interp_type ist gl c + else pf_interp_constr ist gl c + in + tclTHEN + (tclEVARS sigma) + (h_change None c_interp (interp_clause ist gl cl)) + gl + end | TacChange (Some op,c,cl) -> - let sign,op = interp_typed_pattern ist env sigma op in + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> + Proofview.V82.tactic begin fun gl -> + let sign,op = interp_typed_pattern ist env sigma op in (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr is dropped as the evar_map taken as input (from extend_gl_hyps) is incorrect. This means that evar instantiated by pf_interp_constr may be lost, there. *) let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let (_,c_interp) = - try pf_interp_constr ist (extend_gl_hyps gl sign) c - 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 - tclTHEN - (tclEVARS sigma) - (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl)) + try pf_interp_constr ist (extend_gl_hyps gl sign) c + 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 + tclTHEN + (tclEVARS sigma) + (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl)) + gl + end (* Equivalence relations *) | TacReflexivity -> h_reflexivity - | TacSymmetry c -> h_symmetry (interp_clause ist gl c) + | TacSymmetry c -> + Tacmach.New.of_old (fun gl -> interp_clause ist gl c) >>- fun cl -> + h_symmetry cl | TacTransitivity c -> - begin match c with - | None -> h_transitivity None - | Some c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - tclTHEN - (tclEVARS sigma) - (h_transitivity (Some c_interp)) - end + begin match c with + | None -> h_transitivity None + | Some c -> + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclEVARS sigma)) + (h_transitivity (Some c_interp)) + end (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> let l = List.map (fun (b,m,c) -> let f env sigma = interp_open_constr_with_bindings ist env sigma c in (b,m,f)) l in - let cl = interp_clause ist gl cl in + Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) >>- fun cl -> Equality.general_multi_multi_rewrite ev l cl - (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) + (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> - let (sigma,c_interp) = - match c with - | None -> sigma , None - | Some c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - sigma , Some c_interp - in + Goal.defs >>- fun sigma -> + begin match c with + | None -> Goal.return (sigma , None) + | Some c -> + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >- fun (sigma,c_interp) -> + Goal.return (sigma , Some c_interp) + end >>- fun (sigma,c_interp) -> + Tacmach.New.of_old (interp_intro_pattern ist) >>- fun interp_intro_pattern -> + Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps -> Inv.dinv k c_interp - (Option.map (interp_intro_pattern ist gl) ids) - (interp_declared_or_quantified_hypothesis ist gl hyp) + (Option.map interp_intro_pattern ids) + dqhyps | TacInversion (NonDepInversion (k,idl,ids),hyp) -> + Tacmach.New.of_old (interp_intro_pattern ist) >>- fun interp_intro_pattern -> + Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>- fun hyps -> + Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps -> Inv.inv_clause k - (Option.map (interp_intro_pattern ist gl) ids) - (interp_hyp_list ist gl idl) - (interp_declared_or_quantified_hypothesis ist gl hyp) + (Option.map interp_intro_pattern ids) + hyps + dqhyps | TacInversion (InversionUsing (c,idl),hyp) -> - let (sigma,c_interp) = pf_interp_constr ist gl c in - Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp) + Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>- fun (sigma,c_interp) -> + Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>- fun dqhyps -> + Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>- fun hyps -> + Leminv.lemInv_clause dqhyps c_interp - (interp_hyp_list ist gl idl) + hyps (* For extensions *) | TacExtend (loc,opn,l) -> + Goal.defs >>- fun goal_sigma -> let tac = lookup_tactic opn in - let (sigma,args) = + Tacmach.New.of_old begin fun gl -> List.fold_right begin fun a (sigma,acc) -> let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in sigma , a_interp::acc - end l (project gl,[]) - in + end l (goal_sigma,[]) + end >>- fun (sigma,args) -> + Proofview.V82.tactic (tclEVARS sigma) <*> tac args ist - | TacAlias (loc,s,l,(_,body)) -> fun gl -> - let evdref = ref gl.sigma in - let rec f x = match genarg_tag x with - | IntOrVarArgType -> - mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x) - | IdentArgType b -> - value_of_ident (interp_fresh_ident ist env - (out_gen (glbwit (wit_ident_gen b)) x)) - | VarArgType -> - mk_hyp_value ist gl (out_gen (glbwit wit_var) x) - | RefArgType -> - Value.of_constr (constr_of_global - (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))) - | GenArgType -> f (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> - let (sigma,v) = mk_constr_value ist gl (out_gen (glbwit wit_constr) x) in - evdref := sigma; - v - | OpenConstrArgType false -> - let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x)) in - evdref := sigma; - v - | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in - evdref := sigma; - Value.of_constr c_interp - | ListArgType ConstrArgType -> - let wit = glbwit (wit_list wit_constr) in - let (sigma,l_interp) = - List.fold_right begin fun c (sigma,acc) -> - let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in - sigma , c_interp::acc - end (out_gen wit x) (project gl,[]) - in - evdref := sigma; - in_gen (topwit (wit_list wit_genarg)) l_interp - | ListArgType VarArgType -> - let wit = glbwit (wit_list wit_var) in - let ans = List.map (mk_hyp_value ist gl) (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 - in_gen (topwit (wit_list wit_genarg)) ans - | ListArgType (IdentArgType b) -> - let wit = glbwit (wit_list (wit_ident_gen b)) 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 - in_gen (topwit (wit_list wit_genarg)) ans - | ListArgType _ -> app_list f x - | ExtraArgType _ -> - (** Special treatment of tactics *) - let gl = { gl with sigma = !evdref } in - if has_type x (glbwit wit_tactic) then - let tac = out_gen (glbwit wit_tactic) x in - let (sigma, v) = val_interp ist gl tac in - let () = evdref := sigma in - v - else - let (sigma, v) = Geninterp.generic_interp ist gl x in - let () = evdref := sigma in - v - | QuantHypArgType | RedExprArgType - | OpenConstrArgType _ | ConstrWithBindingsArgType - | BindingsArgType - | OptArgType _ | PairArgType _ - -> error "This argument type is not supported in tactic notations." - - in - let addvar (x, v) accu = Id.Map.add x (f v) accu in - let lfun = List.fold_right addvar l ist.lfun in - let trace = push_trace (loc,LtacNotationCall s) ist in - let gl = { gl with sigma = !evdref } in - let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in - interp_tactic ist body gl + | TacAlias (loc,s,l,(_,body)) -> + Goal.env >>- fun env -> + let rec f x = match genarg_tag x with + | IntOrVarArgType -> + Proofview.tclUNIT (Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))) + | IdentArgType b -> + Proofview.tclUNIT begin + Goal.return (value_of_ident (interp_fresh_ident ist env + (out_gen (glbwit (wit_ident_gen b)) x))) + end + | VarArgType -> + Proofview.tclUNIT + (Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))) + | RefArgType -> + Proofview.tclUNIT begin + Tacmach.New.of_old (fun gl -> + Value.of_constr (constr_of_global + (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x)))) + end + + | GenArgType -> f (out_gen (glbwit wit_genarg) x) + | ConstrArgType -> + Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>-- fun (sigma,v) -> + Proofview.V82.tactic (tclEVARS sigma) <*> + Proofview.tclUNIT (Goal.return v) + | OpenConstrArgType false -> + Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>-- fun (sigma,v) -> + Proofview.V82.tactic (tclEVARS sigma) <*> + Proofview.tclUNIT (Goal.return v) + | ConstrMayEvalArgType -> + Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>-- fun (sigma,c_interp) -> + Proofview.V82.tactic (tclEVARS sigma) <*> + Proofview.tclUNIT (Goal.return (Value.of_constr c_interp)) + | ListArgType ConstrArgType -> + let wit = glbwit (wit_list wit_constr) in + Tacmach.New.of_old begin fun gl -> + List.fold_right begin fun c (sigma,acc) -> + let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in + sigma , c_interp::acc + end (out_gen wit x) (project gl,[]) + end >>-- fun (sigma,l_interp) -> + Proofview.V82.tactic (tclEVARS sigma) <*> + Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp)) + | ListArgType VarArgType -> + let wit = glbwit (wit_list wit_var) in + Proofview.tclUNIT (Tacmach.New.of_old (fun gl -> + let ans = List.map (mk_hyp_value ist gl) (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 + Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) + | ListArgType (IdentArgType b) -> + let wit = glbwit (wit_list (wit_ident_gen b)) 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 + Proofview.tclUNIT (Goal.return (in_gen (topwit (wit_list wit_genarg)) ans)) + | ListArgType t -> + (* arnaud: unsafe, faire avec des combinateurs. Dans la version originale c'était juste [Genarg.app_list f x] *) + fold_list begin fun a l -> + f a >>== fun a' -> + l >>== fun l -> + Proofview.tclUNIT (Goal.return (a'::l)) + end x (Proofview.tclUNIT (Goal.return [])) >>== fun l -> + Proofview.tclUNIT (Goal.return (in_gen + (topwit (wit_list (Obj.magic t))) + l)) + | 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 >>== fun v -> + Proofview.tclUNIT (Goal.return v) + else + Tacmach.New.of_old (fun gl -> + Geninterp.generic_interp ist gl x) >>-- fun (newsigma,v) -> + Proofview.V82.tactic (tclEVARS newsigma) <*> + Proofview.tclUNIT (Goal.return v) + | QuantHypArgType | RedExprArgType + | OpenConstrArgType _ | ConstrWithBindingsArgType + | BindingsArgType + | OptArgType _ | PairArgType _ + -> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations.")) + in + let addvar (x, v) accu = + accu >>== fun accu -> + f v >>== fun v -> + Proofview.tclUNIT (Goal.return (Id.Map.add x v accu)) + in + List.fold_right addvar l (Proofview.tclUNIT (Goal.return 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 + interp_tactic ist body (* Initial call for interpretation *) @@ -1951,13 +2173,17 @@ let default_ist () = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in { lfun = Id.Map.empty; extra = extra } -let eval_tactic t gls = +let eval_tactic t = + Proofview.tclUNIT () >= fun () -> (* delay for [db_initialize] and [default_ist] *) db_initialize (); - interp_tactic (default_ist ()) t gls + interp_tactic (default_ist ()) t (* globalization + interpretation *) -let interp_tac_gen lfun avoid_ids debug t gl = + +let interp_tac_gen lfun avoid_ids debug t = + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun = lfun; extra = extra } in @@ -1965,24 +2191,27 @@ let interp_tac_gen lfun avoid_ids debug t gl = interp_tactic ist (intern_pure_tactic { ltacvars; ltacrecvars = Id.Map.empty; - gsigma = project gl; genv = pf_env gl } t) gl + gsigma = sigma; genv = env } t) let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t let _ = Proof_global.set_interp_tac interp -let eval_ltac_constr gl t = - interp_ltac_constr (default_ist ()) gl +let eval_ltac_constr t = + Proofview.tclUNIT () >= fun () -> (* delay for [make_empty_glob_sign] and [default_ist] *) + interp_ltac_constr (default_ist ()) (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) (* Used to hide interpretation for pretty-print, now just launch tactics *) -let hide_interp t ot gl = +let hide_interp t ot = + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = project gl; genv = pf_env gl } in + gsigma = sigma; genv = env } in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with - | None -> t gl - | Some t' -> (tclTHEN t t') gl + | None -> t + | Some t' -> Tacticals.New.tclTHEN t t' (***************************************************************************) (** Register standard arguments *) |