Getting rid of the awkward unpack mechanism from Genarg.

9 files changed, 122 insertions, 204 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 7795946d56..7a5f84704f 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -37,20 +37,16 @@ module Subst = Register (SubstObj)
 let intern = Intern.obj
 let register_intern0 = Intern.register0
 
-let generic_intern ist v =
-  let unpacker wit v =
-    let (ist, v) = intern wit ist (raw v) in
-    (ist, in_gen (glbwit wit) v)
-  in
-  unpack { unpacker; } v
+let generic_intern ist (GenArg (Rawwit wit, v)) =
+  let (ist, v) = intern wit ist v in
+  (ist, in_gen (glbwit wit) v)
 
 (** Substitution functions *)
 
 let substitute = Subst.obj
 let register_subst0 = Subst.register0
 
-let generic_substitute subs v =
-  let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in
-  unpack { unpacker; } v
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+  in_gen (glbwit wit) (substitute wit subs v)
 
 let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 6c10dee2ae..58d83ce7ae 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -203,14 +203,6 @@ let raw : ('a, 'b, 'c, rlevel) cast -> _ = function Rcast x -> x
 let glb : ('a, 'b, 'c, glevel) cast -> _ = function Gcast x -> x
 let top : ('a, 'b, 'c, tlevel) cast -> _ = function Tcast x -> x
 
-type ('r, 'l) unpacker =
-  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-let unpack (type l) (pack : (_, l) unpacker) (GenArg (t, obj) : l generic_argument) = match t with
-| Rawwit t -> pack.unpacker t (Rcast obj)
-| Glbwit t -> pack.unpacker t (Gcast obj)
-| Topwit t -> pack.unpacker t (Tcast obj)
-
 (** Type transformers *)
 
 type ('r, 'l) list_unpacker =
diff --git a/lib/genarg.mli b/lib/genarg.mli
index a1b74c6744..8d1a439827 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -179,44 +179,6 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
-(** {6 Destructors} *)
-
-type ('a, 'b, 'c, 'l) cast
-
-val raw : ('a, 'b, 'c, rlevel) cast -> 'a
-val glb : ('a, 'b, 'c, glevel) cast -> 'b
-val top : ('a, 'b, 'c, tlevel) cast -> 'c
-
-type ('r, 'l) unpacker =
-  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r
-(** Existential-type destructors. *)
-
-(** {6 Manipulation of generic arguments}
-
-Those functions fail if they are applied to an argument which has not the right
-dynamic type. *)
-
-type ('r, 'l) list_unpacker =
-  { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a list, 'b list, 'c list, 'l) cast -> 'r }
-
-val list_unpack : ('r, 'l) list_unpacker -> 'l generic_argument -> 'r
-
-type ('r, 'l) opt_unpacker =
-  { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a option, 'b option, 'c option, 'l) cast -> 'r }
-
-val opt_unpack : ('r, 'l) opt_unpacker -> 'l generic_argument -> 'r
-
-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 }
-
-val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
-
 (** {6 Dynamic toplevel values} *)
 
 val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
diff --git a/printing/genprint.ml b/printing/genprint.ml
index ade69ef831..58c41e839e 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -40,6 +40,6 @@ let raw_print wit v = (Print.obj wit).raw v
 let glb_print wit v = (Print.obj wit).glb v
 let top_print wit v = (Print.obj wit).top v
 
-let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
-let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
-let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
+let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v
+let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
+let generic_top_print (GenArg (Topwit w, v)) = top_print w v
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e7443fd02e..53b0c091a5 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -265,84 +265,71 @@ module Make
   let with_evars ev s = if ev then "e" ^ s else s
 
 
-  let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
-    match Genarg.genarg_tag x with
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
-          pr_sequence map (raw l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match raw o with
+  let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
           | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
         in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = raw o in
-          let p = in_gen (rawwit wit1) p in
-          let q = in_gen (rawwit wit2) q in
-          pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]
-        in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_raw_print x
-
-
-  let rec pr_glb_generic_rec prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
-          pr_sequence map (glb l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match glb o with
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (rawwit wit1) p in
+        let q = in_gen (rawwit wit2) q in
+        hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
+      | ExtraArg s ->
+        try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
+        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+  let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
           | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
         in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = glb o in
-          let p = in_gen (glbwit wit1) p in
-          let q = in_gen (glbwit wit2) q in
-          pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q]
-        in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_glb_print x
-
-  let rec pr_top_generic_rec prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
-          pr_sequence map (top l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match top o with
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (glbwit wit1) p in
+        let q = in_gen (glbwit wit2) q in
+        let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
+        hov 0 ans
+      | ExtraArg s ->
+        try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
+        with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
+
+  let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
           | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
         in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = top o in
-          let p = in_gen (topwit wit1) p in
-          let q = in_gen (topwit wit2) q in
-          pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q]
-        in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_top_print x
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (topwit wit1) p in
+        let q = in_gen (topwit wit2) q in
+        let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in
+        hov 0 ans
+      | ExtraArg s ->
+        try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x)
+        with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x)
 
   let rec tacarg_using_rule_token pr_gen = function
     | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index dff87d3a82..fd4f7315e3 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -29,10 +29,7 @@ module Interp = Register(InterpObj)
 let interp = Interp.obj
 let register_interp0 = Interp.register0
 
-let generic_interp ist v =
+let generic_interp ist (GenArg (Glbwit wit, v)) =
   let open Ftactic.Notations in
-  let unpacker wit v =
-    interp wit ist (glb v) >>= fun ans ->
-    Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
-  in
-  unpack { unpacker; } v
+  interp wit ist v >>= fun ans ->
+  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6f6c4a05a1..14e0fed31d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -718,35 +718,29 @@ and intern_match_rule onlytac ist = function
       Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
-and intern_genarg ist x =
-  match genarg_tag x with
-  | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x =
-          let ans = intern_genarg ist (in_gen (rawwit wit) x) in
-          out_gen (glbwit wit) ans
-        in
-        in_gen (glbwit (wit_list wit)) (List.map map (raw l))
+and intern_genarg ist (GenArg (Rawwit wit, x)) =
+  match wit with
+  | ListArg wit ->
+      let map x =
+        let ans = intern_genarg ist (in_gen (rawwit wit) x) in
+        out_gen (glbwit wit) ans
       in
-      list_unpack { list_unpacker } x
-  | OptArgType _ ->
-      let opt_unpacker wit o = match raw o with
+      in_gen (glbwit (wit_list wit)) (List.map map x)
+  | OptArg wit ->
+      let ans = match x with
       | None -> in_gen (glbwit (wit_opt wit)) None
       | Some x ->
         let s = out_gen (glbwit wit) (intern_genarg ist (in_gen (rawwit wit) x)) in
         in_gen (glbwit (wit_opt wit)) (Some s)
       in
-      opt_unpack { opt_unpacker } x
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = raw o in
-        let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in
-        let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in
-        in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
-      in
-      pair_unpack { pair_unpacker } x
-  | ExtraArgType s ->
-      snd (Genintern.generic_intern ist x)
+      ans
+  | PairArg (wit1, wit2) ->
+      let p, q = x in
+      let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in
+      let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in
+      in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
+  | ExtraArg s ->
+      snd (Genintern.generic_intern ist (in_gen (rawwit wit) x))
 
 (** Other entry points *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71a6e043b5..8a16ed3899 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1524,38 +1524,34 @@ and interp_genarg ist x : Val.t Ftactic.t =
       interp_genarg_var_list ist x
     else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
       interp_genarg_constr_list ist x
-    else match tag with
-    | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x =
-          interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
-          Ftactic.return (Value.cast (topwit wit) x)
-        in
-        Ftactic.List.map map (glb l) >>= fun l ->
-        Ftactic.return (Value.of_list (val_tag wit) l)
+    else
+    let GenArg (Glbwit wit, x) = x in
+    match wit with
+    | ListArg wit ->
+      let map x =
+        interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
+        Ftactic.return (Value.cast (topwit wit) x)
       in
-      list_unpack { list_unpacker } x
-    | OptArgType _ ->
-      let opt_unpacker wit o = match glb o with
+      Ftactic.List.map map x >>= fun l ->
+      Ftactic.return (Value.of_list (val_tag wit) l)
+    | OptArg wit ->
+      let ans = match x with
       | None -> Ftactic.return (Value.of_option (val_tag wit) None)
       | Some x ->
         interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
         let x = Value.cast (topwit wit) x in
         Ftactic.return (Value.of_option (val_tag wit) (Some x))
       in
-      opt_unpack { opt_unpacker } x
-    | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let (p, q) = glb o in
-        interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
-        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)))
-      in
-      pair_unpack { pair_unpacker } x
-    | ExtraArgType _ ->
-      Geninterp.generic_interp ist x
+      ans
+    | PairArg (wit1, wit2) ->
+      let (p, q) = x in
+      interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
+      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)))
+    | ExtraArg s ->
+      Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x)
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4f79115240..c74f6093a2 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -274,35 +274,29 @@ and subst_match_rule subst = function
       ::(subst_match_rule subst tl)
   | [] -> []
 
