Skip to content
Permalink
Browse files

Merge PR #167: Ran the update of the code formatter

  • Loading branch information
mariari authored and cwgoes committed Nov 9, 2019
1 parent 2b14f06 commit d1bd6f66a5ab0b92f4cff7a704c15f9a998d364b
@@ -92,8 +92,11 @@ transformAndEvaluateErasedCore debug term = do
net = INet.astToNet ast INet.defaultEnv net = INet.astToNet ast INet.defaultEnv
when debug $ H.outputStrLn ("Translated to net: " <> show net) when debug $ H.outputStrLn ("Translated to net: " <> show net)
let reduced = Graph.runFlipNet (INet.reduceAll 1000000) net let reduced = Graph.runFlipNet (INet.reduceAll 1000000) net

info = Env.info reduced info = Env.info reduced

res = Env.net reduced res = Env.net reduced

when debug $ H.outputStrLn ("Reduced net: " <> show res) when debug $ H.outputStrLn ("Reduced net: " <> show res)
let readback = INet.netToAst res let readback = INet.netToAst res
when debug $ H.outputStrLn ("Reduction info: " <> show info) when debug $ H.outputStrLn ("Reduction info: " <> show info)
@@ -87,9 +87,13 @@ typeOf (App t1 t2) = do
f p = do f p = do
(ArrowType (_ Proxy k), ArrowType (_ Proxy to)) pure (isFromA p) (ArrowType (_ Proxy k), ArrowType (_ Proxy to)) pure (isFromA p)
let ta = R.typeRep R.TypeRep k let ta = R.typeRep R.TypeRep k

tb = R.typeRep R.TypeRep Int tb = R.typeRep R.TypeRep Int

tc = R.typeRep R.TypeRep to tc = R.typeRep R.TypeRep to

td = R.typeRep Arrowable to R.TypeRep to td = R.typeRep Arrowable to R.TypeRep to

case (R.eqTypeRep ta tb) of case (R.eqTypeRep ta tb) of
Nothing [False, False] Nothing [False, False]
Just T.HRefl Just T.HRefl
@@ -103,8 +103,11 @@ addBlock bname = do
ix get @"blockCount" ix get @"blockCount"
nms get @"names" nms get @"names"
let new = emptyBlock ix let new = emptyBlock ix

(qname, supply) = uniqueName bname nms (qname, supply) = uniqueName bname nms

name = internName qname name = internName qname

put @"blocks" (Map.insert name new bls) put @"blocks" (Map.insert name new bls)
put @"blockCount" (succ ix) put @"blockCount" (succ ix)
put @"names" supply put @"names" supply
@@ -254,6 +254,7 @@ intOfNumPorts typ numPort cont = do
generateIf typ tag smallBranch largeBranch generateIf typ tag smallBranch largeBranch
where where
smallBranch = branchGen numPortsSmall numPortsSmallValue return smallBranch = branchGen numPortsSmall numPortsSmallValue return

largeBranch = branchGen numPortsLarge numPortsLargeValuePtr $ largeBranch = branchGen numPortsLarge numPortsLargeValuePtr $
\vPtr do \vPtr do
deref2 Block.getElementPtr $ deref2 Block.getElementPtr $
@@ -263,6 +264,7 @@ intOfNumPorts typ numPort cont = do
Types.indincies' = Block.constant32List [0, 1] Types.indincies' = Block.constant32List [0, 1]
} }
load numPortsLargeValue deref2 load numPortsLargeValue deref2

-- Generic logic -- Generic logic
branchGen variant variantType extraDeref = do branchGen variant variantType extraDeref = do
casted bitCast numPort (varientToType variant) casted bitCast numPort (varientToType variant)
@@ -99,10 +99,14 @@ insertSums ∷
insertSums sumName variants symTbl varTbl typTbl = (newSymTbl, newVarTbl, newTypTbl) insertSums sumName variants symTbl varTbl typTbl = (newSymTbl, newVarTbl, newTypTbl)
where where
sum' = createSum variants sum' = createSum variants

tag' = tagSizeIntExn (tagSize variants) tag' = tagSizeIntExn (tagSize variants)

typTbl' = Map.insert sumName sum' typTbl typTbl' = Map.insert sumName sum' typTbl

