diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 114 |
1 files changed, 44 insertions, 70 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 11f2c5943..4ef1beb03 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -97,7 +97,6 @@ let intern_or_var f ist = function | ArgArg x -> ArgArg (f x) let intern_int_or_var = intern_or_var (fun (n : int) -> n) -let intern_id_or_var = intern_or_var (fun (id : Id.t) -> id) let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function @@ -259,8 +258,11 @@ and intern_intro_pattern_action lf ist = function | IntroApplyOn (c,pat) -> IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat) -and intern_or_and_intro_pattern lf ist = - List.map (List.map (intern_intro_pattern lf ist)) +and intern_or_and_intro_pattern lf ist = function + | IntroAndPattern l -> + IntroAndPattern (List.map (intern_intro_pattern lf ist) l) + | IntroOrPattern ll -> + IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> @@ -339,7 +341,7 @@ let intern_typed_pattern ist p = (* type it, so we remember the pattern as a glob_constr only *) (intern_constr_gen true false ist p,dummy_pat) -let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) = +let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = try Inl (intern_evaluable ist r) with e when Logic.catchable_exception e -> @@ -517,12 +519,6 @@ let rec intern_atomic lf ist x = (clause_app (intern_hyp_location ist) cls),b, (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat)) - (* Automation tactics *) - | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l) - | TacAuto (d,n,lems,l) -> - TacAuto (d,Option.map (intern_int_or_var ist) n, - List.map (intern_constr ist) lems,l) - (* Derived basic tactics *) | TacInductionDestruct (ev,isrec,(l,el)) -> TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) -> @@ -663,16 +659,16 @@ and intern_tactic_seq onlytac ist = function (* For extensions *) | TacAlias (loc,s,l) -> - let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in + let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (loc,s,l) | TacML (loc,opn,l) -> let _ignore = Tacenv.interp_ml_tactic opn in - ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l) + ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l) and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with | TacCall _ | Reference _ - | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) + | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) @@ -707,15 +703,8 @@ and intern_tacarg strict onlytac ist = function | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (intern_tactic onlytac ist t) | TacGeneric arg -> - let (_, arg) = Genintern.generic_intern ist arg in + let arg = intern_genarg ist arg in TacGeneric arg - | TacDynamic(loc,t) as x -> - if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x - else if Dyn.has_tag t "constr" then - if onlytac then error_tactic_expected loc else x - else - let tag = Dyn.tag t in - anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">") (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist = function @@ -732,57 +721,29 @@ and intern_match_rule onlytac ist = function Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) | [] -> [] -and intern_genarg ist x = - match genarg_tag x with - | IntOrVarArgType -> map_raw wit_int_or_var intern_int_or_var ist x - | IdentArgType -> - let lf = ref Id.Set.empty in - map_raw wit_ident (intern_ident lf) ist x - | VarArgType -> - map_raw wit_var intern_hyp ist x - | GenArgType -> - map_raw wit_genarg intern_genarg ist x - | ConstrArgType -> - map_raw wit_constr intern_constr ist x - | ConstrMayEvalArgType -> - map_raw wit_constr_may_eval intern_constr_may_eval ist x - | QuantHypArgType -> - map_raw wit_quant_hyp intern_quantified_hypothesis ist x - | RedExprArgType -> - map_raw wit_red_expr intern_red_expr ist x - | OpenConstrArgType -> - map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x - | ConstrWithBindingsArgType -> - map_raw wit_constr_with_bindings intern_constr_with_bindings ist x - | BindingsArgType -> - map_raw wit_bindings intern_bindings ist x - | ListArgType _ -> - let list_unpacker wit l = - let map x = - let ans = intern_genarg ist (in_gen (rawwit wit) x) in - out_gen (glbwit wit) ans - in - in_gen (glbwit (wit_list wit)) (List.map map (raw l)) +and intern_genarg ist (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = + let ans = intern_genarg ist (in_gen (rawwit wit) x) in + out_gen (glbwit wit) ans in - list_unpack { list_unpacker } x - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + in_gen (glbwit (wit_list wit)) (List.map map x) + | OptArg wit -> + let ans = match x with | None -> in_gen (glbwit (wit_opt wit)) None | Some x -> let s = out_gen (glbwit wit) (intern_genarg ist (in_gen (rawwit wit) x)) in in_gen (glbwit (wit_opt wit)) (Some s) in - opt_unpack { opt_unpacker } x - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in - let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in - in_gen (glbwit (wit_pair wit1 wit2)) (p, q) - in - pair_unpack { pair_unpacker } x - | ExtraArgType s -> - snd (Genintern.generic_intern ist x) + ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in + let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in + in_gen (glbwit (wit_pair wit1 wit2)) (p, q) + | ExtraArg s -> + snd (Genintern.generic_intern ist (in_gen (rawwit wit) x)) (** Other entry points *) @@ -852,13 +813,26 @@ let () = in Genintern.register_intern0 wit_clause_dft_concl intern_clause +let intern_ident' ist id = + let lf = ref Id.Set.empty in + (ist, intern_ident lf ist id) + let () = + Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); + Genintern.register_intern0 wit_ident intern_ident'; + Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); - Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)) - -let () = - Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)) + Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); + Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); + Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); + Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); + Genintern.register_intern0 wit_open_constr (fun ist c -> (ist,intern_constr ist c)); + Genintern.register_intern0 wit_red_expr (lift intern_red_expr); + Genintern.register_intern0 wit_bindings (lift intern_bindings); + Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings); + Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval); + () (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) |