diff --git a/base/coq/Free.v b/base/coq/Free.v index 9acf70e7..3756ab2f 100644 --- a/base/coq/Free.v +++ b/base/coq/Free.v @@ -1,6 +1,7 @@ From Base Require Export Free.Class. From Base Require Export Free.ForFree. From Base Require Export Free.Induction. +From Base Require Export Free.Instance.Identity. From Base Require Export Free.Malias. From Base Require Export Free.Monad. From Base Require Export Free.Tactic.ProveInd. diff --git a/base/coq/Free/Class/Normalform.v b/base/coq/Free/Class/Normalform.v index d6e0cb83..f645fcc7 100644 --- a/base/coq/Free/Class/Normalform.v +++ b/base/coq/Free/Class/Normalform.v @@ -5,32 +5,37 @@ From Base Require Import Free.Monad. +From Base Require Import Free.Instance.Identity. + Class Normalform (Shape : Type) (Pos : Shape -> Type) - (A B : Type) := + (A : Type) := { + (** The normalized return type. *) + nType : Type; (** The function is split into two parts due to termination check errors for recursive data types. *) - nf' : A -> Free Shape Pos B + nf' : A -> Free Shape Pos nType }. -Definition nf {Shape : Type} {Pos : Shape -> Type} {A B : Type} - `{Normalform Shape Pos A B} (n : Free Shape Pos A) - : Free Shape Pos B +(* Normalizes a Free value. *) +Definition nf {Shape : Type} {Pos : Shape -> Type} {A : Type} + `{Normalform Shape Pos A} (n : Free Shape Pos A) + : Free Shape Pos nType := n >>= nf'. -Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A B : Type} - `{Normalform Shape Pos A B} +Lemma nfImpure {Shape : Type} {Pos : Shape -> Type} {A : Type} + `{Normalform Shape Pos A} : forall s (pf : _ -> Free Shape Pos A), nf (impure s pf) = impure s (fun p => nf (pf p)). Proof. trivial. Qed. -Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A B : Type} - `{Normalform Shape Pos A B} : forall (x : A), +Lemma nfPure {Shape : Type} {Pos : Shape -> Type} {A : Type} + `{Normalform Shape Pos A} : forall (x : A), nf (pure x) = nf' x. Proof. trivial. Qed. (* Normalform instance for functions. Effects inside of functions are not pulled to the root. *) Instance NormalformFunc (Shape : Type) (Pos : Shape -> Type) (A B : Type) - : Normalform Shape Pos (A -> B) (A -> B) := + : Normalform Shape Pos (A -> B) := { nf' := pure }. diff --git a/base/coq/Free/Handlers.v b/base/coq/Free/Handlers.v index 2992e6cf..dbc54778 100644 --- a/base/coq/Free/Handlers.v +++ b/base/coq/Free/Handlers.v @@ -18,9 +18,9 @@ Require Import Coq.Lists.List. Section NoEffect. (* Identity handler *) - Definition handleNoEffect {A B : Type} - `{Normalform _ _ A B} - (p : Free Identity.Shape Identity.Pos A) : B + Definition handleNoEffect {A : Type} + `{Normalform _ _ A} + (p : Free Identity.Shape Identity.Pos A) := run (nf p). End NoEffect. @@ -32,19 +32,19 @@ Section OneEffect. Definition SMId := Comb.Shape Maybe.Shape Identity.Shape. Definition PMId := Comb.Pos Maybe.Pos Identity.Pos. - Definition handleMaybe {A B : Type} - `{Normalform SMId PMId A B} + Definition handleMaybe {A : Type} + `{Normalform SMId PMId A} (p : Free SMId PMId A) - : option B := run (runMaybe (nf p)). + : option nType := run (runMaybe (nf p)). (* Error :+: Identity handler *) Definition SErrId := Comb.Shape (Error.Shape string) Identity.Shape. Definition PErrId := Comb.Pos (@Error.Pos string) Identity.Pos. - Definition handleError {A B : Type} - `{Normalform SErrId PErrId A B} - (p : Free SErrId PErrId A) : (B + string) + Definition handleError {A : Type} + `{Normalform SErrId PErrId A} + (p : Free SErrId PErrId A) : (nType + string) := run (runError (nf p)). @@ -52,9 +52,9 @@ Section OneEffect. Definition SNDId := Comb.Shape ND.Shape Identity.Shape. Definition PNDId := Comb.Pos ND.Pos Identity.Pos. - Definition handleND {A B : Type} - `{Normalform SNDId PNDId A B} - (p : Free SNDId PNDId A) : list B + Definition handleND {A : Type} + `{Normalform SNDId PNDId A} + (p : Free SNDId PNDId A) : list nType := collectVals (run (runChoice (nf p))). (* Trace :+: Identity handler *) @@ -62,10 +62,10 @@ Section OneEffect. Definition STrcId := Comb.Shape Trace.Shape Identity.Shape. Definition PTrcId := Comb.Pos Trace.Pos Identity.Pos. - Definition handleTrace {A B : Type} - `{Normalform STrcId PTrcId A B} + Definition handleTrace {A : Type} + `{Normalform STrcId PTrcId A} (p : Free STrcId PTrcId A) - : (B * list string) := + : (nType * list string) := collectMessages (run (runTracing (nf p))). (* Share :+: Identity handler *) @@ -73,9 +73,9 @@ Section OneEffect. Definition SShrId := Comb.Shape Share.Shape Identity.Shape. Definition PShrId := Comb.Pos Share.Pos Identity.Pos. - Definition handleShare {A B : Type} - `{Normalform SShrId PShrId A B} - (p : Free SShrId PShrId A) : B := + Definition handleShare {A : Type} + `{Normalform SShrId PShrId A} + (p : Free SShrId PShrId A) : nType := run (runEmptySharing (0,0) (nf p)). End OneEffect. @@ -92,9 +92,9 @@ Section TwoEffects. Definition PShrND := Comb.Pos Share.Pos (Comb.Pos ND.Pos Identity.Pos). - Definition handleShareND {A B : Type} - `{Normalform SShrND PShrND A B} - (p : Free SShrND PShrND A) : (list B) + Definition handleShareND {A : Type} + `{Normalform SShrND PShrND A} + (p : Free SShrND PShrND A) : (list nType) := collectVals (run (runChoice (runNDSharing (0,0) (nf p)))). (* Share :+: Trace :+: Identity handler *) @@ -103,10 +103,10 @@ Section TwoEffects. Definition PShrTrc := Comb.Pos Share.Pos (Comb.Pos Trace.Pos Identity.Pos). - Definition handleShareTrace {A B : Type} - `{Normalform SShrTrc PShrTrc A B} + Definition handleShareTrace {A : Type} + `{Normalform SShrTrc PShrTrc A} (p : Free SShrTrc PShrTrc A) - : (B * list string) := + : (nType * list string) := collectMessages (run (runTracing (runTraceSharing (0,0) (nf p)))). (* Share :+: Maybe :+: Identity handler *) @@ -114,9 +114,9 @@ Section TwoEffects. Definition SShrMaybe := Comb.Shape Share.Shape (Comb.Shape Maybe.Shape Identity.Shape). Definition PShrMaybe := Comb.Pos Share.Pos (Comb.Pos Maybe.Pos Identity.Pos). - Definition handleShareMaybe {A B : Type} - `{Normalform SShrMaybe PShrMaybe A B} - (p : Free SShrMaybe PShrMaybe A) : option B := + Definition handleShareMaybe {A : Type} + `{Normalform SShrMaybe PShrMaybe A} + (p : Free SShrMaybe PShrMaybe A) : option nType := run (runMaybe (runEmptySharing (0,0) (nf p))). (* ND :+: Maybe :+: Identity handler *) @@ -124,10 +124,10 @@ Section TwoEffects. Definition SNDMaybe := Comb.Shape ND.Shape (Comb.Shape Maybe.Shape Identity.Shape). Definition PNDMaybe := Comb.Pos ND.Pos (Comb.Pos Maybe.Pos Identity.Pos). - Definition handleNDMaybe {A B : Type} - `{Normalform SNDMaybe PNDMaybe A B} + Definition handleNDMaybe {A : Type} + `{Normalform SNDMaybe PNDMaybe A} (p : Free SNDMaybe PNDMaybe A) - : option (list B) := match run (runMaybe (runChoice (nf p))) with + : option (list nType) := match run (runMaybe (runChoice (nf p))) with | None => None | Some t => Some (collectVals t) end. @@ -137,10 +137,10 @@ Section TwoEffects. Definition SMaybeTrc := Comb.Shape Maybe.Shape (Comb.Shape Trace.Shape Identity.Shape). Definition PMaybeTrc := Comb.Pos Maybe.Pos (Comb.Pos Trace.Pos Identity.Pos). - Definition handleMaybeTrace {A B : Type} - `{Normalform SMaybeTrc PMaybeTrc A B} + Definition handleMaybeTrace {A : Type} + `{Normalform SMaybeTrc PMaybeTrc A} (p : Free SMaybeTrc PMaybeTrc A) - : option B * list string := + : option nType * list string := collectMessages (run (runTracing (runMaybe (nf p)))). (* Share :+: Error :+: Identity handler *) @@ -148,9 +148,9 @@ Section TwoEffects. Definition SShrErr := Comb.Shape Share.Shape (Comb.Shape (Error.Shape string) Identity.Shape). Definition PShrErr := Comb.Pos Share.Pos (Comb.Pos (@Error.Pos string) Identity.Pos). - Definition handleShareError {A B : Type} - `{Normalform SShrErr PShrErr A B} - (p : Free SShrErr PShrErr A) : (B + string) + Definition handleShareError {A : Type} + `{Normalform SShrErr PShrErr A} + (p : Free SShrErr PShrErr A) : (nType + string) := run (runError (runEmptySharing (0,0) (nf p))). @@ -159,9 +159,9 @@ Section TwoEffects. Definition SNDErr := Comb.Shape ND.Shape (Comb.Shape (Error.Shape string) Identity.Shape). Definition PNDErr := Comb.Pos ND.Pos (Comb.Pos (@Error.Pos string) Identity.Pos). - Definition handleNDError {A B : Type} - `{Normalform SNDErr PNDErr A B} - (p : Free SNDErr PNDErr A) : list B + string + Definition handleNDError {A : Type} + `{Normalform SNDErr PNDErr A} + (p : Free SNDErr PNDErr A) : list nType + string := match run (runError (runChoice (nf p))) with | inl t => inl (collectVals t) | inr e => inr e @@ -175,10 +175,10 @@ Section TwoEffects. Definition SErrorTrc := Comb.Shape (Error.Shape string) (Comb.Shape Trace.Shape Identity.Shape). Definition PErrorTrc := Comb.Pos (@Error.Pos string) (Comb.Pos Trace.Pos Identity.Pos). - Definition handleErrorTrc {A B : Type} - `{Normalform SErrorTrc PErrorTrc A B} + Definition handleErrorTrc {A : Type} + `{Normalform SErrorTrc PErrorTrc A} (p : Free SErrorTrc PErrorTrc A) - : (B + string) * list string + : (nType + string) * list string := collectMessages (run (runTracing (runError (nf p)))). (* Trace :+: ND :+: Identity handler *) @@ -186,12 +186,12 @@ Section TwoEffects. Definition STrcND := Comb.Shape Trace.Shape (Comb.Shape ND.Shape Identity.Shape). Definition PTrcND := Comb.Pos Trace.Pos (Comb.Pos ND.Pos Identity.Pos). - Definition handleTraceND {A B : Type} - `{Normalform STrcND PTrcND A B} + Definition handleTraceND {A : Type} + `{Normalform STrcND PTrcND A} (p : Free STrcND PTrcND A) - : list (B * list string) := - map (@collectMessages B) - (@collectVals (B * list (option Sharing.ID * string)) + : list (nType * list string) := + map (@collectMessages nType) + (@collectVals (nType * list (option Sharing.ID * string)) (run (runChoice (runTracing (nf p))))). End TwoEffects. @@ -214,13 +214,13 @@ Section ThreeEffects. (Comb.Pos ND.Pos (Comb.Pos Maybe.Pos Identity.Pos)). - Definition handleShareNDMaybe {A B : Type} - `{Normalform SShrNDMaybe PShrNDMaybe A B} + Definition handleShareNDMaybe {A : Type} + `{Normalform SShrNDMaybe PShrNDMaybe A} (p : Free SShrNDMaybe PShrNDMaybe A) - : option (list B) := + : option (list nType) := match (run (runMaybe (runChoice (runNDSharing (0,0) (nf p))))) with | None => None - | Some t => Some (@collectVals B t) + | Some t => Some (@collectVals nType t) end. (* Maybe :+: Share :+: Trace :+: Identity handler *) @@ -235,10 +235,10 @@ Section ThreeEffects. (Comb.Pos Share.Pos (Comb.Pos Trace.Pos Identity.Pos)). - Definition handleMaybeShareTrace {A B : Type} - `{Normalform SMaybeShrTrc PMaybeShrTrc A B} + Definition handleMaybeShareTrace {A : Type} + `{Normalform SMaybeShrTrc PMaybeShrTrc A} (p : Free SMaybeShrTrc PMaybeShrTrc A) - : option B * list string := + : option nType * list string := collectMessages (run (runTracing (runTraceSharing (0,0) (runMaybe (nf p))))). @@ -254,10 +254,10 @@ Section ThreeEffects. (Comb.Pos Maybe.Pos (Comb.Pos Trace.Pos Identity.Pos)). - Definition handleNDMaybeTrc {A B : Type} - `{Normalform SNDMaybeTrc PNDMaybeTrc A B} + Definition handleNDMaybeTrc {A : Type} + `{Normalform SNDMaybeTrc PNDMaybeTrc A} (p : Free SNDMaybeTrc PNDMaybeTrc A) - : (option (list B) * list string) := + : (option (list nType) * list string) := let (val,log) := (collectMessages (run (runTracing (runMaybe (runChoice (nf p)))))) in match val with | None => (None, log) @@ -277,10 +277,10 @@ Section ThreeEffects. (Comb.Pos ND.Pos (Comb.Pos (@Error.Pos string) Identity.Pos)). - Definition handleShareNDError {A B : Type} - `{Normalform SShrNDErr PShrNDErr A B} + Definition handleShareNDError {A : Type} + `{Normalform SShrNDErr PShrNDErr A} (p : Free SShrNDErr PShrNDErr A) - : list B + string + : list nType + string := match run (runError (runChoice (runNDSharing (0,0) (nf p)))) with | inl t => inl (collectVals t) | inr e => inr e @@ -298,10 +298,10 @@ Section ThreeEffects. (Comb.Pos Share.Pos (Comb.Pos Trace.Pos Identity.Pos)). - Definition handleErrorShareTrace {A B : Type} - `{Normalform SErrShrTrc PErrShrTrc A B} + Definition handleErrorShareTrace {A : Type} + `{Normalform SErrShrTrc PErrShrTrc A} (p : Free SErrShrTrc PErrShrTrc A) - : (B + string) * list string + : (nType + string) * list string := collectMessages (run (runTracing (runTraceSharing (0,0) (runError (nf p))))). (* ND :+: Error :+: Trace :+: Identity handler *) @@ -316,10 +316,10 @@ Section ThreeEffects. (Comb.Pos (@Error.Pos string) (Comb.Pos Trace.Pos Identity.Pos)). - Definition handleNDErrorTrace {A B : Type} - `{Normalform SNDErrTrc PNDErrTrc A B} + Definition handleNDErrorTrace {A : Type} + `{Normalform SNDErrTrc PNDErrTrc A} (p : Free SNDErrTrc PNDErrTrc A) - : (list B + string) * list string + : (list nType + string) * list string := match collectMessages (run (runTracing (runError (runChoice (nf p))))) with | (inl t, log) => (inl (collectVals t), log) | (inr e, log) => (inr e, log) diff --git a/base/coq/Free/Instance/Identity.v b/base/coq/Free/Instance/Identity.v index ed7c2d79..240aaf1e 100644 --- a/base/coq/Free/Instance/Identity.v +++ b/base/coq/Free/Instance/Identity.v @@ -1,7 +1,7 @@ (** * Definition of the identity monad in terms of the free monad. *) -From Base Require Import Free. -From Base Require Import Free.Instance.Comb. +From Base Require Import Free.Class.Injectable. +From Base Require Import Free.Monad. From Base Require Import Free.Util.Void. Module Identity. diff --git a/base/coq/Prelude/Bool.v b/base/coq/Prelude/Bool.v index 8a1d46c7..df91ac78 100644 --- a/base/coq/Prelude/Bool.v +++ b/base/coq/Prelude/Bool.v @@ -40,7 +40,7 @@ End SecBool. (* Normalform instance for Bool *) Instance NormalformBool (Shape : Type) (Pos : Shape -> Type) - : Normalform Shape Pos (Bool Shape Pos) (Bool Identity.Shape Identity.Pos) + : Normalform Shape Pos (Bool Shape Pos) := { nf' := pure }. (* ShareableArgs instance for Bool *) diff --git a/base/coq/Prelude/Integer.v b/base/coq/Prelude/Integer.v index dd4c7409..f6201b91 100644 --- a/base/coq/Prelude/Integer.v +++ b/base/coq/Prelude/Integer.v @@ -99,7 +99,7 @@ End SecInteger. (* Normalform instance for Integer *) Instance NormalformInteger (Shape : Type) (Pos : Shape -> Type) - : Normalform Shape Pos (Integer Shape Pos) (Integer Identity.Shape Identity.Pos) + : Normalform Shape Pos (Integer Shape Pos) := { nf' := pure }. (* ShareableArgs instance for Integer *) diff --git a/base/coq/Prelude/List.v b/base/coq/Prelude/List.v index bdab5f69..c4bdb112 100644 --- a/base/coq/Prelude/List.v +++ b/base/coq/Prelude/List.v @@ -43,24 +43,25 @@ Section SecListNF. Variable Shape : Type. Variable Pos : Shape -> Type. - Variable A B : Type. + Variable A : Type. - Fixpoint nf'List `{Normalform Shape Pos A B} + Fixpoint nf'List `{Normalform Shape Pos A} (l : List Shape Pos A) - : Free Shape Pos (List Identity.Shape Identity.Pos B) + : Free Shape Pos (List Identity.Shape Identity.Pos nType) := match l with | nil => pure nil | cons fx fxs => nf fx >>= fun nx => fxs >>= fun xs => nf'List xs >>= fun nxs => - pure (cons (pure nx) (pure nxs)) + pure (cons (pure nx) + (pure nxs)) end. - Global Instance NormalformList `{Normalform Shape Pos A B} + Global Instance NormalformList `{Normalform Shape Pos A} : Normalform Shape Pos (List Shape Pos A) - (List Identity.Shape Identity.Pos B) := { nf' := nf'List }. + End SecListNF. diff --git a/base/coq/Prelude/Pair.v b/base/coq/Prelude/Pair.v index 5a0728f2..1066504a 100644 --- a/base/coq/Prelude/Pair.v +++ b/base/coq/Prelude/Pair.v @@ -2,6 +2,8 @@ From Base Require Import Free. From Base Require Import Free.Instance.Identity. From Base Require Import Free.Malias. +From Base Require Import Prelude.Bool. + Section SecPair. Variable Shape : Type. Variable Pos : Shape -> Type. @@ -30,22 +32,22 @@ Section SecNFPair. Variable Shape : Type. Variable Pos : Shape -> Type. - Variable A B C D : Type. + Variable A B : Type. - Definition nf'Pair `{Normalform Shape Pos A C} - `{Normalform Shape Pos B D} + Definition nf'Pair `{Normalform Shape Pos A} + `{Normalform Shape Pos B} (p : Pair Shape Pos A B) - : Free Shape Pos (Pair Identity.Shape Identity.Pos C D) + : Free Shape Pos (Pair Identity.Shape Identity.Pos + (@nType Shape Pos A _) (@nType Shape Pos B _)) := match p with | pair_ fa fb => nf fa >>= fun na => nf fb >>= fun nb => pure (pair_ (pure na) (pure nb)) end. - Global Instance NormalformPair `{Normalform Shape Pos A C} - `{Normalform Shape Pos B D} + Global Instance NormalformPair `{Normalform Shape Pos A} + `{Normalform Shape Pos B} : Normalform Shape Pos (Pair Shape Pos A B) - (Pair Identity.Shape Identity.Pos C D) := { nf' := nf'Pair }. End SecNFPair. diff --git a/base/coq/Prelude/Unit.v b/base/coq/Prelude/Unit.v index a03dedf8..d29969dd 100644 --- a/base/coq/Prelude/Unit.v +++ b/base/coq/Prelude/Unit.v @@ -26,7 +26,7 @@ Notation "'@Tt' Shape Pos" := (@pure Shape Pos unit tt) (* Normalform instance for Unit *) Instance NormalformUnit (Shape : Type) (Pos : Shape -> Type) - : Normalform Shape Pos (Unit Shape Pos) (Unit Identity.Shape Identity.Pos) + : Normalform Shape Pos (Unit Shape Pos) := { nf' := pure }. (* ShareableArgs instance for Unit *) diff --git a/example/Proofs/TypeclassInstances.hs b/example/Proofs/TypeclassInstances.hs new file mode 100644 index 00000000..6d6cf90c --- /dev/null +++ b/example/Proofs/TypeclassInstances.hs @@ -0,0 +1,81 @@ +-- | This example defines some data types to check whether the [Normalform] +-- and [ShareableArgs] instances are generated correctly. +module Proofs.TypeclassInstances where + +-- Prelude head function +head :: [a] -> a +head (x : _) = x + +-- Basic recursive data type. +data MyList a = MyNil | MyCons a (MyList a) + +-- Custom head function. +myHead :: MyList a -> a +myHead (MyCons x _) = x + +-- Mutually recursive data types. +data Foo a = Foo (Bar a) + +data Bar a = Bar (Foo a) | Baz + +-- Data type with 'hidden' recursion. +data Tree a = Leaf | Branch a [Tree a] + +-- The root of a non-empty tree. +root :: Tree a -> a +root (Branch x _) = x + +-- The root of the leftmost child of a tree with a non-empty leftmost child. +headRoot :: Tree a -> a +headRoot (Branch _ ts) = root (head ts) + +-- Data type with multiple type vars. +data Map k v = Empty | Entry k v (Map k v) + +-- The first entry of a non-empty map. +firstMapEntry :: Map k v -> v +firstMapEntry (Entry _ v _) = v + +-- A function that shares a data structure, transforms +-- it into a Bool twice and connects the results with a +-- disjunction. +doubleDisjunction :: a -> (a -> Bool) -> Bool +doubleDisjunction x f = let y = x + in f y || f y + +-- doubleDisjunction specialized for MyList. +doubleDisjunctionHead :: MyList Bool -> Bool +doubleDisjunctionHead l = doubleDisjunction l myHead + +-- doubleDisjunction specialized for Tree. +doubleDisjunctionRoot :: Tree Bool -> Bool +doubleDisjunctionRoot t = doubleDisjunction t root + +-- doubleDisjunction specialized for Tree. +doubleDisjunctionHeadRoot :: Tree Bool -> Bool +doubleDisjunctionHeadRoot t = doubleDisjunction t headRoot + +-- doubleDisjunction specialized for Map. +doubleDisjunctionMap :: Map Bool Bool -> Bool +doubleDisjunctionMap m = doubleDisjunction m firstMapEntry + +-- Additional data types to check that the generated +-- instances are valid Coq code. +--Types with potential name conflict. +data T a = TCons a + +data T_ = T_Cons + +-- Type with nested recursion and type variable instantiation. +data Rose a = Rose (Rose Integer, Rose a) + +-- Mutually recursive types with nested recursion and type variable +-- instantiation. +data A a = ConsA [B Bool] | AVal a + +data B a = ConsB [A Bool] | BVal a + +-- Indirect recursion hidden in a type synonym. +type IntGatherings = MyList (Gathering Integer) + +data Gathering a = Many IntGatherings | Single a diff --git a/example/Proofs/TypeclassInstancesProofs.v b/example/Proofs/TypeclassInstancesProofs.v new file mode 100644 index 00000000..c79c7600 --- /dev/null +++ b/example/Proofs/TypeclassInstancesProofs.v @@ -0,0 +1,180 @@ +(* This file includes some examples that show the normalisation of + some data types in a nondeterministic context. *) + +From Base Require Import Free. +From Base Require Import Free.Handlers. +From Base Require Import Free.Instance.Identity. +From Base Require Import Free.Instance.ND. +From Base Require Import Free.Util.Search. +From Base Require Import Prelude. + +From Generated Require Import Proofs.TypeclassInstances. + +Require Import Lists.List. +Import List.ListNotations. + +(* Shortcuts for the Identity effect (i.e. the lack of an effect). *) +Notation IdS := Identity.Shape. +Notation IdP := Identity.Pos. + +Section Data. + + Variable Shape : Type. + Variable Pos : Shape -> Type. + + Notation "'ND'" := (Injectable ND.Shape ND.Pos Shape Pos). + + Notation Bool_ := (Bool Shape Pos). + Notation True' := (True_ Shape Pos). + Notation False' := (False_ Shape Pos). + + Notation "x ? y" := (Choice Shape Pos x y) (at level 50). + + (* true : ([] ? [true ? false]) *) + Definition ndList `{ND} : Free Shape Pos (MyList Shape Pos Bool_) + := MyCons Shape Pos + True' + ( MyNil Shape Pos + ? MyCons Shape Pos + (True' ? False') + (MyNil Shape Pos)). + + (* [true ? false] *) + Definition ndList2 `{ND} : Free Shape Pos (MyList Shape Pos Bool_) + := MyCons Shape Pos + (True' ? False') + (MyNil Shape Pos). + + (* (foo (bar (foo baz))) ? (foo baz) *) + Definition ndFoo `{ND} : Free Shape Pos (Foo Shape Pos Bool_) + := Foo0 Shape Pos + ( Bar0 Shape Pos + (Foo0 Shape Pos + (Baz Shape Pos)) + ? Baz Shape Pos). + + (* branch (true ? false) (leaf : ([] ? [leaf])) *) + Definition ndTree `{ND} : Free Shape Pos (Tree Shape Pos Bool_) + := Branch Shape Pos + (True' ? False') + (Cons Shape Pos + (Leaf Shape Pos) + (Nil Shape Pos + ? Cons Shape Pos + (Leaf Shape Pos) + (Nil Shape Pos))). + + (* branch true [branch true ? false []] *) + Definition ndTree2 `{ND} : Free Shape Pos (Tree Shape Pos Bool_) + := Branch Shape Pos + True' + (Cons Shape Pos + (Branch Shape Pos (True' ? False') (Nil Shape Pos)) + (Nil Shape Pos)). + + (* (true -> (true ? false)) : ([] ? [(true ? false) -> false]) *) + Definition ndMap `{ND} : Free Shape Pos (Map Shape Pos Bool_ Bool_) + := Entry0 Shape Pos + True' + (True' ? False') + ( Empty Shape Pos + ? Entry0 Shape Pos + (True' ? False') + False' + (Empty Shape Pos)). + +End Data. + +Arguments ndList {_} {_} {_}. +Arguments ndList2 {_} {_} {_}. +Arguments ndFoo {_} {_} {_}. +Arguments ndTree {_} {_} {_}. +Arguments ndTree2 {_} {_} {_}. +Arguments ndMap {_} {_} {_}. + +(* Tests for the generated Normalform instances. *) + +(* true : ([] ? [true ? false]) + --> [ [true], [true, true], [true, false] ] *) +Example nondeterministic_list : handleND ndList + = [ myCons (pure true) (MyNil IdS IdP) + ; myCons (pure true) (MyCons IdS IdP (pure true) (MyNil IdS IdP)) + ; myCons (pure true) (MyCons IdS IdP (pure false) (MyNil IdS IdP)) + ]. +Proof. trivial. Qed. + +(* (foo baz) ? (foo (bar (foo baz))) + --> [ foo baz, foo (bar (foo baz)) ] *) +Example nondeterministic_foo : handleND ndFoo + = [ foo (Bar0 IdS IdP (Foo0 IdS IdP (Baz IdS IdP))) + ; foo (Baz IdS IdP) + ]. +Proof. trivial. Qed. + +(* branch (true ? false) (leaf : ([] ? [leaf])) + --> [ branch true leaf, branch true [leaf, leaf] + , branch false leaf, branch false [leaf, leaf] ] *) +Example nondeterministic_tree : handleND ndTree + = [ branch (pure true) (Cons IdS IdP (Leaf IdS IdP) (Nil IdS IdP)) + ; branch (pure true) (Cons IdS IdP (Leaf IdS IdP) + (Cons IdS IdP (Leaf IdS IdP) (Nil IdS IdP))) + ; branch (pure false) (Cons IdS IdP (Leaf IdS IdP) (Nil IdS IdP)) + ; branch (pure false) (Cons IdS IdP (Leaf IdS IdP) + (Cons IdS IdP (Leaf IdS IdP) (Nil IdS IdP))) + ]. +Proof. trivial. Qed. + +(* (true -> (true ? false)) : ([] ? [(true ? false) -> false]) + --> [ [true -> true] , [true -> true, true -> false] + , [true -> true, false -> false], [false -> true] + , [false -> true, true -> false], [false -> true, false -> false] ] *) +Example nondeterministic_map : handleND ndMap + = [ entry (pure true) (pure true) (Empty IdS IdP) + ; entry (pure true) (pure true) + (Entry0 IdS IdP (pure true) (pure false) (Empty IdS IdP)) + ; entry (pure true) (pure true) + (Entry0 IdS IdP (pure false) (pure false) (Empty IdS IdP)) + ; entry (pure true) (pure false) (Empty IdS IdP) + ; entry (pure true) (pure false) + (Entry0 IdS IdP (pure true) (pure false) (Empty IdS IdP)) + ; entry (pure true) (pure false) + (Entry0 IdS IdP (pure false) (pure false) (Empty IdS IdP)) + ]. +Proof. trivial. Qed. + +(* Tests for the generated ShareableArgs instances. *) + +(* let x = [true ? false] in myHead x || myHead x + --> true || true ? false || false + --> true ? false *) +Example deepSharingNDList +: handleShareND (doubleDisjunctionHead _ _ (Cbneed _ _) (ND.Partial _ _) ndList2) += [true;false]. +Proof. trivial. Qed. + +(* let x = branch (true ? false) (leaf : ([] ? [leaf])) + in root x || root x + --> true || true ? false || false + --> true ? false *) +Example deepSharingNDTree +: handleShareND (doubleDisjunctionRoot _ _ (Cbneed _ _) (ND.Partial _ _) ndTree) += [true;false]. +Proof. trivial. Qed. + +(* let x = branch true [branch true ? false []] + in headRoot x || headRoot x + --> true || true ? false || false + --> true ? false *) +Example deepSharingNDTree2 +: handleShareND (doubleDisjunctionHeadRoot _ _ (Cbneed _ _) (ND.Partial _ _) ndTree2) += [true;false]. +Proof. trivial. Qed. + +(* let x = true -> (true ? false)) : ([] ? [(true ? false) -> false] + in firstMapEntry x || firstMapEntry x + --> true || true ? false || false + --> true ? false *) +Example deepSharingNDMap +: handleShareND (doubleDisjunctionMap _ _ (Cbneed _ _) (ND.Partial _ _) ndMap) += [true;false]. +Proof. trivial. Qed. diff --git a/free-compiler.cabal b/free-compiler.cabal index a454e957..acba05b6 100644 --- a/free-compiler.cabal +++ b/free-compiler.cabal @@ -114,6 +114,8 @@ library freec-internal , FreeC.Backend.Coq.Converter.Module , FreeC.Backend.Coq.Converter.Type , FreeC.Backend.Coq.Converter.TypeDecl + , FreeC.Backend.Coq.Converter.TypeDecl.InductionScheme + , FreeC.Backend.Coq.Converter.TypeDecl.TypeclassInstances , FreeC.Backend.Coq.Keywords , FreeC.Backend.Coq.Pretty , FreeC.Backend.Coq.Syntax diff --git a/src/lib/FreeC/Backend/Coq/Base.hs b/src/lib/FreeC/Backend/Coq/Base.hs index 1df123ac..290ab768 100644 --- a/src/lib/FreeC/Backend/Coq/Base.hs +++ b/src/lib/FreeC/Backend/Coq/Base.hs @@ -9,10 +9,14 @@ module FreeC.Backend.Coq.Base , free , shape , pos + , idShape + , idPos , freePureCon , freeImpureCon , freeBind , freeArgs + , shapeIdent + , posIdent , forFree -- * Partiality , partial @@ -28,8 +32,15 @@ module FreeC.Backend.Coq.Base , strategyArg , shareableArgs , shareableArgsBinder + , shareArgs + , normalform + , normalformBinder + , nf' + , nf + , nType , implicitArg , share + , cbneed , call -- * Effect Selection , selectExplicitArgs @@ -87,6 +98,14 @@ pos = Coq.Bare posIdent posIdent :: Coq.Ident posIdent = Coq.ident "Pos" +-- | The Coq identifier for the @Identity@ shape. +idShape :: Coq.Qualid +idShape = Coq.Qualified (Coq.ident "Identity") shapeIdent + +-- | The Coq identifier for the @Identity@ position function. +idPos :: Coq.Qualid +idPos = Coq.Qualified (Coq.ident "Identity") posIdent + -- | The Coq identifier for the @pure@ constructor of the @Free@ monad. freePureCon :: Coq.Qualid freePureCon = Coq.bare "pure" @@ -143,6 +162,7 @@ partialError = Coq.bare "error" qualifiedSmartConstructorModule :: Coq.Ident qualifiedSmartConstructorModule = Coq.ident "QualifiedSmartConstructorModule" +------------------------------------------------------------------------------- -- Sharing -- ------------------------------------------------------------------------------- -- | The Coq identifier for the @Share@ module. @@ -176,7 +196,7 @@ strategyBinder :: Coq.Binder strategyBinder = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit strategyArg $ Coq.app (Coq.Qualid strategy) [Coq.Qualid shape, Coq.Qualid pos] --- | The Coq binder for the @ShareableArgs@ type class. +-- | The Coq identifier for the @ShareableArgs@ type class. shareableArgs :: Coq.Qualid shareableArgs = Coq.bare "ShareableArgs" @@ -187,6 +207,10 @@ shareableArgsBinder typeArg = Coq.Generalized Coq.Implicit $ Coq.app (Coq.Qualid shareableArgs) $ map Coq.Qualid [shape, pos, typeArg] +-- | The Coq identifier of the @ShareableArgs@ class function. +shareArgs :: Coq.Qualid +shareArgs = Coq.bare "shareArgs" + -- | The Coq identifier for an implicit argument. implicitArg :: Coq.Term implicitArg = Coq.Underscore @@ -199,6 +223,36 @@ share = Coq.bare "share" call :: Coq.Qualid call = Coq.bare "call" +-- | The Coq identifier for the @cbneed@ operator. +cbneed :: Coq.Qualid +cbneed = Coq.bare "cbneed" + +------------------------------------------------------------------------------- +-- Handling -- +------------------------------------------------------------------------------- +-- | The Coq identifier for the @Normalform@ type class. +normalform :: Coq.Qualid +normalform = Coq.bare "Normalform" + +-- | The Coq binder for the @Normalform@ type class with the source and target +-- type variable with the given names. +normalformBinder :: Coq.Qualid -> Coq.Binder +normalformBinder sourceType = Coq.Generalized Coq.Implicit + $ Coq.app (Coq.Qualid normalform) + $ map Coq.Qualid [shape, pos, sourceType] + +-- | The Coq identifier of the @Normalform@ class function. +nf' :: Coq.Qualid +nf' = Coq.bare "nf'" + +-- | The Coq identifier of the function @nf@. +nf :: Coq.Qualid +nf = Coq.bare "nf" + +-- | The Coq identifier for a normalized type. +nType :: Coq.Qualid +nType = Coq.bare "nType" + ------------------------------------------------------------------------------- -- Effect selection -- ------------------------------------------------------------------------------- @@ -272,7 +326,12 @@ reservedIdents , strategy , strategyArg , shareableArgs + , shareArgs + , normalform + , nf' + , nf , share , call + , cbneed ] ++ map fst freeArgs diff --git a/src/lib/FreeC/Backend/Coq/Converter/Free.hs b/src/lib/FreeC/Backend/Coq/Converter/Free.hs index c482e4f9..163a7ade 100644 --- a/src/lib/FreeC/Backend/Coq/Converter/Free.hs +++ b/src/lib/FreeC/Backend/Coq/Converter/Free.hs @@ -48,7 +48,7 @@ genericApply' -> [Coq.Term] -- ^ The implicit type class instances to pass to the callee. -> [Coq.Term] -- ^ Implicit arguments to pass explicitly to the callee. -> [Coq.Term] -- ^ The implicit type class arguments that are dependent on - -- the implicit argumnets. + -- the implicit arguments. -> [Coq.Term] -- ^ The actual arguments of the callee. -> Coq.Term genericApply' func explicitEffectArgs implicitEffectArgs implicitArgs diff --git a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs index 842f27c0..6a3cba2d 100644 --- a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs +++ b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs @@ -13,26 +13,33 @@ module FreeC.Backend.Coq.Converter.TypeDecl , convertDataDecl ) where -import Control.Monad ( mapAndUnzipM ) -import Control.Monad.Extra ( concatMapM ) -import Data.List ( partition ) -import Data.List.Extra ( concatUnzip ) -import qualified Data.List.NonEmpty as NonEmpty -import Data.Maybe ( catMaybes, fromJust ) -import qualified Data.Set as Set -import qualified Data.Text as Text +import Control.Monad + ( mapAndUnzipM ) +import Control.Monad.Extra + ( concatMapM ) +import Data.List + ( partition ) +import Data.List.Extra + ( concatUnzip ) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe + ( catMaybes, fromJust ) +import qualified Data.Set as Set -import qualified FreeC.Backend.Coq.Base as Coq.Base +import qualified FreeC.Backend.Coq.Base as Coq.Base import FreeC.Backend.Coq.Converter.Arg import FreeC.Backend.Coq.Converter.Free import FreeC.Backend.Coq.Converter.Type -import qualified FreeC.Backend.Coq.Syntax as Coq +import FreeC.Backend.Coq.Converter.TypeDecl.InductionScheme +import FreeC.Backend.Coq.Converter.TypeDecl.TypeclassInstances +import qualified FreeC.Backend.Coq.Syntax as Coq import FreeC.Environment import FreeC.Environment.Fresh - ( freshArgPrefix, freshCoqIdent, freshCoqQualid ) -import FreeC.Environment.Renamer ( renameAndDefineTypeVar ) + ( freshArgPrefix, freshCoqIdent ) +import FreeC.Environment.Renamer + ( renameAndDefineTypeVar ) import FreeC.IR.DependencyGraph -import qualified FreeC.IR.Syntax as IR +import qualified FreeC.IR.Syntax as IR import FreeC.IR.TypeSynExpansion import FreeC.Monad.Converter import FreeC.Monad.Reporter @@ -127,11 +134,12 @@ convertDataDecls :: [IR.TypeDecl] -> Converter ([Coq.Sentence], [Coq.Sentence]) convertDataDecls dataDecls = do (indBodies, extraSentences') <- mapAndUnzipM convertDataDecl dataDecls let (extraSentences, qualSmartConDecls) = concatUnzip extraSentences' + instances <- generateTypeclassInstances dataDecls return ( Coq.comment ("Data type declarations for " ++ showPretty (map IR.typeDeclName dataDecls)) : Coq.InductiveSentence (Coq.Inductive (NonEmpty.fromList indBodies) []) - : extraSentences + : extraSentences ++ instances , qualSmartConDecls ) @@ -144,26 +152,27 @@ convertDataDecls dataDecls = do -- not visible outside of this function. convertDataDecl :: IR.TypeDecl -> Converter (Coq.IndBody, ([Coq.Sentence], [Coq.Sentence])) -convertDataDecl (IR.DataDecl _ (IR.DeclIdent _ name) typeVarDecls conDecls) = do - (body, argumentsSentences) <- generateBodyAndArguments - (smartConDecls, qualSmartConDecls) - <- concatUnzip <$> mapM generateSmartConDecl conDecls - inductionScheme <- generateInductionScheme - return ( body - , ( Coq.commentedSentences - ("Arguments sentences for " ++ showPretty (IR.toUnQual name)) - argumentsSentences - ++ Coq.commentedSentences - ("Induction scheme for " ++ showPretty (IR.toUnQual name)) - inductionScheme - ++ Coq.commentedSentences - ("Smart constructors for " ++ showPretty (IR.toUnQual name)) - smartConDecls - , Coq.commentedSentences ("Qualified smart constructors for " - ++ showPretty (IR.toUnQual name)) - qualSmartConDecls - ) - ) +convertDataDecl + dataDecl@(IR.DataDecl _ (IR.DeclIdent _ name) typeVarDecls conDecls) = do + (body, argumentsSentences) <- generateBodyAndArguments + (smartConDecls, qualSmartConDecls) + <- concatUnzip <$> mapM generateSmartConDecl conDecls + inductionScheme <- generateInductionScheme dataDecl + return ( body + , ( Coq.commentedSentences + ("Arguments sentences for " ++ showPretty (IR.toUnQual name)) + argumentsSentences + ++ Coq.commentedSentences + ("Induction scheme for " ++ showPretty (IR.toUnQual name)) + inductionScheme + ++ Coq.commentedSentences + ("Smart constructors for " ++ showPretty (IR.toUnQual name)) + smartConDecls + , Coq.commentedSentences ("Qualified smart constructors for " + ++ showPretty (IR.toUnQual name)) + qualSmartConDecls + ) + ) where -- | Generates the body of the @Inductive@ sentence and the @Arguments@ -- sentences for the constructors but not the smart constructors @@ -298,79 +307,6 @@ convertDataDecl (IR.DataDecl _ (IR.DeclIdent _ name) typeVarDecls conDecls) = do , Coq.sModLevel 10 , Coq.sModIdentLevel (NonEmpty.fromList expArgIdents) (Just 9) ] - - -- | Generates an induction scheme for the data type. - generateInductionScheme :: Converter [Coq.Sentence] - generateInductionScheme = localEnv $ do - Just tIdent <- inEnv $ lookupIdent IR.TypeScope name - -- Create variables and binders. - let generateArg :: Coq.Term -> Converter (Coq.Qualid, Coq.Binder) - generateArg argType = do - ident <- freshCoqQualid freshArgPrefix - return - $ ( ident - , Coq.typedBinder Coq.Ungeneralizable Coq.Explicit [ident] argType - ) - (tvarIdents, tvarBinders) <- convertTypeVarDecls' Coq.Explicit typeVarDecls - (propIdent, propBinder) <- generateArg - (Coq.Arrow (genericApply tIdent [] [] (map Coq.Qualid tvarIdents)) - (Coq.Sort Coq.Prop)) - (_hIdents, hBinders) <- mapAndUnzipM (generateInductionCase propIdent) - conDecls - (valIdent, valBinder) <- generateArg - (genericApply tIdent [] [] (map Coq.Qualid tvarIdents)) - -- Stick everything together. - schemeName <- freshCoqQualid $ fromJust (Coq.unpackQualid tIdent) ++ "_Ind" - hypothesisVar <- freshCoqIdent "H" - let binders = genericArgDecls Coq.Explicit - ++ tvarBinders - ++ [propBinder] - ++ hBinders - term = Coq.Forall (NonEmpty.fromList [valBinder]) - (Coq.app (Coq.Qualid propIdent) [Coq.Qualid valIdent]) - scheme = Coq.Assertion Coq.Definition schemeName binders term - proof = Coq.ProofDefined - (Text.pack - $ " fix " - ++ hypothesisVar - ++ " 1; intro; " - ++ fromJust (Coq.unpackQualid Coq.Base.proveInd) - ++ ".") - return [Coq.AssertionSentence scheme proof] - - -- | Generates an induction case for a given property and constructor. - generateInductionCase - :: Coq.Qualid -> IR.ConDecl -> Converter (Coq.Qualid, Coq.Binder) - generateInductionCase pIdent (IR.ConDecl _ declIdent argTypes) = do - let conName = IR.declIdentName declIdent - Just conIdent <- inEnv $ lookupIdent IR.ValueScope conName - Just conType' <- inEnv $ lookupReturnType IR.ValueScope conName - conType <- convertType' conType' - fConType <- convertType conType' - fArgTypes <- mapM convertType argTypes - (argIdents, argBinders) <- mapAndUnzipM convertAnonymousArg - (map Just argTypes) - let - -- We need an induction hypothesis for every argument that has the same - -- type as the constructor but lifted into the free monad. - addHypotheses' :: [(Coq.Term, Coq.Qualid)] -> Coq.Term -> Coq.Term - addHypotheses' [] = id - addHypotheses' ((argType, argIdent) : args) - | argType == fConType = Coq.Arrow - (genericForFree conType pIdent argIdent) - . addHypotheses' args - addHypotheses' (_ : args) = addHypotheses' args - addHypotheses = addHypotheses' (zip fArgTypes argIdents) - -- Create induction case. - term = addHypotheses - (Coq.app (Coq.Qualid pIdent) - [Coq.app (Coq.Qualid conIdent) (map Coq.Qualid argIdents)]) - indCase = if null argBinders - then term - else Coq.Forall (NonEmpty.fromList argBinders) term - indCaseIdent <- freshCoqQualid freshArgPrefix - indCaseBinder <- generateArgBinder indCaseIdent (Just indCase) - return (indCaseIdent, indCaseBinder) -- Type synonyms are not allowed in this function. convertDataDecl (IR.TypeSynDecl _ _ _ _) = error "convertDataDecl: Type synonym not allowed." diff --git a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/InductionScheme.hs b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/InductionScheme.hs new file mode 100644 index 00000000..824cb170 --- /dev/null +++ b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/InductionScheme.hs @@ -0,0 +1,97 @@ +-- | This module contains functions to generate induction schemes for +-- user-defined data types. +module FreeC.Backend.Coq.Converter.TypeDecl.InductionScheme + ( generateInductionScheme + ) where + +import Control.Monad ( mapAndUnzipM ) +import qualified Data.List.NonEmpty as NonEmpty +import Data.Maybe ( fromJust ) +import qualified Data.Text as Text + +import qualified FreeC.Backend.Coq.Base as Coq.Base +import FreeC.Backend.Coq.Converter.Arg +import FreeC.Backend.Coq.Converter.Free +import FreeC.Backend.Coq.Converter.Type +import qualified FreeC.Backend.Coq.Syntax as Coq +import FreeC.Environment +import FreeC.Environment.Fresh + ( freshArgPrefix, freshCoqIdent, freshCoqQualid ) +import qualified FreeC.IR.Syntax as IR +import FreeC.Monad.Converter + +-- | Generates an induction scheme for the given data type. +generateInductionScheme :: IR.TypeDecl -> Converter [Coq.Sentence] +generateInductionScheme + (IR.DataDecl _ (IR.DeclIdent _ name) typeVarDecls conDecls) = localEnv $ do + Just tIdent <- inEnv $ lookupIdent IR.TypeScope name + -- Create variables and binders. + let generateArg :: Coq.Term -> Converter (Coq.Qualid, Coq.Binder) + generateArg argType = do + ident <- freshCoqQualid freshArgPrefix + return + $ ( ident + , Coq.typedBinder Coq.Ungeneralizable Coq.Explicit [ident] argType + ) + (tvarIdents, tvarBinders) <- convertTypeVarDecls' Coq.Explicit typeVarDecls + (propIdent, propBinder) <- generateArg + (Coq.Arrow (genericApply tIdent [] [] (map Coq.Qualid tvarIdents)) + (Coq.Sort Coq.Prop)) + (_hIdents, hBinders) <- mapAndUnzipM (generateInductionCase propIdent) + conDecls + (valIdent, valBinder) <- generateArg + (genericApply tIdent [] [] (map Coq.Qualid tvarIdents)) + -- Stick everything together. + schemeName <- freshCoqQualid $ fromJust (Coq.unpackQualid tIdent) ++ "_Ind" + hypothesisVar <- freshCoqIdent "H" + let binders = genericArgDecls Coq.Explicit + ++ tvarBinders + ++ [propBinder] + ++ hBinders + term = Coq.Forall (NonEmpty.fromList [valBinder]) + (Coq.app (Coq.Qualid propIdent) [Coq.Qualid valIdent]) + scheme = Coq.Assertion Coq.Definition schemeName binders term + proof = Coq.ProofDefined + (Text.pack + $ " fix " + ++ hypothesisVar + ++ " 1; intro; " + ++ fromJust (Coq.unpackQualid Coq.Base.proveInd) + ++ ".") + return [Coq.AssertionSentence scheme proof] +-- Type synonyms are not allowed in this function. +generateInductionScheme (IR.TypeSynDecl _ _ _ _) + = error "generateInductionScheme: Type synonym not allowed." + +-- | Generates an induction case for a given property and constructor. +generateInductionCase + :: Coq.Qualid -> IR.ConDecl -> Converter (Coq.Qualid, Coq.Binder) +generateInductionCase pIdent (IR.ConDecl _ declIdent argTypes) = do + let conName = IR.declIdentName declIdent + Just conIdent <- inEnv $ lookupIdent IR.ValueScope conName + Just conType' <- inEnv $ lookupReturnType IR.ValueScope conName + conType <- convertType' conType' + fConType <- convertType conType' + fArgTypes <- mapM convertType argTypes + (argIdents, argBinders) <- mapAndUnzipM convertAnonymousArg + (map Just argTypes) + let + -- We need an induction hypothesis for every argument that has the same + -- type as the constructor but lifted into the free monad. + addHypotheses' :: [(Coq.Term, Coq.Qualid)] -> Coq.Term -> Coq.Term + addHypotheses' [] = id + addHypotheses' ((argType, argIdent) : args) + | argType == fConType = Coq.Arrow (genericForFree conType pIdent argIdent) + . addHypotheses' args + addHypotheses' (_ : args) = addHypotheses' args + addHypotheses = addHypotheses' (zip fArgTypes argIdents) + -- Create induction case. + term = addHypotheses + (Coq.app (Coq.Qualid pIdent) + [Coq.app (Coq.Qualid conIdent) (map Coq.Qualid argIdents)]) + indCase = if null argBinders + then term + else Coq.Forall (NonEmpty.fromList argBinders) term + indCaseIdent <- freshCoqQualid freshArgPrefix + indCaseBinder <- generateArgBinder indCaseIdent (Just indCase) + return (indCaseIdent, indCaseBinder) diff --git a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/TypeclassInstances.hs b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/TypeclassInstances.hs new file mode 100644 index 00000000..c35397e2 --- /dev/null +++ b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/TypeclassInstances.hs @@ -0,0 +1,649 @@ +-- | This module contains functions to generate instances for supported +-- typeclasses for user-defined Haskell data types. +-- +-- Suppose we have a type +-- > data T α₁ … αₙ = C₁ τ₍₁,₁₎ … τ₍₁,ₘ₁₎ | … | Cₖ τ₍ₖ,₁₎ … τ₍ₖ,ₘₖ₎. +-- We wish to generate an instance of class @C@ providing the function +-- @f : T α₁ … αₙ -> τ@, where @τ@ is a type. +-- For example, for the @Normalform@ class, @f@ would be +-- > nf' : T α₁ … αₙ -> Free Shape Pos (T α₁ … αₙ). +-- +-- The generated function has the following basic structure: +-- +-- > f'T < class-specific binders > (x : T α₁ … αₙ) : B +-- > := match x with +-- > | C₁ fx₍₁,₁₎ … fx₍₁,ₘ₁₎ => < buildValue x [fx₍₁,₁₎, …, fx₍₁,ₘ₁₎ > +-- > | … +-- > | Cₖ fx₍ₖ,₁₎ … fx₍ₖ,ₘₖ₎ => < buildValue x [fx₍ₖ,₁₎, …, fxk₍ₖ,ₘₖ₎] > +-- > end. +-- +-- @buildValue x [fx₍ᵢ,₁₎, …, fx₍ᵢ,ₘᵢ₎]@ represents class-specific code that +-- actually constructs a value of type @τ@ when given @x@ and the +-- constructor's parameters as arguments. +-- +-- For example, for a @Normalform@ instance of a type +-- @data List a = Nil | Cons a (List a)@, +-- the function would look as follows. +-- +-- > nf'List_ {Shape : Type} {Pos : Shape -> Type} +-- > {a b : Type} `{Normalform Shape Pos a b} +-- > (x : List Shape Pos a) +-- > : Free Shape Pos (List Identity.Shape Identity.Pos b) +-- > := match x with +-- > | nil => pure nil +-- > | cons fx_0 fx_1 => nf fx_0 >>= fun nx_0 => +-- > fx_1 >>= fun x_1 => +-- > nf'List x_1 >>= fun nx_1 => +-- > pure (cons (pure nx_0) (pure nx_1)) +-- > end. +-- +-- Typically, @buildValue@ will use the class function @f@ on all components, +-- then reconstruct the value using the results of those function calls. +-- In the example above, we use @nf@ on @fx_0@ of type @a@. @nf fx_0@ means +-- the same as @fx_0 >>= fun x_0 => nf' x_0@. +-- +-- Since we translate types in topological order and @C@ instances exist for +-- all previously translated types (and types from the Prelude), we can use +-- @f@ on most arguments. +-- For all type variables, we introduce class constraints into the type +-- signature of the function. +-- However, this is not possible for (indirectly) recursive arguments. +-- +-- A directly recursive argument has the type @T τ₁ … τₙ@, where @τᵢ@ is a +-- type expressions (not necessarily type variables). We assume that @τᵢ'@ +-- does not contain @T@ for any @i@, as this would constitute a non-positive +-- occurrence of @T@ and make @T@ invalid in Coq. +-- For these arguments, instead of the function @f@ we call @fT@ recursively. +-- +-- An indirectly recursive argument is an argument of a type that is not @T@, +-- but contains @T@. +-- These arguments are problematic because we can neither use @f@ on them +-- (as that would generally require a @C@ instance of @T@) nor can we use +-- @fT@. +-- +-- The problem is solved by introducing a local function @fT'@ for every type +-- @T'@ that contains @T@ that inlines the definition of a @T'@ instance of +-- @C@, and call this function for arguments of type @T'@. +-- These local functions are as polymorphic as possible to reduce the number +-- of local functions we need. +-- +-- For example, if we want to generate an instance for the Haskell type +-- +-- > data Forest a = AForest [Forest a] +-- > | IntForest [Forest Int] +-- > | BoolForest [Forest Bool] +-- +-- only one local function is needed. In the case of @Normalform@, the local +-- function would look as follows. +-- +-- > nf'ListForest_ {a b : Type} `{Normalform Shape Pos a b} +-- > : List Shape Pos (Forest Shape Pos a) +-- > -> Free Shape Pos (List Identity.Shape Identity.Pos +-- > (Forest Identity.Shape Identity.Pos b)) +-- +-- To generate these local functions, for every type expression @τ₍ᵢ,ⱼ₎@ in the +-- constructors of @T@, we collect all types that contain the original type +-- @T@. +-- More specifically, a type expression @T' τ₁ … τₙ@ is collected if +-- @τᵢ = T τ₁' … τₙ'@ for some type expressions @τ₁, …, τₙ@, or if @τᵢ@ +-- is collected for some @i@. +-- During this process, any type expression that does not contain @T@ is +-- replaced by a placeholder variable @_@. +-- +-- We keep track of which types correspond to which function with a map. +-- +-- The generated functions @fT₁, …, fTₙ@ for @n@ mutually recursive types +-- @T₁, … Tₙ@ are a set of @n@ @Fixpoint@ definitions linked with @with@. +-- Indirectly recursive types and local functions based on them are computed +-- for each type. +-- In this case, a type @T'@ is considered indirectly recursive if it +-- contains any of the types @T₁, …, Tₙ@. +-- Arguments of type @Tᵢ@ can be treated like directly recursive arguments. +module FreeC.Backend.Coq.Converter.TypeDecl.TypeclassInstances where + +import Control.Monad + ( foldM, mapAndUnzipM, replicateM ) +import Control.Monad.Extra ( concatMapM ) +import Data.List ( nub ) +import qualified Data.List.NonEmpty as NonEmpty +import qualified Data.Map.Strict as Map +import Data.Maybe ( fromJust ) +import Language.Coq.Subst + +import qualified FreeC.Backend.Coq.Base as Coq.Base +import FreeC.Backend.Coq.Converter.Free +import qualified FreeC.Backend.Coq.Syntax as Coq +import FreeC.Environment +import FreeC.Environment.Entry +import FreeC.Environment.Fresh +import FreeC.Environment.LookupOrFail +import FreeC.IR.SrcSpan ( SrcSpan(NoSrcSpan) ) +import FreeC.IR.Subst +import qualified FreeC.IR.Syntax as IR +import FreeC.IR.TypeSynExpansion +import FreeC.IR.Unification +import FreeC.Monad.Converter +import FreeC.Pretty + +------------------------------------------------------------------------------- +-- Instance Generation -- +------------------------------------------------------------------------------- +-- | Data type for a type with certain components replaced by underscores. +data StrippedType + = StrippedType + | StrippedTypeCon IR.TypeConName [StrippedType] + deriving ( Eq, Ord, Show ) + +isStripped :: StrippedType -> Bool +isStripped StrippedType = True +isStripped _ = False + +-- | Type synonym for a map mapping types to function names. +type TypeMap' = Map.Map IR.Type Coq.Qualid + +type TypeMap = Map.Map StrippedType Coq.Qualid + +-- | Builds instances for all supported typeclasses. +-- Currently, @Normalform@ and @ShareableArgs@ instances are generated. +generateTypeclassInstances :: [IR.TypeDecl] -> Converter [Coq.Sentence] +generateTypeclassInstances dataDecls = do + -- The types of the data declaration's constructors' arguments. + let argTypes = map (concatMap IR.conDeclFields . IR.dataDeclCons) dataDecls + -- The same types where all type synonyms are expanded. + argTypesExpanded <- mapM (mapM expandAllTypeSynonyms) argTypes + -- A list where all fully-applied type constructors that do not contain one of the types + -- for which we are defining instances and all type variables are replaced with + -- the same type variable (an underscore). The list is reversed so its entries are + -- in topological order. + let reducedTypes = map (nub . reverse . concatMap collectSubTypes) + argTypesExpanded + -- Like 'reducedTypes', but with all occurrences of the types for which we are defining + -- instances and all type variables removed from the list. + -- This leaves exactly the types with indirect recursion, with all non-recursive + -- components replaced by underscores. + let recTypeList = map + (filter (\t -> not (t `elem` declTypes || isStripped t))) reducedTypes + -- Construct @Normalform@ instances. + nfInstances <- buildInstances recTypeList + (fromJust $ Coq.unpackQualid Coq.Base.nf') + (fromJust $ Coq.unpackQualid Coq.Base.normalform) nfBindersAndReturnType + buildNormalformValue + -- Construct @ShareableArgs@ instances. + shareableArgsInstances <- buildInstances recTypeList + (fromJust $ Coq.unpackQualid Coq.Base.shareArgs) + (fromJust $ Coq.unpackQualid Coq.Base.shareableArgs) + shareArgsBindersAndReturnType buildShareArgsValue + return (nfInstances ++ shareableArgsInstances) + where + -- | The (mutually recursive) data types for which we are defining + -- instances, converted to types. All type variable are converted + -- to underscores. + declTypes :: [StrippedType] + declTypes = [StrippedTypeCon (IR.typeDeclQName dataDecl) + (replicate (length (IR.typeDeclArgs dataDecl)) StrippedType) + | dataDecl <- dataDecls + ] + + -- The names of the type constructors of the data types for which + -- we are defining instances. + typeConNames :: [IR.TypeConName] + typeConNames = map IR.typeDeclQName dataDecls + + -- | Constructs instances of a typeclass for a set of mutually recursive + -- types. The typeclass is specified by the arguments. + buildInstances + :: [[StrippedType]] + -- ^ For each data declaration, this list contains the occurrences of + -- indirect recursion in the constructors of that data declaration. + -> String -- ^ The name of the class function. + -> String -- ^ The name of the typeclass. + -> (StrippedType + -> Coq.Qualid + -> Converter ([Coq.Binder], Coq.Binder, Coq.Term, Coq.Term)) + -- ^ A function to get class-specific binders and return types. + -> (TypeMap + -> Coq.Qualid + -> [(StrippedType, Coq.Qualid)] + -> Converter Coq.Term) + -- ^ A function to compute a class-specific value given a data constructor + -- with arguments. + -> Converter [Coq.Sentence] + buildInstances recTypeList functionPrefix className getBindersAndReturnTypes + buildValue = do + -- This map defines the name of the top-level class function for each + -- of the mutually recursive types. + -- It must be defined outside of a local environment to prevent any + -- clashes of the function names with other names. + topLevelMap <- nameFunctionsAndInsert functionPrefix Map.empty declTypes + (fixBodies, instances) <- mapAndUnzipM + (uncurry (buildFixBodyAndInstance topLevelMap)) + (zip declTypes recTypeList) + return + $ Coq.comment (className + ++ " instance" + ++ ['s' | length dataDecls > 1] + ++ " for " + ++ showPretty (map IR.typeDeclName dataDecls)) + : Coq.FixpointSentence (Coq.Fixpoint (NonEmpty.fromList fixBodies) []) + : instances + where + -- Constructs the class function and class instance for a single type. + buildFixBodyAndInstance + :: TypeMap + -- ^ A map to map occurrences of the top-level types to recursive + -- function calls. + -> StrippedType -- ^ The type for which we are defining an instance. + -> [StrippedType] -- ^ The list of indirectly recursive types. + -> Converter (Coq.FixBody, Coq.Sentence) + buildFixBodyAndInstance topLevelMap t recTypes = do + -- Locally visible definitions are defined in a local environment. + (fixBody, typeLevelMap, binders, instanceRetType) <- localEnv $ do + -- This map names necessary local functions and maps indirectly + -- recursive types to the appropriate function names. + typeLevelMap + <- nameFunctionsAndInsert functionPrefix topLevelMap recTypes + -- Name the argument of type @t@ given to the class + -- function. + topLevelVar <- freshCoqQualid freshArgPrefix + -- Compute class-specific binders and return types. + (binders, varBinder, retType, instanceRetType) + <- getBindersAndReturnTypes t topLevelVar + -- Build the implementation of the class function. + fixBody <- makeFixBody typeLevelMap topLevelVar t + (binders ++ [varBinder]) retType recTypes + return (fixBody, typeLevelMap, binders, instanceRetType) + -- Build the class instance for the given type. + -- The instance must be defined outside of a local environment so + -- that the instance name does not clash with any other names. + instanceDefinition <- buildInstance typeLevelMap t binders instanceRetType + return (fixBody, instanceDefinition) + + -- | Builds an instance for a specific type and typeclass. + buildInstance + :: TypeMap + -- ^ A mapping from (in)directly recursive types to function names. + -> StrippedType -- ^ The type for which we are defining an instance. + -> [Coq.Binder] -- ^ The binders for the type class instance. + -> Coq.Term -- ^ The type of the instance. + -> Converter Coq.Sentence + buildInstance m t binders retType = do + -- Define the class function as the function to which the current type + -- is mapped. + let instanceBody + = (Coq.bare functionPrefix, Coq.Qualid (fromJust (Map.lookup t m))) + instanceName <- nameFunction className t + return + $ Coq.InstanceSentence + (Coq.InstanceDefinition instanceName (freeArgsBinders ++ binders) + retType [instanceBody] Nothing) + + -- | Generates the implementation of the body of a class function for the + -- given type. + makeFixBody + :: TypeMap + -- ^ A mapping from (in)directly recursive types to function names. + -> Coq.Qualid -- ^ The name of the argument of type @t@. + -> StrippedType -- ^ The type for which we are defining an instance. + -> [Coq.Binder] -- ^ The binders for the class function. + -> Coq.Term -- ^ The return type of the class function. + -> [StrippedType] -- ^ The list of indirectly recursive types. + -> Converter Coq.FixBody + makeFixBody m varName t binders retType recTypes = do + rhs <- generateBody m varName t recTypes + return + $ Coq.FixBody (fromJust (Map.lookup t m)) + (NonEmpty.fromList (freeArgsBinders ++ binders)) Nothing (Just retType) + rhs + + -- | Creates the function body for a class function by creating local + -- functions for all indirectly recursive types. + generateBody + :: TypeMap + -- ^ A mapping from (in)directly recursive types to function names. + -> Coq.Qualid -- ^ The name of the argument of type @t@. + -> StrippedType -- ^ The type for which we are defining an instance. + -> [StrippedType] -- ^ The list of indirectly recursive types. + -> Converter Coq.Term + + -- If there are no indirectly recursive types, match on the constructors of + -- the original type. + generateBody m varName t [] + = matchConstructors m varName t + -- For each indirectly recursive type, create a local function as a + -- @let fix@ declaration and generate the definition of the class function + -- for that type. + -- This local declaration is wrapped around all remaining declarations and + -- is therefore visible when defining them. + generateBody m varName t (recType : recTypes) = do + inBody <- generateBody m varName t recTypes + var <- freshCoqQualid freshArgPrefix + -- Create the body of the local function by matching on the type's + -- constructors. + letBody <- matchConstructors m var recType + (binders, varBinder, retType, _) <- getBindersAndReturnTypes recType var + let Just localFuncName = Map.lookup recType m + return + $ Coq.Let localFuncName [] Nothing + (Coq.Fix (Coq.FixOne (Coq.FixBody localFuncName + (NonEmpty.fromList (binders ++ [varBinder])) + Nothing (Just retType) letBody))) inBody + + -- | Matches on the constructors of a type. + matchConstructors + :: TypeMap -> Coq.Qualid -> StrippedType -> Converter Coq.Term + matchConstructors m varName t@(StrippedTypeCon conName _) = do + entry <- lookupEntryOrFail NoSrcSpan IR.TypeScope conName + equations <- mapM (buildEquation m t) (entryConsNames entry) + return $ Coq.match (Coq.Qualid varName) equations + matchConstructors _ _ StrippedType + = error "generateTypeclassInstances: unexpected type placeholder." + + -- | Creates a match equation on a given data constructor with a + -- class-specific right-hand side. + buildEquation + :: TypeMap -> StrippedType -> IR.ConName -> Converter Coq.Equation + buildEquation m t conName = do + conEntry <- lookupEntryOrFail NoSrcSpan IR.ValueScope conName + retType <- expandAllTypeSynonyms (entryReturnType conEntry) + -- Get the Coq name of the constructor. + let conIdent = entryIdent conEntry + -- Generate fresh variables for the constructor's parameters. + conArgIdents <- freshQualids (entryArity conEntry) freshArgPrefix + -- Replace all underscores with fresh variables before unification. + tFreshVars <- insertFreshVariables t + sub <- unifyOrFail NoSrcSpan tFreshVars retType + -- Find out the type of each constructor argument by unifying its return + -- type with the given type expression and applying the resulting + -- substitution to each constructor argument's type. + -- Then convert all irrelevant components to underscores again so the + -- type can be looked up in the type map. + expandedArgTypes <- mapM expandAllTypeSynonyms (entryArgTypes conEntry) + let modArgTypes = map (stripType . applySubst sub) expandedArgTypes + let lhs = Coq.ArgsPat conIdent (map Coq.QualidPat conArgIdents) + -- Build the right-hand side of the equation by applying the + -- class-specific function @buildValue@. + rhs <- buildValue m conIdent (zip modArgTypes conArgIdents) + return $ Coq.equation lhs rhs + + ------------------------------------------------------------------------------- + -- Functions to Produce @Normalform@ Instances -- + ------------------------------------------------------------------------------- + -- | The binders and return types for the @Normalform@ class function and instance. + nfBindersAndReturnType + :: StrippedType + -- ^ The type @t@ for which we are defining an instance. + -> Coq.Qualid -- ^ The name of the argument of type @t@. + -> Converter + ( [Coq.Binder] -- Type variable binders and @Normalform@ constraints. + , Coq.Binder -- Binder for the argument of type @t@. + , Coq.Term -- Return type of @nf'@. + , Coq.Term -- Return type of the @Normalform@ instance. + ) + nfBindersAndReturnType t varName = do + (sourceType, sourceVars) <- toCoqType t + -- The return types of the type variables' @Normalform@ instances. + let nTypes = map + (\v -> Coq.explicitApp Coq.Base.nType + (shapeAndPos ++ Coq.Qualid v : [Coq.Underscore])) sourceVars + -- Build a substitution to create the normalized type from the source + -- type. + targetTypeMap = buildNFSubst (zip sourceVars nTypes) + targetType = subst targetTypeMap sourceType + -- For each type variable @aᵢ@, build a constraint + -- @`{Normalform Shape Pos aᵢ}@. + constraints = map Coq.Base.normalformBinder sourceVars + varBinder = [typeVarBinder sourceVars | not (null sourceVars)] + binders = varBinder ++ constraints + -- Create an explicit argument binder for the value to be normalized. + topLevelVarBinder + = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit varName sourceType + instanceRetType = Coq.app (Coq.Qualid Coq.Base.normalform) + (shapeAndPos ++ [sourceType]) + funcRetType = applyFree targetType + return (binders, topLevelVarBinder, funcRetType, instanceRetType) + where + buildNFSubst :: [(Coq.Qualid, Coq.Term)] -> Map.Map Coq.Qualid Coq.Term + buildNFSubst kvs = Map.insert Coq.Base.shape (Coq.Qualid Coq.Base.idShape) + (Map.insert Coq.Base.pos (Coq.Qualid Coq.Base.idPos) + (foldr (uncurry Map.insert) Map.empty kvs)) + + -- | Builds a normalized @Free@ value for the given constructor + -- and constructor arguments. + buildNormalformValue + :: TypeMap + -- ^ A map to associate types with the appropriate functions to call. + -> Coq.Qualid -- ^ The data constructor used to build a value. + -> [(StrippedType, Coq.Qualid)] + -- ^ The types and names of the constructor's arguments. + -> Converter Coq.Term + buildNormalformValue nameMap consName = buildNormalformValue' [] + where + -- | Like 'buildNormalformValue', but with an additional parameter to accumulate + -- bound variables. + buildNormalformValue' + :: [Coq.Term] -> [(StrippedType, Coq.Qualid)] -> Converter Coq.Term + + -- If all components have been normalized, apply the constructor to + -- the normalized components. + buildNormalformValue' boundVars [] = do + args <- mapM generatePure (reverse boundVars) + generatePure (Coq.app (Coq.Qualid consName) args) + -- For each component, apply the appropriate function, bind the + -- result and do the remaining computation. + buildNormalformValue' boundVars ((t, varName) : consVars) + = let f = (\nx -> buildNormalformValue' (nx : boundVars) consVars) + in case Map.lookup t nameMap of + -- For recursive or indirectly recursive calls, the type map + -- returns the name of the appropriate function to call. + Just funcName -> do + -- Because the functions work on bare values, the component + -- must be bound before applying the normalization. + generateBind (Coq.Qualid varName) freshArgPrefix Nothing + (\x -> generateBind (Coq.app (Coq.Qualid funcName) [x]) + freshNormalformArgPrefix Nothing f) + -- If there is no entry in the type map, we can assume that an instance + -- already exists. Therefore, we apply @nf@ to the component to receive + -- a normalized value. + Nothing -> generateBind + (Coq.app (Coq.Qualid Coq.Base.nf) [Coq.Qualid varName]) + freshNormalformArgPrefix Nothing f + + ------------------------------------------------------------------------------- + -- Functions to Produce @ShareableArgs@ Instances -- + ------------------------------------------------------------------------------- + -- | The binders and return types for the @ShareableArgs@ class function and instance. + shareArgsBindersAndReturnType + :: StrippedType + -- ^ The type @t@ for which we are defining an instance. + -> Coq.Qualid -- ^ The name of the argument of type @t@. + -> Converter + ( [Coq.Binder] -- Type variable binders and @ShareableArgs@ constraints. + , Coq.Binder -- Binder for the argument of type @t@. + , Coq.Term -- Return type of @shareArgs@. + , Coq.Term -- Return type of the @ShareableArgs@ instance. + ) + shareArgsBindersAndReturnType t varName = do + (coqType, vars) <- toCoqType t + let constraints + = Coq.Base.injectableBinder : map Coq.Base.shareableArgsBinder vars + let varBinder = [typeVarBinder vars | not (null vars)] + let binders = varBinder ++ constraints + let topLevelVarBinder + = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit varName coqType + let instanceRetType = Coq.app (Coq.Qualid Coq.Base.shareableArgs) + (shapeAndPos ++ [coqType]) + let funcRetType = applyFree coqType + return (binders, topLevelVarBinder, funcRetType, instanceRetType) + + -- | Shares all arguments of the given constructor and reconstructs the + -- value with the shared components. + buildShareArgsValue + :: TypeMap + -- ^ A map to associate types with the appropriate functions to call. + -> Coq.Qualid -- ^ The data constructor used to build a value. + -> [(StrippedType, Coq.Qualid)] + -- ^ The types and names of the constructor's arguments. + -> Converter Coq.Term + buildShareArgsValue nameMap consName = buildShareArgsValue' [] + where + buildShareArgsValue' + :: [Coq.Term] -> [(StrippedType, Coq.Qualid)] -> Converter Coq.Term + buildShareArgsValue' vals [] = generatePure + (Coq.app (Coq.Qualid consName) (reverse vals)) + buildShareArgsValue' vals ((t, varName) : consVars) = do + let lhs = case Map.lookup t nameMap of + Just funcName -> Coq.app (Coq.Qualid Coq.Base.cbneed) + (shapeAndPos ++ [Coq.Qualid funcName, Coq.Qualid varName]) + Nothing -> Coq.app (Coq.Qualid Coq.Base.cbneed) + (shapeAndPos + ++ [Coq.Qualid Coq.Base.shareArgs, Coq.Qualid varName]) + generateBind lhs freshSharingArgPrefix Nothing + (\val -> buildShareArgsValue' (val : vals) consVars) + + ------------------------------------------------------------------------------- + -- Helper Functions -- + ------------------------------------------------------------------------------- + -- | Creates an entry with a unique name for each of the given types and + -- inserts them into the given map. + nameFunctionsAndInsert + :: String -> TypeMap -> [StrippedType] -> Converter TypeMap + nameFunctionsAndInsert prefix = foldM (nameFunctionAndInsert prefix) + + -- | Like 'nameFunctionsAndInsert', but for a single type. + nameFunctionAndInsert + :: String -> TypeMap -> StrippedType -> Converter TypeMap + nameFunctionAndInsert prefix m t = do + name <- nameFunction prefix t + return (Map.insert t name m) + + -- | Names a function based on a type expression while avoiding name clashes + -- with other identifiers. + nameFunction :: String -> StrippedType -> Converter Coq.Qualid + nameFunction prefix t = do + prettyType <- showPrettyType t + freshCoqQualid (prefix ++ prettyType) + + -- | Collects all fully-applied type constructors of arity at least 1 + -- (including their arguments) that occur in the given type. All arguments + -- that do not contain occurrences of the types for which we are defining + -- an instance are replaced by the type variable @_@. + -- The resulting list contains (in reverse topological order) exactly all + -- types for which we must define a separate function in the instance + -- definition, where all occurrences of @_@ represent the polymorphic + -- components of the function. + collectSubTypes :: IR.Type -> [StrippedType] + collectSubTypes = collectFullyAppliedTypes True + where + -- | Like 'collectSubTypes', but with an additional flag to denote whether + -- @t@ is a full application of a type constructor, e.g. @Pair Int Bool@, + -- or a partial application, e.g. @Pair Int@. + -- Only full applications are collected. + collectFullyAppliedTypes :: Bool -> IR.Type -> [StrippedType] + collectFullyAppliedTypes fullApplication t@(IR.TypeApp _ l r) + -- The left-hand side of a type application is the partial + -- application of a type constructor. + -- The right-hand side is a fully-applied type constructor, + -- a variable or a function type. + = let remainingTypes = collectFullyAppliedTypes False l + ++ collectFullyAppliedTypes True r + in if fullApplication + then stripType t : remainingTypes + else remainingTypes + -- Type variables, function types and type constructors with arity 0 are not + -- collected. + collectFullyAppliedTypes _ _ = [] + + -- | Returns the same type with all type expressions that do not contain one + -- of the type constructors for which we are defining instances replaced + -- with the type variable @_@. + stripType :: IR.Type -> StrippedType + stripType = stripType' False + where + -- | Like 'stripType', but with an additional flag to denote whether an + -- occurrence of a relevant type was found in an argument of a type + -- application. + -- This is necessary so that, for example, @Pair Bool t@ is not + -- transformed to @_ t@, but to @Pair _ t@. + stripType' :: Bool -> IR.Type -> StrippedType + stripType' flag (IR.TypeCon _ conName) + | flag || conName `elem` typeConNames = StrippedTypeCon conName [] + | otherwise = StrippedType + -- For a type application, check if a relevant type occurs in its + -- right-hand side. + stripType' flag (IR.TypeApp _ l r) = case stripType' False r of + -- If not, check if a relevant type occurs in its left-hand side, + -- otherwise replace the whole expression with an underscore. + StrippedType -> case stripType' flag l of + StrippedType -> StrippedType + StrippedTypeCon con args -> StrippedTypeCon con (args ++ [StrippedType]) + -- If a relevant type does occur in the right-hand side, + -- the type application must be preserved, so only its arguments are + -- stripped. + r' -> let StrippedTypeCon con args = stripType' True l + in StrippedTypeCon con (args ++ [r']) + -- Type variables and function types are not relevant and are replaced by @_@. + stripType' _ _ = StrippedType + + showPrettyType :: StrippedType -> Converter String + + -- For a placeholder, show "_". + showPrettyType StrippedType = return "_" + -- For a type constructor and its arguments, return the constructor's + -- Coq identifier as a string with the conversions of the arguments appended. + showPrettyType (StrippedTypeCon con args) = do + prettyCon <- fromJust . (>>= Coq.unpackQualid) + <$> inEnv (lookupIdent IR.TypeScope con) + prettyArgs <- concatMapM showPrettyType args + return (prettyCon ++ prettyArgs) + + -- | Converts a @StrippedType@ to an @IR.Type@, replacing all + -- placeholders with fresh variables. + insertFreshVariables :: StrippedType -> Converter IR.Type + insertFreshVariables StrippedType = do + freshVar <- freshHaskellIdent freshArgPrefix + return (IR.TypeVar NoSrcSpan freshVar) + insertFreshVariables (StrippedTypeCon con args) = do + args' <- mapM insertFreshVariables args + return (foldl (IR.TypeApp NoSrcSpan) (IR.TypeCon NoSrcSpan con) args') + + -- | Binders for (implicit) Shape and Pos arguments. + -- + -- > freeArgsBinders = [ {Shape : Type}, {Pos : Shape -> Type} ] + freeArgsBinders :: [Coq.Binder] + freeArgsBinders = genericArgDecls Coq.Implicit + + -- | Shortcut for the construction of an implicit binder for type variables. + -- + -- > typeVarBinder [α₁, …, an] = {α₁ …αₙ : Type} + typeVarBinder :: [Coq.Qualid] -> Coq.Binder + typeVarBinder typeVars + = Coq.typedBinder Coq.Ungeneralizable Coq.Implicit typeVars Coq.sortType + + -- | Given an @A@, returns @Free Shape Pos A@. + applyFree :: Coq.Term -> Coq.Term + applyFree a = genericApply Coq.Base.free [] [] [a] + + -- | @Shape@ and @Pos@ arguments as Coq terms. + shapeAndPos :: [Coq.Term] + shapeAndPos = [Coq.Qualid Coq.Base.shape, Coq.Qualid Coq.Base.pos] + + -- | Converts a type into a Coq type (a term) with fresh Coq + -- identifiers for all underscores. + -- Returns a pair of the result term and a list of the fresh variables. + toCoqType :: StrippedType -- ^ The type to convert. + -> Converter (Coq.Term, [Coq.Qualid]) + + -- A type variable is translated into a fresh type variable. + toCoqType StrippedType = do + x <- freshCoqQualid freshTypeVarPrefix + return (Coq.Qualid x, [x]) + toCoqType (StrippedTypeCon con args) = do + entry <- lookupEntryOrFail NoSrcSpan IR.TypeScope con + (coqArgs, freshVars) <- mapAndUnzipM toCoqType args + return ( Coq.app (Coq.Qualid (entryIdent entry)) (shapeAndPos ++ coqArgs) + , concat freshVars + ) + + -- | Produces @n@ new Coq identifiers (Qualids) with the same prefix. + freshQualids :: Int -> String -> Converter [Coq.Qualid] + freshQualids n prefix = replicateM n (freshCoqQualid prefix) diff --git a/src/lib/FreeC/Backend/Coq/Syntax.hs b/src/lib/FreeC/Backend/Coq/Syntax.hs index 4c93b545..1db59075 100644 --- a/src/lib/FreeC/Backend/Coq/Syntax.hs +++ b/src/lib/FreeC/Backend/Coq/Syntax.hs @@ -11,6 +11,7 @@ module FreeC.Backend.Coq.Syntax -- * Identifiers , ident , bare + , qualified , unpackQualid , access -- * Functions @@ -87,10 +88,14 @@ blankProof = ProofAdmitted (Text.pack " (* FILL IN HERE *)") ident :: String -> Ident ident = Text.pack --- | Smart constructor for Coq identifiers. +-- | Smart constructor for unqualified Coq identifiers. bare :: String -> Qualid bare = Bare . ident +-- | Smart constructor for qualified Coq identifiers. +qualified :: String -> String -> Qualid +qualified modName name = Qualified (ident modName) (ident name) + -- | Gets the identifier for the given unqualified Coq identifier. Returns -- @Nothing@ if the given identifier is qualified. unpackQualid :: Qualid -> Maybe String diff --git a/src/lib/FreeC/Environment/Fresh.hs b/src/lib/FreeC/Environment/Fresh.hs index 600888ad..06fc8c08 100644 --- a/src/lib/FreeC/Environment/Fresh.hs +++ b/src/lib/FreeC/Environment/Fresh.hs @@ -6,6 +6,8 @@ module FreeC.Environment.Fresh ( -- * Prefixes freshArgPrefix + , freshNormalformArgPrefix + , freshSharingArgPrefix , freshFuncPrefix , freshBoolPrefix , freshTypeVarPrefix @@ -44,6 +46,14 @@ import FreeC.Monad.Converter freshArgPrefix :: String freshArgPrefix = "x" +-- | The prefix to use for variables artificially introduced by normalization. +freshNormalformArgPrefix :: String +freshNormalformArgPrefix = "nx" + +-- | The prefix to use for variables artificially introduced by sharing. +freshSharingArgPrefix :: String +freshSharingArgPrefix = "sx" + -- | The prefix to use for artificially introduced variables of type @a -> b@. freshFuncPrefix :: String freshFuncPrefix = "f" diff --git a/src/lib/FreeC/IR/Syntax/Type.hs b/src/lib/FreeC/IR/Syntax/Type.hs index 8f03cacb..9cba7ebe 100644 --- a/src/lib/FreeC/IR/Syntax/Type.hs +++ b/src/lib/FreeC/IR/Syntax/Type.hs @@ -68,6 +68,33 @@ splitFuncType (FuncType _ t1 t2) arity in (t1 : argTypes, returnType) splitFuncType returnType _ = ([], returnType) +-- | Returns the name of the outermost type constructor, or @Nothing@ if there +-- is no such type constructor. +getTypeConName :: Type -> Maybe ConName +getTypeConName (TypeCon _ conName) = Just conName +getTypeConName (TypeApp _ l _) = getTypeConName l +getTypeConName _ = Nothing + +-- | Checks whether the given type is a type variable. +isTypeVar :: Type -> Bool +isTypeVar (TypeVar _ _) = True +isTypeVar _ = False + +-- | Checks whether the given type is a type constructor. +isTypeCon :: Type -> Bool +isTypeCon (TypeCon _ _) = True +isTypeCon _ = False + +-- | Checks whether the given type is a type application. +isTypeApp :: Type -> Bool +isTypeApp (TypeApp _ _ _) = True +isTypeApp _ = False + +-- | Checks whether the given type is a function type. +isFuncType :: Type -> Bool +isFuncType (FuncType _ _ _) = True +isFuncType _ = False + -- | Pretty instance for type expressions. instance Pretty Type where pretty = prettyTypePred 0 diff --git a/src/lib/FreeC/Pass/CompletePatternPass.hs b/src/lib/FreeC/Pass/CompletePatternPass.hs index 419cde27..0b0efffb 100644 --- a/src/lib/FreeC/Pass/CompletePatternPass.hs +++ b/src/lib/FreeC/Pass/CompletePatternPass.hs @@ -101,7 +101,7 @@ checkPatternFuncDecl funcDecl = checkPatternExpr (IR.funcDeclRhs funcDecl) -- The usage of 'fromJust' is safe, because all types are annotated. let tau = fromJust $ IR.exprType exprScrutinee tau' <- expandAllTypeSynonyms tau - case getTypeConName tau' of + case IR.getTypeConName tau' of Nothing -> failedPatternCheck srcSpan Just typeName -> do -- If an entry is found we can assume that it is 'DataEntry' because @@ -136,11 +136,3 @@ checkPatternFuncDecl funcDecl = checkPatternExpr (IR.funcDeclRhs funcDecl) $ Message srcSpan Error $ "Incomplete pattern in function: " ++ showPretty (IR.funcDeclName funcDecl) - - -- | Selects the name of the outermost type constructor from a type. - getTypeConName :: IR.Type -> Maybe IR.TypeConName - getTypeConName (IR.TypeCon _ typeConName) = Just typeConName - getTypeConName (IR.TypeApp _ typeAppLhs _) = getTypeConName typeAppLhs - -- The type of the scrutinee shouldn't be a function or type variable. - getTypeConName IR.TypeVar {} = Nothing - getTypeConName IR.FuncType {} = Nothing diff --git a/src/test/FreeC/Backend/Coq/Converter/TypeDeclTests.hs b/src/test/FreeC/Backend/Coq/Converter/TypeDeclTests.hs index 540051c3..7577a6b1 100644 --- a/src/test/FreeC/Backend/Coq/Converter/TypeDeclTests.hs +++ b/src/test/FreeC/Backend/Coq/Converter/TypeDeclTests.hs @@ -69,9 +69,12 @@ testConvertTypeDecl it "expands type synonyms in mutually recursive data type declarations" $ shouldSucceedWith $ do - "List" <- defineTestTypeCon "List" 1 [] + "List" <- defineTestTypeCon "List" 1 ["Nil", "Cons"] + ("nil", "Nil") <- defineTestCon "Nil" 0 "forall a. List a" + ("cons", "Cons") + <- defineTestCon "Cons" 2 "forall a . a -> List a -> List a" "Forest" <- defineTestTypeSyn "Forest" ["a"] "List (Tree a)" - "Tree" <- defineTestTypeCon "Tree" 1 [] + "Tree" <- defineTestTypeCon "Tree" 1 ["Leaf", "Branch"] ("leaf", "Leaf") <- defineTestCon "Leaf" 1 "forall a. a -> Tree a" ("branch", "Branch") <- defineTestCon "Branch" 1 "forall a. Forest a -> Tree a" @@ -110,9 +113,77 @@ testConvertTypeDecl ++ "Notation \"'@Branch' Shape Pos a x\" :=" ++ " (@pure Shape Pos (Tree Shape Pos a) (@branch Shape Pos a x))" ++ " ( only parsing, at level 10, Shape, Pos, a, x at level 9 ). " - ++ "Definition Forest (Shape : Type) (Pos : Shape -> Type)" - ++ " (a : Type)" - ++ " : Type" + ++ " (* Normalform instance for Tree *) " + ++ "Fixpoint nf'Tree_" + ++ " {Shape : Type} {Pos : Shape -> Type} " + ++ " {a : Type} `{Normalform Shape Pos a} " + ++ " (x : Tree Shape Pos a) " + ++ " : Free Shape Pos" + ++ " (Tree Identity.Shape Identity.Pos (@nType Shape Pos a _))" + ++ " := let fix nf'ListTree_" + ++ " {a0 : Type} `{Normalform Shape Pos a0} " + ++ " (x2 : List Shape Pos (Tree Shape Pos a0)) " + ++ " : Free Shape Pos (List Identity.Shape Identity.Pos " + ++ " (Tree Identity.Shape Identity.Pos" + ++ " (@nType Shape Pos a0 _)))" + ++ " := match x2 with " + ++ " | nil => pure nil " + ++ " | cons x3 x4 =>" + ++ " x3 >>= (fun x5 =>" + ++ " nf'Tree_ x5 >>= (fun nx =>" + ++ " x4 >>= (fun x6 =>" + ++ " nf'ListTree_ x6 >>= (fun nx0 =>" + ++ " pure (cons (pure nx) (pure nx0))))))" + ++ " end " + ++ " in match x with " + ++ " | leaf x0 => nf x0 >>= (fun nx =>" + ++ " pure (leaf (pure nx)))" + ++ " | branch x1 => x1 >>= (fun x2 => " + ++ " nf'ListTree_ x2 >>= (fun nx =>" + ++ " pure (branch (pure nx))))" + ++ " end. " + ++ "Instance NormalformTree_" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a : Type} `{Normalform Shape Pos a}" + ++ " : Normalform Shape Pos (Tree Shape Pos a)" + ++ " := { nf' := nf'Tree_ }. " + ++ "(* ShareableArgs instance for Tree *) " + ++ "Fixpoint shareArgsTree_" + ++ " {Shape : Type} {Pos : Shape -> Type} " + ++ " {a : Type} `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " `{ShareableArgs Shape Pos a} (x : Tree Shape Pos a) " + ++ " : Free Shape Pos (Tree Shape Pos a) " + ++ " := let fix shareArgsListTree_" + ++ " {a0 : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " `{ShareableArgs Shape Pos a0}" + ++ " (x2 : List Shape Pos (Tree Shape Pos a0))" + ++ " : Free Shape Pos (List Shape Pos (Tree Shape Pos a0))" + ++ " := match x2 with " + ++ " | nil => pure nil " + ++ " | cons x3 x4 => " + ++ " cbneed Shape Pos shareArgsTree_ x3 >>= (fun sx =>" + ++ " cbneed Shape Pos shareArgsListTree_ x4 >>=" + ++ " (fun sx0 => " + ++ " pure (cons sx sx0))) " + ++ " end " + ++ " in match x with " + ++ " | leaf x0 => cbneed Shape Pos shareArgs x0 >>= (fun sx =>" + ++ " pure (leaf sx)) " + ++ " | branch x1 => " + ++ " cbneed Shape Pos shareArgsListTree_ x1 >>=" + ++ " (fun sx =>" + ++ " pure (branch sx)) " + ++ " end. " + ++ "Instance ShareableArgsTree_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos} " + ++ " `{ShareableArgs Shape Pos a} " + ++ " : ShareableArgs Shape Pos (Tree Shape Pos a) " + ++ " := { shareArgs := shareArgsTree_ }. " + ++ "Definition Forest" + ++ " (Shape : Type) (Pos : Shape -> Type) (a : Type)" + ++ " : Type" ++ " := List Shape Pos (Tree Shape Pos a)." it "sorts type synonym declarations topologically" $ shouldSucceedWith $ do "Bar" <- defineTestTypeSyn "Bar" [] "Baz" @@ -147,6 +218,36 @@ testConvertTypeDecl ++ "Notation \"'@Foo0' Shape Pos x x0\" :=" ++ " (@pure Shape Pos (Foo Shape Pos) (@foo Shape Pos x x0))" ++ " ( only parsing, at level 10, Shape, Pos, x, x0 at level 9 ). " + ++ " (* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo" + ++ " {Shape : Type} {Pos : Shape -> Type} " + ++ " (x : Foo Shape Pos) " + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos) " + ++ " := let 'foo x0 x1 := x" + ++ " in x0 >>= (fun x2 =>" + ++ " nf'Foo x2 >>= (fun nx =>" + ++ " x1 >>= (fun x3 =>" + ++ " nf'Foo x3 >>= (fun nx0 =>" + ++ " pure (foo (pure nx) (pure nx0)))))). " + ++ "Instance NormalformFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " : Normalform Shape Pos (Foo Shape Pos)" + ++ " := { nf' := nf'Foo }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type} " + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " (x : Foo Shape Pos) " + ++ " : Free Shape Pos (Foo Shape Pos)" + ++ " := let 'foo x0 x1 := x" + ++ " in cbneed Shape Pos shareArgsFoo x0 >>= (fun sx =>" + ++ " cbneed Shape Pos shareArgsFoo x1 >>= (fun sx0 =>" + ++ " pure (foo sx sx0))). " + ++ "Instance ShareableArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos)" + ++ " := { shareArgs := shareArgsFoo }. " ++ "Definition Baz (Shape : Type) (Pos : Shape -> Type)" ++ " : Type" ++ " := Foo Shape Pos. " @@ -203,6 +304,33 @@ testConvertDataDecls ++ "Notation \"'@Baz' Shape Pos\" :=" ++ " (@pure Shape Pos (Foo Shape Pos) (@baz Shape Pos))" ++ " ( only parsing, at level 10, Shape, Pos at level 9 ). " + ++ "(* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo" + ++ " {Shape : Type} {Pos : Shape -> Type} (x : Foo Shape Pos)" + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos)" + ++ " := match x with" + ++ " | bar => pure bar" + ++ " | baz => pure baz" + ++ " end. " + ++ "Instance NormalformFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " : Normalform Shape Pos (Foo Shape Pos)" + ++ " := { nf' := nf'Foo }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " (x : Foo Shape Pos)" + ++ " : Free Shape Pos (Foo Shape Pos)" + ++ " := match x with" + ++ " | bar => pure bar" + ++ " | baz => pure baz" + ++ " end. " + ++ "Instance ShareableArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos) " + ++ " := { shareArgs := shareArgsFoo }. " it "translates polymorphic data types correctly" $ shouldSucceedWith $ do "Foo" <- defineTestTypeCon "Foo" 2 ["Bar", "Baz"] ("bar", "Bar") <- defineTestCon "Bar" 1 "forall a b. a -> Foo a b" @@ -238,6 +366,43 @@ testConvertDataDecls ++ "Notation \"'@Baz' Shape Pos a b x\" :=" ++ " (@pure Shape Pos (Foo Shape Pos a b) (@baz Shape Pos a b x))" ++ " ( only parsing, at level 10, Shape, Pos, a, b, x at level 9 ). " + ++ "(* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo__" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a a0 : Type} `{Normalform Shape Pos a}" + ++ " `{Normalform Shape Pos a0} (x : Foo Shape Pos a a0)" + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos" + ++ " (@nType Shape Pos a _)" + ++ " (@nType Shape Pos a0 _))" + ++ " := match x with" + ++ " | bar x0 => nf x0 >>= (fun nx => pure (bar (pure nx)))" + ++ " | baz x1 => nf x1 >>= (fun nx => pure (baz (pure nx)))" + ++ " end. " + ++ "Instance NormalformFoo__" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a a0 : Type} `{Normalform Shape Pos a}" + ++ " `{Normalform Shape Pos a0}" + ++ " : Normalform Shape Pos (Foo Shape Pos a a0)" + ++ " := { nf' := nf'Foo__ }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo__" + ++ " {Shape : Type} {Pos : Shape -> Type} {a a0 : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos} " + ++ " `{ShareableArgs Shape Pos a} `{ShareableArgs Shape Pos a0}" + ++ " (x : Foo Shape Pos a a0)" + ++ " : Free Shape Pos (Foo Shape Pos a a0)" + ++ " := match x with" + ++ " | bar x0 => cbneed Shape Pos shareArgs x0 >>= (fun sx =>" + ++ " pure (bar sx))" + ++ " | baz x1 => cbneed Shape Pos shareArgs x1 >>= (fun sx =>" + ++ " pure (baz sx))" + ++ " end. " + ++ "Instance ShareableArgsFoo__" + ++ " {Shape : Type} {Pos : Shape -> Type} {a a0 : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " `{ShareableArgs Shape Pos a} `{ShareableArgs Shape Pos a0}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos a a0)" + ++ " := { shareArgs := shareArgsFoo__ }. " it "renames constructors with same name as their data type" $ shouldSucceedWith $ do @@ -262,6 +427,27 @@ testConvertDataDecls ++ "Notation \"'@Foo0' Shape Pos\" :=" ++ " (@pure Shape Pos (Foo Shape Pos) (@foo Shape Pos))" ++ " ( only parsing, at level 10, Shape, Pos at level 9 ). " + ++ "(* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo" + ++ " {Shape : Type} {Pos : Shape -> Type} (x : Foo Shape Pos)" + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos) " + ++ " := let 'foo := x in pure foo. " + ++ "Instance NormalformFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " : Normalform Shape Pos (Foo Shape Pos)" + ++ " := { nf' := nf'Foo }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " (x : Foo Shape Pos)" + ++ " : Free Shape Pos (Foo Shape Pos)" + ++ " := let 'foo := x in pure foo. " + ++ "Instance ShareableArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos)" + ++ " := { shareArgs := shareArgsFoo }. " it "renames type variables with same name as generated constructors" $ shouldSucceedWith $ do @@ -288,6 +474,35 @@ testConvertDataDecls ++ "Notation \"'@A' Shape Pos a0 x\" :=" ++ " (@pure Shape Pos (Foo Shape Pos a0) (@a Shape Pos a0 x))" ++ " ( only parsing, at level 10, Shape, Pos, a0, x at level 9 ). " + ++ "(* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo_" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a0 : Type} `{Normalform Shape Pos a0}" + ++ " (x : Foo Shape Pos a0)" + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos" + ++ " (@nType Shape Pos a0 _))" + ++ " := let 'a x0 := x" + ++ " in nf x0 >>= (fun nx => pure (a (pure nx))). " + ++ "Instance NormalformFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a0 : Type} `{Normalform Shape Pos a0}" + ++ " : Normalform Shape Pos (Foo Shape Pos a0)" + ++ " := { nf' := nf'Foo_ }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a0 : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos} " + ++ " `{ShareableArgs Shape Pos a0} (x : Foo Shape Pos a0) " + ++ " : Free Shape Pos (Foo Shape Pos a0)" + ++ " := let 'a x0 := x" + ++ " in cbneed Shape Pos shareArgs x0 >>= (fun sx =>" + ++ " pure (a sx)). " + ++ "Instance ShareableArgsFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a0 : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " `{ShareableArgs Shape Pos a0}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos a0)" + ++ " := { shareArgs := shareArgsFoo_ }." it "translates mutually recursive data types correctly" $ shouldSucceedWith $ do @@ -332,6 +547,57 @@ testConvertDataDecls ++ "Notation \"'@Bar0' Shape Pos x\" :=" ++ " (@pure Shape Pos (Bar Shape Pos) (@bar Shape Pos x))" ++ " ( only parsing, at level 10, Shape, Pos, x at level 9 ). " + ++ "(* Normalform instances for Foo, Bar *) " + ++ "Fixpoint nf'Foo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " (x : Foo Shape Pos)" + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos)" + ++ " := let 'foo x0 := x" + ++ " in x0 >>= (fun x1 =>" + ++ " nf'Bar x1 >>= (fun nx => pure (foo (pure nx)))) " + ++ "with nf'Bar" + ++ " {Shape : Type} {Pos : Shape -> Type} (x : Bar Shape Pos)" + ++ " : Free Shape Pos (Bar Identity.Shape Identity.Pos)" + ++ " := let 'bar x0 := x" + ++ " in x0 >>= (fun x1 =>" + ++ " nf'Foo x1 >>= (fun nx =>" + ++ " pure (bar (pure nx)))). " + ++ "Instance NormalformFoo" + ++ " {Shape : Type} {Pos : Shape -> Type} " + ++ " : Normalform Shape Pos (Foo Shape Pos) " + ++ " := { nf' := nf'Foo }. " + ++ "Instance NormalformBar" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " : Normalform Shape Pos (Bar Shape Pos)" + ++ " := { nf' := nf'Bar }. " + ++ "(* ShareableArgs instances for Foo, Bar *) " + ++ "Fixpoint shareArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " (x : Foo Shape Pos) " + ++ " : Free Shape Pos (Foo Shape Pos)" + ++ " := let 'foo x0 := x" + ++ " in cbneed Shape Pos shareArgsBar x0 >>= (fun sx =>" + ++ " pure (foo sx)) " + ++ "with " + ++ "shareArgsBar" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " (x : Bar Shape Pos)" + ++ " : Free Shape Pos (Bar Shape Pos)" + ++ " := let 'bar x0 := x" + ++ " in cbneed Shape Pos shareArgsFoo x0 >>= (fun sx =>" + ++ " pure (bar sx)). " + ++ "Instance ShareableArgsFoo" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos)" + ++ " := { shareArgs := shareArgsFoo }. " + ++ "Instance ShareableArgsBar" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " : ShareableArgs Shape Pos (Bar Shape Pos)" + ++ " := { shareArgs := shareArgsBar }. " context "Generation of induction schemes" $ do it "creates a correct induction scheme" $ shouldSucceedWith $ do "Foo" <- defineTestTypeCon "Foo" 1 ["Foo"] @@ -368,6 +634,41 @@ testConvertDataDecls ++ " (@pure Shape Pos (Foo Shape Pos a) (@foo Shape Pos a x x0 x1))" ++ " ( only parsing, at level 10, " ++ " Shape, Pos, a, x, x0, x1 at level 9 ). " + ++ "(* Normalform instance for Foo *) " + ++ "Fixpoint nf'Foo_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a : Type}" + ++ " `{Normalform Shape Pos a} (x : Foo Shape Pos a) " + ++ " : Free Shape Pos (Foo Identity.Shape Identity.Pos" + ++ " (@nType Shape Pos a _)) " + ++ " := let 'foo x0 x1 x2 := x" + ++ " in x0 >>= (fun x3 => " + ++ " nf'Foo_ x3 >>= (fun nx =>" + ++ " nf x1 >>= (fun nx0 =>" + ++ " x2 >>= (fun x4 =>" + ++ " nf'Foo_ x4 >>= (fun nx1 =>" + ++ " pure (foo (pure nx) (pure nx0) (pure nx1))))))). " + ++ "Instance NormalformFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type}" + ++ " {a : Type} `{Normalform Shape Pos a}" + ++ " : Normalform Shape Pos (Foo Shape Pos a)" + ++ " := { nf' := nf'Foo_ }. " + ++ "(* ShareableArgs instance for Foo *) " + ++ "Fixpoint shareArgsFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos} " + ++ " `{ShareableArgs Shape Pos a} (x : Foo Shape Pos a) " + ++ " : Free Shape Pos (Foo Shape Pos a)" + ++ " := let 'foo x0 x1 x2 := x " + ++ " in cbneed Shape Pos shareArgsFoo_ x0 >>= (fun sx =>" + ++ " cbneed Shape Pos shareArgs x1 >>= (fun sx0 =>" + ++ " cbneed Shape Pos shareArgsFoo_ x2 >>= (fun sx1 =>" + ++ " pure (foo sx sx0 sx1)))). " + ++ "Instance ShareableArgsFoo_" + ++ " {Shape : Type} {Pos : Shape -> Type} {a : Type}" + ++ " `{Injectable Share.Shape Share.Pos Shape Pos}" + ++ " `{ShareableArgs Shape Pos a}" + ++ " : ShareableArgs Shape Pos (Foo Shape Pos a)" + ++ " := { shareArgs := shareArgsFoo_ }. " context "Generation of qualified smart constructor notations" $ do it "produces qualified notations for a single type correctly" $ shouldSucceedWith @@ -421,24 +722,24 @@ testConvertDataDecls it "produces notations for two mutually recursive types correctly" $ shouldSucceedWith $ do - _ <- defineTestTypeCon "A.Foo1" 1 ["A.Bar1"] - _ <- defineTestTypeCon "A.Foo2" 1 ["A.Bar2"] + _ <- defineTestTypeCon "A.Foo1" 0 ["A.Bar1"] + _ <- defineTestTypeCon "A.Foo2" 0 ["A.Bar2"] _ <- defineTestCon "A.Bar1" 1 "A.Foo2 -> A.Foo1" _ <- defineTestCon "A.Bar2" 1 "A.Foo1 -> A.Foo2" shouldProduceQualifiedNotations (Recursive - ["data A.Foo1 a = A.Bar1 A.Foo2", "data A.Foo2 a = A.Bar2 A.Foo1"]) + ["data A.Foo1 = A.Bar1 A.Foo2", "data A.Foo2 = A.Bar2 A.Foo1"]) $ "(* Qualified smart constructors for Foo1 *) " ++ "Notation \"'A.Bar1' Shape Pos x\" := " - ++ "(@pure Shape Pos _ (@bar1 Shape Pos _ x)) " + ++ "(@pure Shape Pos (Foo1 Shape Pos) (@bar1 Shape Pos x)) " ++ "( at level 10, Shape, Pos, x at level 9 ). " - ++ "Notation \"'@A.Bar1' Shape Pos a x\" := " - ++ "(@pure Shape Pos (Foo1 Shape Pos) (@bar1 Shape Pos a x)) " - ++ "( only parsing, at level 10, Shape, Pos, a, x at level 9 ). " + ++ "Notation \"'@A.Bar1' Shape Pos x\" := " + ++ "(@pure Shape Pos (Foo1 Shape Pos) (@bar1 Shape Pos x)) " + ++ "( only parsing, at level 10, Shape, Pos, x at level 9 ). " ++ "(* Qualified smart constructors for Foo2 *) " ++ "Notation \"'A.Bar2' Shape Pos x\" := " - ++ "(@pure Shape Pos _ (@bar2 Shape Pos _ x)) " + ++ "(@pure Shape Pos (Foo2 Shape Pos) (@bar2 Shape Pos x)) " ++ "( at level 10, Shape, Pos, x at level 9 ). " - ++ "Notation \"'@A.Bar2' Shape Pos a x\" := " - ++ "(@pure Shape Pos (Foo2 Shape Pos) (@bar2 Shape Pos a x)) " - ++ "( only parsing, at level 10, Shape, Pos, a, x at level 9 )." + ++ "Notation \"'@A.Bar2' Shape Pos x\" := " + ++ "(@pure Shape Pos (Foo2 Shape Pos) (@bar2 Shape Pos x)) " + ++ "( only parsing, at level 10, Shape, Pos, x at level 9 )."