-and subst_genarg subst (x:glob_generic_argument) =
-  match genarg_tag x with
-  | ListArgType _ ->
-    let list_unpacker wit l =
-      let map x =
-        let ans = subst_genarg subst (in_gen (glbwit wit) x) in
-        out_gen (glbwit wit) ans
-      in
-      in_gen (glbwit (wit_list wit)) (List.map map (glb l))
+and subst_genarg subst (GenArg (Glbwit wit, x)) =
+  match wit with
+  | ListArg wit ->
+    let map x =
+      let ans = subst_genarg subst (in_gen (glbwit wit) x) in
+      out_gen (glbwit wit) ans
     in
-    list_unpack { list_unpacker } x
-  | OptArgType _ ->
-    let opt_unpacker wit o = match glb o with
+    in_gen (glbwit (wit_list wit)) (List.map map x)
+  | OptArg wit ->
+    let ans = match x with
     | None -> in_gen (glbwit (wit_opt wit)) None
     | Some x ->
       let s = out_gen (glbwit wit) (subst_genarg subst (in_gen (glbwit wit) x)) in
       in_gen (glbwit (wit_opt wit)) (Some s)
     in
-    opt_unpack { opt_unpacker } x
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = glb o in
-        let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in
-        let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
-        in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
-      in
-      pair_unpack { pair_unpacker } x
-  | ExtraArgType s ->
-      Genintern.generic_substitute subst x
+    ans
+  | PairArg (wit1, wit2) ->
+    let p, q = x in
+    let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in
+    let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
+    in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
+  | ExtraArg s ->
+      Genintern.generic_substitute subst (in_gen (glbwit wit) x)
 
 (** Registering *)