From a0c900b09abf32351cfcc17247c7e60c35a1da44 Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Tue, 15 Sep 2015 14:09:21 +0100
Subject: [PATCH] No longer any need for constant extraction of var_gen
---
generator/tests/lambda/Lambda.v | 3 ---
generator/tests/lambda/LibVar.ml | 13 ++++++++++++-
generator/tests/lambda/Specif.ml | 4 ++++
3 files changed, 16 insertions(+), 4 deletions(-)
diff --git a/generator/tests/lambda/Lambda.v b/generator/tests/lambda/Lambda.v
index 703e41c..cc4390e 100644
--- a/generator/tests/lambda/Lambda.v
+++ b/generator/tests/lambda/Lambda.v
@@ -130,9 +130,6 @@ Extraction Inline nat_comparable var_comp var_comparable.
(otherwise, useless errors will be launched). *)
Extraction Inline classicT LibEpsilon.Inhab_witness LibEpsilon.epsilon LibEpsilon.epsilon_def indefinite_description.
-(* Suppress dependency on Specif.ml... *)
-Extract Constant var_gen => "failwith ""AXIOM NOT REALISED""".
-
Set Extraction AccessOpaque.
Unset Extraction Optimize.
Unset Extraction KeepSingleton.
diff --git a/generator/tests/lambda/LibVar.ml b/generator/tests/lambda/LibVar.ml
index ece715d..bbe34f7 100644
--- a/generator/tests/lambda/LibVar.ml
+++ b/generator/tests/lambda/LibVar.ml
@@ -4,6 +4,7 @@ open LibList
open LibNat
open LibReflect
open Peano
+open Specif
let __ = let rec f _ = Obj.repr f in Obj.repr f
@@ -45,7 +46,17 @@ module Variables =
(** val var_gen : vars -> var **)
- let var_gen = failwith "AXIOM NOT REALISED"
+ let var_gen e =
+ var_gen_list
+ (let s =
+ let h = failwith "AXIOM TO BE REALIZED" in
+ (match h with
+ | Coq_true -> (fun _ -> Coq_left)
+ | Coq_false -> (fun _ -> Coq_right)) __
+ in
+ match s with
+ | Coq_left -> failwith "AXIOM TO BE REALIZED"
+ | Coq_right -> failwith "AXIOM TO BE REALIZED")
(** val var_fresh : vars -> var **)
diff --git a/generator/tests/lambda/Specif.ml b/generator/tests/lambda/Specif.ml
index 7481ce4..119dd63 100644
--- a/generator/tests/lambda/Specif.ml
+++ b/generator/tests/lambda/Specif.ml
@@ -2,3 +2,7 @@ type 'a coq_sig =
'a
(* singleton inductive, whose constructor was exist *)
+type sumbool =
+| Coq_left [@f] (** Auto Generated Attributes **)
+| Coq_right [@f] (** Auto Generated Attributes **)
+
--
GitLab