Removing the untyped representation of genargs.

4 files changed, 27 insertions, 42 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 7aada461f..27d7b50e5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -56,29 +56,6 @@ struct
 
 end
 
-type argument_type =
-  (* Specific types *)
-  | 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
-| 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
-| 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 (_, _, _) 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
@@ -86,6 +63,8 @@ type (_, _, _) 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 =
@@ -111,6 +90,22 @@ fun t1 t2 -> match t1, t2 with
   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 rec 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 rec pr_argument_type (ArgumentType t) = pr_genarg_type t
+
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision *)
 
@@ -177,16 +172,10 @@ let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
 | None -> false
 | Some _ -> true
 
-let rec untype : type a b c. (a, b, c) genarg_type -> argument_type = function
-| ExtraArg t -> ExtraArgType (ArgT.repr t)
-| ListArg t -> ListArgType (untype t)
-| OptArg t -> OptArgType (untype t)
-| PairArg (t1, t2) -> PairArgType (untype t1, untype t2)
-
 let unquote : type l. (_, l) abstract_argument_type -> _ = function
-| Rawwit t -> untype t
-| Glbwit t -> untype t
-| Topwit t -> untype t
+| Rawwit t -> ArgumentType t
+| Glbwit t -> ArgumentType t
+| Topwit t -> ArgumentType t
 
 let genarg_tag (GenArg (t, _)) = unquote t
 
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d509649f2..ac13f545b 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -187,12 +187,7 @@ val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
 
 (** {6 Type reification} *)
 
-type argument_type =
-  (** Specific types *)
-  | ListArgType of argument_type
-  | OptArgType of argument_type
-  | PairArgType of argument_type * argument_type
-  | ExtraArgType of string
+type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
 
 (** {6 Equalities} *)
 
diff --git a/printing/genprint.ml b/printing/genprint.ml
index d8bd81c4c..0ec35e07b 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,8 +19,9 @@ module PrintObj =
 struct
   type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
   let name = "printer"
-  let default wit = match unquote (rawwit wit) with
-  | ExtraArgType name ->
+  let default wit = match wit with
+  | ExtraArg tag ->
+    let name = ArgT.repr tag in
     let printer = {
       raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
       glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7d5e7772c..d99a5f0d8 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -67,8 +67,8 @@ type 'a extra_genarg_printer =
 let genarg_pprule = ref String.Map.empty
 
 let declare_extra_genarg_pprule wit f g h =
-  let s = match unquote (topwit wit) with
-    | ExtraArgType s -> s
+  let s = match wit with
+    | ExtraArg s -> ArgT.repr s
     | _ -> error
       "Can declare a pretty-printing rule only for extra argument types."
   in