Switching to an untyped toplevel representation for Ltac values.

2 files changed, 23 insertions, 32 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index ef0de89af..3ff9afa60 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -36,38 +36,23 @@ struct
   | 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
+  type t = Dyn : 'a typ * 'a -> t
 
+  let eq = ValT.eq
   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 ")"
+  let rec pr : type a. a typ -> std_ppcmds = fun t -> str (repr t)
+
+  let list_tag = ValT.create "list"
+  let opt_tag = ValT.create "option"
+  let pair_tag = ValT.create "pair"
+
+  let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
+  | Base t -> Dyn (t, x)
+  | List tag -> Dyn (list_tag, List.map (fun x -> inject tag x) x)
+  | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x)
+  | Pair (tag1, tag2) ->
+    Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x)))
 
 end
 
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 93665fd45..04113ae28 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -96,11 +96,17 @@ sig
   | Opt : 'a tag -> 'a option tag
   | Pair : 'a tag * 'b tag -> ('a * 'b) tag
 
-  type t = Dyn : 'a tag * 'a -> t
+  type t = Dyn : 'a typ * 'a -> t
 
-  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
   val repr : 'a typ -> string
-  val pr : 'a tag -> Pp.std_ppcmds
+  val pr : 'a typ -> Pp.std_ppcmds
+
+  val list_tag : t list typ
+  val opt_tag : t option typ
+  val pair_tag : (t * t) typ
+
+  val inject : 'a tag -> 'a -> t
 
 end
 (** Dynamic types for toplevel values. While the generic types permit to relate