From bb64d76f9fe80ecdef4f09c797914022783ccb80 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 25 Jul 2019 20:09:28 +0200
Subject: 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>
---
 test-suite/output/bug7348.out | 45 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/output/bug7348.v   | 25 ++++++++++++++++++++++++
 2 files changed, 70 insertions(+)
 create mode 100644 test-suite/output/bug7348.out
 create mode 100644 test-suite/output/bug7348.v

(limited to 'test-suite')

diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out
new file mode 100644
index 0000000000..325ee95ae2
--- /dev/null
+++ b/test-suite/output/bug7348.out
@@ -0,0 +1,45 @@
+Extracted code successfully compiled
+
+type __ = Obj.t
+
+type unit0 =
+| Tt
+
+type bool =
+| True
+| False
+
+module Case1 =
+ struct
+  type coq_rec = { f : bool }
+
+  (** val f : bool -> coq_rec -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f
+    | False -> Obj.magic Tt
+ end
+
+module Case2 =
+ struct
+  type coq_rec = { f : (bool -> bool) }
+
+  (** val f : bool -> coq_rec -> bool -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f False
+    | False -> Obj.magic Tt
+ end
+
diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v
new file mode 100644
index 0000000000..782b27ce96
--- /dev/null
+++ b/test-suite/output/bug7348.v
@@ -0,0 +1,25 @@
+Require Extraction.
+
+Extraction Language OCaml.
+Set Extraction KeepSingleton.
+
+Module Case1.
+
+Record rec (x : bool) := { f : bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b else tt.
+
+End Case1.
+
+Module Case2.
+
+Record rec (x : bool) := { f : bool -> bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b false else tt.
+
+End Case2.
+
+Extraction TestCompile Case1.silly Case2.silly.
+Recursive Extraction Case1.silly Case2.silly.
-- 
cgit v1.2.3