Parameterizing FFI functions for parameterized types.

4 files changed, 47 insertions, 53 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 6d9ede4421..f28c5c5dcf 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -48,17 +48,17 @@ open Core
 let v_unit = ValInt 0
 
 let of_name c = match c with
-| Anonymous -> Value.of_option None
-| Name id -> Value.of_option (Some (Value.of_ident id))
+| Anonymous -> Value.of_option Value.of_ident None
+| Name id -> Value.of_option Value.of_ident (Some id)
 
 let of_instance sigma u =
   let u = Univ.Instance.to_array (EConstr.EInstance.kind sigma u) in
-  Value.of_array (Array.map (fun v -> Value.of_ext Value.val_univ v) u)
+  Value.of_array (fun v -> Value.of_ext Value.val_univ v) u
 
 let of_rec_declaration (nas, ts, cs) =
-  (Value.of_array (Array.map of_name nas),
-  Value.of_array (Array.map Value.of_constr ts),
-  Value.of_array (Array.map Value.of_constr cs))
+  (Value.of_array of_name nas,
+  Value.of_array Value.of_constr ts,
+  Value.of_array Value.of_constr cs)
 
 let val_valexpr = Val.create "ltac2:valexpr"
 
@@ -183,11 +183,8 @@ let prm_ident_to_string : ml_tactic = function
 let prm_ident_of_string : ml_tactic = function
 | [s] ->
   let s = Value.to_string s in
-  let id =
-    try Value.of_option (Some (Value.of_ident (Id.of_string s)))
-    with _ -> Value.of_option None
-  in
-  return id
+  let id = try Some (Id.of_string s) with _ -> None in
+  return (Value.of_option Value.of_ident id)
 | _ -> assert false
 
 (** Int *)
@@ -282,7 +279,7 @@ let prm_constr_kind : ml_tactic = function
   | Evar (evk, args) ->
     ValBlk (3, [|
       Value.of_int (Evar.repr evk);
-      Value.of_array (Array.map Value.of_constr args)
+      Value.of_array Value.of_constr args;
     |])
   | Sort s ->
     ValBlk (4, [|Value.of_ext Value.val_sort s|])