symTbl' = symTbl' =
Map.insert sumName (LocalReference sum' (mkName (unintern sumName))) symTbl Map.insert sumName (LocalReference sum' (mkName (unintern sumName))) symTbl

newVarTbl = newVarTbl =
fst $ fst $
foldr foldr
@@ -121,13 +125,15 @@ insertSums sumName variants symTbl varTbl typTbl = (newSymTbl, newVarTbl, newTyp
) )
(varTbl, 0) (varTbl, 0)
variants variants

newTypTbl = newTypTbl =
foldr foldr
( \(Variant _s n t) tbl ( \(Variant _s n t) tbl
Map.insert (createVariantName sumName n) t tbl Map.insert (createVariantName sumName n) t tbl
) )
typTbl' typTbl'
variants variants

newSymTbl = newSymTbl =
foldr foldr
( \(Variant _s n t) tbl ( \(Variant _s n t) tbl
@@ -12,6 +12,7 @@ import qualified Z3.Monad as Z3
runMultipleConstraints a. Int [Constraint] RPT a IO () runMultipleConstraints a. Int [Constraint] RPT a IO ()
runMultipleConstraints numRepeat constraints syntax = do runMultipleConstraints numRepeat constraints syntax = do
let numset = grabTermNumbers syntax mempty let numset = grabTermNumbers syntax mempty

recGen _ _ _ 0 = pure () recGen _ _ _ 0 = pure ()
recGen constraintCall printModel consZ3 num = do recGen constraintCall printModel consZ3 num = do
(r, v, s) Z3.evalZ3 constraintCall (r, v, s) Z3.evalZ3 constraintCall
@@ -21,27 +22,32 @@ runMultipleConstraints numRepeat constraints syntax = do
case s of case s of
Just x Just x
let bounds = filter (\(i, _) Set.member i numset) (zip [0 ..] x) let bounds = filter (\(i, _) Set.member i numset) (zip [0 ..] x)

newCons = newCons =
bounds bounds
>>| ( \(i, x) >>| ( \(i, x)
Constraint Constraint
[ConstraintVar 1 i] [ConstraintVar 1 i]
(Eq (fromInteger x)) (Eq (fromInteger x))
) )

extraConstraint = extraConstraint =
makeVarMap newCons makeVarMap newCons
>>= flip constraintsToZ3 newCons >>= flip constraintsToZ3 newCons
>>= Z3.mkNot >>= Z3.mkNot

in recNext in recNext
extraConstraint extraConstraint
consZ3 consZ3
(pred num) (pred num)
Nothing pure () Nothing pure ()

recFirst = recFirst =
recGen recGen
(constraintSystem constraints) (constraintSystem constraints)
putStrLn putStrLn
(pure []) (pure [])

recNext extra consZ3 = recNext extra consZ3 =
recGen recGen
( do ( do
@@ -51,6 +57,7 @@ runMultipleConstraints numRepeat constraints syntax = do
) )
(\_ pure ()) (\_ pure ())
((:) <$> extra <*> consZ3) ((:) <$> extra <*> consZ3)

recFirst numRepeat recFirst numRepeat
where where
-- Could use a list, since this should be ascending, but I do not assume that -- Could use a list, since this should be ascending, but I do not assume that
@@ -37,6 +37,7 @@ generateParser ∷
generateParser parameterisation = generateParser parameterisation =
let opNames [String] let opNames [String]
opNames = baseReservedOpNames <> reservedOpNames parameterisation opNames = baseReservedOpNames <> reservedOpNames parameterisation

languageDef GenLanguageDef String u Identity languageDef GenLanguageDef String u Identity
languageDef = languageDef =
emptyDef emptyDef
@@ -49,64 +50,84 @@ generateParser parameterisation =
baseReservedNames <> reservedNames parameterisation, baseReservedNames <> reservedNames parameterisation,
Token.reservedOpNames = opNames Token.reservedOpNames = opNames
} }

ops [[Operator Char () (Elim primTy primVal)]] ops [[Operator Char () (Elim primTy primVal)]]
ops = [[Infix appl AssocLeft]] ops = [[Infix appl AssocLeft]]

