Switching to an untyped toplevel representation for Ltac values.

9 files changed, 107 insertions, 107 deletions

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 008075800..0d6721367 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,4 +32,4 @@ let register_interp0 = Interp.register0
 let generic_interp ist (GenArg (Glbwit wit, v)) =
   let open Ftactic.Notations in
   interp wit ist v >>= fun ans ->
-  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
+  Ftactic.return (Val.inject (val_tag (topwit wit)) ans)
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
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9b41a276b..90784f5e8 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -48,18 +48,27 @@ let ltac_trace_info = Tactic_debug.ltac_trace_info
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
-  match Val.eq t (val_tag wit) with
+  let t' = match val_tag wit with
+  | Val.Base t' -> t'
+  | _ -> assert false (** not used in this module *)
+  in
+  match Val.eq t t' with
   | None -> false
   | Some Refl -> true
 
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   let Val.Dyn (t', x) = v in
   match Val.eq t t' with
   | None -> None
   | Some Refl -> Some x
 
-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 in_gen wit v = Val.inject (val_tag wit) v
+let out_gen wit v =
+  let t = match val_tag wit with
+  | Val.Base t -> t
+  | _ -> assert false (** not used in this module *)
+  in
+  match prj t v with None -> assert false | Some x -> x
 
 let val_tag wit = val_tag (topwit wit)
 
@@ -152,47 +161,31 @@ module Value = struct
     let Val.Dyn (tag, _) = v in
     let tag = Val.pr tag in
     errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag
-      ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.")
+      ++ str " while type " ++ Val.pr wit ++ str " was expected.")
+
+  let unbox wit v ans = match ans with
+  | None -> cast_error wit v
+  | Some x -> x
 
-  let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+  let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
+  | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.list_tag v (to_list v))
+  | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.opt_tag v (to_option v))
+  | Val.Pair (tag1, tag2) ->
+    let (x, y) = unbox Val.pair_tag v (to_pair v) in
+    (prj tag1 x, prj tag2 y)
+  | Val.Base t ->
     let Val.Dyn (t', x) = v in
     match Val.eq t t' with
-    | None -> None
-    | Some Refl -> Some x
+    | None -> cast_error t v
+    | Some Refl -> x
 
-  let try_prj wit v = match prj (val_tag wit) v with
-  | None -> cast_error wit v
-  | Some x -> x
+  let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
+  | ExtraArg _ -> val_tag wit
+  | ListArg t -> Val.List (tag_of_arg t)
+  | OptArg t -> Val.Opt (tag_of_arg t)
+  | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
 
-  let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c =
-  fun wit v -> match wit with
-  | ExtraArg _ -> try_prj wit v
-  | ListArg t ->
-    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
-      List.map map v
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
-  | OptArg t ->
-    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
-      Option.map map v
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
-  | PairArg (t1, t2) ->
-    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
-      (val_cast t1 v1, val_cast t2 v2)
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
+  let rec val_cast arg v = prj (tag_of_arg arg) v
 
   let cast (Topwit wit) v = val_cast wit v
 
@@ -1574,7 +1567,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
       interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
       let p = Value.cast (topwit wit1) p in
       let q = Value.cast (topwit wit2) q in
-      Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)))
+      Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q))
     | ExtraArg s ->
       Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x)
 
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index a86fdb98a..b0958b394 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -256,7 +256,7 @@ let tauto_power_flags = {
 let with_flags flags _ ist =
   let f = (loc, Id.of_string "f") in
   let x = (loc, Id.of_string "x") in
-  let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in
+  let arg = Val.inject (val_tag (topwit wit_tauto_flags)) flags in
   let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
   eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7949bafcb..018e29cd2 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -97,23 +97,38 @@ module Make
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
-  let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
-  | Val.List tag ->
-    pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
-  | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
-  | Val.Pair (tag1, tag2) ->
-    str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
-      pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
-  | Val.Base t ->
-    let name = Val.repr t in
-    let default = str "<" ++ str name ++ str ">" in
-    match ArgT.name name with
-    | None -> default
-    | Some (ArgT.Any arg) ->
-      let wit = ExtraArg arg in
-      match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
+  let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+  | None -> false
+  | Some _ -> true
+
+  let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
+  match Val.eq tag t with
+  | None -> assert false
+  | Some Refl -> x
+
+  let rec pr_value lev v : std_ppcmds =
+    if has_type v Val.list_tag then
+      pr_sequence (fun x -> pr_value lev x) (unbox v Val.list_tag)
+    else if has_type v Val.opt_tag then
+      pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.opt_tag)
+    else if has_type v Val.pair_tag then
+      let (v1, v2) = unbox v Val.pair_tag in
+      str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
+    else
+      let Val.Dyn (tag, x) = v in
+      let name = Val.repr tag in
+      let default = str "<" ++ str name ++ str ">" in
+      match ArgT.name name with
       | None -> default
-      | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+      | Some (ArgT.Any arg) ->
+        let wit = ExtraArg arg in
+        match val_tag (Topwit wit) with
+        | Val.Base t ->
+          begin match Val.eq t tag with
+          | None -> default
+          | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+          end
+        | _ -> default
 
   let pr_with_occurrences pr (occs,c) =
     match occs with
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc6ff03b4..d7ce0d4c1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,7 +156,7 @@ let conclPattern concl pat tac =
        constr_bindings env sigma >>= fun constr_bindings ->
      let open Genarg in
      let open Geninterp in
-     let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+     let inj c = Val.inject (val_tag (topwit Constrarg.wit_constr)) c in
      let fold id c accu = Id.Map.add id (inj c) accu in
      let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
      let ist = { lfun; extra = TacStore.empty } in
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 358f6d646..298257e45 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -24,13 +24,18 @@ let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
   Genarg.create_arg "constr_under_binders"
 
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
+
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
   match Val.eq t (val_tag wit) with
   | None -> false
   | Some Refl -> true
 
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   let Val.Dyn (t', x) = v in
   match Val.eq t t' with
   | None -> None
@@ -74,23 +79,17 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
-let to_list v =
-  let v = normalize v in
-  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 to_list v = prj Val.list_tag v
 
-let of_list t v = Val.Dyn (Val.List t, v)
+let of_list t v = Val.Dyn (Val.list_tag, List.map (fun v -> Val.inject t v) v)
 
-let to_option v =
-  let v = normalize v in
-  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 to_option v = prj Val.opt_tag v
+
+let of_option t v = Val.Dyn (Val.opt_tag, Option.map (fun v -> Val.inject t v) v)
+
+let to_pair v = prj Val.pair_tag v
 
-let of_option t v = Val.Dyn (Val.Opt t, v)
+let of_pair t1 t2 (v1, v2) = Val.Dyn (Val.pair_tag, (Val.inject t1 v1, Val.inject t2 v2))
 
 end
 
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 87137fd2e..75a3b347d 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -44,6 +44,8 @@ sig
   val of_list : 'a Val.tag -> 'a list -> t
   val to_option : t -> t option option
   val of_option : 'a Val.tag -> 'a option -> t
+  val to_pair : t -> (t * t) option
+  val of_pair : 'a Val.tag -> 'b Val.tag -> ('a * 'b) -> t
 end
 
 (** {5 Coercion functions} *)