diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-30 12:09:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-30 12:20:23 +0200 |
| commit | c0aefc5323cb4393297adcaffd2967ab93ab815e (patch) | |
| tree | 6e9d4dad66807a231083e9965d2e22436b56a793 /lib/genarg.ml | |
| parent | 051c9a8a1112174769670cb0dc8cebb85ccb803c (diff) | |
Ensuring that the type of base generic arguments contain triples.
Diffstat (limited to 'lib/genarg.ml')
| -rw-r--r-- | lib/genarg.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index a43466c62..5d5b29c99 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -10,7 +10,20 @@ open Pp open Util module ValT = Dyn.Make(struct end) -module ArgT = 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 module Val = struct @@ -57,7 +70,7 @@ struct end type (_, _, _) genarg_type = -| ExtraArg : ('a * 'b * 'c) ArgT.tag -> ('a, 'b, 'c) 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 -> |