From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/ltac/tacinterp.ml | 99 +++++++++++++++++++++++++++++------------------ 1 file changed, 61 insertions(+), 38 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index c6c4f469..b9e892e5 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -12,6 +12,7 @@ open Constrintern open Patternops open Pp open CAst +open Namegen open Genredexpr open Glob_term open Glob_ops @@ -35,7 +36,8 @@ open Stdarg open Tacarg open Printer open Pretyping -open Misctypes +open Tactypes +open Tactics open Locus open Tacintern open Taccoerce @@ -140,16 +142,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with | None -> [] | Some l -> l -module Value = struct - - include Taccoerce.Value - - let of_closure ist tac = - let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in - of_tacvalue closure - -end - let print_top_val env v = Pptactic.pr_value Pptactic.ltop v let catching_error call_trace fail (e, info) = @@ -291,6 +283,12 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) +let ensure_freshness env = + (* We anonymize declarations which we know will not be used *) + (* This assumes that the original context had no rels *) + process_rel_context + (fun d e -> EConstr.push_rel (Context.Rel.Declaration.set_name Anonymous d) e) env + (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in @@ -311,11 +309,11 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id let interp_int ist ({loc;v=id} as locid) = @@ -356,11 +354,11 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar {loc;v=id} -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -376,14 +374,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) + | _ -> error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -450,7 +448,7 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) + try try_interp_ltac_var (coerce_to_ident_not_fresh sigma) ist (Some (env,sigma)) (make id) with Not_found -> id in let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in @@ -473,7 +471,7 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = let add_uconstr id v map = - try Id.Map.add id (coerce_to_uconstr env v) map + try Id.Map.add id (coerce_to_uconstr v) map with CannotCoerceTo _ -> map in let add_constr id v map = @@ -642,7 +640,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (make ?loc @@ qualid_of_ident id)) + error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -689,13 +687,11 @@ let interp_may_eval f ist env sigma = function | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in - let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in + let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in let ctxt = EConstr.Unsafe.to_constr ctxt in - let evdref = ref sigma in - let ic = EConstr.Unsafe.to_constr ic in + let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in - !evdref , c + Typing.solve_evars env sigma (EConstr.of_constr c) with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" @@ -800,7 +796,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [{loc;v=IntroNaming (IntroIdentifier id)}] as l -> - (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_left_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l @@ -843,7 +839,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) + (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma {loc;v=(b,c)} = @@ -926,7 +922,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) @@ -1126,17 +1122,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,(s,l)) -> - let (ids, body) = Tacenv.interp_alias s in + let alias = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = let addvar x v accu = Id.Map.add x v accu in - let lfun = List.fold_right2 addvar ids l ist.lfun in + let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in - val_interp ist body >>= fun v -> + val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in let tac = @@ -1148,7 +1144,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with some more elaborate solution will have to be used. *) in let tac = - let len1 = List.length ids in + let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ @@ -1308,7 +1304,7 @@ and tactic_of_value ist vle = match appl with UnnamedAppl -> "An unnamed user-defined tactic" | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in match nms with [] -> assert false | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) @@ -1748,15 +1744,15 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars sigma = + let c_interp patvars env 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 if is_onhyps && is_onconcl - then interp_type ist (pf_env gl) sigma c - else interp_constr ist (pf_env gl) sigma c + then interp_type ist env sigma c + else interp_constr ist env sigma c in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) end @@ -1769,11 +1765,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in - let c_interp patvars sigma = + let c_interp patvars env sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in + let env = ensure_freshness env in let ist = { ist with lfun = lfun' } in try interp_constr ist env sigma c @@ -1861,6 +1858,31 @@ let eval_tactic_ist ist t = Proofview.tclLIFT db_initialize <*> interp_tactic ist t +(** FFI *) + +module Value = struct + + include Taccoerce.Value + + let of_closure ist tac = + let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in + of_tacvalue closure + + (** Apply toplevel tactic values *) + let apply (f : value) (args: value list) = + let fold arg (i, vars, lfun) = + let id = Id.of_string ("x" ^ string_of_int i) in + let x = Reference (ArgVar CAst.(make id)) in + (succ i, x :: vars, Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in + let lfun = Id.Map.add (Id.of_string "F") f lfun in + let ist = { (default_ist ()) with lfun = lfun; } in + let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + eval_tactic_ist ist tac + +end + (* globalization + interpretation *) @@ -2009,7 +2031,8 @@ let interp_redexp env sigma r = let _ = let eval lfun env sigma ty tac = - let ist = { lfun = lfun; extra = TacStore.empty; } in + let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in + let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in (EConstr.of_constr c, sigma) -- cgit v1.2.3