@@ -314,7 +311,7 @@ let prm_constr_kind : ml_tactic = function
   | App (c, cl) ->
     ValBlk (9, [|
       Value.of_constr c;
-      Value.of_array (Array.map Value.of_constr cl)
+      Value.of_array Value.of_constr cl;
     |])
   | Const (cst, u) ->
     ValBlk (10, [|
@@ -335,12 +332,12 @@ let prm_constr_kind : ml_tactic = function
     ValBlk (13, [|
       Value.of_constr c;
       Value.of_constr t;
-      Value.of_array (Array.map (fun c -> Value.of_constr c) bl);
+      Value.of_array Value.of_constr bl;
     |])
   | Fix ((recs, i), def) ->
     let (nas, ts, cs) = of_rec_declaration def in
     ValBlk (14, [|
-      Value.of_array (Array.map Value.of_int recs);
+      Value.of_array Value.of_int recs;
       Value.of_int i;
       nas;
       ts;
@@ -378,7 +375,7 @@ let prm_pattern_matches : ml_tactic = function
     | Some ans ->
       let ans = Id.Map.bindings ans in
       let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
-      return (Value.of_list (List.map of_pair ans))
+      return (Value.of_list of_pair ans)
     end
   end
 | _ -> assert false
@@ -393,7 +390,7 @@ let prm_pattern_matches_subterm : ml_tactic = function
   | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
     let ans = Id.Map.bindings sub in
     let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
-    let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list (List.map of_pair ans) |] in
+    let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list of_pair ans |] in
     Proofview.tclOR (return ans) (fun _ -> of_ans s)
   in
   pf_apply begin fun env sigma ->
@@ -441,19 +438,16 @@ let prm_once : ml_tactic = function
 (** (unit -> unit) list -> unit *)
 let prm_dispatch : ml_tactic = function
 | [l] ->
-  let l = Value.to_list l in
-  let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in
+  let l = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) l in
   Proofview.tclDISPATCH l >>= fun () -> return v_unit
 | _ -> assert false
 
 (** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
 let prm_extend : ml_tactic = function
 | [lft; tac; rgt] ->
-  let lft = Value.to_list lft in
-  let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in
+  let lft = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) lft in
   let tac = Proofview.tclIGNORE (thaw tac) in
-  let rgt = Value.to_list rgt in
-  let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
+  let rgt = Value.to_list (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
   Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
 | _ -> assert false
 
@@ -540,18 +534,17 @@ let prm_hyps : ml_tactic = function
 | [_] ->
   pf_apply begin fun env _ ->
     let open Context.Named.Declaration in
-    let hyps = Environ.named_context env in
+    let hyps = List.rev (Environ.named_context env) in
     let map = function
     | LocalAssum (id, t) ->
       let t = EConstr.of_constr t in
-      Value.of_tuple [|Value.of_ident id; Value.of_option None; Value.of_constr t|]
+      Value.of_tuple [|Value.of_ident id; Value.of_option Value.of_constr None; Value.of_constr t|]
     | LocalDef (id, c, t) ->
       let c = EConstr.of_constr c in
       let t = EConstr.of_constr t in
-      Value.of_tuple [|Value.of_ident id; Value.of_option (Some (Value.of_constr c)); Value.of_constr t|]
+      Value.of_tuple [|Value.of_ident id; Value.of_option Value.of_constr (Some c); Value.of_constr t|]
     in
-    let hyps = List.rev_map map hyps in
-    return (Value.of_list hyps)
+    return (Value.of_list map hyps)
   end
 | _ -> assert false
 
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 5f1341ea80..74e2b02aeb 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -67,13 +67,13 @@ let to_string = function
 | ValStr s -> s
 | _ -> assert false
 
-let rec of_list = function
+let rec of_list f = function
 | [] -> ValInt 0
-| x :: l -> ValBlk (0, [| x; of_list l |])
+| x :: l -> ValBlk (0, [| f x; of_list f l |])
 
-let rec to_list = function
+let rec to_list f = function
 | ValInt 0 -> []
-| ValBlk (0, [|v; vl|]) -> v :: to_list vl
+| ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
 | _ -> assert false
 
 let of_ext tag c =
@@ -101,13 +101,13 @@ let to_exn c = match c with
 | ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
 | _ -> to_ext val_exn c
 
-let of_option = function
+let of_option f = function
 | None -> ValInt 0
-| Some c -> ValBlk (0, [|c|])
+| Some c -> ValBlk (0, [|f c|])
 
-let to_option = function
+let to_option f = function
 | ValInt 0 -> None
-| ValBlk (0, [|c|]) -> Some c
+| ValBlk (0, [|c|]) -> Some (f c)
 | _ -> assert false
 
 let of_pp c = of_ext val_pp c
@@ -118,5 +118,7 @@ let to_tuple = function
 | ValBlk (0, cl) -> cl
 | _ -> assert false
 
-let of_array = of_tuple
-let to_array = to_tuple
+let of_array f vl = ValBlk (0, Array.map f vl)
+let to_array f = function
+| ValBlk (0, vl) -> Array.map f vl
+| _ -> assert false
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index d72d0452a0..3f429995ce 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -32,8 +32,8 @@ val to_char : valexpr -> char
 val of_string : string -> valexpr
 val to_string : valexpr -> string
 
-val of_list : valexpr list -> valexpr
-val to_list : valexpr -> valexpr list
+val of_list : ('a -> valexpr) -> 'a list -> valexpr
+val to_list : (valexpr -> 'a) -> valexpr -> 'a list
 
 val of_constr : EConstr.t -> valexpr
 val to_constr : valexpr -> EConstr.t
@@ -44,14 +44,14 @@ val to_exn : valexpr -> Exninfo.iexn
 val of_ident : Id.t -> valexpr
 val to_ident : valexpr -> Id.t
 
-val of_array : valexpr array -> valexpr
-val to_array : valexpr -> valexpr array
+val of_array : ('a -> valexpr) -> 'a array -> valexpr
+val to_array : (valexpr -> 'a) -> valexpr -> 'a array
 
 val of_tuple : valexpr array -> valexpr
 val to_tuple : valexpr -> valexpr array
 
-val of_option : valexpr option -> valexpr
-val to_option : valexpr -> valexpr option
+val of_option : ('a -> valexpr) -> 'a option -> valexpr
+val to_option : (valexpr -> 'a) -> valexpr -> 'a option
 
 val of_pattern : Pattern.constr_pattern -> valexpr
 val to_pattern : valexpr -> Pattern.constr_pattern
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 25d83c06fb..0aeccbd9c6 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -112,45 +112,44 @@ let () = define_prim0 "tac_split" (Tactics.split_with_bindings false [NoBindings
 let () = define_prim0 "tac_esplit" (Tactics.split_with_bindings true [NoBindings])
 
 let () = define_prim1 "tac_rename" begin fun ids ->
-  let ids = Value.to_list ids in
   let map c = match Value.to_tuple c with
   | [|x; y|] -> (Value.to_ident x, Value.to_ident y)
   | _ -> assert false
   in
-  let ids = List.map map ids in
+  let ids = Value.to_list map ids in
   Tactics.rename_hyp ids
 end
 
 let () = define_prim1 "tac_revert" begin fun ids ->
-  let ids = List.map Value.to_ident (Value.to_list ids) in
+  let ids = Value.to_list Value.to_ident ids in
   Tactics.revert ids
 end
 
 let () = define_prim0 "tac_admit" Proofview.give_up
 
 let () = define_prim2 "tac_fix" begin fun idopt n ->
-  let idopt = Option.map Value.to_ident (Value.to_option idopt) in
+  let idopt = Value.to_option Value.to_ident idopt in
   let n = Value.to_int n in
   Tactics.fix idopt n
 end
 
 let () = define_prim1 "tac_cofix" begin fun idopt ->
-  let idopt = Option.map Value.to_ident (Value.to_option idopt) in
+  let idopt = Value.to_option Value.to_ident idopt in
   Tactics.cofix idopt
 end
 
 let () = define_prim1 "tac_clear" begin fun ids ->
-  let ids = List.map Value.to_ident (Value.to_list ids) in
+  let ids = Value.to_list Value.to_ident ids in
   Tactics.clear ids
 end
 
 let () = define_prim1 "tac_keep" begin fun ids ->
-  let ids = List.map Value.to_ident (Value.to_list ids) in
+  let ids = Value.to_list Value.to_ident ids in
   Tactics.keep ids
 end
 
 let () = define_prim1 "tac_clearbody" begin fun ids ->
-  let ids = List.map Value.to_ident (Value.to_list ids) in
+  let ids = Value.to_list Value.to_ident ids in
   Tactics.clear_body ids
 end
 
@@ -161,7 +160,7 @@ let () = define_prim1 "tac_absurd" begin fun c ->
 end
 
 let () = define_prim1 "tac_subst" begin fun ids ->
-  let ids = List.map Value.to_ident (Value.to_list ids) in
+  let ids = Value.to_list Value.to_ident ids in
   Equality.subst ids
 end