diff --git a/base/Prelude.toml b/base/Prelude.toml index 9e5e5f08..468d9a3d 100644 --- a/base/Prelude.toml +++ b/base/Prelude.toml @@ -208,14 +208,17 @@ exported-values = [ ############################################################################## [[types]] - haskell-name = 'Prelude.([])' - coq-name = 'List' - agda-name = 'List' - arity = 1 - cons-names = [ + haskell-name = 'Prelude.([])' + coq-name = 'List' + agda-name = 'List' + arity = 1 + cons-names = [ 'Prelude.([])', 'Prelude.(:)', ] + coq-for-property-name = 'ForList' + coq-in-property-names = ['InList'] + coq-forall-lemma-name = 'ForList_forall' [[constructors]] haskell-type = 'Prelude.([]) a' @@ -240,11 +243,17 @@ exported-values = [ ############################################################################## [[types]] - haskell-name = 'Prelude.(,)' - coq-name = 'Pair' - agda-name = 'Pair' - arity = 2 - cons-names = ['Prelude.(,)'] + haskell-name = 'Prelude.(,)' + coq-name = 'Pair' + agda-name = 'Pair' + arity = 2 + cons-names = ['Prelude.(,)'] + coq-for-property-name = 'ForPair' + coq-in-property-names = [ + 'InPair_1', + 'InPair_2' + ] + coq-forall-lemma-name = 'ForPair_forall' [[constructors]] haskell-type = 'a -> b -> Prelude.(,) a b' diff --git a/base/coq/Free.v b/base/coq/Free.v index 9acf70e7..e081ec8e 100644 --- a/base/coq/Free.v +++ b/base/coq/Free.v @@ -4,4 +4,5 @@ From Base Require Export Free.Induction. From Base Require Export Free.Malias. From Base Require Export Free.Monad. From Base Require Export Free.Tactic.ProveInd. +From Base Require Export Free.Tactic.ProveForall. From Base Require Export Free.Tactic.Simplify. diff --git a/base/coq/Free/Tactic/ProveForall.v b/base/coq/Free/Tactic/ProveForall.v new file mode 100644 index 00000000..898ed0b9 --- /dev/null +++ b/base/coq/Free/Tactic/ProveForall.v @@ -0,0 +1,121 @@ +(* This file contains the tactic [prove_forall] that proofs such a the + [ForallT_forall] lemmas for datatypes. + For each datatype [T] that has type variables, there should be the inductive + property [ForT] and for every tpe variable of that type a Property [InT_a]. + The lemma [ForT_forall] that states the connection between those properties. +*) + +From Base Require Import Free.ForFree. + +Require Import Coq.Program.Equality. + +(* This is the hint database which is used by [prove_forall]. *) +Create HintDb prove_forall_db. + +(* This tactic splits all hypotheses, which are conjunctions, into smaller + hypotheses. *) +Ltac prove_forall_split_hypotheses := + repeat (match goal with + | [H : _ /\ _ |- _] => destruct H + end). + +(* This tactic rewrites a 'ForT' hypothesis [HF] using a forall lemma + [forType_forall] and specializes it using a value [x] for which an 'InT' + hypothesis [IF] exists. + This tactic should be instantiated for types with type variables and added to + [prove_forall_db]. *) +Ltac prove_forall_ForType_InType HF HI x forType_forall := + rewrite forType_forall in HF; + prove_forall_split_hypotheses; + match goal with + | [ HF1 : forall y, _ -> _ |- _ ] => + specialize (HF1 x HI); + auto with prove_forall_db + end. + +(* [prove_forall_ForType_InType] instance of [Free]. + You can use this as reference for instances of + [prove_forall_ForType_InType]. *) +Hint Extern 0 => + match goal with + | [ HF : ForFree _ _ _ _ ?fx + , HI : InFree _ _ _ ?x ?fx + |- _ ] => + prove_forall_ForType_InType HF HI x ForFree_forall + end : prove_forall_db. + +(* Rewrites the goal using the given 'forall' lemma. + This tactic should be instantiated for types with type variables and added to + [prove_forall_db]. *) + Ltac prove_forall_prove_ForType forType_forall := + rewrite forType_forall; + repeat split; + let x := fresh "x" + in let HI := fresh "HI" + in intros x HI; + auto with prove_forall_db. + +(* [prove_forall_prove_ForType] instance of [Free]. *) +Hint Extern 0 (ForFree _ _ _ _ _) => + prove_forall_prove_ForType ForFree_forall : prove_forall_db. + +(* Applies a hypothesis which is an implication with two fulfilled + preconditions to prove the goal. *) +Ltac prove_forall_trivial_imp := + match goal with + | [ HImp : ?TF -> ?TI -> ?P + , HF : ?TF + , HI : ?TI + |- ?P ] => + apply (HImp HF HI) + end. + +Hint Extern 1 => prove_forall_trivial_imp : prove_forall_db. + +(* Tries to prove an 'InT' property by using an constructor for that type. + This tactic should be instantiated locally with all 'InT' constructors of a + type with type variables and added to [prove_forall_db] when proving the + corresponding 'forall' lemma. *) + Ltac prove_forall_finish_rtl Con := + match goal with + | [ H : (forall y, _ -> ?P y) -> _ + |- _ ] => + apply H; + let x := fresh "x" + in let HI := fresh "HI" + in intros x HI; + auto with prove_forall_db + | [ H : forall y, ?TI -> ?P y |- ?P ?x ] => + apply H; + eapply Con; + eauto + end. + +Hint Extern 1 => prove_forall_finish_rtl : prove_forall_db. + +(* This tactic proves a 'forall' lemma using a given induction scheme for the + corresponding type using the database [prove_forall_db]. + The database should contain an instance of [prove_forall_finish_rtl] for + every 'InT' constructor of that type and instances of + [prove_forall_ForType_InType] and [prove_forall_prove_ForType] for every + dependent type. *) +Ltac prove_forall type_ind := + let C := fresh "C" + in intro C; split; + [ let HF := fresh "HF" + in intro HF; + repeat split; + let x := fresh "x" + in let HI := fresh "HI" + in intros x HI; + induction C using type_ind; + dependent destruction HI; + dependent destruction HF; + auto with prove_forall_db + | let H := fresh "H" + in intro H; + prove_forall_split_hypotheses; + induction C using type_ind; + constructor; + auto with prove_forall_db + ]. diff --git a/base/coq/Free/Tactic/ProveInd.v b/base/coq/Free/Tactic/ProveInd.v index 3b42edc5..e0938839 100644 --- a/base/coq/Free/Tactic/ProveInd.v +++ b/base/coq/Free/Tactic/ProveInd.v @@ -1,41 +1,138 @@ +(* This file contains tactics that help to prove induction schemes for types. + [prove_ind] is able to do such a proof if all required instances of + [prove_ind_prove_for_type] were added to [prove_ind_db]. *) + From Base Require Import Free.ForFree. From Base Require Import Free.Induction. From Base Require Import Free.Monad. Require Import Coq.Program.Equality. -Local Ltac is_fixpoint H P := - match type of H with - | forall x, P x => idtac - end. +(* The hint database that contains instances of [prove_ind_prove_for_type]. *) +Create HintDb prove_ind_db. -Local Ltac prove_ind_apply_assumption := +(* Trivial property. *) +Definition NoProperty {A : Type} : A -> Prop := fun _ => True. +Hint Extern 0 (NoProperty _) => unfold NoProperty; constructor : prove_ind_db. + +(* This tactic is applied at the beginning of the proof of an induction scheme + to select the correct hypothesis for the current induction case. *) +Ltac prove_ind_select_case FP := match goal with - | [ H : _ |- ?P ?x ] => tryif is_fixpoint H P then fail else apply H + | [ H : ?T |- _ ] => + lazymatch type of FP with + | T => fail + | _ => apply H; clear H + end end. -Local Ltac prove_ind_prove_for_free FP := +(* This tactic eliminates the monadic layer of an induction hypothesis. *) +Ltac prove_ind_prove_ForFree := match goal with - | [ fx: Free ?Shape ?Pos ?T |- _ ] => + | [ fx : Free ?Shape ?Pos _ |- _ ] => match goal with - | [ |- ForFree Shape Pos T ?P fx ] => - let x1 := fresh "x" - in let H := fresh "H" - in let x2 := fresh "x" + | [ |- ForFree Shape Pos ?T ?P fx ] => + apply ForFree_forall; + let x1 := fresh "x" + in let H := fresh "H" + in intros x1 H; + let x2 := fresh "x" in let s := fresh "s" in let pf := fresh "pf" in let IHpf := fresh "IHpf" - in let p := fresh "p" - in apply ForFree_forall; intros x1 H; - induction fx as [ x2 | s pf IHpf ] using Free_Ind; - [ inversion H; subst; apply FP - | dependent destruction H; subst; destruct H as [ p ]; - apply (IHpf p); apply H ] + in induction fx as [ x2 | s pf IHpf ] using Free_Ind; + [ inversion H; subst; clear H + | dependent destruction H; + match goal with + | [ IHpf : forall p : Pos s, InFree Shape Pos T ?x1 (pf p) -> P ?x1 + , H : exists q : Pos s, InFree Shape Pos T ?x1 (pf q) + |- _ ] => + let p := fresh "p" + in destruct H as [ p H ]; + apply (IHpf p H) + end ] + end + end. + +(* This tactic tries to finish the proof with a given hypothesis with fulfilled + preconditions. *) +Ltac prove_ind_apply_hypothesis H := + match type of H with + | ?PC -> _ => + match goal with + | [ H2 : PC |- _ ] => specialize (H H2); prove_ind_apply_hypothesis H end + | _ => apply H end. +Hint Extern 0 => prove_ind_apply_hypothesis : prove_ind_db. + +(* This tactic splits all hypotheses, which are conjunctions, into smaller + hypotheses. *) +Ltac prove_ind_split_hypotheses := + repeat (match goal with + | [H : _ /\ _ |- _] => destruct H + end). + +(* This tactic rewrites a 'ForT' hypothesis [HF] using a forall lemma + [forType_forall] and specializes it using a value [x] for which an 'InT' + hypothesis [IF] exists. *) +Ltac prove_ind_ForType_InType HF HI x forType_forall := + rewrite forType_forall in HF; + prove_ind_split_hypotheses; + match goal with + | [ HF1 : forall y, _ -> _ |- _ ] => + specialize (HF1 x HI); + try (prove_ind_apply_hypothesis HF1) + end. + +(* This tactic eliminates intermediate monadic layers. *) +Ltac prove_ind_prove_ForFree_InFree := + match goal with + | [ HIF : InFree ?Shape ?Pos ?T ?x ?fx + , IH : ForFree ?Shape ?Pos ?T _ ?fx + |- _ ] => + rewrite ForFree_forall in IH; + specialize (IH x HIF); clear HIF; + try (prove_ind_apply_hypothesis IH) + | [ HIF : InFree ?Shape ?Pos ?T ?x ?fx + |- ?P ?x ] => + let x1 := fresh "x" + in let s := fresh "s" + in let pf := fresh "pf" + in let IHpf := fresh "IHpf" + in induction fx as [ x1 | s pf IHpf ] using Free_Ind; + [ inversion HIF; subst; clear HIF + | dependent destruction HIF; + match goal with + | [H : exists p : Pos s, InFree Shape Pos T x (pf p) |- _ ] => + let p := fresh "p" + in destruct H as [ p H ]; apply (IHpf p H); easy + end + ] + end. + +(* Tries to prove a 'ForT' property for [x] by using the given 'forall' lemma + and induction scheme. + This tactic should be instantiated for types with type variables and added + to [prove_ind_db]. *) +Ltac prove_ind_prove_ForType x forType_forall type_ind := + apply forType_forall; + repeat split; + induction x using type_ind; + let y := fresh "y" + in let H := fresh "H" + in intros y H; inversion H; subst; clear H; + prove_ind_prove_ForFree_InFree. + +(* This tactic proves the induction scheme for a type. + It requires the database [prove_ind_db] to contain instances of + [prove_ind_prove_ForType] for all dependent types. *) Ltac prove_ind := match goal with | [ FP : forall y, ?P y |- ?P ?x ] => - destruct x; prove_ind_apply_assumption; prove_ind_prove_for_free FP + destruct x; + prove_ind_select_case FP; + prove_ind_prove_ForFree; + auto with prove_ind_db end. diff --git a/base/coq/Prelude/List.v b/base/coq/Prelude/List.v index bdab5f69..fd555bc5 100644 --- a/base/coq/Prelude/List.v +++ b/base/coq/Prelude/List.v @@ -9,11 +9,13 @@ Section SecList. Variable Pos : Shape -> Type. Notation "'Free''" := (Free Shape Pos). + Unset Elimination Schemes. Inductive List (A : Type) : Type := | nil : List A | cons : Free' A -> Free' (List A) -> List A. + Set Elimination Schemes. -End SecList. + End SecList. (* smart constructors *) @@ -105,14 +107,14 @@ Section SecListInd. (fxs : Free Shape Pos (List Shape Pos A)), ForFree Shape Pos (List Shape Pos A) P fxs -> P (cons fx fxs). - Fixpoint List_Ind (l : List Shape Pos A) : P l. + Fixpoint List_ind (l : List Shape Pos A) : P l. Proof. destruct l. - apply nilP. - apply consP. apply (ForFree_forall Shape Pos). intros xs HIn. induction f0 using Free_Ind. - + inversion HIn; subst. apply List_Ind. + + inversion HIn; subst. apply List_ind. + dependent destruction HIn; subst. destruct H0 as [ p ]. apply H with (p := p). apply H0. Defined. @@ -174,3 +176,58 @@ Section SecFreeListInd. FreeList_rect Shape Pos A PF P NilFP ConsFP PureListF ImpureP fxs. End SecFreeListInd. + +(* [ForList] property to generate induction hypotheses over lists. *) +Inductive ForList (Shape : Type) (Pos : Shape -> Type) (a : Type) (P0 : a -> Prop) + : List Shape Pos a -> Prop + := ForList_nil : ForList Shape Pos a P0 (@nil Shape Pos a) + | ForList_cons + : forall (x : Free Shape Pos a) (x0 : Free Shape Pos (List Shape Pos a)), + ForFree Shape Pos a P0 x -> + ForFree Shape Pos (List Shape Pos a) (ForList Shape Pos a P0) x0 -> + ForList Shape Pos a P0 (@cons Shape Pos a x x0). + +Inductive InList (Shape : Type) (Pos : Shape -> Type) (a : Type) + : a -> List Shape Pos a -> Prop + := InList_cons + : forall (x1 : a) + (x : Free Shape Pos a) + (x0 : Free Shape Pos (List Shape Pos a)), + InFree Shape Pos a x1 x -> InList Shape Pos a x1 (@cons Shape Pos a x x0) + | InList_cons0 + : forall (x1 : a) + (x2 : List Shape Pos a) + (x : Free Shape Pos a) + (x0 : Free Shape Pos (List Shape Pos a)), + InList Shape Pos a x1 x2 -> + InFree Shape Pos (List Shape Pos a) x2 x0 -> + InList Shape Pos a x1 (@cons Shape Pos a x x0). + + +(* 'Forall' lemma to rewrite [ForList] properties. *) +Lemma ForList_forall : forall (Shape : Type) + (Pos : Shape -> Type) + (a : Type) + (P0 : a -> Prop) + (x : List Shape Pos a), + ForList Shape Pos a P0 x <-> + (forall (y : a), InList Shape Pos a y x -> P0 y). +Proof. + intros Shape Pos a P0. + Local Hint Extern 1 => prove_forall_finish_rtl InList_cons : prove_forall_db. + Local Hint Extern 1 => prove_forall_finish_rtl InList_cons0 : prove_forall_db. + prove_forall List_ind. +Defined. + +(* Add hints for proof generation. *) +Hint Extern 0 (ForList _ _ _ _ ?x) => + prove_ind_prove_ForType x ForList_forall List_ind : prove_ind_db. +Hint Extern 0 => + match goal with + | [ HF : ForList ?Shape ?Pos ?T _ ?fx + , HI : InList ?Shape ?Pos ?T ?x ?fx + |- _ ] => + prove_forall_ForType_InType HF HI x ForList_forall + end : prove_forall_db. +Hint Extern 0 (ForList _ _ _ _ _) => + prove_forall_prove_ForType ForList_forall : prove_forall_db. diff --git a/base/coq/Prelude/Pair.v b/base/coq/Prelude/Pair.v index 5a0728f2..50ad2a8c 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. +Require Import Coq.Program.Equality. + Section SecPair. Variable Shape : Type. Variable Pos : Shape -> Type. @@ -62,3 +64,62 @@ Instance ShareableArgsPair {Shape : Type} {Pos : Shape -> Type} (A B : Type) (pure (pair_ sx sy)) end }. + +(* [ForPair] property to generate induction hypotheses over pairs. *) +Inductive ForPair (Shape : Type) (Pos : Shape -> Type) (a b : Type) (P0 : a -> Prop) (P1 : b -> Prop) + : Pair Shape Pos a b -> Prop + := ForPair_pair_ + : forall (x : Free Shape Pos a) (x0 : Free Shape Pos b), + ForFree Shape Pos a P0 x -> + ForFree Shape Pos b P1 x0 -> + ForPair Shape Pos a b P0 P1 (@pair_ Shape Pos a b x x0). + +Inductive InPair_1 (Shape : Type) (Pos : Shape -> Type) (a b : Type) + : a -> Pair Shape Pos a b -> Prop + := InPair_1_pair_ + : forall (x1 : a) (x : Free Shape Pos a) (x0 : Free Shape Pos b), + InFree Shape Pos a x1 x -> + InPair_1 Shape Pos a b x1 (@pair_ Shape Pos a b x x0) +with InPair_2 (Shape : Type) (Pos : Shape -> Type) (a b : Type) + : b -> Pair Shape Pos a b -> Prop + := InPair_2_pair_ + : forall (x1 : b) (x : Free Shape Pos a) (x0 : Free Shape Pos b), + InFree Shape Pos b x1 x0 -> + InPair_2 Shape Pos a b x1 (@pair_ Shape Pos a b x x0). + +(* 'Forall' lemma to rewrite [ForPair] properties. *) +Lemma ForPair_forall : forall (Shape : Type) + (Pos : Shape -> Type) + (a b : Type) + (P0 : a -> Prop) + (P1 : b -> Prop) + (x : Pair Shape Pos a b), + ForPair Shape Pos a b P0 P1 x <-> + ((forall (y : a), InPair_1 Shape Pos a b y x -> P0 y) /\ + (forall (y : b), InPair_2 Shape Pos a b y x -> P1 y)). +Proof. + intros Shape Pos a b P0 P1. + Local Hint Extern 1 => prove_forall_finish_rtl InPair_1_pair_ : prove_forall_db. + Local Hint Extern 1 => prove_forall_finish_rtl InPair_2_pair_ : prove_forall_db. + prove_forall Pair_ind. +Defined. + +(* Add hints for proof generation. *) +Hint Extern 0 (ForPair _ _ _ _ _ _ ?x) => + prove_ind_prove_ForType x ForPair_forall Pair_ind : prove_ind_db. +Hint Extern 0 => + match goal with + | [ HF : ForPair ?Shape ?Pos ?T1 ?T2 _ _ ?fx + , HI : InPair_1 ?Shape ?Pos ?T1 ?T2 ?x ?fx + |- _ ] => + prove_forall_ForType_InType HF HI x ForPair_forall + end : prove_forall_db. +Hint Extern 0 => + match goal with + | [ HF : ForPair ?Shape ?Pos ?T1 ?T2 _ _ ?fx + , HI : InPair_2 ?Shape ?Pos ?T1 ?T2 ?x ?fx + |- _ ] => + prove_forall_ForType_InType HF HI x ForPair_forall + end : prove_forall_db. +Hint Extern 0 (ForPair _ _ _ _ _ _ _) => + prove_forall_prove_ForType ForPair_forall : prove_forall_db. diff --git a/cabal.project b/cabal.project index 9b693742..11438d5c 100644 --- a/cabal.project +++ b/cabal.project @@ -3,7 +3,7 @@ source-repository-package type: git location: git://github.com/FreeProving/language-coq.git - tag: v0.2.0.0 + tag: v0.3.0.0 -- The `haskell-src-transformations` package is still in an early development -- state and thus not available on Hackage. The dependency is downloaded diff --git a/example/Proofs/InductionSchemes.hs b/example/Proofs/InductionSchemes.hs new file mode 100644 index 00000000..bb7f6481 --- /dev/null +++ b/example/Proofs/InductionSchemes.hs @@ -0,0 +1,7 @@ +module Proofs.InductionSchemes where + +data MyList a = MyNil | MyCons a (MyList a) + +data Tree a = Forest a (MyList (Tree a)) + +data MyType a = MyCon (Tree (MyType a)) diff --git a/free-compiler.cabal b/free-compiler.cabal index 533050c0..4833057d 100644 --- a/free-compiler.cabal +++ b/free-compiler.cabal @@ -48,7 +48,7 @@ common deps -- ASTs: , Agda ==2.6.* , haskell-src-exts ==1.23.* - , language-coq ==0.2.* + , language-coq ==0.3.* -- Configuration: , aeson ==1.4.* , aeson-pretty ==0.8.* @@ -114,6 +114,7 @@ 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.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 96d98c87..793923a3 100644 --- a/src/lib/FreeC/Backend/Coq/Base.hs +++ b/src/lib/FreeC/Backend/Coq/Base.hs @@ -14,6 +14,7 @@ module FreeC.Backend.Coq.Base , freeBind , freeArgs , forFree + , inFree -- * Partiality , partial , partialArg @@ -30,6 +31,8 @@ module FreeC.Backend.Coq.Base , shareableArgsBinder , implicitArg , share + -- * Induction Schemes + , noProperty -- * Effect Selection , selectExplicitArgs , selectImplicitArgs @@ -41,6 +44,15 @@ module FreeC.Backend.Coq.Base , stringScope -- * Tactics , proveInd + , proveIndProveForType + , proveIndForTypeInType + , proveForall + , proveForallForTypeInType + , proveForallProveForType + , proveForallFinish + -- * Hint Databases + , proveIndDb + , proveForallDb -- * Reserved Identifiers , reservedIdents ) where @@ -110,6 +122,10 @@ freeArgs = [ (shape, Coq.Sort Coq.Type) forFree :: Coq.Qualid forFree = Coq.bare "ForFree" +-- | The Coq identifier for the @InFree@ property. +inFree :: Coq.Qualid +inFree = Coq.bare "InFree" + ------------------------------------------------------------------------------- -- Partiality -- ------------------------------------------------------------------------------- @@ -194,6 +210,13 @@ implicitArg = Coq.Underscore share :: Coq.Qualid share = Coq.bare "share" +------------------------------------------------------------------------------- +-- Induction Schemes -- +------------------------------------------------------------------------------- +-- | The Coq Identifier for a trivial property. +noProperty :: Coq.Qualid +noProperty = Coq.bare "NoProperty" + ------------------------------------------------------------------------------- -- Effect selection -- ------------------------------------------------------------------------------- @@ -239,8 +262,46 @@ stringScope = Coq.ident "string" -- Tactics -- ------------------------------------------------------------------------------- -- | The tactic that is needed to prove induction schemes. -proveInd :: Coq.Qualid -proveInd = Coq.bare "prove_ind" +proveInd :: Coq.Ident +proveInd = Coq.ident "prove_ind" + +-- | The tactic that has to be instantiated for data types and added to +-- 'proveIndDb'. +proveIndProveForType :: Coq.Ident +proveIndProveForType = Coq.ident "prove_ind_prove_ForType" + +proveIndForTypeInType :: Coq.Ident +proveIndForTypeInType = Coq.ident "prove_ind_ForType_InType" + +-- | The tactic that is needed to prove 'forall' lemmas. +proveForall :: Coq.Ident +proveForall = Coq.ident "prove_forall" + +-- | One of the tactics that have to be instantiated for data types and added +-- to 'proveIndDb'. +proveForallForTypeInType :: Coq.Ident +proveForallForTypeInType = Coq.ident "prove_forall_ForType_InType" + +-- | One of the tactics that have to be instantiated for data types and added +-- to 'proveIndDb'. +proveForallProveForType :: Coq.Ident +proveForallProveForType = Coq.ident "prove_forall_prove_ForType" + +-- | This tactic has to be instantiated for data types and added locally to +-- 'proveIndDb' in the proof of the corresponding 'forall' lemma. +proveForallFinish :: Coq.Ident +proveForallFinish = Coq.ident "prove_forall_finish_rtl" + +------------------------------------------------------------------------------- +-- Hint Databases -- +------------------------------------------------------------------------------- +-- | The hint database that is used by 'proveInd'. +proveIndDb :: Coq.Ident +proveIndDb = Coq.ident "prove_ind_db" + +-- | The hint database that is used by 'proveForall'. +proveForallDb :: Coq.Ident +proveForallDb = Coq.ident "prove_forall_db" ------------------------------------------------------------------------------- -- Reserved Identifiers -- @@ -255,6 +316,7 @@ reservedIdents , freePureCon , freeImpureCon , forFree + , inFree -- Partiality , partial , partialArg @@ -268,5 +330,7 @@ reservedIdents , strategyArg , shareableArgs , share + -- Induction Schemes + , noProperty ] ++ map fst freeArgs diff --git a/src/lib/FreeC/Backend/Coq/Converter/Arg.hs b/src/lib/FreeC/Backend/Coq/Converter/Arg.hs index a9acabcb..8fcc075c 100644 --- a/src/lib/FreeC/Backend/Coq/Converter/Arg.hs +++ b/src/lib/FreeC/Backend/Coq/Converter/Arg.hs @@ -92,3 +92,12 @@ convertAnonymousArg mArgType = do mArgType' <- mapM convertType mArgType binder <- generateArgBinder ident' mArgType' return (ident', binder) + +-- | Like 'convertAnonymousArg' but does not lift the type into the @Free@ +-- monad. +convertAnonymousArg' :: Maybe IR.Type -> Converter (Coq.Qualid, Coq.Binder) +convertAnonymousArg' mArgType = do + ident' <- freshCoqQualid freshArgPrefix + mArgType' <- mapM convertType' mArgType + binder <- generateArgBinder ident' mArgType' + return (ident', binder) diff --git a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs index b70de9eb..74f1be10 100644 --- a/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs +++ b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl.hs @@ -13,26 +13,32 @@ 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 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 @@ -126,12 +132,15 @@ convertTypeSynDecl (IR.DataDecl _ _ _ _) convertDataDecls :: [IR.TypeDecl] -> Converter ([Coq.Sentence], [Coq.Sentence]) convertDataDecls dataDecls = do (indBodies, extraSentences') <- mapAndUnzipM convertDataDecl dataDecls + inductionSentences <- generateInductionSchemes dataDecls let (extraSentences, qualSmartConDecls) = concatUnzip extraSentences' return ( Coq.comment ("Data type declarations for " ++ showPretty (map IR.typeDeclName dataDecls)) + : Coq.unsetOption (Just Coq.Local) "Elimination Schemes" : Coq.InductiveSentence (Coq.Inductive (NonEmpty.fromList indBodies) []) - : extraSentences + : Coq.setOption (Just Coq.Local) "Elimination Schemes" Nothing + : extraSentences ++ inductionSentences , qualSmartConDecls ) @@ -148,15 +157,11 @@ 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 " @@ -298,79 +303,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..912cc2c1 --- /dev/null +++ b/src/lib/FreeC/Backend/Coq/Converter/TypeDecl/InductionScheme.hs @@ -0,0 +1,902 @@ +-- This module defines and proofs induction schemes for data declarations. +-- It also creates helper types and lemmas for those induction schemes. +module FreeC.Backend.Coq.Converter.TypeDecl.InductionScheme where + +import Control.Monad ( mapAndUnzipM, zipWithM ) +import Control.Monad.Extra ( concatMapM ) +import Data.List ( intercalate, nub ) +import qualified Data.List.NonEmpty as NonEmpty +import qualified Data.Map.Strict as Map +import Data.Maybe + ( catMaybes, fromJust, fromMaybe ) +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 FreeC.Environment.LookupOrFail ( lookupIdentOrFail ) +import qualified FreeC.IR.Syntax as IR +import FreeC.IR.TypeSynExpansion +import FreeC.Monad.Converter +import FreeC.Pretty + +type LookupMap a = Map.Map IR.QName a + +-- | Creates induction schemes and helpers for a list of data declarations. +generateInductionSchemes :: [IR.TypeDecl] -> Converter [Coq.Sentence] +generateInductionSchemes dataDecls = do + -- Filter the data declarations that need helpers. + let complexDataDecls = filter hasTypeVar dataDecls + -- Generate names. + forQualidMap <- Map.fromList + <$> mapM (generateName "For" "" . IR.typeDeclQName) complexDataDecls + inQualidMap <- Map.fromList + <$> mapM (generateInNames . IR.typeDeclQName) complexDataDecls + schemeQualidMap <- Map.fromList + <$> mapM (generateName "" "_ind" . IR.typeDeclQName) dataDecls + forallQualidMap <- Map.fromList + <$> mapM (generateName "For" "_forall" . IR.typeDeclQName) complexDataDecls + -- Generate properties. + forBodies <- mapM (generateForProperty forQualidMap) complexDataDecls + (inBodies', inConNames) <- mapAndUnzipM (generateInProperties inQualidMap) + complexDataDecls + let inBodies = concat inBodies' + -- Generate induction schemes. + schemeBodies <- mapM (generateSchemeLemma schemeQualidMap forQualidMap) + dataDecls + -- Generate lemmas and hints. + forallBodies <- zipWithM (generateForallLemma schemeQualidMap forallQualidMap + forQualidMap inQualidMap) inConNames + complexDataDecls + hintSentences <- concatMapM + (generateHints schemeQualidMap forallQualidMap forQualidMap inQualidMap) + complexDataDecls + -- Insert names into environment. + mapM_ (insertPropertiesInEnv forQualidMap inQualidMap forallQualidMap + . IR.typeDeclQName) complexDataDecls + -- Return result + return + (Coq.commentedSentences + ("ForType properties for " ++ showPretty (map IR.typeDeclName dataDecls)) + [Coq.InductiveSentence (Coq.Inductive (NonEmpty.fromList forBodies) []) + | not (null forBodies) + ] + ++ Coq.commentedSentences + ("InType properties for " ++ showPretty (map IR.typeDeclName dataDecls)) + [Coq.InductiveSentence (Coq.Inductive (NonEmpty.fromList inBodies) []) + | not (null inBodies) + ] + ++ Coq.commentedSentences + ("Induction schemes for " ++ showPretty (map IR.typeDeclName dataDecls)) + (map (\(name, binders, term, proof) -> Coq.AssertionSentence + (Coq.Assertion Coq.Lemma name binders term) proof) schemeBodies) + ++ Coq.commentedSentences + ("Forall lemmas for " ++ showPretty (map IR.typeDeclName dataDecls)) + (map (\(name, binders, term, proof) -> Coq.AssertionSentence + (Coq.Assertion Coq.Lemma name binders term) proof) forallBodies) + ++ Coq.commentedSentences "Give hints" hintSentences) + where + ----------------------------------------------------------------------------- + -- @ForType@ Properties -- + ----------------------------------------------------------------------------- + -- | Generates the 'For-' property for a given data declaration. + -- If the data declaration has @n@ type variables @a1 ... an@ then the property + -- will be of the form: + -- > ForType Shape Pos a_1 ... a_n P_1 ... P_n x + -- This property states that for every @1 <= i <= n@ and every element @y@ of + -- type @a_i@ which is contained in @x@, the property @P_i y@ holds. + generateForProperty + :: LookupMap Coq.Qualid -> IR.TypeDecl -> Converter Coq.IndBody + generateForProperty _ (IR.TypeSynDecl _ _ _ _) + = error "generateForProperty: Type synonym not allowed" + generateForProperty forQualidMap + (IR.DataDecl _ (IR.DeclIdent srcSpan typeName) typeVarDecls conDecls) = do + -- Generate constructor names. + forConQualids <- mapM (generateConName forQualid . IR.conDeclQName) + conDecls + -- Enter local environment. + localEnv $ do + -- Collect and generate relevant Coq names. + typeQualid <- lookupIdentOrFail srcSpan IR.TypeScope typeName + (typeVarQualids, typeVarBinders) + <- convertTypeVarDecls' Coq.Explicit typeVarDecls + propertyQualids <- mapM (const $ freshCoqQualid "P") typeVarQualids + -- Generate constructors for the 'For-' property. + forCons <- zipWithM + (generateForConstructor typeVarQualids propertyQualids) conDecls + forConQualids + -- Stick everything together. + let propertyTypes = map + (\a -> Coq.Arrow (Coq.Qualid a) (Coq.Sort Coq.Prop)) + typeVarQualids + propertyBinders = zipWith + (Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit) + propertyQualids propertyTypes + binders = genericArgDecls Coq.Explicit + ++ typeVarBinders + ++ propertyBinders + returnType = Coq.Arrow + (genericApply typeQualid [] [] (map Coq.Qualid typeVarQualids)) + (Coq.Sort Coq.Prop) + return $ Coq.IndBody forQualid binders returnType forCons + where + -- | The name of the 'For-' property which we are generating. + forQualid :: Coq.Qualid + forQualid = forQualidMap Map.! typeName + + -- | Generates a constructor for the 'For-' property. + generateForConstructor + :: [Coq.Qualid] + -> [Coq.Qualid] + -> IR.ConDecl + -> Coq.Qualid + -> Converter (Coq.Qualid, [Coq.Binder], Maybe Coq.Term) + generateForConstructor typeVarQualids propertyQualids + (IR.ConDecl _ (IR.DeclIdent srcSpan' conName) args) forConQualid + = localEnv $ do + -- Collect and generate relevant Coq names. + conQualid <- lookupIdentOrFail srcSpan' IR.ValueScope conName + (argQualids, binders) <- unzip + <$> mapM (convertAnonymousArg . Just) args + -- Generate a hypothesis for every argument of the constructor. + -- But ignore trivial hypotheses. + forHypotheses + <- catMaybes <$> zipWithM generateForHypothesis argQualids args + -- Generate constructor. + let forResult = genericApply forQualid [] [] + (map Coq.Qualid typeVarQualids + ++ map Coq.Qualid propertyQualids + ++ [ genericApply conQualid [] (map Coq.Qualid typeVarQualids) + (map Coq.Qualid argQualids) + ]) + returnType = Coq.forall binders + (foldr Coq.Arrow forResult forHypotheses) + return (forConQualid, [], Just returnType) + where + propertyMap :: Map.Map Coq.Qualid Coq.Qualid + propertyMap = Map.fromList $ zip typeVarQualids propertyQualids + + -- | Generates an hypothesis for an argument of a 'For-' constructor. + generateForHypothesis + :: Coq.Qualid -> IR.Type -> Converter (Maybe Coq.Term) + generateForHypothesis argQualid argType = do + -- Expand type synonyms in the argument type and search for occurrences of the type variables. + coqType <- convertType' argType + argType' <- expandAllTypeSynonyms argType + mbHyp <- generateForHypothesis_1 0 argType' + -- Wrap generated hypothesis in a @ForFree@ property and apply it to the argument. + return $ case mbHyp of + Just hyp -> Just + $ genericApply Coq.Base.forFree [] [] + [coqType, hyp, Coq.Qualid argQualid] + Nothing -> Nothing + + -- | Generates an hypothesis for a by searching in the given IR type. + -- Memorizes the depth of the current search path. + generateForHypothesis_1 :: Int -> IR.Type -> Converter (Maybe Coq.Term) + generateForHypothesis_1 _ (IR.FuncType _ _ _) = + -- Ignore functions. + return Nothing + generateForHypothesis_1 d (IR.TypeApp _ tcon lastArg) = + -- Unfold the type application. + generateForHypothesis_2 d tcon [lastArg] + generateForHypothesis_1 _ (IR.TypeCon _ _) = + -- Ignore type constructors that do not have any type variable or are partially applied. + return Nothing + generateForHypothesis_1 _ tvar@(IR.TypeVar _ _) = do + -- Lookup hypothesis that has to hold for the given type variable. + Coq.Qualid tvarQualid <- convertType' tvar + return $ Coq.Qualid <$> propertyMap Map.!? tvarQualid + + -- | Unfolds a type application + -- Memorizes the depth of the current search path. + generateForHypothesis_2 + :: Int -> IR.Type -> [IR.Type] -> Converter (Maybe Coq.Term) + generateForHypothesis_2 _ (IR.FuncType _ _ _) _ = + -- Ignore functions. + return Nothing + generateForHypothesis_2 d (IR.TypeApp _ tcon lastArg) typeArgs = + -- Continue unfolding. + generateForHypothesis_2 d tcon (lastArg : typeArgs) + generateForHypothesis_2 d (IR.TypeCon _ tconName) typeArgs = do + -- Recursively generate hypotheses for type arguments. + hypotheses <- mapM (generateForHypothesis_1 (d + 1)) typeArgs + -- Only consider fully applied type constructors and only generate a + -- complex hypothesis, if any of the hypotheses for the arguments is + -- non trivial. + Just tconArity <- inEnv $ lookupArity IR.TypeScope tconName + if (tconArity == length typeArgs) && not (null $ catMaybes hypotheses) + then do + let hypotheses' = map (fromMaybe (Coq.Qualid Coq.Base.noProperty)) + hypotheses + coqArgs <- mapM convertType' typeArgs + -- Prevent mutual recursion in the hypotheses and prevent + -- direct recursion which is deeper than @maxDepth@. + mbForType <- if tconName == typeName + && all (\(tvar, targ) -> Coq.Qualid tvar == targ) + (zip typeVarQualids coqArgs) + && d <= maxDepth + then + -- Legal recursion. + return $ Just forQualid + else + -- Use already defined 'For-' property + inEnv $ lookupForProperty tconName + -- Wrap generated hypotheses in a 'For-' property. + return ((\forType -> genericApply forType [] [] + (coqArgs ++ hypotheses')) <$> mbForType) + else return Nothing + generateForHypothesis_2 _ (IR.TypeVar _ _) _ = + -- Ignore type variables that are used as type constructors. + return Nothing + + ----------------------------------------------------------------------------- + -- @InType@ Properties -- + ----------------------------------------------------------------------------- + -- | Generate a name for a 'In-' property for each type variable of the given + -- type constructor. + generateInNames :: IR.QName -> Converter (IR.QName, [Coq.Qualid]) + generateInNames typeName = do + Just arity <- inEnv $ lookupArity IR.TypeScope typeName + inQualids <- map snd + <$> if arity == 1 + then mapM (generateName "In" "") [typeName] + else mapM (\index -> generateName "In" ("_" ++ show index) typeName) + [1 .. arity] + return (typeName, inQualids) + + -- | Generates the 'In-' properties for a given data declaration. + generateInProperties :: LookupMap [Coq.Qualid] + -> IR.TypeDecl + -> Converter ([Coq.IndBody], [Coq.Qualid]) + generateInProperties _ (IR.TypeSynDecl _ _ _ _) + = error "generateInProperty: Type synonym not allowed" + generateInProperties inQualidMap + (IR.DataDecl _ (IR.DeclIdent _ typeName) typeVarDecls conDecls) = do + (bodies, inConNames) <- mapAndUnzipM + (generateInProperty inQualidMap typeName typeVarDecls conDecls) + [0 .. length typeVarDecls - 1] + return (bodies, concat inConNames) + + -- | Generates an 'In-' property for a given data declaration and the type + -- variable number @index@ of that type and returns the names of its + -- constructors. + -- If the data declaration has @n@ type variables @a1 ... an@ then the + -- property will be of the form: + -- > InType Shape Pos a_1 ... a_n y x + -- This property states that the element @y@ of type @a_index@ is contained + -- in @x@. + generateInProperty :: LookupMap [Coq.Qualid] + -> IR.QName + -> [IR.TypeVarDecl] + -> [IR.ConDecl] + -> Int + -> Converter (Coq.IndBody, [Coq.Qualid]) + generateInProperty inQualidMap typeName typeVarDecls conDecls index = do + -- In contrast to the generation of the 'For-' properties the number of + -- constructors for a 'In-' property is not known yet. + -- Therefore we retrieve components from the local environment and connect + -- them outside of the local environment where we can add the required + -- environment entries. + (cons, mkBody) <- localEnv $ do + -- Collect and generate relevant Coq names. + Just typeQualid <- inEnv $ lookupIdent IR.TypeScope typeName + (typeVarQualids, typeVarBinders) + <- convertTypeVarDecls' Coq.Explicit typeVarDecls + -- Generate constructors for the 'In-' property. + cons <- concatMapM (generateInConstructors typeVarQualids) conDecls + -- Start sticking everything together. + let binders = genericArgDecls Coq.Explicit ++ typeVarBinders + returnType = Coq.Arrow (Coq.Qualid $ typeVarQualids !! index) + (Coq.Arrow (genericApply typeQualid [] [] + (map Coq.Qualid typeVarQualids)) (Coq.Sort Coq.Prop)) + mkBody = Coq.IndBody inQualid binders returnType + return (cons, mkBody) + -- Generate constructor names and add empty binding list. + inConNames <- mapM (generateConName inQualid . fst) cons + let cons' = zipWith (\inConName mbConType -> (inConName, [], mbConType)) + inConNames + $ map snd cons + return (mkBody cons', inConNames) + where + -- | The name of the 'In-' property which we are generating. + inQualid :: Coq.Qualid + inQualid = (inQualidMap Map.! typeName) !! index + + -- | Generates constructors for the 'In-' property. + generateInConstructors + :: [Coq.Qualid] -> IR.ConDecl -> Converter [(IR.QName, Maybe Coq.Term)] + generateInConstructors typeVarQualids + (IR.ConDecl _ (IR.DeclIdent srcSpan conName) args) = localEnv $ do + -- Collect and generate relevant Coq names. + conQualid <- lookupIdentOrFail srcSpan IR.ValueScope conName + (argQualids, argBinders) <- unzip + <$> mapM (convertAnonymousArg . Just) args + elemQualid <- freshCoqQualid "x" + -- Find occurrences of the relevant type variable in the arguments. + occurrences <- concatMapM (uncurry $ findOccurrences elemQualid) + $ zip argQualids args + -- Generate a constructor for each occurrence. + let inResult = genericApply inQualid [] [] + (map Coq.Qualid typeVarQualids + ++ [Coq.Qualid elemQualid] + ++ [ genericApply conQualid [] (map Coq.Qualid typeVarQualids) + (map Coq.Qualid argQualids) + ]) + elemBinder = Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit + elemQualid elemType + mkConType (occBinders, inHypotheses) = Coq.forall + (elemBinder : occBinders ++ argBinders) + (foldr Coq.Arrow inResult (reverse inHypotheses)) + conTypes = map mkConType occurrences + return $ map ((,) conName . Just) conTypes + where + -- | The type variable we are looking for. + elemType :: Coq.Term + elemType = Coq.Qualid (typeVarQualids !! index) + + -- | Smart constructor for an 'In-' property. + inHypothesis + :: Coq.Qualid -> [Coq.Term] -> Coq.Qualid -> Coq.Qualid -> Coq.Term + inHypothesis inQualid' typeArgs containerQualid elemQualid + = genericApply inQualid' [] [] + (typeArgs ++ [Coq.Qualid elemQualid, Coq.Qualid containerQualid]) + + -- | Find occurrences of the relevant type variable in the given type. + findOccurrences :: Coq.Qualid + -> Coq.Qualid + -> IR.Type + -> Converter [([Coq.Binder], [Coq.Term])] + findOccurrences elemQualid argQualid argType = do + -- Expand type synonyms in the argument type and search for occurrences of the type variable. + coqType <- convertType' argType + argType' <- expandAllTypeSynonyms argType + findOccurrences_1 0 elemQualid + (inHypothesis Coq.Base.inFree [coqType] argQualid) argType' + + -- | Find occurrences of the relevant type variable in the given type. + -- Memorizes the depth of the current search path. + findOccurrences_1 :: Int + -> Coq.Qualid + -> (Coq.Qualid -> Coq.Term) + -> IR.Type + -> Converter [([Coq.Binder], [Coq.Term])] + findOccurrences_1 _ _ _ (IR.FuncType _ _ _) = + -- Ignore functions. + return [] + findOccurrences_1 _ _ _ (IR.TypeCon _ _) = + -- Ignore type constructors that do not have any type variable or are partially applied + return [] + findOccurrences_1 _ elemQualid mkInHyp tvar@(IR.TypeVar _ _) = do + -- If this is the desired type variable, return an occurrence. + tvarType <- convertType' tvar + return [([], [mkInHyp elemQualid]) | tvarType == elemType] + findOccurrences_1 d elemQualid mkInHyp fullType@(IR.TypeApp _ _ _) = + -- Unfold type application. + findOccurrences_2 fullType [] + where + -- | Unfolds a type application. + findOccurrences_2 + :: IR.Type -> [IR.Type] -> Converter [([Coq.Binder], [Coq.Term])] + findOccurrences_2 (IR.FuncType _ _ _) _ = + -- Ignore functions. + return [] + findOccurrences_2 (IR.TypeApp _ tcon lastArg) typeArgs = + -- Continue unfolding. + findOccurrences_2 tcon (lastArg : typeArgs) + findOccurrences_2 (IR.TypeVar _ _) _ = + -- Ignore type variables that are used as type constructors. + return [] + findOccurrences_2 (IR.TypeCon _ tconName) typeArgs = localEnv $ do + -- Only consider fully applied type constructors. + Just tconArity <- inEnv $ lookupArity IR.TypeScope tconName + if tconArity == length typeArgs then do + coqArgs <- mapM convertType' typeArgs + -- Prevent mutual recursion in the hypotheses and prevent + -- direct recursion which is deeper than @maxDepth@. + mbInTypes <- if tconName == typeName + && all (\(tvar, targ) -> Coq.Qualid tvar == targ) + (zip typeVarQualids coqArgs) + && d <= maxDepth + then + -- Legal recursion. + return $ inQualidMap Map.!? tconName + else + -- Use already defined 'In-' properties + inEnv $ lookupInProperties tconName + case mbInTypes of + Just inTypes -> do + -- Generate intermediate container and recursively search in type arguments. + (containerQualid, containerBinder) <- convertAnonymousArg' + (Just fullType) + occurrences <- concatMapM + (\(it, arg) -> findOccurrences_1 (d + 1) elemQualid + (inHypothesis it coqArgs containerQualid) arg) + $ zip inTypes typeArgs + let mkNewOcc (occBinders, inHypotheses) + = ( containerBinder : reverse occBinders + , mkInHyp containerQualid : inHypotheses + ) + return $ map mkNewOcc occurrences + Nothing -> return [] else return [] + + ----------------------------------------------------------------------------- + -- Induction Schemes -- + ----------------------------------------------------------------------------- + -- | Generates an induction scheme for the give data type declaration. + generateSchemeLemma + :: LookupMap Coq.Qualid + -> LookupMap Coq.Qualid + -> IR.TypeDecl + -> Converter (Coq.Qualid, [Coq.Binder], Coq.Term, Coq.Proof) + generateSchemeLemma _ _ (IR.TypeSynDecl _ _ _ _) + = error "generateInductionLemma: Type synonym not allowed" + generateSchemeLemma schemeQualidMap forQualidMap + (IR.DataDecl _ (IR.DeclIdent srcSpan typeName) typeVarDecls conDecls) + = localEnv $ do + -- Collect and generate relevant Coq names. + typeQualid <- lookupIdentOrFail srcSpan IR.TypeScope typeName + (tvarQualids, tvarBinders) + <- convertTypeVarDecls' Coq.Explicit typeVarDecls + (propQualid, propBinder) <- generateArg "P" + (Coq.Arrow (genericApply typeQualid [] [] (map Coq.Qualid tvarQualids)) + (Coq.Sort Coq.Prop)) + -- Generate induction cases for constructors. + indCases <- mapM (generateInductionCase propQualid) conDecls + -- Generate lemma. + (valIdent, valBinder) <- generateArg freshArgPrefix + (genericApply typeQualid [] [] (map Coq.Qualid tvarQualids)) + (indCaseQualids, fixpointQualid, varQualid) <- localEnv $ do + indCaseQualids <- mapM (const $ freshCoqQualid "InductionCase") indCases + fixpointQualid <- freshCoqQualid "FP" + varQualid <- freshCoqQualid "x" + return (indCaseQualids, fixpointQualid, varQualid) + let schemeName = schemeQualidMap Map.! typeName + binders + = genericArgDecls Coq.Explicit ++ tvarBinders ++ [propBinder] + goal = Coq.forall [valBinder] + (Coq.app (Coq.Qualid propQualid) [Coq.Qualid valIdent]) + term = Coq.forall binders (foldr Coq.Arrow goal indCases) + -- Generate proof. + vars = map (fromJust . Coq.unpackQualid) + (Coq.Base.shape + : Coq.Base.pos + : tvarQualids ++ [propQualid] ++ indCaseQualids) + fixpoint = fromJust $ Coq.unpackQualid fixpointQualid + var = fromJust $ Coq.unpackQualid varQualid + proof = Coq.ProofDefined + (Text.pack + $ " intros " + ++ unwords vars + ++ ";\n" + ++ " fix " + ++ fixpoint + ++ " 1; intro " + ++ var + ++ ";\n" + ++ " " + ++ Text.unpack Coq.Base.proveInd + ++ ".") + return (schemeName, [], term, proof) + where + -- | Generates an induction case for a given property and constructor. + generateInductionCase :: Coq.Qualid -> IR.ConDecl -> Converter Coq.Term + generateInductionCase propQualid + (IR.ConDecl _ (IR.DeclIdent srcSpan' conName) argTypes) = localEnv $ do + -- Collect and generate relevant Coq names. + conQualid <- lookupIdentOrFail srcSpan' IR.ValueScope conName + (argQualids, argBinders) <- mapAndUnzipM convertAnonymousArg + (map Just argTypes) + -- Expand type synonyms in the argument types and create induction hypotheses. + argTypes' <- mapM expandAllTypeSynonyms argTypes + Just conType <- inEnv $ lookupReturnType IR.ValueScope conName + conType' <- convertType' conType + hypotheses <- catMaybes + <$> zipWithM (generateInductionHypothesis propQualid conType') + argQualids argTypes' + -- Generate induction case. + let term = foldr Coq.Arrow + (Coq.app (Coq.Qualid propQualid) + [Coq.app (Coq.Qualid conQualid) (map Coq.Qualid argQualids)]) + hypotheses + indCase = Coq.forall argBinders term + return indCase + + -- | Generates an induction hypothesis for a given property and constructor argument. + generateInductionHypothesis + :: Coq.Qualid + -> Coq.Term + -> Coq.Qualid + -> IR.Type + -> Converter (Maybe Coq.Term) + generateInductionHypothesis propQualid conType argQualid argType = do + -- Generate induction hypotheses with a maximal depth of @maxDepth@. + mbHypothesis <- generateInductionHypothesis_1 maxDepth argType + -- Wrap generated hypothesis in a @ForFree@ property and apply it to the argument. + argType' <- convertType' argType + case mbHypothesis of + Just hypothesis -> return + $ Just + $ genericApply Coq.Base.forFree [] [] + [argType', hypothesis, Coq.Qualid argQualid] + Nothing -> return Nothing + where + -- | Generates an induction hypothesis by searching in the given type for recursive occurrences. + -- Has an argument limiting the search depth. + generateInductionHypothesis_1 + :: Int -> IR.Type -> Converter (Maybe Coq.Term) + generateInductionHypothesis_1 _ (IR.FuncType _ _ _) = + -- Ignore functions. + return Nothing + generateInductionHypothesis_1 md t@(IR.TypeApp _ tcon lastArg) = do + -- Check whether we found a recursive occurrence. + t' <- convertType' t + if conType == t' + then return $ Just $ Coq.Qualid propQualid + else + -- If we do not have an recursive occurrence and did not reach the + -- search limit yet, unfold type application. + if md > 0 + then generateInductionHypothesis_2 (md - 1) tcon [lastArg] + else return Nothing + generateInductionHypothesis_1 _ t@(IR.TypeCon _ _) = do + -- Check whether we found a recursive occurrence. + t' <- convertType' t + if conType == t' + then return $ Just $ Coq.Qualid propQualid + else + -- Ignore type constructors that do not have any type variable or are partially applied. + return Nothing + generateInductionHypothesis_1 _ (IR.TypeVar _ _) = + -- There is no induction hypothesis for type variables. + return Nothing + + -- Unfolds a type application. + generateInductionHypothesis_2 + :: Int -> IR.Type -> [IR.Type] -> Converter (Maybe Coq.Term) + generateInductionHypothesis_2 _ (IR.FuncType _ _ _) _ = + -- Ignore functions. + return Nothing + generateInductionHypothesis_2 md (IR.TypeApp _ tcon lastArg) typeArgs = + -- Continue unfolding. + generateInductionHypothesis_2 md tcon (lastArg : typeArgs) + generateInductionHypothesis_2 md (IR.TypeCon _ tconName) typeArgs = do + -- Recursively generate hypotheses for type arguments. + hypotheses <- mapM (generateInductionHypothesis_1 md) typeArgs + -- Only consider fully applied type constructors and only generate a + -- complex hypothesis, if any of the hypotheses for the arguments is + -- non trivial. + Just tconArity <- inEnv $ lookupArity IR.TypeScope tconName + if (tconArity == length typeArgs) && not (null $ catMaybes hypotheses) + then do + let hypotheses' = map (fromMaybe (Coq.Qualid Coq.Base.noProperty)) + hypotheses + coqArgs <- mapM convertType' typeArgs + mbForType <- getForType forQualidMap tconName + -- Wrap generated hypotheses in a 'For-' property. + return ((\forType -> genericApply forType [] [] + (coqArgs ++ hypotheses')) <$> mbForType) + else return Nothing + generateInductionHypothesis_2 _ (IR.TypeVar _ _) _ = + -- Ignore type variables that are used as type constructors. + return Nothing + + ----------------------------------------------------------------------------- + -- Forall Lemmas -- + ----------------------------------------------------------------------------- + -- | Generates a lemma which states the relation between the 'For-' property + -- and the 'In-' properties for a data declaration with type variables. + generateForallLemma + :: LookupMap Coq.Qualid + -> LookupMap Coq.Qualid + -> LookupMap Coq.Qualid + -> LookupMap [Coq.Qualid] + -> [Coq.Qualid] + -> IR.TypeDecl + -> Converter (Coq.Qualid, [Coq.Binder], Coq.Term, Coq.Proof) + generateForallLemma _ _ _ _ _ (IR.TypeSynDecl _ _ _ _) + = error "generateForallLemma: Type synonym not allowed" + generateForallLemma schemeQualidMap forallQualidMap forQualidMap inQualidMap + inConNames (IR.DataDecl _ (IR.DeclIdent _ typeName) typeVarDecls _) + = localEnv $ do + Just typeQualid <- inEnv $ lookupIdent IR.TypeScope typeName + (tvarQualids, tvarBinders) + <- convertTypeVarDecls' Coq.Explicit typeVarDecls + (propQualids, propBinders) <- mapAndUnzipM + (\tv -> generateArg "P" (Coq.Arrow (Coq.Qualid tv) (Coq.Sort Coq.Prop))) + tvarQualids + (valQualid, valBinder) <- generateArg freshArgPrefix + (genericApply typeQualid [] [] (map Coq.Qualid tvarQualids)) + inTerms <- zipWithM (generateInTerm valQualid tvarQualids) [0 ..] + propQualids + let forallQualid = forallQualidMap Map.! typeName + forQualid = forQualidMap Map.! typeName + binders = genericArgDecls Coq.Explicit + ++ tvarBinders + ++ propBinders + ++ [valBinder] + lhs = genericApply forQualid [] [] + (map Coq.Qualid $ tvarQualids ++ propQualids ++ [valQualid]) + rhs = let (inQualids', [lastIn]) + = splitAt (length inTerms - 1) $ inTerms + in foldr Coq.conj lastIn inQualids' + term = Coq.forall binders (Coq.equiv lhs rhs) + vars = map (fromJust . Coq.unpackQualid) + (Coq.Base.shape : Coq.Base.pos : tvarQualids ++ propQualids) + Just schemeName = Coq.unpackQualid $ schemeQualidMap Map.! typeName + proof = Coq.ProofDefined + (Text.pack + $ concatMap generateForallHint inConNames + ++ " intros " + ++ unwords vars + ++ ";\n" + ++ " " + ++ Text.unpack Coq.Base.proveForall + ++ ' ' : schemeName ++ ".") + return (forallQualid, [], term, proof) + where + -- | Generates a term stating that for all elements @y@ of type @a_index@ + -- that are contained in @valQualid@, the property @propQualid y@ holds. + generateInTerm + :: Coq.Qualid -> [Coq.Qualid] -> Int -> Coq.Qualid -> Converter Coq.Term + generateInTerm valQualid tvarQualids index propQualid = localEnv $ do + let inQualid = (inQualidMap Map.! typeName) !! index + (val2Qualid, val2Binder) <- generateArg "y" + (Coq.Qualid $ tvarQualids !! index) + let isIn = genericApply inQualid [] [] + (map Coq.Qualid $ tvarQualids ++ [val2Qualid, valQualid]) + return + $ Coq.forall [val2Binder] + $ Coq.Arrow isIn + (Coq.app (Coq.Qualid propQualid) [Coq.Qualid val2Qualid]) + + -- | Generate a local hint which is used in the proof of this 'forall' lemma. + generateForallHint :: Coq.Qualid -> String + generateForallHint inCon + = let Just inStr = Coq.unpackQualid inCon + in " Local Hint Extern 1 => " + ++ Text.unpack Coq.Base.proveForallFinish + ++ ' ' + : inStr ++ " : " ++ Text.unpack Coq.Base.proveForallDb ++ ".\n" + + ----------------------------------------------------------------------------- + -- Hints -- + ----------------------------------------------------------------------------- + -- | Generates hints that are used in the proofs of induction schemes and + -- 'forall' sentences. + generateHints :: LookupMap Coq.Qualid + -> LookupMap Coq.Qualid + -> LookupMap Coq.Qualid + -> LookupMap [Coq.Qualid] + -> IR.TypeDecl + -> Converter [Coq.Sentence] + generateHints _ _ _ _ (IR.TypeSynDecl _ _ _ _) + = error "generateHint: Type synonym not allowed" + generateHints schemeQualidMap forallQualidMap forQualidMap inQualidMap + (IR.DataDecl _ (IR.DeclIdent _ typeName) typeVarDecls tconDecls) = do + let forall = forallQualidMap Map.! typeName + forType = forQualidMap Map.! typeName + inTypes = inQualidMap Map.! typeName + scheme = schemeQualidMap Map.! typeName + proveIndHint <- generateProveIndHint typeName forType forall scheme + (length typeVarDecls) tconDecls + proveForallHint1 <- generateProveForallHint1 forType forall + (length typeVarDecls) + proveForallHints2 <- mapM + (generateProveForallHint2 forType forall (length typeVarDecls)) inTypes + return $ [proveIndHint, proveForallHint1] ++ proveForallHints2 + + -- | Generates a hint for induction scheme generation, using the template + -- @Coq.Base.proveIndProveForType@. + generateProveIndHint + :: IR.QName + -> Coq.Qualid + -> Coq.Qualid + -> Coq.Qualid + -> Int + -> [IR.ConDecl] + -> Converter Coq.Sentence + generateProveIndHint typeName forType forall scheme nTvars conDecls = do + valStr <- localEnv $ freshCoqIdent freshArgPrefix + dTypes <- concatMapM getDTypes conDecls + unfoldSubProps <- nub <$> concatMapM unfoldSubProp dTypes + let tacticConStr = Text.unpack Coq.Base.proveIndProveForType + Just forallStr = Coq.unpackQualid forall + Just schemeStr = Coq.unpackQualid scheme + underscores = replicate (2 + 2 * nTvars) Coq.UnderscorePat + valPattern = Coq.QualidPat $ Coq.bare $ '?' : valStr + forTypePattern = Coq.ArgsPat forType $ underscores ++ [valPattern] + tactic = unwords [tacticConStr, valStr, forallStr, schemeStr] + ++ (if null unfoldSubProps + then "" + else ";\nrepeat (\n" ++ tacticUnlines unfoldSubProps ++ ")") + return + $ Coq.externHint (Just Coq.Global) 0 (Just forTypePattern) tactic + [Coq.Base.proveIndDb] + where + -- | Tries to simplify a pair of 'For-' and 'In-' hypotheses. + unfoldSubProp :: IR.QName -> Converter [String] + unfoldSubProp dname = do + -- Filter complex data types. + mbInTs <- inEnv $ lookupInProperties dname + case mbInTs of + Nothing -> return [] + Just inTs -> mapM (unfoldSubProp' dname) inTs + + -- | Tries to simplify a pair of 'For-' and 'In-' hypotheses. + unfoldSubProp' :: IR.QName -> Coq.Qualid -> Converter String + unfoldSubProp' dName inT = localEnv $ do + hForStr <- freshCoqIdent "HF" + hInStr <- freshCoqIdent "HI" + valStr1 <- freshCoqIdent freshArgPrefix + valStr2 <- freshCoqIdent freshArgPrefix + Just forT <- inEnv $ lookupForProperty dName + Just forallT <- inEnv $ lookupForallLemma dName + Just dArity <- inEnv $ lookupArity IR.TypeScope dName + let forStr = unpackQualid' forT + inStr = unpackQualid' inT + forallStr = unpackQualid' forallT + forPatStrs = forStr + : replicate (2 + 2 * dArity) "_" ++ ['?' : valStr2] + inPatStrs = inStr + : replicate (2 + dArity) "_" ++ ['?' : valStr1, '?' : valStr2] + tactic = unlines' + [ " try match goal with" + , " | [ " ++ hForStr ++ " : " ++ unwords forPatStrs + , " , " ++ hInStr ++ " : " ++ unwords inPatStrs + , " |- _ ] =>" + , " " + ++ unwords [ Text.unpack Coq.Base.proveIndForTypeInType + , hForStr + , hInStr + , valStr1 + , forallStr + ] + , " end" + ] + return tactic + + -- | Like @unpackQualid@ but does also return a string for qualified names. + unpackQualid' :: Coq.Qualid -> String + unpackQualid' (Coq.Bare n) = Text.unpack n + unpackQualid' (Coq.Qualified p n) = Text.unpack p ++ "." ++ Text.unpack n + + -- | Like @unlines@, but does not put a line break after the last string. + unlines' :: [String] -> String + unlines' = intercalate "\n" + + -- | Like @unlines'@, but inserts also semicolons to connect Coq tactics. + tacticUnlines :: [String] -> String + tacticUnlines = intercalate ";\n" + + -- | Collects all types that occur in an argument of the given constructor. + getDTypes :: IR.ConDecl -> Converter [IR.QName] + getDTypes (IR.ConDecl _ _ argTypes) = do + argTypes' <- mapM expandAllTypeSynonyms argTypes + concatMapM getDTypes' argTypes' + + -- | Collects all types that occur in the given type. + getDTypes' :: IR.Type -> Converter [IR.QName] + getDTypes' (IR.TypeApp _ t1 t2) = do + ts1 <- getDTypes' t1 + ts2 <- getDTypes' t2 + return (ts1 ++ ts2) + getDTypes' (IR.TypeCon _ tconName) + | showPretty tconName == showPretty typeName = return [] + | otherwise = return [tconName] + getDTypes' (IR.TypeVar _ _) = return [] + getDTypes' (IR.FuncType _ _ _) = return [] + + -- | Generates a hint for forall lemma generation, using the template + -- @Coq.Base.proveForallProveForType@. + generateProveForallHint1 + :: Coq.Qualid -> Coq.Qualid -> Int -> Converter Coq.Sentence + generateProveForallHint1 forType forall nTvars = do + let tacticConStr = Text.unpack Coq.Base.proveForallProveForType + Just forallStr = Coq.unpackQualid forall + tactic = tacticConStr ++ ' ' : forallStr + underscores = replicate (3 + 2 * nTvars) Coq.UnderscorePat + forTypePattern = Coq.ArgsPat forType $ underscores + return + $ Coq.externHint (Just Coq.Global) 0 (Just forTypePattern) tactic + [Coq.Base.proveForallDb] + + -- | Generates a hint for forall lemma generation, using the template + -- @Coq.Base.proveForallForTypeInType@. + generateProveForallHint2 + :: Coq.Qualid -> Coq.Qualid -> Int -> Coq.Qualid -> Converter Coq.Sentence + generateProveForallHint2 forType forall nTvars inType = localEnv $ do + hForStr <- freshCoqIdent "HF" + hInStr <- freshCoqIdent "HI" + valStr1 <- freshCoqIdent freshArgPrefix + valStr2 <- freshCoqIdent freshArgPrefix + let tacticConStr = Text.unpack Coq.Base.proveForallForTypeInType + Just forStr = Coq.unpackQualid forType + Just inStr = Coq.unpackQualid inType + Just forallStr = Coq.unpackQualid forall + forPatStrs = forStr + : replicate (2 + 2 * nTvars) "_" ++ ['?' : valStr2] + inPatStrs = inStr + : replicate (2 + nTvars) "_" ++ ['?' : valStr1, '?' : valStr2] + tactic = unlines + [ "" + , " match goal with" + , " | [ " ++ hForStr ++ " : " ++ unwords forPatStrs + , " , " ++ hInStr ++ " : " ++ unwords inPatStrs + , " |- _ ] =>" + , " " + ++ unwords [tacticConStr, hForStr, hInStr, valStr1, forallStr] + , " end" + ] + return + $ Coq.externHint (Just Coq.Global) 0 Nothing tactic + [Coq.Base.proveForallDb] + + ----------------------------------------------------------------------------- + -- Helper Functions -- + ----------------------------------------------------------------------------- + -- | The maximal depth to search for recursive occurrences when construction + -- induction hypotheses. + -- @0@ -> Create only induction hypotheses for direct recursion. + -- @n@ -> Create only induction hypotheses for constructor arguments where + -- the recursive occurrence is encapsulated in at most @n@ data + -- types. + maxDepth :: Int + maxDepth = 1 + + -- | Checks whether the type eclaration includes at least one type variable. + hasTypeVar :: IR.TypeDecl -> Bool + hasTypeVar (IR.TypeSynDecl _ _ _ _) + = error "hasTypeVar: Type synonym not allowed" + hasTypeVar (IR.DataDecl _ _ typeVarDecls _) = not $ null typeVarDecls + + -- | Generate a name from a name by adding a prefix and a suffix. + generateName + :: String -> String -> IR.QName -> Converter (IR.QName, Coq.Qualid) + generateName prefix suffix typeQName = do + Just typeQualid <- inEnv $ lookupIdent IR.TypeScope typeQName + let Just typeIdent = Coq.unpackQualid typeQualid + newQualid <- freshCoqQualid $ prefix ++ typeIdent ++ suffix + return (typeQName, newQualid) + + -- | Generate a name from a name by adding the constructor name to it. + generateConName :: Coq.Qualid -> IR.QName -> Converter Coq.Qualid + generateConName baseQualid conQName = do + Just conQualid <- inEnv $ lookupIdent IR.ValueScope conQName + let Just baseName = Coq.unpackQualid baseQualid + Just conName = Coq.unpackQualid conQualid + freshCoqQualid $ baseName ++ "_" ++ conName + + -- | Returns the name corresponding 'For-' property by using the given Map + -- first and the environment on failure. + getForType + :: LookupMap Coq.Qualid -> IR.QName -> Converter (Maybe Coq.Qualid) + getForType forQualidMap name = case forQualidMap Map.!? name of + Just qualid -> return $ Just qualid + Nothing -> inEnv $ lookupForProperty name + + -- | Insert the property names and the forall lemma for a type in the + -- environment. + insertPropertiesInEnv :: LookupMap Coq.Qualid + -> LookupMap [Coq.Qualid] + -> LookupMap Coq.Qualid + -> IR.QName + -> Converter () + insertPropertiesInEnv forQualidMap inQualidMap forallQualidMap name = do + let forName = forQualidMap Map.!? name + inNames = inQualidMap Map.!? name + forallName = forallQualidMap Map.!? name + modifyEnv $ addPropertyNamesToEntry name forName inNames forallName + + -- | Generates an argument with the given name and type. + generateArg :: String -> Coq.Term -> Converter (Coq.Qualid, Coq.Binder) + generateArg argName argType = do + qualid <- freshCoqQualid argName + let binder + = Coq.typedBinder Coq.Ungeneralizable Coq.Explicit [qualid] argType + return (qualid, binder) diff --git a/src/lib/FreeC/Backend/Coq/Syntax.hs b/src/lib/FreeC/Backend/Coq/Syntax.hs index 4c93b545..dc774d91 100644 --- a/src/lib/FreeC/Backend/Coq/Syntax.hs +++ b/src/lib/FreeC/Backend/Coq/Syntax.hs @@ -26,7 +26,7 @@ module FreeC.Backend.Coq.Syntax , variable -- * Definition Sentences , definitionSentence - -- * Notation sentences + -- * Notation Sentences , notationSentence , nSymbol , nIdent @@ -42,6 +42,13 @@ module FreeC.Backend.Coq.Syntax , notEquals , conj , disj + , equiv + , forall + -- * Options + , setOption + , unsetOption + -- * Hints + , externHint -- * Imports , requireImportFrom , requireExportFrom @@ -186,7 +193,7 @@ definitionSentence qualid binders returnType term = DefinitionSentence (DefinitionDef Global qualid binders returnType term) ------------------------------------------------------------------------------- --- Definition sentences -- +-- Notation sentences -- ------------------------------------------------------------------------------- -- | Smart constructor for a Coq notation sentence. notationSentence @@ -257,6 +264,41 @@ conj t1 t2 = app (Qualid (bare "op_/\\__")) [t1, t2] disj :: Term -> Term -> Term disj t1 t2 = app (Qualid (bare "op_\\/__")) [t1, t2] +-- | Smart constructor for a equivalence in Coq. +equiv :: Term -> Term -> Term +equiv t1 t2 = app (Qualid (bare "op_<->__")) [t1, t2] + +-- | Smart constructor for a forall term in Coq. +forall :: [Binder] -> Term -> Term +forall [] t = t +forall bs t = Forall (NonEmpty.fromList bs) t + +------------------------------------------------------------------------------- +-- Options -- +------------------------------------------------------------------------------- +-- | Smart constructor for a sentence which sets an option or flag. +setOption :: Maybe Locality -> String -> Maybe (Either Num String) -> Sentence +setOption mbLoc opt mbArg = OptionSentence + $ SetOption mbLoc (Text.pack opt) mbArg' + where + mbArg' = case mbArg of + Nothing -> Nothing + (Just (Left num)) -> Just (OVNum num) + (Just (Right str)) -> Just (OVText (Text.pack str)) + +-- | Smart constructor for a sentence which unsets an option or flag. +unsetOption :: Maybe Locality -> String -> Sentence +unsetOption mbLoc opt = OptionSentence $ UnsetOption mbLoc (Text.pack opt) + +------------------------------------------------------------------------------- +-- Hints -- +------------------------------------------------------------------------------- +-- | Smart constructor for an extern hint. +externHint + :: Maybe Locality -> Num -> Maybe Pattern -> String -> [Ident] -> Sentence +externHint mbLoc num mbPat tactic dbs = HintSentence + $ Hint mbLoc (HintExtern num mbPat $ Text.pack tactic) dbs + ------------------------------------------------------------------------------- -- Imports -- ------------------------------------------------------------------------------- diff --git a/src/lib/FreeC/Environment.hs b/src/lib/FreeC/Environment.hs index ea3c242c..ff13b9f8 100644 --- a/src/lib/FreeC/Environment.hs +++ b/src/lib/FreeC/Environment.hs @@ -16,6 +16,7 @@ module FreeC.Environment -- * Modifying Entries in the Environment , modifyEntryIdent , addEffectsToEntry + , addPropertyNamesToEntry -- * Looking up Entries from the Environment , lookupEntry , isFunction @@ -34,6 +35,9 @@ module FreeC.Environment , lookupReturnType , lookupTypeScheme , lookupArity + , lookupForProperty + , lookupInProperties + , lookupForallLemma , lookupTypeSynonym , needsFreeArgs , hasEffect @@ -155,6 +159,27 @@ addEffectsToEntry name effects env = case lookupEntry IR.ValueScope name env of then addEntry (entry { entryEffects = entryEffects entry ++ effects }) env else env +-- | Adds the given Coq identifiers for the 'For-' property and 'In-' +-- properties for the data entry with the given name. +-- +-- If such a data entry does not exist, the environment is not changed. +addPropertyNamesToEntry + :: IR.QName + -> Maybe Coq.Qualid + -> Maybe [Coq.Qualid] + -> Maybe Coq.Qualid + -> Environment + -> Environment +addPropertyNamesToEntry name forIdent inIdents forallIdent env + = case lookupEntry IR.TypeScope name env of + Nothing -> env + Just entry -> if isDataEntry entry + then addEntry (entry { entryForPropertyIdent = forIdent + , entryInPropertyIdents = inIdents + , entryForallIdent = forallIdent + }) env + else env + ------------------------------------------------------------------------------- -- Looking up Entries from the Environment -- ------------------------------------------------------------------------------- @@ -295,6 +320,46 @@ lookupArity :: IR.Scope -> IR.QName -> Environment -> Maybe Int lookupArity = fmap entryArity . find (not . (isVarEntry .||. isTypeVarEntry)) .:. lookupEntry +-- | Looks up the Coq identifier for the 'For-' property of the data entry with +-- the given name. +-- +-- Returns @Nothing@ if there is no such data entry or if the data entry has +-- no 'For-' property. +lookupForProperty :: IR.QName -> Environment -> Maybe Coq.Qualid +lookupForProperty = concatMaybe . fmap entryForPropertyIdent . find isDataEntry + .: lookupEntry IR.TypeScope + where + concatMaybe :: Maybe (Maybe a) -> Maybe a + concatMaybe (Just mb) = mb + concatMaybe Nothing = Nothing + +-- | Looks up the Coq identifiers for the 'In-' properties of the data entry +-- with the given name. +-- +-- Returns @Nothing@ if there is no such data entry or if the data entry has +-- no 'In-' properties. +lookupInProperties :: IR.QName -> Environment -> Maybe [Coq.Qualid] +lookupInProperties + = concatMaybe . fmap entryInPropertyIdents . find isDataEntry + .: lookupEntry IR.TypeScope + where + concatMaybe :: Maybe (Maybe a) -> Maybe a + concatMaybe (Just mb) = mb + concatMaybe Nothing = Nothing + +-- | Looks up the Coq identifier for the 'forall' lemma of the data entry with +-- the given name. +-- +-- Returns @Nothing@ if there is no such data entry or if the data entry has +-- no 'forall' lemma. +lookupForallLemma :: IR.QName -> Environment -> Maybe Coq.Qualid +lookupForallLemma = concatMaybe . fmap entryForallIdent . find isDataEntry + .: lookupEntry IR.TypeScope + where + concatMaybe :: Maybe (Maybe a) -> Maybe a + concatMaybe (Just mb) = mb + concatMaybe Nothing = Nothing + -- | Looks up the type the type synonym with the given name is associated with. -- -- Returns @Nothing@ if there is no such type synonym. diff --git a/src/lib/FreeC/Environment/Entry.hs b/src/lib/FreeC/Environment/Entry.hs index 00038307..c6c9c2d3 100644 --- a/src/lib/FreeC/Environment/Entry.hs +++ b/src/lib/FreeC/Environment/Entry.hs @@ -17,18 +17,24 @@ import FreeC.Util.Predicate data EnvEntry = -- | Entry for a data type declaration. DataEntry - { entrySrcSpan :: SrcSpan + { entrySrcSpan :: SrcSpan -- ^ The source code location where the data type was declared. - , entryArity :: Int + , entryArity :: Int -- ^ The number of type arguments expected by the type constructor. - , entryIdent :: Coq.Qualid + , entryIdent :: Coq.Qualid -- ^ The name of the data type in Coq. - , entryAgdaIdent :: Agda.QName + , entryAgdaIdent :: Agda.QName -- ^ The name of the data type in Agda. - , entryName :: IR.QName + , entryName :: IR.QName -- ^ The name of the data type in the module it has been defined in. - , entryConsNames :: [IR.ConName] + , entryConsNames :: [IR.ConName] -- ^ The names of the constructors of the data type. + , entryForPropertyIdent :: Maybe Coq.Qualid + -- ^ The name of the 'For-' property in Coq. + , entryInPropertyIdents :: Maybe [Coq.Qualid] + -- ^ The names of the 'In-' properties in Coq. + , entryForallIdent :: Maybe Coq.Qualid + -- ^ The names of the 'forall' lemma in Coq. } -- | Entry for a type synonym declaration. | TypeSynEntry diff --git a/src/lib/FreeC/Environment/ModuleInterface/Decoder.hs b/src/lib/FreeC/Environment/ModuleInterface/Decoder.hs index f824fda7..1441b0c9 100644 --- a/src/lib/FreeC/Environment/ModuleInterface/Decoder.hs +++ b/src/lib/FreeC/Environment/ModuleInterface/Decoder.hs @@ -215,13 +215,20 @@ instance Aeson.FromJSON ModuleInterface where coqName <- obj .: "coq-name" agdaName <- obj .: "agda-name" consNames <- obj .: "cons-names" - return DataEntry { entrySrcSpan = NoSrcSpan - , entryArity = arity - , entryIdent = coqName - , entryAgdaIdent = agdaName - , entryName = haskellName - , entryConsNames = consNames - } + coqForPropertyName <- obj .:? "coq-for-property-name" + coqInPropertyNames <- obj .:? "coq-in-property-names" + coqForallName <- obj .:? "coq-forall-lemma-name" + return DataEntry + { entrySrcSpan = NoSrcSpan + , entryArity = arity + , entryIdent = coqName + , entryAgdaIdent = agdaName + , entryName = haskellName + , entryConsNames = consNames + , entryForPropertyIdent = coqForPropertyName + , entryInPropertyIdents = coqInPropertyNames + , entryForallIdent = coqForallName + } parseConfigTypeSyn :: Aeson.Value -> Aeson.Parser EnvEntry parseConfigTypeSyn = Aeson.withObject "Type synonym" $ \obj -> do diff --git a/src/lib/FreeC/Environment/ModuleInterface/Encoder.hs b/src/lib/FreeC/Environment/ModuleInterface/Encoder.hs index f61ee409..a46be8d3 100644 --- a/src/lib/FreeC/Environment/ModuleInterface/Encoder.hs +++ b/src/lib/FreeC/Environment/ModuleInterface/Encoder.hs @@ -17,7 +17,7 @@ module FreeC.Environment.ModuleInterface.Encoder ( writeModuleInterface ) where import Control.Monad.IO.Class ( MonadIO ) import Data.Aeson ( (.=) ) import qualified Data.Aeson as Aeson -import Data.Maybe ( mapMaybe ) +import Data.Maybe ( catMaybes, mapMaybe ) import qualified Data.Set as Set import FreeC.Backend.Agda.Pretty @@ -90,12 +90,17 @@ instance Aeson.ToJSON ModuleInterface where encodeEntry :: EnvEntry -> Maybe Aeson.Value encodeEntry entry | isDataEntry entry = return - $ Aeson.object [ "haskell-name" .= haskellName - , "coq-name" .= coqName - , "agda-name" .= agdaName - , "cons-names" .= consNames - , "arity" .= arity - ] + $ Aeson.object + $ [ "haskell-name" .= haskellName + , "coq-name" .= coqName + , "agda-name" .= agdaName + , "cons-names" .= consNames + , "arity" .= arity + ] + ++ catMaybes [ ("coq-for-property-name" .=) <$> coqForPropertyName + , ("coq-in-property-names" .=) <$> coqInPropertyNames + , ("coq-forall-lemma-name" .=) <$> coqForallName + ] | isTypeSynEntry entry = return $ Aeson.object [ "haskell-name" .= haskellName @@ -135,6 +140,13 @@ encodeEntry entry coqSmartName = Aeson.toJSON (entrySmartIdent entry) + coqForPropertyName, coqInPropertyNames, coqForallName :: Maybe Aeson.Value + coqForPropertyName = Aeson.toJSON <$> entryForPropertyIdent entry + + coqInPropertyNames = Aeson.toJSON <$> entryInPropertyIdents entry + + coqForallName = Aeson.toJSON <$> entryForallIdent entry + -- @entryAgdaIdent entry@ is undefined because the agda renamer isn't -- implemented at the moment. To allow encoding a dummy value is needed. -- I decided to insert the placeholder at this point to avoid placing diff --git a/src/lib/FreeC/Pass/DefineDeclPass.hs b/src/lib/FreeC/Pass/DefineDeclPass.hs index 65bc455f..f9f67987 100644 --- a/src/lib/FreeC/Pass/DefineDeclPass.hs +++ b/src/lib/FreeC/Pass/DefineDeclPass.hs @@ -71,12 +71,15 @@ defineTypeDecl (IR.TypeSynDecl srcSpan declIdent typeArgs typeExpr) = do return () defineTypeDecl (IR.DataDecl srcSpan declIdent typeArgs conDecls) = do _ <- renameAndAddEntry DataEntry - { entrySrcSpan = srcSpan - , entryArity = length typeArgs - , entryName = IR.declIdentName declIdent - , entryConsNames = map IR.conDeclQName conDecls - , entryIdent = undefined -- filled by renamer - , entryAgdaIdent = undefined -- filled by renamer + { entrySrcSpan = srcSpan + , entryArity = length typeArgs + , entryName = IR.declIdentName declIdent + , entryConsNames = map IR.conDeclQName conDecls + , entryIdent = undefined -- filled by renamer + , entryAgdaIdent = undefined -- filled by renamer + , entryForPropertyIdent = Nothing -- may be filled by induction scheme generator + , entryInPropertyIdents = Nothing -- may be filled by induction scheme generator + , entryForallIdent = Nothing -- may be filled by induction scheme generator } mapM_ defineConDecl conDecls where