From 78832226d6e472a6592dfffe91242613ec76841c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 1 Oct 2017 20:33:26 +0200
Subject: Abstracting away the implementation of value representations.

---
 src/tac2core.ml  |  6 +++---
 src/tac2ffi.ml   |  3 +++
 src/tac2ffi.mli  | 10 ++++------
 src/tac2print.ml |  2 +-
 4 files changed, 11 insertions(+), 10 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 9e3cefc6f5..1756e44f76 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -157,15 +157,15 @@ let define_primitive name arity f =
 let define0 name f = define_primitive name arity_one (fun _ -> f)
 
 let define1 name r0 f = define_primitive name arity_one begin fun x ->
-  f (r0.Value.r_to x)
+  f (Value.repr_to r0 x)
 end
 
 let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
-  f (r0.Value.r_to x) (r1.Value.r_to y)
+  f (Value.repr_to r0 x) (Value.repr_to r1 y)
 end
 
 let define3 name r0 r1 r2 f = define_primitive name (arity_suc (arity_suc arity_one)) begin fun x y z ->
-  f (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
+  f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)
 end
 
 (** Printing *)
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 923a29e5c5..c612cb85a5 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -76,6 +76,9 @@ type 'a repr = {
   r_id : bool;
 }
 
+let repr_of r x = r.r_of x
+let repr_to r x = r.r_to x
+
 (** Dynamic tags *)
 
 let val_exn = Val.create "exn"
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index cb6d5a1e49..9f200b439d 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -49,12 +49,10 @@ end
 
 (** {5 Ltac2 FFI} *)
 
-type 'a repr = {
-  r_of : 'a -> valexpr;
-  r_to : valexpr -> 'a;
-  r_id : bool;
-  (** True if the functions above are physical identities. *)
-}
+type 'a repr
+
+val repr_of : 'a repr -> 'a -> valexpr
+val repr_to : 'a repr -> valexpr -> 'a
 
 (** These functions allow to convert back and forth between OCaml and Ltac2
     data representation. The [to_*] functions raise an anomaly whenever the data
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 45360a61f4..018346ad6a 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -401,7 +401,7 @@ let rec pr_valexpr env sigma v t = match kind t with
   end
 | GTypArrow _ -> str "<fun>"
 | GTypRef (Tuple _, tl) ->
-  let blk = Array.to_list (snd (block.r_to v)) in
+  let blk = Array.to_list (snd (to_block v)) in
   if List.length blk == List.length tl then
     let prs = List.map2 (fun v t -> pr_valexpr env sigma v t) blk tl in
     hv 2 (str "(" ++ prlist_with_sep pr_comma (fun p -> p) prs ++ str ")")
-- 
cgit v1.2.3