diff options
Diffstat (limited to 'lib/genarg.ml')
| -rw-r--r-- | lib/genarg.ml | 380 |
1 files changed, 209 insertions, 171 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 42458ecb31..ef0de89afb 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,167 +9,228 @@ open Pp open Util -type argument_type = - (* Basic types *) - | IntOrVarArgType - | IdentArgType - | VarArgType - (* Specific types *) - | GenArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | ListArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string - -let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| IntOrVarArgType, IntOrVarArgType -> true -| IdentArgType, IdentArgType -> true -| VarArgType, VarArgType -> true -| GenArgType, GenArgType -> true -| ConstrArgType, ConstrArgType -> true -| ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType, OpenConstrArgType -> true -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true -| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 -| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 -| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> - argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r -| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 -| _ -> false - -let rec pr_argument_type = function -| IntOrVarArgType -> str "int_or_var" -| IdentArgType -> str "ident" -| VarArgType -> str "var" -| GenArgType -> str "genarg" -| ConstrArgType -> str "constr" -| ConstrMayEvalArgType -> str "constr_may_eval" -| QuantHypArgType -> str "qhyp" -| OpenConstrArgType -> str "open_constr" -| ConstrWithBindingsArgType -> str "constr_with_bindings" -| BindingsArgType -> str "bindings" -| RedExprArgType -> str "redexp" -| ListArgType t -> pr_argument_type t ++ spc () ++ str "list" -| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" -| PairArgType (t1, t2) -> - str "("++ pr_argument_type t1 ++ spc () ++ - str "*" ++ spc () ++ pr_argument_type t2 ++ str ")" -| ExtraArgType s -> str s - -type ('raw, 'glob, 'top) genarg_type = argument_type +module ValT = Dyn.Make(struct end) +module ArgT = +struct + module DYN = Dyn.Make(struct end) + module Map = DYN.Map + type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag + type any = Any : ('a, 'b, 'c) tag -> any + let eq = DYN.eq + let repr = DYN.repr + let create = DYN.create + let name s = match DYN.name s with + | None -> None + | Some (DYN.Any t) -> + Some (Any (Obj.magic t)) (** All created tags are made of triples *) +end -type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type -(** Alias for concision *) +module Val = +struct -(* Dynamics but tagged by a type expression *) + type 'a typ = 'a ValT.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 -> ValT.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 repr = ValT.repr + + let rec pr : type a. a tag -> std_ppcmds = function + | Base t -> str (repr t) + | List t -> pr t ++ spc () ++ str "list" + | Opt t -> pr t ++ spc () ++ str "option" + | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")" -type rlevel -type glevel -type tlevel +end -type 'a generic_argument = argument_type * Obj.t -type raw_generic_argument = rlevel generic_argument -type glob_generic_argument = glevel generic_argument -type typed_generic_argument = tlevel generic_argument +type (_, _, _) genarg_type = +| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type +| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type + +type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type + +let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2. + (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type -> + (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option = +fun t1 t2 -> match t1, t2 with +| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2 +| ListArg t1, ListArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| OptArg t1, OptArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| PairArg (t1, u1), PairArg (t2, u2) -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> + match genarg_type_eq u1 u2 with + | None -> None + | Some Refl -> Some Refl + end +| _ -> None + +let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function +| ListArg t -> pr_genarg_type t ++ spc () ++ str "list" +| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt" +| PairArg (t1, t2) -> + str "("++ pr_genarg_type t1 ++ spc () ++ + str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")" +| ExtraArg s -> str (ArgT.repr s) + +let argument_type_eq arg1 arg2 = match arg1, arg2 with +| ArgumentType t1, ArgumentType t2 -> + match genarg_type_eq t1 t2 with + | None -> false + | Some Refl -> true + +let pr_argument_type (ArgumentType t) = pr_genarg_type t -let rawwit t = t -let glbwit t = t -let topwit t = t +type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type +(** Alias for concision *) -let wit_list t = ListArgType t +(* Dynamics but tagged by a type expression *) -let wit_opt t = OptArgType t +type rlevel = [ `rlevel ] +type glevel = [ `glevel ] +type tlevel = [ `tlevel ] -let wit_pair t1 t2 = PairArgType (t1,t2) +type (_, _) abstract_argument_type = +| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type -let in_gen t o = (t,Obj.repr o) -let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen" -let genarg_tag (s,_) = s +type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument -let has_type (t, v) u = argument_type_eq t u +type raw_generic_argument = rlevel generic_argument +type glob_generic_argument = glevel generic_argument +type typed_generic_argument = tlevel generic_argument -let unquote x = x +let rawwit t = Rawwit t +let glbwit t = Glbwit t +let topwit t = Topwit t + +let wit_list t = ListArg t + +let wit_opt t = OptArg t + +let wit_pair t1 t2 = PairArg (t1, t2) + +let in_gen t o = GenArg (t, o) + +let abstract_argument_type_eq : + type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option = + fun t1 t2 -> match t1, t2 with + | Rawwit t1, Rawwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Glbwit t1, Glbwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Topwit t1, Topwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + +let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a = + let GenArg (t', v) = o in + match abstract_argument_type_eq t t' with + | None -> failwith "out_gen" + | Some Refl -> v + +let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with +| None -> false +| Some _ -> true + +let unquote : type l. (_, l) abstract_argument_type -> _ = function +| Rawwit t -> ArgumentType t +| Glbwit t -> ArgumentType t +| Topwit t -> ArgumentType t + +let genarg_tag (GenArg (t, _)) = unquote t -type ('a,'b) abstract_argument_type = argument_type type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type -type ('a, 'b, 'c, 'l) cast = Obj.t - -let raw = Obj.obj -let glb = Obj.obj -let top = Obj.obj - -type ('r, 'l) unpacker = - { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r } - -let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj) - -(** Type transformers *) - -type ('r, 'l) list_unpacker = - { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a list, 'b list, 'c list, 'l) cast -> 'r } - -let list_unpack pack (t, obj) = match t with -| ListArgType t -> pack.list_unpacker t (Obj.obj obj) -| _ -> failwith "out_gen" - -type ('r, 'l) opt_unpacker = - { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a option, 'b option, 'c option, 'l) cast -> 'r } - -let opt_unpack pack (t, obj) = match t with -| OptArgType t -> pack.opt_unpacker t (Obj.obj obj) -| _ -> failwith "out_gen" +(** Creating args *) -type ('r, 'l) pair_unpacker = - { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2. - ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> - (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r } +module type Param = sig type ('raw, 'glb, 'top) t end +module ArgMap(M : Param) = +struct + type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack + include ArgT.Map(struct type 'a t = 'a pack end) +end -let pair_unpack pack (t, obj) = match t with -| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj) -| _ -> failwith "out_gen" +type ('raw, 'glb, 'top) load = { + dyn : 'top Val.tag; +} -(** Creating args *) +module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end) -let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty +let arg0_map = ref LoadMap.empty -let create_arg opt name = - if String.Map.mem name !arg0_map then +let create_arg ?dyn name = + match ArgT.name name with + | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) - else - let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in - ExtraArgType name + | None -> + let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in + let obj = LoadMap.Pack { dyn; } in + let name = ArgT.create name in + let () = arg0_map := LoadMap.add name obj !arg0_map in + ExtraArg name let make0 = create_arg -let default_empty_value t = - let rec aux = function - | ListArgType _ -> Some (Obj.repr []) - | OptArgType _ -> Some (Obj.repr None) - | PairArgType(t1, t2) -> - (match aux t1, aux t2 with - | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) - | _ -> None) - | ExtraArgType s -> - String.Map.find s !arg0_map - | _ -> None in - match aux t with - | Some v -> Some (Obj.obj v) - | None -> None +let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function +| ListArg t -> Val.List (val_tag t) +| OptArg t -> Val.Opt (val_tag t) +| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) +| ExtraArg s -> + match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn + +let val_tag = function Topwit t -> val_tag t (** Registering genarg-manipulating functions *) @@ -182,54 +243,31 @@ end module Register (M : GenObj) = struct - let arg0_map = - ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t) + module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) + let arg0_map = ref GenMap.empty let register0 arg f = match arg with - | ExtraArgType s -> - if String.Map.mem s !arg0_map then - let msg = str M.name ++ str " function already registered: " ++ str s in + | ExtraArg s -> + if GenMap.mem s !arg0_map then + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in Errors.anomaly msg else - arg0_map := String.Map.add s (Obj.magic f) !arg0_map + arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map | _ -> assert false let get_obj0 name = - try String.Map.find name !arg0_map + try + let GenMap.Pack obj = GenMap.find name !arg0_map in obj with Not_found -> - match M.default (ExtraArgType name) with + match M.default (ExtraArg name) with | None -> - Errors.anomaly (str M.name ++ str " function not found: " ++ str name) + Errors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) | Some obj -> obj (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) let obj t = match t with - | ExtraArgType s -> Obj.magic (get_obj0 s) + | ExtraArg s -> get_obj0 s | _ -> assert false end - -(** Hackish part *) - -let arg0_names = ref (String.Map.empty : string String.Map.t) -(** We use this table to associate a name to a given witness, to use it with - the extension mechanism. This is REALLY ad-hoc, but I do not know how to - do so nicely either. *) - -let register_name0 t name = match t with -| ExtraArgType s -> - let () = assert (not (String.Map.mem s !arg0_names)) in - arg0_names := String.Map.add s name !arg0_names -| _ -> failwith "register_name0" - -let get_name0 name = - String.Map.find name !arg0_names - -module Unsafe = -struct - -let inj tpe x = (tpe, x) -let prj (_, x) = x - -end |