appl appl
Parser (Elim primTy primVal Elim primTy primVal Elim primTy primVal) Parser (Elim primTy primVal Elim primTy primVal Elim primTy primVal)
appl = do appl = do
whiteSpace whiteSpace
notFollowedBy (choice (map reservedOp opNames)) notFollowedBy (choice (map reservedOp opNames))
pure (\f x App f (Elim x)) pure (\f x App f (Elim x))

lexer Token.GenTokenParser String u Identity lexer Token.GenTokenParser String u Identity
lexer = Token.makeTokenParser languageDef lexer = Token.makeTokenParser languageDef

identifier Parser String identifier Parser String
identifier = Token.identifier lexer identifier = Token.identifier lexer

reserved String Parser () reserved String Parser ()
reserved = Token.reserved lexer reserved = Token.reserved lexer

reservedOp String Parser () reservedOp String Parser ()
reservedOp = Token.reservedOp lexer reservedOp = Token.reservedOp lexer

parens Parser a Parser a parens Parser a Parser a
parens = Token.parens lexer parens = Token.parens lexer

natural Parser Integer natural Parser Integer
natural = Token.natural lexer natural = Token.natural lexer

whiteSpace Parser () whiteSpace Parser ()
whiteSpace = Token.whiteSpace lexer whiteSpace = Token.whiteSpace lexer

usage Parser Usage usage Parser Usage
usage = (reserved "w" >> return Omega) <|> SNat . fromInteger <$> natural usage = (reserved "w" >> return Omega) <|> SNat . fromInteger <$> natural

primTyTerm Parser (Term primTy primVal) primTyTerm Parser (Term primTy primVal)
primTyTerm = PrimTy |<< parseTy parameterisation lexer primTyTerm = PrimTy |<< parseTy parameterisation lexer

sortTerm Parser (Term primTy primVal) sortTerm Parser (Term primTy primVal)
sortTerm = do sortTerm = do
reserved "*" reserved "*"
n natural n natural
return $ Star (fromInteger n) return $ Star (fromInteger n)

piTerm Parser (Term primTy primVal) piTerm Parser (Term primTy primVal)
piTerm = do piTerm = do
reserved "[Π]" reserved "[Π]"
pi usage pi usage
input term input term
func term func term
return $ Pi pi input func return $ Pi pi input func

lamTerm Parser (Term primTy primVal) lamTerm Parser (Term primTy primVal)
lamTerm = do lamTerm = do
reservedOp "\\" reservedOp "\\"
binder binder binder binder
reservedOp "->" reservedOp "->"
func term func term
return $ Lam binder func return $ Lam binder func

binder Parser Symbol binder Parser Symbol
binder = intern |<< identifier binder = intern |<< identifier

term Parser (Term primTy primVal) term Parser (Term primTy primVal)
term = try termOnly <|> elimTerm term = try termOnly <|> elimTerm

termOnly Parser (Term primTy primVal) termOnly Parser (Term primTy primVal)
termOnly = termOnly =
parens termOnly <|> primTyTerm <|> sortTerm <|> piTerm <|> lamTerm parens termOnly <|> primTyTerm <|> sortTerm <|> piTerm <|> lamTerm

elimTerm Parser (Term primTy primVal) elimTerm Parser (Term primTy primVal)
elimTerm = do elimTerm = do
elim elim elim elim
pure (Elim elim) pure (Elim elim)

primElim Parser (Elim primTy primVal) primElim Parser (Elim primTy primVal)
primElim = Prim |<< parseVal parameterisation lexer primElim = Prim |<< parseVal parameterisation lexer

annElim Parser (Elim primTy primVal) annElim Parser (Elim primTy primVal)
annElim = do annElim = do
reservedOp "@" reservedOp "@"
@@ -115,19 +136,24 @@ generateParser parameterisation =
pi usage pi usage
theType term theType term
pure (Ann pi theTerm theType) pure (Ann pi theTerm theType)

varElim Parser (Elim primTy primVal) varElim Parser (Elim primTy primVal)
varElim = Var |<< binder varElim = Var |<< binder

elim Parser (Elim primTy primVal) elim Parser (Elim primTy primVal)
elim = buildExpressionParser ops elim' elim = buildExpressionParser ops elim'

elim' Parser (Elim primTy primVal) elim' Parser (Elim primTy primVal)
elim' = try primElim <|> annElim <|> varElim <|> parens elim elim' = try primElim <|> annElim <|> varElim <|> parens elim

