mirror of
https://github.com/anoma/juvix.git
synced 2025-01-08 08:39:26 +03:00
parent
227a51a56d
commit
e8fa77a58d
@ -201,7 +201,19 @@ instance (SingI s) => PrettyPrint (PatternAtoms s) where
|
|||||||
ppCode (PatternAtoms ps _) = hsep (ppCode <$> ps)
|
ppCode (PatternAtoms ps _) = hsep (ppCode <$> ps)
|
||||||
|
|
||||||
instance (SingI s) => PrettyPrint (ExpressionAtoms s) where
|
instance (SingI s) => PrettyPrint (ExpressionAtoms s) where
|
||||||
ppCode as = hsep (ppCode <$> as ^. expressionAtoms)
|
ppCode ::
|
||||||
|
forall r.
|
||||||
|
(Members '[ExactPrint, Reader Options] r) =>
|
||||||
|
ExpressionAtoms s ->
|
||||||
|
Sem r ()
|
||||||
|
ppCode as = go (toList $ as ^. expressionAtoms)
|
||||||
|
where
|
||||||
|
go :: [ExpressionAtom s] -> Sem r ()
|
||||||
|
go = \case
|
||||||
|
[] -> return ()
|
||||||
|
[x] -> ppCode x
|
||||||
|
(x : xs@(AtomRecordUpdate {} : _)) -> ppCode x >> go xs
|
||||||
|
(x : xs) -> ppCode x >> space >> go xs
|
||||||
|
|
||||||
instance (SingI s) => PrettyPrint (Initializer s) where
|
instance (SingI s) => PrettyPrint (Initializer s) where
|
||||||
ppCode Initializer {..} = do
|
ppCode Initializer {..} = do
|
||||||
|
@ -72,11 +72,16 @@ ppUChain (UChain opFix f links) = do
|
|||||||
pp <- asks (^. apePP)
|
pp <- asks (^. apePP)
|
||||||
let f' = ppLinkExpr fx f
|
let f' = ppLinkExpr fx f
|
||||||
args = hsep (fmap pp links)
|
args = hsep (fmap pp links)
|
||||||
f' <+> args
|
f' <> sp <> args
|
||||||
where
|
where
|
||||||
fx :: Precedence
|
fx :: Precedence
|
||||||
fx = opFix ^. fixityPrecedence
|
fx = opFix ^. fixityPrecedence
|
||||||
|
|
||||||
|
sp :: Sem r ()
|
||||||
|
sp = case fx of
|
||||||
|
PrecUpdate -> return ()
|
||||||
|
_ -> space
|
||||||
|
|
||||||
ppLinkExpr ::
|
ppLinkExpr ::
|
||||||
(Members '[Reader (ApeParams a), ExactPrint] r) => Precedence -> Cape a -> Sem r ()
|
(Members '[Reader (ApeParams a), ExactPrint] r) => Precedence -> Cape a -> Sem r ()
|
||||||
ppLinkExpr opFix e = parensIf cond (ppCape e)
|
ppLinkExpr opFix e = parensIf cond (ppCape e)
|
||||||
|
@ -17,20 +17,19 @@ type Pair (A B : Type) :=
|
|||||||
};
|
};
|
||||||
|
|
||||||
mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
|
mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
|
||||||
| mkPair@{fst := mkPair@{fst; snd := nil}; snd := zero :: _} := fst
|
| mkPair@{fst := mkPair@{fst; snd := nil};
|
||||||
|
snd := zero :: _} := fst
|
||||||
| _ := false;
|
| _ := false;
|
||||||
|
|
||||||
main : Triple Nat Nat Nat :=
|
main : Triple Nat Nat Nat :=
|
||||||
let
|
let
|
||||||
p : Triple Nat Nat Nat := mkTriple 2 2 2;
|
p : Triple Nat Nat Nat := mkTriple 2 2 2;
|
||||||
p' :
|
p' : Triple Nat Nat Nat :=
|
||||||
Triple Nat Nat Nat :=
|
|
||||||
p@Triple{
|
p@Triple{
|
||||||
fst := fst + 1;
|
fst := fst + 1;
|
||||||
snd := snd * 3 + thd + fst
|
snd := snd * 3 + thd + fst
|
||||||
};
|
};
|
||||||
f :
|
f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
|
||||||
Triple Nat Nat Nat -> Triple Nat Nat Nat :=
|
|
||||||
(@Triple{fst := fst * 10});
|
(@Triple{fst := fst * 10});
|
||||||
in if
|
in if
|
||||||
(mf (mkPair (fst := mkPair true nil; snd := 0 :: nil)))
|
(mf (mkPair (fst := mkPair true nil; snd := 0 :: nil)))
|
||||||
|
Loading…
Reference in New Issue
Block a user