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

4 files changed, 86 insertions, 13 deletions

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index a88268621a..3d3c97b54a 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 cf8cda014d..eea3cd98ca 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 afd08026e5..9ff0b49234 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 288ebc33e9..33f4f499a5 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