Type-safe version of genarg list / pair / opt functions.

7 files changed, 181 insertions, 123 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index b85fef087..ce0041036 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -96,60 +96,6 @@ let in_gen t o = (t,Obj.repr o)
 let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
 let genarg_tag (s,_) = s
 
-let fold_list f = function
-  | (ListArgType t, l) ->
-      List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
-  | _ -> failwith "Genarg: not a list"
-
-let fold_opt f a = function
-  | (OptArgType t, l) ->
-      (match Obj.magic l with
-	| None -> a
-	| Some x -> f (in_gen t x))
-  | _ -> failwith "Genarg: not a opt"
-
-let fold_pair f = function
-  | (PairArgType (t1,t2), l) ->
-      let (x1,x2) = Obj.magic l in
-      f (in_gen t1 x1) (in_gen t2 x2)
-  | _ -> failwith "Genarg: not a pair"
-
-let app_list f = function
-  | (ListArgType t as u, l) ->
-      let o = Obj.magic l in
-      (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
-  | _ -> failwith "Genarg: not a list0"
-
-let app_opt f = function
-  | (OptArgType t as u, l) ->
-      let o = Obj.magic l in
-      (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
-  | _ -> failwith "Genarg: not an opt"
-
-let app_pair f1 f2 = function
-  | (PairArgType (t1,t2) as u, l) ->
-      let (o1,o2) = Obj.magic l in
-      let o1 = out_gen t1 (f1 (in_gen t1 o1)) in
-      let o2 = out_gen t2 (f2 (in_gen t2 o2)) in
-      (u, Obj.repr (o1,o2))
-  | _ -> failwith "Genarg: not a pair"
-
-module Monadic (M:Monad.S) = struct
-
-  let app_list f = function
-  | (ListArgType t as u, l) ->
-      let o = Obj.magic l in
-      let open M in
-      let apply x =
-        f (in_gen t x) >>= fun y ->
-        return (out_gen t y)
-      in
-      M.List.map apply o >>= fun r ->
-      return (u, Obj.repr r)
-  | _ -> failwith "Genarg: not a list0"
-
-end
-
 let has_type (t, v) u = argument_type_eq t u
 
 let unquote x = x
@@ -170,6 +116,33 @@ type ('r, 'l) unpacker =
 
 let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj)
 
+(** Type transformers *)
+
+type ('r, 'l) list_unpacker =
+  { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
+    ('a list, 'b list, 'c list, 'l) cast -> 'r }
+
+let list_unpack pack (t, obj) = match t with
+| ListArgType t -> pack.list_unpacker t (Obj.obj obj)
+| _ -> failwith "out_gen"
+
+type ('r, 'l) opt_unpacker =
+  { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
+    ('a option, 'b option, 'c option, 'l) cast -> 'r }
+
+let opt_unpack pack (t, obj) = match t with
+| OptArgType t -> pack.opt_unpacker t (Obj.obj obj)
+| _ -> failwith "out_gen"
+
+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 }
+
+let pair_unpack pack (t, obj) = match t with
+| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj)
+| _ -> failwith "out_gen"
+
 (** Creating args *)
 
 let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
diff --git a/lib/genarg.mli b/lib/genarg.mli
index e96f21c10..90e701239 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -160,39 +160,24 @@ val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r
 Those functions fail if they are applied to an argument which has not the right
 dynamic type. *)
 
-val fold_list :
- ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
+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 fold_opt :
- ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
+val list_unpack : ('r, 'l) list_unpacker -> 'l generic_argument -> 'r
 
