WIP on Polymorphic Task.

Author: Ian Kariniemi

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/edits

@@ -1,8 +1,2 @@
-skip Build.Task.compose
-
-
-# TODO: Handwrite these
-skip Build.Task.liftTask
-skip Build.Task.liftTasks
 
 rename type GHC.Integer.Type.Integer = GHC.Num.Integer

examples/build-systems-ala-carte/lib/Build/Store.v

@@ -10,6 +10,11 @@ Unset Printing Implicit Defensive.
 Require Coq.Program.Tactics.
 Require Coq.Program.Wf.
 
+(* Preamble *)
+
+Require Import HsToCoq.Unpeel.
+Require Import Coq.ZArith.ZArith.
+
 (* Converted imports: *)
 
 Require GHC.Base.
@@ -46,6 +51,12 @@ Definition values {i} {k} {v} (arg_0__ : Store i k v) :=
   let 'Mk_Store _ values := arg_0__ in
   values.
 
+(* Midamble *)
+
+Instance Unpeel__Hash {A : Type}  : Unpeel (Hash A) A :=
+  {| unpeel := fun hashA : Hash A => match hashA with | Mk_Hash a => a end;
+     repeel := Mk_Hash |}.
+
 (* Converted value declarations: *)
 
 Local Definition Eq___Hash_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
@@ -161,10 +172,10 @@ Program Instance Hashable__Int : Hashable GHC.Num.Int :=
   fun _ k__ => k__ {| hash__ := Hashable__Int_hash |}.
 
 Local Definition Hashable__Integer_hash
-   : GHC.Integer.Type.Integer -> Hash GHC.Integer.Type.Integer :=
+   : GHC.Num.Integer -> Hash GHC.Num.Integer :=
   Mk_Hash.
 
-Program Instance Hashable__Integer : Hashable GHC.Integer.Type.Integer :=
+Program Instance Hashable__Integer : Hashable GHC.Num.Integer :=
   fun _ k__ => k__ {| hash__ := Hashable__Integer_hash |}.
 
 Local Definition Hashable__list_hash {inst_a : Type} `{Hashable inst_a}
@@ -234,6 +245,5 @@ Definition initialise {i : Type} {k : Type} {v : Type}
      GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zl__ GHC.Base.op_zl____
      GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze__ GHC.Base.op_zlze____
      GHC.Base.op_zlztzg____ GHC.Base.op_zsze__ GHC.Base.op_zsze____
-     GHC.Base.op_ztzg____ GHC.Base.pure__ GHC.Integer.Type.Integer GHC.Num.Int
-     GHC.Prim.coerce
+     GHC.Base.op_ztzg____ GHC.Base.pure__ GHC.Num.Int GHC.Num.Integer GHC.Prim.coerce
 *)

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

@@ -0,0 +1 @@
+../../manual/Build/Task.v

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

@@ -0,0 +1,64 @@
+(* 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.
+
+(* Converted imports: *)
+
+Require Build.Store.
+Require Build.Task.
+Require Data.Either.
+Require Data.Maybe.
+Require GHC.Base.
+Import GHC.Base.Notations.
+
+(* No type declarations to convert. *)
+
+(* Converted value declarations: *)
+
+Axiom trackPure : forall {k : Type},
+                  forall {v : Type},
+                  Build.Task.Task GHC.Base.Monad__Dict k v -> (k -> v) -> (v * list k)%type.
+
+Axiom track : forall {m : Type -> Type},
+              forall {k : Type},
+              forall {v : Type},
+              forall `{GHC.Base.Monad__Dict m},
+              Build.Task.Task GHC.Base.Monad__Dict k v ->
+              (k -> m v) -> m (v * list (k * v)%type)%type.
+
+Definition isInput {k : Type} {v : Type}
+   : Build.Task.Tasks GHC.Base.Monad__Dict k v -> k -> bool :=
+  fun tasks => Data.Maybe.isNothing GHC.Base.∘ tasks.
+
+Axiom computePure : forall {k : Type},
+                    forall {v : Type}, Build.Task.Task GHC.Base.Monad__Dict k v -> (k -> v) -> v.
+
+Axiom compute : forall {k : Type},
+                forall {v : Type},
+                forall {i : Type},
+                Build.Task.Task GHC.Base.Monad__Dict k v -> Build.Store.Store i k v -> v.
+
+Axiom liftMaybe : forall {k : Type},
+                  forall {v : Type},
+                  Build.Task.Task GHC.Base.Monad__Dict k v ->
+                  Build.Task.Task GHC.Base.Monad__Dict k (option v).
+
+Axiom liftEither : forall {k : Type},
+                   forall {v : Type},
+                   forall {e : Type},
+                   Build.Task.Task GHC.Base.Monad__Dict k v ->
+                   Build.Task.Task GHC.Base.Monad__Dict k (Data.Either.Either e v).
+
+(* External variables:
+     Type bool list op_zt__ option Build.Store.Store Build.Task.Task Build.Task.Tasks
+     Data.Either.Either Data.Maybe.isNothing GHC.Base.Monad__Dict
+     GHC.Base.op_z2218U__
+*)