parseWhole Parser a Parser a parseWhole Parser a Parser a
parseWhole p = do parseWhole p = do
whiteSpace whiteSpace
t p t p
whiteSpace whiteSpace
eof eof
return t return t

in parseString' (parseWhole term) in parseString' (parseWhole term)


parseString' Parser a String Maybe a parseString' Parser a String Maybe a
@@ -41,9 +41,13 @@ caseGen (Case on cases@(C c _ _ : _)) onNoArg onRec = do
pure (f idL) pure (f idL)
Just ([], body) pure (f $ onNoArg body) Just ([], body) pure (f $ onNoArg body)
Just (args, body) pure (f (foldr Lambda body args)) Just (args, body) pure (f (foldr Lambda body args))

recCase t accLam = lambdaFromEnv (flip onRec accLam) t recCase t accLam = lambdaFromEnv (flip onRec accLam) t

initial t = lambdaFromEnv identity t initial t = lambdaFromEnv identity t

butLastadtCon = reverse (tailSafe (reverse adtConstructors)) butLastadtCon = reverse (tailSafe (reverse adtConstructors))

last initial (lastDef (error "doesn't happen") adtConstructors) last initial (lastDef (error "doesn't happen") adtConstructors)
expandedCase foldrM recCase last butLastadtCon expandedCase foldrM recCase last butLastadtCon
return $ Application on expandedCase return $ Application on expandedCase
@@ -136,7 +136,9 @@ inl =
$ Application (Value k) (Value x) $ Application (Value k) (Value x)
where where
x = intern "x" x = intern "x"

k = intern "k" k = intern "k"

l = intern "l" l = intern "l"


-- | Op of inl that has the first argument call the 2nd -- | Op of inl that has the first argument call the 2nd
@@ -149,7 +151,9 @@ inlOp =
$ Application (Value x) (Value k) $ Application (Value x) (Value k)
where where
x = intern "x" x = intern "x"

k = intern "k" k = intern "k"

l = intern "l" l = intern "l"


inr Lambda inr Lambda
@@ -160,7 +164,9 @@ inr =
$ Application (Value l) (Value y) $ Application (Value l) (Value y)
where where
y = intern "y" y = intern "y"

k = intern "k" k = intern "k"

l = intern "l" l = intern "l"


-- | Op of inr that has the first argument call the 2nd -- | Op of inr that has the first argument call the 2nd
@@ -173,7 +179,9 @@ inrOp =
$ Application (Value y) (Value l) $ Application (Value y) (Value l)
where where
y = intern "y" y = intern "y"

k = intern "k" k = intern "k"

l = intern "l" l = intern "l"


foldM' Lambda foldM' Lambda
@@ -19,11 +19,13 @@ adtToScott (Adt name s) = sumRec s 1 (adtLength s)
where where
adtLength Single {} = 1 adtLength Single {} = 1
adtLength (Branch _ _ s) = succ (adtLength s) adtLength (Branch _ _ s) = succ (adtLength s)

sumRec (Branch s p next) posAdt lenAdt = do sumRec (Branch s p next) posAdt lenAdt = do
adtConstructor s (sumProd p posAdt lenAdt) name adtConstructor s (sumProd p posAdt lenAdt) name
sumRec next (succ posAdt) lenAdt sumRec next (succ posAdt) lenAdt
sumRec (Single s p) posAdt lenAdt = sumRec (Single s p) posAdt lenAdt =
adtConstructor s (sumProd p posAdt lenAdt) name adtConstructor s (sumProd p posAdt lenAdt) name

sumProd None posAdt lengthAdt = generateLam posAdt lengthAdt identity sumProd None posAdt lengthAdt = generateLam posAdt lengthAdt identity
sumProd Term posAdt lengthAdt = sumProd Term posAdt lengthAdt =
Lambda Lambda
@@ -40,6 +42,7 @@ adtToScott (Adt name s) = sumRec s 1 (adtLength s)
(\spot Lambda (intern $ "%arg" <> show spot)) (\spot Lambda (intern $ "%arg" <> show spot))
(encoding prodLen) (encoding prodLen)
[1 .. prodLen] [1 .. prodLen]

