diff options
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | lib/genarg.ml | 110 | ||||
| -rw-r--r-- | lib/genarg.mli | 21 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 14 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 52 |
6 files changed, 137 insertions, 66 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 20c8f690b..0894e0378 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -468,7 +468,7 @@ let pp_generic_argument arg = let prgenarginfo arg = let Val.Dyn (tag, _) = arg in - let tpe = str (Val.repr tag) in + let tpe = Val.repr tag in (** FIXME *) (* try *) (* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) diff --git a/lib/genarg.ml b/lib/genarg.ml index 11a042117..2b8e0c9fd 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,7 +9,51 @@ open Pp open Util -module Val = Dyn.Make(struct end) +module Dyn = Dyn.Make(struct end) + +module Val = +struct + + type 'a typ = 'a Dyn.tag + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a tag * 'a -> t + + let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option = + fun t1 t2 -> match t1, t2 with + | Base t1, Base t2 -> Dyn.eq t1 t2 + | List t1, List t2 -> + begin match eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Opt t1, Opt t2 -> + begin match eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Pair (t1, u1), Pair (t2, u2) -> + begin match eq t1 t2 with + | None -> None + | Some Refl -> + match eq u1 u2 with + | None -> None + | Some Refl -> Some Refl + end + | _ -> None + + let rec repr : type a. a tag -> std_ppcmds = function + | Base t -> str (Dyn.repr t) + | List t -> repr t ++ spc () ++ str "list" + | Opt t -> repr t ++ spc () ++ str "option" + | Pair (t1, t2) -> str "(" ++ repr t1 ++ str " * " ++ repr t2 ++ str ")" + +end type argument_type = (* Basic types *) @@ -139,7 +183,7 @@ let create_arg opt ?dyn name = if String.Map.mem name !arg0_map then Errors.anomaly (str "generic argument already declared: " ++ str name) else - let dyn = match dyn with None -> Val.create name | Some dyn -> cast_tag dyn in + let dyn = match dyn with None -> Val.Base (Dyn.create name) | Some dyn -> cast_tag dyn in let obj = { nil = Option.map Obj.repr opt; dyn; } in let () = arg0_map := String.Map.add name obj !arg0_map in ExtraArgType name @@ -162,26 +206,22 @@ let default_empty_value t = | None -> None (** Beware: keep in sync with the corresponding types *) -let ident_T = Val.create "ident" -let genarg_T = Val.create "genarg" -let constr_T = Val.create "constr" -let open_constr_T = Val.create "open_constr" - -let option_val = Val.create "option" -let list_val = Val.create "list" -let pair_val = Val.create "pair" +let base_create n = Val.Base (Dyn.create n) +let ident_T = base_create "ident" +let genarg_T = base_create "genarg" +let constr_T = base_create "constr" +let open_constr_T = base_create "open_constr" -let val_tag = function +let rec val_tag = function | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T | OpenConstrArgType -> cast_tag open_constr_T -| ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn -(** Recursive types have no associated dynamic tag *) -| ListArgType t -> assert false -| OptArgType t -> assert false -| PairArgType (t1, t2) -> assert false +| ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn +| ListArgType t -> cast_tag (Val.List (val_tag t)) +| OptArgType t -> cast_tag (Val.Opt (val_tag t)) +| PairArgType (t1, t2) -> cast_tag (Val.Pair (val_tag t1, val_tag t2)) exception CastError of argument_type * Val.t @@ -202,23 +242,31 @@ fun wit v -> match unquote wit with | ConstrArgType | OpenConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> - let v = match prj list_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (List.map (fun x -> val_cast t x) v) + 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 + Obj.magic (List.map map v) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end | OptArgType t -> - let v = match prj option_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (Option.map (fun x -> val_cast t x) v) + 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 + Obj.magic (Option.map map v) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end | PairArgType (t1, t2) -> - let (v1, v2) = match prj pair_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (val_cast t1 v1, val_cast t2 v2) + 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 + Obj.magic (val_cast t1 v1, val_cast t2 v2) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end (** Registering genarg-manipulating functions *) diff --git a/lib/genarg.mli b/lib/genarg.mli index 83ba1dd04..090496093 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -72,7 +72,22 @@ type ('raw, 'glob, 'top) genarg_type (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized one, and ['top] the internalized one. *) -module Val : Dyn.S +module Val : +sig + type 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a tag * 'a -> t + + val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + val repr: 'a tag -> Pp.std_ppcmds + +end (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the @@ -193,10 +208,6 @@ val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a -val option_val : Val.t option Val.tag -val list_val : Val.t list Val.tag -val pair_val : (Val.t * Val.t) Val.tag - (** {6 Type reification} *) type argument_type = diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 88e36be14..7fb79d4fe 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -76,15 +76,21 @@ let to_int v = let to_list v = let v = normalize v in - prj list_val v + let Val.Dyn (tag, v) = v in + match tag with + | Val.List t -> Some (List.map (fun x -> Val.Dyn (t, x)) v) + | _ -> None -let of_list v = Val.Dyn (list_val, v) +let of_list t v = Val.Dyn (Val.List t, v) let to_option v = let v = normalize v in - prj option_val v + let Val.Dyn (tag, v) = v in + match tag with + | Val.Opt t -> Some (Option.map (fun x -> Val.Dyn (t, x)) v) + | _ -> None -let of_option v = Val.Dyn (option_val, v) +let of_option t v = Val.Dyn (Val.Opt t, v) end diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 4d85ae709..0754c1536 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -41,9 +41,9 @@ sig val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option - val of_list : t list -> t + val of_list : 'a Val.tag -> 'a list -> t val to_option : t -> t option option - val of_option : t option -> t + val of_option : 'a Val.tag -> 'a option -> t end (** {5 Coercion functions} *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 37d9f1825..570ab245b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -58,9 +58,11 @@ let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> 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 - Pp.str (Val.repr tag) + Val.repr tag let safe_msgnl s = Proofview.NonLogical.catch @@ -80,7 +82,7 @@ let push_appl appl args = | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) let pr_generic arg = (** FIXME *) let Val.Dyn (tag, _) = arg in - str"<" ++ str (Val.repr tag) ++ str ">" + str"<" ++ Val.repr tag ++ str ">" let pr_appl h vs = Pptactic.pr_ltac_constant h ++ spc () ++ Pp.prlist_with_sep spc pr_generic vs @@ -146,7 +148,7 @@ module Value = struct 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 " ++ str tag + errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag ++ str " while type " ++ Genarg.pr_argument_type wit ++ str " was expected.") let cast wit v = @@ -284,9 +286,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 @@ -1125,7 +1127,7 @@ 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)) + (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;} @@ -1263,7 +1265,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.return (value_of_ident (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))) | VarArgType -> - Ftactic.return (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)) + Ftactic.return (Value.of_constr (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x))) | OpenConstrArgType -> let (sigma,v) = Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in @@ -1271,20 +1273,20 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in - Ftactic.return (Value.of_list ans) + Ftactic.return (Value.of_list (val_tag wit_constr) 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 mk_ident x = intro_pattern_of_ident (interp_ident ist env sigma x) in let ans = List.map mk_ident (Genarg.out_gen wit x) in - Ftactic.return (Value.of_list ans) + Ftactic.return (Value.of_list (val_tag wit_intro_pattern) ans) | ListArgType t -> let open Ftactic in - let list_unpacker wit l = + list_unpack { list_unpacker = fun wit l -> let map x = f (Genarg.in_gen (glbwit wit) x) in Ftactic.List.map map (glb l) >>= fun l -> - Ftactic.return (Value.of_list l) - in - list_unpack { list_unpacker } x + let l = CList.map (fun x -> Value.cast (topwit wit) x) l in + Ftactic.return (Value.of_list (val_tag wit) l) + } x | ExtraArgType _ -> (** Special treatment of tactics *) if Genarg.has_type x (glbwit wit_tactic) then @@ -1650,16 +1652,20 @@ and interp_genarg ist env sigma concl gl x = | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x | ListArgType _ -> let list_unpacker wit l = - let map x = interp_genarg (Genarg.in_gen (glbwit wit) x) in - Value.of_list (List.map map (glb l)) + let map x = + let x = interp_genarg (Genarg.in_gen (glbwit wit) x) in + Value.cast (topwit wit) x + in + Value.of_list (val_tag wit) (List.map map (glb l)) in list_unpack { list_unpacker } x | OptArgType _ -> let opt_unpacker wit o = match glb o with - | None -> Value.of_option None + | None -> Value.of_option (val_tag wit) None | Some x -> let x = interp_genarg (Genarg.in_gen (glbwit wit) x) in - Value.of_option (Some x) + let x = Value.cast (topwit wit) x in + Value.of_option (val_tag wit) (Some x) in opt_unpack { opt_unpacker } x | PairArgType _ -> @@ -1667,7 +1673,9 @@ and interp_genarg ist env sigma concl gl x = let (p, q) = glb o in let p = interp_genarg (Genarg.in_gen (glbwit wit1) p) in let q = interp_genarg (Genarg.in_gen (glbwit wit2) q) in - Val.Dyn (pair_val, (p, q)) + let p = Value.cast (topwit wit1) p in + let q = Value.cast (topwit wit2) q in + Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)) in pair_unpack { pair_unpacker } x | ExtraArgType s -> @@ -1694,14 +1702,12 @@ and global_genarg = and interp_genarg_constr_list ist env sigma x = let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in - let lc = List.map Value.of_constr lc in - sigma , Value.of_list lc + sigma , Value.of_list (val_tag wit_constr) lc and interp_genarg_var_list ist env sigma x = let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in - let lc = List.map (fun id -> Val.Dyn (val_tag (topwit wit_var), id)) lc in - Value.of_list lc + Value.of_list (val_tag wit_var) lc (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : constr Ftactic.t = |