Experimentation with polymorphic task definition.

examples/build-systems-ala-carte/Makefile

@@ -20,6 +20,7 @@ HS_SPEC=hs-spec
 
 # Handwritten modules (usually by modification of generated version)
 HANDMOD = \
+   Build/Task \
 
 
 
@@ -67,7 +68,6 @@ HANDMOD = \
 #   | Script : k -> Key k v s s
 #   | Value : k -> Key k v s v.
 MODULES = \
-   Build/Task \
    Build/Store \
    Build/Trace \
    Build/Task/Monad \

examples/build-systems-ala-carte/manual/Build/Task.v

@@ -0,0 +1,51 @@
+(* Default settings (from HsToCoq.Coq.Preamble) *)
+
+Generalizable All Variables.
+
+Unset Implicit Arguments.
+Set Maximal Implicit Insertion.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Require Coq.Program.Tactics.
+Require Coq.Program.Wf.
+
+(* Preamble *)
+
+
+(* No imports to convert. *)
+
+(* Converted type declarations: *)
+Set Universe Polymorphism.
+
+Polymorphic Inductive Task (c : (Type -> Type) -> Type) (k : Type) (v : Type) : Type :=
+  | Mk_Task (run : forall {f}, forall `{c f}, (k -> f v) -> f v) : Task c k v.
+
+Polymorphic Definition Tasks c k v :=
+  (k -> option (Task c k v))%type.
+
+
+Arguments Mk_Task {_} {_} {_} _.
+
+Definition run {c : (Type -> Type) -> Type} {k : Type} {v : Type} (arg_0__
+    : Task c k v) :=
+  let 'Mk_Task run := arg_0__ in
+  run.
+
+(* No value declarations to convert. *)
+
+(* Skipping definition `Build.Task.compose' *)
+
+(* Skipping definition `Build.Task.liftTask' *)
+
+(* Skipping definition `Build.Task.liftTasks' *)
+
+(* External variables:
+     Type option
+*)
+
+
+Definition pidentity {A : Type} (a : A) := a.
+
+Check pidentity.
+Unset Universe Polymorphism.