an example with type classes, but no class inference triggered yet

6 files changed, 80 insertions, 6 deletions

diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 5f1bd0450c..23ba975de4 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -1,6 +1,7 @@
 -R theories Tuto3
 -I src
 
+theories/Data.v
 theories/Loader.v
 
 src/construction_game.ml
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index df3bfd5d21..953687cce2 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -43,12 +43,11 @@ let dangling_identity2 env evd =
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =
-(* Next, I wish to construct a lambda-abstraction without giving precisely
-   the type for the abstracted variable. *)
     let env = Global.env () in
     let evd = Evd.from_env env in
     let c_v = c_one () in
-    let evd, c_f = dangling_identity env evd in
+(* dangling_identity and dangling_identity2 can be used interchangeably here *)
+    let evd, c_f = dangling_identity2 env evd in
     let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
     let _ = Feedback.msg_notice
        (Termops.print_constr_env env evd c_1) in
@@ -62,4 +61,62 @@ let example_sort_app_lambda () =
     Feedback.msg_notice
       ((Termops.print_constr_env env evd c_1) ++
        str " has type " ++
-       (Termops.print_constr_env env evd the_type))
\ No newline at end of file
+       (Termops.print_constr_env env evd the_type))
+
+let constants = ref ([] : EConstr.constr list)
+
+let collect_constants () =
+  if (!constants = []) then
+    let open Coqlib in
+    let open EConstr in
+    let open Universes in
+    let gr_S = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+    let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+    let gr_E = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+    let gr_D = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+    constants := List.map (fun x -> of_constr (constr_of_global x))
+      [gr_S; gr_O; gr_E; gr_D];
+    !constants
+  else
+    !constants
+
+let c_S () =
+  match collect_constants () with
+    it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of S : nat"
+
+let c_O () =
+  match collect_constants () with
+    _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of 0 : nat"
+
+let c_E () =
+  match collect_constants () with
+    _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of EvenNat"
+
+let c_D () =
+  match collect_constants () with
+    _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of tuto_div2"
+
+let mk_nat n =
+  let c_S = c_S () in  
+  let c_O = c_O () in
+  let rec buildup = function
+    | 0 -> c_O
+    | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
+  if n <= 0 then c_O else buildup n
+
+let example_classes n =
+  let c_n = mk_nat n in
+  let c_div = c_D () in
+  let c_even = c_E () in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let c_1 = EConstr.mkApp (c_div, [|c_n; instance|]) in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_1) in
+  let evd, the_type = Typing.type_of env evd c_1 in
+  Feedback.msg_notice (Termops.print_constr_env env evd c_1)
\ No newline at end of file
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
index dbd33c0f1c..a4172734fd 100644
--- a/tuto3/src/construction_game.mli
+++ b/tuto3/src/construction_game.mli
@@ -1 +1,2 @@
-val example_sort_app_lambda : unit -> unit
\ No newline at end of file
+val example_sort_app_lambda : unit -> unit
+val example_classes : int -> unit
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index 2c9bd5b121..e0f60b34c8 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -21,6 +21,10 @@ VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] -> [ example_sort_app_lambda() ]
+| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
+END
+
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
 END
 
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
new file mode 100644
index 0000000000..15e36bc6ec
--- /dev/null
+++ b/tuto3/theories/Data.v
@@ -0,0 +1,9 @@
+Class EvenNat n := {half : nat; half_prop : 2 * half = n}.
+
+Instance EvenNat2 : EvenNat 2 := {half := 1; half_prop := eq_refl}.
+
+Instance EvenNat4 : EvenNat 4 := {half := 2; half_prop := eq_refl}.
+
+Definition tuto_div2 n (p : EvenNat n) := @half n p.
+
+
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
index cff239af41..eb3182cdaa 100644
--- a/tuto3/theories/Loader.v
+++ b/tuto3/theories/Loader.v
@@ -1 +1,3 @@
+From Tuto3 Require Import Data.
+
 Declare ML Module "tuto3_plugin".
\ No newline at end of file