Fixing Lambda.v extraction.

generator/Makefile

@@ -40,6 +40,7 @@ tests/%.ml: tests/%.v
 	$(MAKE) -C $(CURDIR)/../../../lib/tlc/src
 	cd $(<D) && coqc -I $(CURDIR)/../../../lib/tlc/src $(<F)
 	cd $(<D) && rm *.mli
+	cd $(<D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
 
 tests/%.ml.d: tests/%.ml
 	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
@@ -57,7 +58,7 @@ clean_stdlib:
 DIRTY_EXTS := cmi,js.pre,js,d
 clean_tests:
 	rm -f $(TEST_DIR)/*.{$(DIRTY_EXTS)}
-	rm -f $(TEST_DIR)/lambda/*.{$(DIRTY_EXTS),glob,vo,d}
+	rm -f $(TEST_DIR)/lambda/*.{$(DIRTY_EXTS),glob,vo,d,ml}
 
 clean:
 	rm -rf _build

generator/tests/lambda/BinNums.ml

 type positive =
-| Coq_xI of positive
-| Coq_xO of positive
-| Coq_xH
+| Coq_xI  [@f label0] of positive (** Auto Generated Attributes **)
+| Coq_xO  [@f label0] of positive (** Auto Generated Attributes **)
+| Coq_xH [@f]  (** Auto Generated Attributes **)
 
 type coq_Z =
-| Z0
-| Zpos of positive
-| Zneg of positive
+| Z0 [@f]  (** Auto Generated Attributes **)
+| Zpos  [@f label0] of positive (** Auto Generated Attributes **)
+| Zneg  [@f label0] of positive (** Auto Generated Attributes **)
 

generator/tests/lambda/Datatypes.ml

 type bool =
-| Coq_true
-| Coq_false
+| Coq_true [@f]  (** Auto Generated Attributes **)
+| Coq_false [@f]  (** Auto Generated Attributes **)
 
 type nat =
-| O
-| S of nat
+| O [@f]  (** Auto Generated Attributes **)
+| S  [@f label0] of nat (** Auto Generated Attributes **)
 
 type 'a list =
-| Coq_nil
-| Coq_cons of 'a * 'a list
+| Coq_nil [@f]  (** Auto Generated Attributes **)
+| Coq_cons  [@f label0 label1] of 'a * 'a list (** Auto Generated Attributes **)
 

generator/tests/lambda/Lambda.ml

 open BinNums
 open Datatypes
-open LibLogic
 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 **)
 | Coq_val_clo  [@f label0 label1] of Variables.var * trm (** Auto Generated Attributes **)
@@ -23,12 +24,18 @@ let rec subst x v t =
   (match t with
    | Coq_trm_val v0 -> t
    | Coq_trm_var y ->
-     (match classicT with
+     (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)
    | Coq_trm_abs (y, t3) ->
      Coq_trm_abs (y,
-       (match classicT with
+       (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))
    | Coq_trm_app (t1, t2) -> Coq_trm_app ((s t1), (s t2))

generator/tests/lambda/Lambda.v

@@ -125,6 +125,13 @@ Fixpoint run (n:nat) (t:trm) : res :=
     end
   end.
 
+(* 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.
+
+Extract Constant nat_comparable => "(=)".
+
+Set Extraction AccessOpaque.
 Unset Extraction Optimize.
 Unset Extraction KeepSingleton.
 Unset Extraction AutoInline.

generator/tests/lambda/LibAxioms.ml

-type __ = Obj.t
-
-(** val indefinite_description : __ -> 'a1 **)
-
-let indefinite_description =
-  failwith "AXIOM TO BE REALIZED"
-

generator/tests/lambda/LibEpsilon.ml

-open LibAxioms
-open LibLogic
-open Specif
-
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
-(** val coq_Inhab_witness : __ -> 'a1 **)
-
-let coq_Inhab_witness _ =
-  indefinite_description __
-
-(** val epsilon_def : __ -> 'a1 **)
-
-let epsilon_def _ =
-  match classicT with
-  | Coq_left -> indefinite_description __
-  | Coq_right -> coq_Inhab_witness __
-
-(** val epsilon : __ -> 'a1 **)
-
-let epsilon _ =
-  epsilon_def __
-

generator/tests/lambda/LibLogic.ml

-open Datatypes
-open LibAxioms
-open Specif
-
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
-(** val classicT : sumbool **)
-
-let classicT =
-  let h = indefinite_description __ in
-  (match h with
-   | Coq_true -> (fun _ -> Coq_left)
-   | Coq_false -> (fun _ -> Coq_right)) __
-

generator/tests/lambda/LibNat.ml

 open Datatypes
 open LibReflect
 
-(** val nat_compare : nat -> nat -> bool **)
-
-let rec nat_compare x y =
-  match x with
-  | O ->
-    (match y with
-     | O -> Coq_true
-     | S n -> Coq_false)
-  | S x' ->
-    (match y with
-     | O -> Coq_false
-     | S y' -> nat_compare x' y')
-
 (** val nat_comparable : nat coq_Comparable **)
 
-let nat_comparable x y =
-  nat_compare x y
+let nat_comparable = (=)
 

generator/tests/lambda/LibVar.ml

 open Datatypes
-open LibEpsilon
 open LibFset
 open LibList
 open LibNat
 open LibReflect
 open Peano
+open Specif
 
 let __ = let rec f _ = Obj.repr f in Obj.repr f
 
@@ -47,7 +47,16 @@ module Variables =
   (** val var_gen : vars -> var **)
   
   let var_gen e =
-    var_gen_list (epsilon __)
+    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 **)
   

generator/tests/lambda/Specif.ml

@@ -3,6 +3,6 @@ type 'a coq_sig =
   (* singleton inductive, whose constructor was exist *)
 
 type sumbool =
-| Coq_left
-| Coq_right
+| Coq_left [@f]  (** Auto Generated Attributes **)
+| Coq_right [@f]  (** Auto Generated Attributes **)