Fix #7348: extraction of dependent record projections

- Inline record projections by default (except for Haskell extraction).
- Extend `pp_record_proj` for record projections involving `MLmagic`.
- Remove special treatments for pretty-printing for record projections other
  than `pp_record_proj`.
- `micromega.ml` had to be changed due to this change of the extraction plugin.

Acknowledgement: This work is financially supported by Peano System Inc.

on-behalf-of: @peano-system <info@peano-system.jp>

1 files changed, 12 insertions, 14 deletions

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 75fb35192b..e7004fe9af 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -229,12 +229,7 @@ let rec pp_expr par env args =
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
-    | MLglob r ->
-	(try
-	   let args = List.skipn (projection_arity r) args in
-	   let record = List.hd args in
-	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with e when CErrors.noncritical e -> apply (pp_global Term r))
+    | MLglob r -> apply (pp_global Term r)
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -324,10 +319,14 @@ and pp_record_proj par env typ t pv args =
   let n = List.length ids in
   let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
   let rel_i,a = match body with
-    | MLrel i when i <= n -> i,[]
-    | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a
+    | MLrel i | MLmagic(MLrel i) when i <= n -> i,[]
+    | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a))
+      | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a
     | _ -> raise Impossible
   in
+  let magic =
+    match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false
+  in
   let rec lookup_rel i idx = function
     | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
     | Pwild :: l -> lookup_rel i (idx+1) l
@@ -343,7 +342,10 @@ and pp_record_proj par env typ t pv args =
   let pp_args = (List.map (pp_expr true env' []) a) @ args in
   let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx
   in
-  pp_apply pp_head par pp_args
+  if magic then
+    pp_apply (str "Obj.magic") par (pp_head :: pp_args)
+  else
+    pp_apply pp_head par pp_args
 
 and pp_record_pat (fields, args) =
    str "{ " ++
@@ -579,14 +581,10 @@ let pp_decl = function
     | Dterm (r, a, t) ->
 	let def =
 	  if is_custom r then str (" = " ^ find_custom r)
-	  else if is_projection r then
-	    (prvect str (Array.make (projection_arity r) " _")) ++
-	    str " x = x."
 	  else pp_function (empty_env ()) a
 	in
 	let name = pp_global Term r in
-	let postdef = if is_projection r then name else mt () in
-	pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
+        pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)