-val fold_pair :
- ('a generic_argument -> 'a generic_argument -> 'c) ->
-      'a generic_argument -> 'c
+type ('r, 'l) opt_unpacker =
+  { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
+    ('a option, 'b option, 'c option, 'l) cast -> 'r }
 
-(** [app_list0] fails if applied to an argument not of tag [List0 t]
-    for some [t]; it's the responsability of the caller to ensure it *)
+val opt_unpack : ('r, 'l) opt_unpacker -> 'l generic_argument -> 'r
 
-val app_list : ('a generic_argument -> 'b generic_argument) ->
-'a generic_argument -> 'b generic_argument
+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 app_opt : ('a generic_argument -> 'b generic_argument) ->
-'a generic_argument -> 'b generic_argument
-
-val app_pair :
-  ('a generic_argument -> 'b generic_argument) ->
-      ('a generic_argument -> 'b generic_argument)
-   -> 'a generic_argument -> 'b generic_argument
-
-module Monadic (M:Monad.S) : sig
-
-  (** [Monadic.app_list f x] maps the monadic computation [f] on
-      elements of [x], provided [x] has the tag [List0 t] for some [t]. It
-      fails otherwise. *)
-  val app_list : ('a generic_argument -> 'b generic_argument M.t) ->
-    'a generic_argument -> 'b generic_argument M.t
-
-end
+val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
 
 (** {6 Type reification} *)
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 8c3e9a7e0..a3a023ce9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -164,15 +164,25 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
   | ListArgType _ ->
-      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
-	(fold_list (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prpat prref) (mt()) x)
+      let list_unpacker wit l =
+        let map x = pr_raw_generic 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
+      | None -> mt ()
+      | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
+      in
+      hov 0 (opt_unpack { opt_unpacker } x)
   | PairArgType _ ->
-      hov 0
-        (fold_pair
-	  (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
-            [a;b])
-	  x)
+      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 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
@@ -201,14 +211,25 @@ let rec pr_glb_generic prc prlc prtac prpat x =
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
   | ListArgType _ ->
-      hov 0 (pr_sequence (pr_glb_generic prc prlc prtac prpat)
-	(fold_list (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_glb_generic prc prlc prtac prpat) (mt()) x)
+      let list_unpacker wit l =
+        let map x = pr_glb_generic 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
+      | None -> mt ()
+      | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
+      in
+      hov 0 (opt_unpack { opt_unpacker } x)
   | PairArgType _ ->
-      hov 0
-        (fold_pair
-	  (fun a b -> pr_sequence (pr_glb_generic prc prlc prtac prpat) [a;b])
-	  x)
+      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 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
@@ -232,14 +253,25 @@ let rec pr_top_generic prc prlc prtac prpat x =
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
   | ListArgType _ ->
-      hov 0 (pr_sequence (pr_top_generic prc prlc prtac prpat)
-	(fold_list (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_top_generic prc prlc prtac prpat) (mt()) x)
+      let list_unpacker wit l =
+        let map x = pr_top_generic 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
+      | None -> mt ()
+      | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+      in
+      hov 0 (opt_unpack { opt_unpacker } x)
   | PairArgType _ ->
-      hov 0
-        (fold_pair (fun a b -> pr_sequence (pr_top_generic prc prlc prtac prpat)
-          [a;b])
-	  x)
+      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 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
@@ -247,13 +279,8 @@ let rec pr_top_generic prc prlc prtac prpat x =
 let rec tacarg_using_rule_token pr_gen = function
   | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
   | None :: l, a :: al ->
-      let print_it =
-        match genarg_tag a with
-        | OptArgType _ -> fold_opt (fun _ -> true) false a
-        | _ -> true
-      in
       let r = tacarg_using_rule_token pr_gen (l,al) in
-      if print_it then pr_gen a :: r else r
+      pr_gen a :: r
   | [], [] -> []
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index a88268621..3d3c97b54 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -64,7 +64,8 @@ let to_int v =
 
 let to_list v =
   let v = normalize v in
-  try Some (fold_list (fun v accu -> v :: accu) v [])
+  let list_unpacker wit l = List.map (fun v -> in_gen (topwit wit) v) (top l) in
+  try Some (list_unpack { list_unpacker } v)
   with Failure _ -> None
 
 end
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index cf8cda014..eea3cd98c 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -751,9 +751,31 @@ and intern_genarg ist x =
   | BindingsArgType ->
       in_gen (glbwit wit_bindings)
         (intern_bindings ist (out_gen (rawwit wit_bindings) x))
-  | ListArgType _ -> app_list (intern_genarg ist) x
-  | OptArgType _ -> app_opt (intern_genarg ist) x
-  | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
+  | 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))
+      in
+      list_unpack { list_unpacker } x
+  | OptArgType _ ->
+      let opt_unpacker wit o = match raw o 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)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index afd08026e..9ff0b4923 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1073,8 +1073,6 @@ end
 module GTac' = Monad_.Make(GTac)
 module GTacList = GTac'.List
 
-module GenargTac = Genarg.Monadic(struct include GTac module List = GTacList end)
-
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist (tac:glob_tactic_expr) : typed_generic_argument GTac.t =
   let value_interp ist = match tac with
@@ -1236,7 +1234,16 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               let ans = List.map mk_ident (out_gen wit x) in
               GTac.return (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType t  ->
-              GenargTac.app_list (fun y -> f y) x
+              let open GTac in
+              let list_unpacker wit l =
+                let map x =
+                  f (in_gen (glbwit wit) x) >>= fun v ->
+                  GTac.return (out_gen (topwit wit) v)
+                in
+                GTacList.map map (glb l) >>= fun l ->
+                GTac.return (in_gen (topwit (wit_list wit)) l)
+              in
+              list_unpack { list_unpacker } x
           | ExtraArgType _ ->
               let (>>=) = GTac.bind in
               (** Special treatment of tactics *)
@@ -1629,9 +1636,30 @@ and interp_genarg ist env sigma concl gl x =
 	evdref := sigma;
 	v
     | ListArgType VarArgType -> interp_genarg_var_list ist env x
-    | ListArgType _ -> app_list interp_genarg x
-    | OptArgType _ -> app_opt interp_genarg x
-    | PairArgType _ -> app_pair interp_genarg interp_genarg x
+    | ListArgType _ ->
+      let list_unpacker wit l =
+        let map x =
+          out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x))
+        in
+        in_gen (topwit (wit_list wit)) (List.map map (glb l))
+      in
+      list_unpack { list_unpacker } x
+    | OptArgType _ ->
+      let opt_unpacker wit o = match glb o with
+      | None -> in_gen (topwit (wit_opt wit)) None
+      | Some x ->
+        let x = out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) in
+        in_gen (topwit (wit_opt wit)) (Some x)
+      in
+      opt_unpack { opt_unpacker } x
+    | PairArgType _ ->
+      let pair_unpacker wit1 wit2 o =
+        let (p, q) = glb o in
+        let p = out_gen (topwit wit1) (interp_genarg (in_gen (glbwit wit1) p)) in
+        let q = out_gen (topwit wit2) (interp_genarg (in_gen (glbwit wit2) q)) in
+        in_gen (topwit (wit_pair wit1 wit2)) (p, q)
+      in
+      pair_unpack { pair_unpacker } x
     | ExtraArgType s ->
         let (sigma,v) = Geninterp.generic_interp ist { Evd.it=gl;sigma=(!evdref) } x in
 	evdref:=sigma;
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 288ebc33e..33f4f499a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -314,9 +314,31 @@ and subst_genarg subst (x:glob_generic_argument) =
   | BindingsArgType ->
       in_gen (glbwit wit_bindings)
         (subst_bindings subst (out_gen (glbwit wit_bindings) x))
-  | ListArgType _ -> app_list (subst_genarg subst) x
-  | OptArgType _ -> app_opt (subst_genarg subst) x
-  | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
+  | 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))
+    in
+    list_unpack { list_unpacker } x
+  | OptArgType _ ->
+    let opt_unpacker wit o = match glb o 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