From 678c8f36b83acf20fb71a9bc602386bbe8e1134f Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Mon, 14 Sep 2015 04:19:25 +0100
Subject: [PATCH] Try to get Lambda.v compiling
---
generator/Makefile | 3 +++
generator/tests/lambda/Lambda.ml | 22 +++++++---------------
generator/tests/lambda/Lambda.v | 8 ++++++--
generator/tests/lambda/LibNat.ml | 6 ------
generator/tests/lambda/LibVar.ml | 21 +++++----------------
generator/tests/lambda/Specif.ml | 4 ----
6 files changed, 21 insertions(+), 43 deletions(-)
diff --git a/generator/Makefile b/generator/Makefile
index eacba78..8a29c54 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -42,6 +42,9 @@ tests/%.ml: tests/%.v
cd $(<D) && rm *.mli
cd $(<D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
+tests/lambda/Lambda.ml.d: tests/lambda/Lambda.ml
+ $(OCAMLDEP) -I $(<D) $(<D)/*.ml | $(DEPSED) > $@
+
tests/%.ml.d: tests/%.ml
$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
diff --git a/generator/tests/lambda/Lambda.ml b/generator/tests/lambda/Lambda.ml
index 33525dd..b00d591 100644
--- a/generator/tests/lambda/Lambda.ml
+++ b/generator/tests/lambda/Lambda.ml
@@ -1,9 +1,7 @@
open BinNums
open Datatypes
+open LibNat
open LibVar
-open Specif
-
-let __ = let rec f _ = Obj.repr f in Obj.repr f
type coq_val =
| Coq_val_int [@f label0] of coq_Z (** Auto Generated Attributes **)
@@ -24,20 +22,14 @@ let rec subst x v t =
(match t with
| Coq_trm_val v0 -> t
| Coq_trm_var y ->
- (match let h = failwith "AXIOM TO BE REALIZED" in
- (match h with
- | Coq_true -> (fun _ -> Coq_left)
- | Coq_false -> (fun _ -> Coq_right)) __ with
- | Coq_left -> Coq_trm_val v
- | Coq_right -> t)
+ (match nat_compare x y with
+ | Coq_true -> Coq_trm_val v
+ | Coq_false -> t)
| Coq_trm_abs (y, t3) ->
Coq_trm_abs (y,
- (match let h = failwith "AXIOM TO BE REALIZED" in
- (match h with
- | Coq_true -> (fun _ -> Coq_left)
- | Coq_false -> (fun _ -> Coq_right)) __ with
- | Coq_left -> t3
- | Coq_right -> s t3))
+ (match nat_compare x y with
+ | Coq_true -> t3
+ | Coq_false -> s t3))
| Coq_trm_app (t1, t2) -> Coq_trm_app ((s t1), (s t2))
| Coq_trm_try (t1, t2) -> Coq_trm_try ((s t1), (s t2))
| Coq_trm_raise t1 -> Coq_trm_raise (s t1))
diff --git a/generator/tests/lambda/Lambda.v b/generator/tests/lambda/Lambda.v
index c29e4f4..703e41c 100644
--- a/generator/tests/lambda/Lambda.v
+++ b/generator/tests/lambda/Lambda.v
@@ -36,8 +36,8 @@ Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
let s := subst x v in
match t with
| trm_val v => t
- | trm_var y => If x = y then trm_val v else t
- | trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
+ | trm_var y => ifb x = y then trm_val v else t
+ | trm_abs y t3 => trm_abs y (ifb x = y then t3 else s t3)
| trm_app t1 t2 => trm_app (s t1) (s t2)
| trm_try t1 t2 => trm_try (s t1) (s t2)
| trm_raise t1 => trm_raise (s t1)
@@ -125,10 +125,14 @@ Fixpoint run (n:nat) (t:trm) : res :=
end
end.
+Extraction Inline nat_comparable var_comp var_comparable.
(* As classical logic statements are now unused, they should not be extracted
(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/LibNat.ml b/generator/tests/lambda/LibNat.ml
index 20e9a84..1598c9d 100644
--- a/generator/tests/lambda/LibNat.ml
+++ b/generator/tests/lambda/LibNat.ml
@@ -1,5 +1,4 @@
open Datatypes
-open LibReflect
(** val nat_compare : nat -> nat -> bool **)
@@ -14,8 +13,3 @@ let rec nat_compare x y =
| O -> Coq_false
| S y' -> nat_compare x' y')
-(** val nat_comparable : nat coq_Comparable **)
-
-let nat_comparable x y =
- nat_compare x y
-
diff --git a/generator/tests/lambda/LibVar.ml b/generator/tests/lambda/LibVar.ml
index d3286da..ece715d 100644
--- a/generator/tests/lambda/LibVar.ml
+++ b/generator/tests/lambda/LibVar.ml
@@ -4,7 +4,6 @@ open LibList
open LibNat
open LibReflect
open Peano
-open Specif
let __ = let rec f _ = Obj.repr f in Obj.repr f
@@ -29,13 +28,13 @@ module Variables =
(** val var_comp : var coq_Comparable **)
- let var_comp =
- nat_comparable
+ let var_comp x y =
+ nat_compare x y
(** val var_comparable : var coq_Comparable **)
- let var_comparable =
- var_comp
+ let var_comparable x y =
+ nat_compare x y
type vars = var FsetImpl.fset
@@ -46,17 +45,7 @@ module Variables =
(** val var_gen : vars -> var **)
- 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")
+ let var_gen = failwith "AXIOM NOT REALISED"
(** val var_fresh : vars -> var **)
diff --git a/generator/tests/lambda/Specif.ml b/generator/tests/lambda/Specif.ml
index 119dd63..7481ce4 100644
--- a/generator/tests/lambda/Specif.ml
+++ b/generator/tests/lambda/Specif.ml
@@ -2,7 +2,3 @@ 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