--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))
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
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"
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
| 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
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
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
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
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 ()
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
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
++ 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 "-"
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)
-ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build
+ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build
open:
make demo
(hetmet_pga_applyr : CoreVar)
(hetmet_pga_curryl : CoreVar)
(hetmet_pga_curryr : CoreVar)
+ (hetmet_pga_loopl : CoreVar)
+ (hetmet_pga_loopr : CoreVar)
.
(* ; 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"
(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
hetmet_pga_copy
hetmet_pga_drop
hetmet_pga_swap
+ hetmet_pga_loopl
+ hetmet_pga_loopr
lbinds
(*
hetmet_pga_applyl
; 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 ]
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.
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.
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.
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.
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.
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
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.
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.
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''.