encoding prodLen = generateLam posAdt lengthAdt $ encoding prodLen = generateLam posAdt lengthAdt $
\body \body
foldl foldl
@@ -52,9 +55,11 @@ adtToScott (Adt name s) = sumRec s 1 (adtLength s)
) )
body body
[1 .. prodLen] [1 .. prodLen]

lengthProd (Product p) = succ (lengthProd p) lengthProd (Product p) = succ (lengthProd p)
lengthProd Term = 1 lengthProd Term = 1
lengthProd None = 0 -- I'm skeptical this case ever happens lengthProd None = 0 -- I'm skeptical this case ever happens

generateLam posAdt lengthAdt onPosAdt = generateLam posAdt lengthAdt onPosAdt =
foldr foldr
(\spot Lambda (intern $ "%genArg" <> show spot)) (\spot Lambda (intern $ "%genArg" <> show spot))
@@ -79,6 +84,8 @@ scottCase c = do
Value {} error "doesn't happen" Value {} error "doesn't happen"
where where
onNoArg = identity onNoArg = identity

onrec c accLam = (Application c accLam) onrec c accLam = (Application c accLam)

reverseApp on (Application b1 b2) = reverseApp (Application on b1) b2 reverseApp on (Application b1 b2) = reverseApp (Application on b1) b2
reverseApp on s = Application on s reverseApp on s = Application on s
@@ -84,9 +84,13 @@ incGraphSizeStep n = do
let memoryAllocated let memoryAllocated
| n > 0 = memAlloced + n | n > 0 = memAlloced + n
| otherwise = memAlloced | otherwise = memAlloced

currentGraphSize = n + currGraph currentGraphSize = n + currGraph

biggestGraphSize = max currentGraphSize largestGraph biggestGraphSize = max currentGraphSize largestGraph

sequentalSteps = succ seqStep sequentalSteps = succ seqStep

put @"info" Info put @"info" Info
{ memoryAllocated, { memoryAllocated,
currentGraphSize, currentGraphSize,
@@ -64,8 +64,11 @@ instance Network FlipNet where
deleteRewire oldNodesToDelete newNodes = do deleteRewire oldNodesToDelete newNodes = do
Flip net get @"net" Flip net get @"net"
let newNodeSet = Set.fromList newNodes let newNodeSet = Set.fromList newNodes

neighbors = fst <$> (oldNodesToDelete >>= lneighbors net) neighbors = fst <$> (oldNodesToDelete >>= lneighbors net)

conflictingNeighbors = findConflict newNodeSet neighbors conflictingNeighbors = findConflict newNodeSet neighbors

traverse_ (uncurry link) conflictingNeighbors traverse_ (uncurry link) conflictingNeighbors
delNodes oldNodesToDelete delNodes oldNodesToDelete


@@ -114,8 +114,11 @@ instance Network Net where
deleteRewire oldNodesToDelete newNodes = do deleteRewire oldNodesToDelete newNodes = do
Net net get @"net" Net net get @"net"
let newNodeSet = Set.fromList newNodes let newNodeSet = Set.fromList newNodes

neighbor = neighbors oldNodesToDelete net neighbor = neighbors oldNodesToDelete net

conflictingNeighbors = findConflict newNodeSet neighbor conflictingNeighbors = findConflict newNodeSet neighbor

traverse_ (uncurry link) conflictingNeighbors traverse_ (uncurry link) conflictingNeighbors
delNodes oldNodesToDelete delNodes oldNodesToDelete


@@ -128,9 +131,11 @@ deleteAllPoints ∷
deleteAllPoints n = foldr f deleteAllPoints n = foldr f
where where
f (n, pt) = Map.adjust (\x deleteIfDiff pt (x ^. edges) x) n f (n, pt) = Map.adjust (\x deleteIfDiff pt (x ^. edges) x) n

deleteIfDiff pt edge deleteIfDiff pt edge
| isSame pt edge = over edges (Map.delete pt) | isSame pt edge = over edges (Map.delete pt)
| otherwise = identity | otherwise = identity

isSame pt edge = case Map.lookup pt edge of isSame pt edge = case Map.lookup pt edge of
Just x | fst x == n True Just x | fst x == n True
_ False _ False

0 comments on commit d1bd6f6

Please sign in to comment.
You can’t perform that action at this time.