diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/geninterp.ml | 9 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 40 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 46 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 40 |
4 files changed, 58 insertions, 77 deletions
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml index dff87d3a82..fd4f7315e3 100644 --- a/tactics/geninterp.ml +++ b/tactics/geninterp.ml @@ -29,10 +29,7 @@ module Interp = Register(InterpObj) let interp = Interp.obj let register_interp0 = Interp.register0 -let generic_interp ist v = +let generic_interp ist (GenArg (Glbwit wit, v)) = let open Ftactic.Notations in - let unpacker wit v = - interp wit ist (glb v) >>= fun ans -> - Ftactic.return (Val.Dyn (val_tag (topwit wit), ans)) - in - unpack { unpacker; } v + interp wit ist v >>= fun ans -> + Ftactic.return (Val.Dyn (val_tag (topwit wit), ans)) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6f6c4a05a1..14e0fed31d 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -718,35 +718,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 - | 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 *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 71a6e043b5..8a16ed3899 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1524,38 +1524,34 @@ and interp_genarg ist x : Val.t Ftactic.t = 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 match tag with - | ListArgType _ -> - let list_unpacker wit l = - let map x = - interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> - Ftactic.return (Value.cast (topwit wit) x) - in - Ftactic.List.map map (glb l) >>= fun l -> - Ftactic.return (Value.of_list (val_tag wit) l) + 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 + 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 -> 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 - 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))) - in - pair_unpack { pair_unpacker } x - | ExtraArgType _ -> - Geninterp.generic_interp ist x + 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. *) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 4f79115240..c74f6093a2 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -274,35 +274,29 @@ and subst_match_rule subst = function ::(subst_match_rule subst tl) | [] -> [] -and subst_genarg subst (x:glob_generic_argument) = - match genarg_tag x with - | ListArgType _ -> - let list_unpacker wit l = - let map x = - let ans = subst_genarg subst (in_gen (glbwit wit) x) in - out_gen (glbwit wit) ans - in - in_gen (glbwit (wit_list wit)) (List.map map (glb l)) +and subst_genarg subst (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = + let ans = subst_genarg subst (in_gen (glbwit wit) x) in + out_gen (glbwit wit) ans in - list_unpack { list_unpacker } x - | OptArgType _ -> - let opt_unpacker wit o = match glb 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) (subst_genarg subst (in_gen (glbwit 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 = glb o in - let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in - let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in - in_gen (glbwit (wit_pair wit1 wit2)) (p, q) - in - pair_unpack { pair_unpacker } x - | ExtraArgType s -> - Genintern.generic_substitute subst x + ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in + let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in + in_gen (glbwit (wit_pair wit1 wit2)) (p, q) + | ExtraArg s -> + Genintern.generic_substitute subst (in_gen (glbwit wit) x) (** Registering *) |