From: Adam Megacz Date: Sun, 5 Jun 2011 21:03:47 +0000 (-0700) Subject: merge X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=18e57e2389c9d2a10f49715fe6234debac04215f;hp=de8bb8acbfd411d7494c1b35f55cd7edba003b7f;p=coq-hetmet.git merge --- diff --git a/examples/Demo.hs b/examples/Demo.hs index 6d0e69d..74fe4de 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -5,11 +5,17 @@ module Demo (demo) where --demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]> demo const mult = - <[ let twelve = ~~(const (12::Int)) - four = ~~(const ( 4::Int)) - in ~~mult four (~~mult four twelve) + <[ let four = ~~mult four ~~(const 4) +-- twelve = {- {- ~~mult four -} ~~(const 12) -} four + in four ]> +demo :: + forall a c . + (Int -> <[a]>@c) -> + <[a -> a -> a]>@c -> + <[a]>@c + {- demo const mult = <[ let twelve = ~~(const (12::Int)) diff --git a/examples/DemoMain.hs b/examples/DemoMain.hs index cc438ba..e3e56b7 100644 --- a/examples/DemoMain.hs +++ b/examples/DemoMain.hs @@ -1,5 +1,15 @@ import Control.Category import GArrowTikZ +import GHC.HetMet.Private +import GHC.HetMet.GArrow import Demo +{- +demo' :: + (Int -> PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) ) -> + ( PGArrow g (GArrowTensor g (GArrowTensor g Int Int) (GArrowUnit g)) Int) -> + (PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) ) +demo' = demo +-} + main = tikz $ \const merge -> demo const merge diff --git a/examples/GArrowPortShape.hs b/examples/GArrowPortShape.hs index 34f14c8..e746b5f 100644 --- a/examples/GArrowPortShape.hs +++ b/examples/GArrowPortShape.hs @@ -186,8 +186,24 @@ detect (GAS_const i) = do { x <- freshM; return $ GASPortShapeWrapper PortUnit detect GAS_merge = do { x <- freshM ; y <- freshM ; return $ GASPortShapeWrapper (PortTensor (PortFree x) (PortFree y)) (PortFree x) GAS_merge } -detect (GAS_loopl f) = error "not implemented" -detect (GAS_loopr f) = error "not implemented" +detect (GAS_loopl f) = do { x <- freshM + ; y <- freshM + ; z <- freshM + ; z' <- freshM -- remove once I fix the occurs check + ; f' <- detect f + ; unifyM (fst $ shapes f') (PortTensor (PortFree z) (PortFree x)) + ; unifyM (snd $ shapes f') (PortTensor (PortFree z') (PortFree y)) + ; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopl (GAS_misc f')) + } +detect (GAS_loopr f) = do { x <- freshM + ; y <- freshM + ; z <- freshM + ; z' <- freshM -- remove once I fix the occurs check + ; f' <- detect f + ; unifyM (fst $ shapes f') (PortTensor (PortFree x) (PortFree z)) + ; unifyM (snd $ shapes f') (PortTensor (PortFree y) (PortFree z')) + ; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopr (GAS_misc f')) + } -detect (GAS_misc f) = error "not implemented" +detect (GAS_misc f) = error "GAS_misc: not implemented" diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index 2c53283..14827ec 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -81,7 +81,7 @@ type instance GArrowTensor (GArrowSkeleton m) = (,) type instance GArrowUnit (GArrowSkeleton m) = () type instance GArrowExponent (GArrowSkeleton m) = (->) -instance GArrowSTKC (GArrowSkeleton m) +instance GArrowSTKCL (GArrowSkeleton m) -- -- | Simple structural equality on skeletons. NOTE: two skeletons diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index 9961830..46929ff 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -81,8 +81,8 @@ data Diagram | DiagramBox TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier | DiagramBypassTop Tracks Diagram | DiagramBypassBot Diagram Tracks - -- | DiagramLoopTop Tracks Diagram - -- | DiagramLoopBot Diagram Tracks + | DiagramLoopTop Tracks Diagram + | DiagramLoopBot Diagram Tracks -- | get the output tracks of a diagram getOut :: Diagram -> Tracks @@ -90,6 +90,8 @@ getOut (DiagramComp f g) = getOut g getOut (DiagramBox ptop pin q pout pbot) = pout getOut (DiagramBypassTop p f) = TT p (getOut f) getOut (DiagramBypassBot f p) = TT (getOut f) p +getOut (DiagramLoopTop t d) = case getOut d of { TT z y -> y ; _ -> error "mismatch" } +getOut (DiagramLoopBot d t) = case getOut d of { TT y z -> y ; _ -> error "mismatch" } -- | get the input tracks of a diagram getIn :: Diagram -> Tracks @@ -97,6 +99,8 @@ getIn (DiagramComp f g) = getIn f getIn (DiagramBox ptop pin q pout pbot) = pin getIn (DiagramBypassTop p f) = TT p (getIn f) getIn (DiagramBypassBot f p) = TT (getIn f) p +getIn (DiagramLoopTop t d) = case getIn d of { TT z x -> x ; _ -> error "mismatch" } +getIn (DiagramLoopBot d t) = case getIn d of { TT x z -> x ; _ -> error "mismatch" } -- | A BoxRenderer is just a routine that, given the dimensions of a -- boxes-and-wires box element, knows how to spit out a bunch of TikZ @@ -264,8 +268,10 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x drawWires tp x1 z x2 z "black" ; return $ DiagramBox top (TT x (TT y z)) r (TT (TT x y) z) bot } - mkdiag' (GAS_loopl f) = error "not implemented" - mkdiag' (GAS_loopr f) = error "not implemented" + mkdiag' (GAS_loopr f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x) + ; return $ DiagramLoopBot f' x } + mkdiag' (GAS_loopl f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f' + ; return $ DiagramLoopTop x f' } mkdiag' (GAS_misc f ) = mkdiag f diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram @@ -290,6 +296,8 @@ constrainTop v i (DiagramComp d1 d2) = do { constrainTop v i d1 constrainTop v i (DiagramBypassTop p d) = constrain v LT (uppermost p) (-1 * i) constrainTop v i (DiagramBypassBot d p) = constrainTop v (i+1) d constrainTop v i (DiagramBox ptop pin r pout pbot) = constrain v LT ptop (-1 * i) +constrainTop v i (DiagramLoopTop p d) = constrain v LT (uppermost p) (-1 * i) +constrainTop v i (DiagramLoopBot d p) = constrainTop v (i+1) d -- constrain that Ports is at least Int units below the bottommost portion of Diagram constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM () @@ -297,6 +305,8 @@ constrainBot (DiagramComp d1 d2) i v = do { constrainBot d1 i v constrainBot (DiagramBypassTop p d) i v = constrainBot d (i+1) v constrainBot (DiagramBypassBot d p) i v = constrain v GT (lowermost p) 2 constrainBot (DiagramBox ptop pin r pout pbot) i v = constrain v GT pbot i +constrainBot (DiagramLoopTop p d) i v = constrainBot d (i+1) v +constrainBot (DiagramLoopBot d p) i v = constrain v GT (lowermost p) 2 -- | The width of a box is easy to calculate width :: Diagram -> Float @@ -304,6 +314,8 @@ width (DiagramComp d1 d2) = (width d1) + 1 + (width d2) width (DiagramBox ptop pin x pout pbot) = 2 width (DiagramBypassTop p d) = (width d) + 2 width (DiagramBypassBot d p) = (width d) + 2 +width (DiagramLoopTop p d) = (width d) + 2 +width (DiagramLoopBot d p) = (width d) + 2 drawWires :: TrackPositions -> Float -> Tracks -> Float -> Tracks -> String -> String drawWires tp x1 (TT a b) x2 (TT a' b') color = drawWires tp x1 a x2 a' color ++ drawWires tp x1 b x2 b' color @@ -335,6 +347,20 @@ tikZ m = tikZ' ++ tikZ' d (x+1) ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black" ++ drawWires m x p (x+1+width d+1) p "black" + tikZ' d'@(DiagramLoopTop p d) x = let top = getTop d' in + let bot = getBot d' in + drawBox x top (x+width d') bot "gray!50" "loopl" + ++ drawWires m x (getIn d) (x+1) (getIn d) "black" + ++ tikZ' d (x+1) + ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black" + ++ drawWires m x p (x+1+width d+1) p "black" + tikZ' d'@(DiagramLoopBot d p) x = let top = getTop d' in + let bot = getBot d' in + drawBox x top (x+width d') bot "gray!50" "loopr" + ++ drawWires m x (getIn d) (x+1) (getIn d) "black" + ++ tikZ' d (x+1) + ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black" + ++ drawWires m x p (x+1+width d+1) p "black" tikZ' d@(DiagramBox ptop pin r pout pbot) x = r m x (m ! ptop) (x + width d) (m ! pbot) wires x1 t x2 c = wires' x1 t x2 c "-" @@ -349,12 +375,16 @@ tikZ m = tikZ' getTop (DiagramBox ptop _ _ _ _) = m ! ptop getTop (DiagramBypassTop p d) = (m ! uppermost p) - 1 getTop (DiagramBypassBot d p) = getTop d - 1 + getTop (DiagramLoopTop p d) = (m ! uppermost p) - 1 + getTop (DiagramLoopBot d p) = getTop d - 1 getBot :: Diagram -> Float getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2) getBot (DiagramBox _ _ _ _ pbot) = m ! pbot getBot (DiagramBypassTop p d) = getBot d + 1 getBot (DiagramBypassBot d p) = (m ! lowermost p) + 1 + getBot (DiagramLoopTop p d) = getBot d + 1 + getBot (DiagramLoopBot d p) = (m ! lowermost p) + 1 -- allocates multiple tracks, adding constraints that they are at least one unit apart alloc :: PortShape a -> ConstraintM (TrackIdentifier,Tracks,TrackIdentifier) diff --git a/examples/Makefile b/examples/Makefile index 7926143..f880d81 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -1,4 +1,4 @@ -ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build +ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build open: make demo diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index d70cd58..e0226d8 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -307,6 +307,8 @@ Section core2proof. (hetmet_pga_applyr : CoreVar) (hetmet_pga_curryl : CoreVar) (hetmet_pga_curryr : CoreVar) + (hetmet_pga_loopl : CoreVar) + (hetmet_pga_loopr : CoreVar) . @@ -411,6 +413,8 @@ Section core2proof. (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*) (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*) (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*) + ; ga_loopl := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + ; ga_loopr := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit" ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry" ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply" @@ -529,7 +533,10 @@ Section core2proof. (hetmet_pga_applyl : CoreVar) (hetmet_pga_applyr : CoreVar) (hetmet_pga_curryl : CoreVar) - (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) := + (hetmet_pga_curryr : CoreVar) + (hetmet_pga_loopl : CoreVar) + (hetmet_pga_loopr : CoreVar) + : list (@CoreBind CoreVar) := coqPassCoreToCore' do_flatten do_skolemize @@ -556,6 +563,8 @@ Section core2proof. hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap + hetmet_pga_loopl + hetmet_pga_loopr lbinds (* hetmet_pga_applyl diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 1731aad..c19f81a 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -272,6 +272,8 @@ Section HaskFlattener. ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ] ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ] ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ] + ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ] + ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ] ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ] @@ -991,7 +993,11 @@ Section HaskFlattener. unfold x1. rewrite drop_to_nothing. apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)). - admit. (* OK *) + induction Σ₁₂; try destruct a; auto. + simpl. + rewrite <- IHΣ₁₂1 at 2. + rewrite <- IHΣ₁₂2 at 2. + reflexivity. eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ]. set (mapOptionTree flatten_type Σ₁₂) as a. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b. @@ -1031,7 +1037,11 @@ Section HaskFlattener. eapply RArrange. eapply ARight. apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). - admit (* FIXME *). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. idtac. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ]. apply boost. @@ -1066,7 +1076,11 @@ Section HaskFlattener. eapply RArrange. eapply ALeft. apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). - admit (* FIXME *). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. idtac. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply boost. @@ -1082,10 +1096,13 @@ Section HaskFlattener. destruct case_RVoid. simpl. - apply nd_rule. destruct l. + apply nd_rule. apply RVoid. - apply (Prelude_error "RVoid at level >0"). + drop_simplify. + take_simplify. + simpl. + apply ga_id. destruct case_RAppT. simpl. destruct lev; simpl. @@ -1156,7 +1173,31 @@ Section HaskFlattener. rewrite IHy1. rewrite IHy2. reflexivity. - apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)"). + repeat drop_simplify. + repeat take_simplify. + simpl. + rewrite drop_to_nothing. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + eapply AComp. + eapply ARight. + apply arrangeCancelEmptyTree with (q:=y). + induction y; try destruct a; auto. + simpl. + rewrite <- IHy1. + rewrite <- IHy2. + reflexivity. + apply ACanL. + rewrite take_lemma'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'. + set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''. + replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y). + apply boost. + apply ga_loopl. + rewrite <- mapOptionTree_compose. + simpl. + reflexivity. destruct case_RCase. simpl. diff --git a/src/HaskProof.v b/src/HaskProof.v index 5e6fac4..f98800d 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -85,7 +85,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ ]@l] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ ]@l] -| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev] +| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), Rule diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 0d90d4c..3dbc81f 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -964,7 +964,7 @@ Section HaskProofToStrong. refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. refine (X_ ((update_xi ξ t (leaves varstypes))) - (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. + ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. rewrite pf1. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 435b687..8764102 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -492,7 +492,30 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply (@RLetRec Γ Δ lri x y nil). - apply (Prelude_error "RLetRec at depth>0"). + destruct (decide_tree_empty (mapOptionTreeAndFlatten take_arg_types_as_tree y @@@ (h :: t))); + [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ]. + destruct (eqd_dec y (mapOptionTree drop_arg_types_as_tree y)); + [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ]. + rewrite <- e. + clear e. + eapply nd_comp. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply ALeft. + eapply AComp. + eapply ARight. + destruct s. + apply (arrangeCancelEmptyTree _ _ e). + apply ACanL. + eapply nd_comp. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AuAssoc. + eapply nd_rule. + eapply SFlat. + eapply RLetRec. destruct case_RCase. simpl. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 1f1229d..114f2d9 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -997,7 +997,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. + set (@factorContextLeftAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. set (q' disti) as q''.