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>

5 files changed, 15 insertions, 40 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 78c6255c1e..cca212f332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -754,18 +754,6 @@ and extract_cst_app env sg mle mlt kn args =
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env sg mle s args metas in
-  let mla =
-    if magic1 || lang () != Ocaml then mla
-    else
-      try
-        (* for better optimisations later, we discard dependent args
-           of projections and replace them by fake args that will be
-           removed during final pretty-print. *)
-        let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in
-	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
-	else mla
-      with e when CErrors.noncritical e -> mla
-  in
   (* For strict languages, purely logical signatures lead to a dummy lam
      (except when [Kill Ktype] everywhere). So a [MLdummy] is left
      accordingly. *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 2d5872718f..baa1881297 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1547,6 +1547,7 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r)
   && (to_inline r (* The user DOES want to inline it *)
-     || (lang () != Haskell && not (is_projection r) &&
-         (is_recursor r || manual_inline r || inline_test r t)))
+     || (lang () != Haskell &&
+         (is_projection r || is_recursor r ||
+          manual_inline r || inline_test r t)))
 
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)
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index a64a5a84b3..11bd2c0946 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1568,14 +1568,6 @@ module PositiveSet =
 
 type q = { qnum : z; qden : positive }
 
-(** val qnum : q -> z **)
-
-let qnum x = x.qnum
-
-(** val qden : q -> positive **)
-
-let qden x = x.qden
-
 (** val qeq_bool : q -> q -> bool **)
 
 let qeq_bool x y =
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 64cb3a8355..6da0c754f4 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -446,10 +446,6 @@ module PositiveSet :
 
 type q = { qnum : z; qden : positive }
 
-val qnum : q -> z
-
-val qden : q -> positive
-
 val qeq_bool : q -> q -> bool
 
 val qle_bool : q -> q -> bool