@@ -140,17 +140,15 @@ parseSymbolHead = parseSymbolOrAliasDeclarationHead Symbol
140
140
-}
141
141
parsePattern :: Parser ParsedPattern
142
142
parsePattern =
143
- (embedParsedPattern <$> parseLiteral) <|> (parseAnyId >>= parseRemainder)
143
+ parseLiteral <|> (parseAnyId >>= parseRemainder)
144
144
where
145
145
parseRemainder identifier =
146
146
parseVariableRemainder identifier
147
147
<|> parseKoreRemainder identifier
148
- <|> ( parseApplicationRemainder identifier)
148
+ <|> parseApplicationRemainder identifier
149
149
150
- parseLiteral :: Parser (PatternF VariableName ParsedPattern )
151
- parseLiteral =
152
- (StringLiteralF . Const <$> parseStringLiteral)
153
- <?> " string literal"
150
+ parseLiteral :: Parser ParsedPattern
151
+ parseLiteral = (from <$> parseStringLiteral) <?> " string literal"
154
152
155
153
parseVariable :: Parser (SomeVariable VariableName )
156
154
parseVariable = do
@@ -176,8 +174,7 @@ parseVariableRemainder identifier = do
176
174
-- variable, not a symbol, and now we will validate it as a variable name.
177
175
variableName <- getSomeVariableName identifier
178
176
variableSort <- parseSort
179
- (pure . embedParsedPattern . VariableF . Const )
180
- Variable { variableName, variableSort }
177
+ (pure . from) Variable { variableName, variableSort }
181
178
182
179
getSomeVariableName :: Id -> Parser (SomeVariableName VariableName )
183
180
getSomeVariableName identifier =
@@ -258,8 +255,7 @@ parseApplicationRemainder :: Id -> Parser ParsedPattern
258
255
parseApplicationRemainder identifier = do
259
256
applicationSymbolOrAlias <- parseSymbolOrAliasRemainder identifier
260
257
applicationChildren <- parens . list $ parsePattern
261
- (pure . embedParsedPattern . ApplicationF )
262
- Application { applicationSymbolOrAlias, applicationChildren }
258
+ (pure . from) Application { applicationSymbolOrAlias, applicationChildren }
263
259
264
260
{- | Parse the tail of a 'SymbolOrAlias', after the @Id@.
265
261
@@ -311,9 +307,7 @@ parseAssoc foldAssoc = do
311
307
braces $ pure ()
312
308
application <- parens $ parseApplication parsePattern
313
309
let mkApplication child1 child2 =
314
- application { applicationChildren = [child1, child2] }
315
- & ApplicationF
316
- & embedParsedPattern
310
+ from application { applicationChildren = [child1, child2] }
317
311
case applicationChildren application of
318
312
[] -> fail " expected one or more arguments"
319
313
children -> pure (foldAssoc mkApplication children)
@@ -363,29 +357,29 @@ parseKoreRemainder :: Id -> Parser ParsedPattern
363
357
parseKoreRemainder identifier =
364
358
getSpecialId identifier >>= \ case
365
359
-- Connectives
366
- " top" -> embedParsedPattern . TopF <$> parseConnective0 Top
367
- " bottom" -> embedParsedPattern . BottomF <$> parseConnective0 Bottom
368
- " not" -> embedParsedPattern . NotF <$> parseConnective1 Not
369
- " and" -> embedParsedPattern . AndF <$> parseConnective2 And
370
- " or" -> embedParsedPattern . OrF <$> parseConnective2 Or
371
- " implies" -> embedParsedPattern . ImpliesF <$> parseConnective2 Implies
372
- " iff" -> embedParsedPattern . IffF <$> parseConnective2 Iff
360
+ " top" -> from <$> parseConnective0 Top
361
+ " bottom" -> from <$> parseConnective0 Bottom
362
+ " not" -> from <$> parseConnective1 Not
363
+ " and" -> from <$> parseConnective2 And
364
+ " or" -> from <$> parseConnective2 Or
365
+ " implies" -> from <$> parseConnective2 Implies
366
+ " iff" -> from <$> parseConnective2 Iff
373
367
-- Quantifiers
374
- " exists" -> embedParsedPattern . ExistsF <$> parseQuantifier Exists
375
- " forall" -> embedParsedPattern . ForallF <$> parseQuantifier Forall
368
+ " exists" -> from <$> parseQuantifier Exists
369
+ " forall" -> from <$> parseQuantifier Forall
376
370
-- Fixpoints
377
- " mu" -> embedParsedPattern . MuF <$> parseFixpoint Mu
378
- " nu" -> embedParsedPattern . NuF <$> parseFixpoint Nu
371
+ " mu" -> from <$> parseFixpoint Mu
372
+ " nu" -> from <$> parseFixpoint Nu
379
373
-- Predicates
380
- " ceil" -> embedParsedPattern . CeilF <$> parsePredicate1 Ceil
381
- " floor" -> embedParsedPattern . FloorF <$> parsePredicate1 Floor
382
- " equals" -> embedParsedPattern . EqualsF <$> parsePredicate2 Equals
383
- " in" -> embedParsedPattern . InF <$> parsePredicate2 In
374
+ " ceil" -> from <$> parsePredicate1 Ceil
375
+ " floor" -> from <$> parsePredicate1 Floor
376
+ " equals" -> from <$> parsePredicate2 Equals
377
+ " in" -> from <$> parsePredicate2 In
384
378
-- Rewriting
385
- " next" -> embedParsedPattern . NextF <$> parseConnective1 Next
386
- " rewrites" -> embedParsedPattern . RewritesF <$> parseConnective2 Rewrites
379
+ " next" -> from <$> parseConnective1 Next
380
+ " rewrites" -> from <$> parseConnective2 Rewrites
387
381
-- Values
388
- " dv" -> embedParsedPattern . DomainValueF <$> parseDomainValue
382
+ " dv" -> from <$> parseDomainValue
389
383
-- Syntax sugar
390
384
" left-assoc" -> parseLeftAssoc
391
385
" right-assoc" -> parseRightAssoc
@@ -403,7 +397,7 @@ getSpecialId Id { getId } = do
403
397
_ ::= _ "{" ⟨sort⟩ "}" "(" ")"
404
398
@
405
399
-}
406
- parseConnective0 :: (Sort -> result ) -> Parser result
400
+ parseConnective0 :: (Sort -> f ParsedPattern ) -> Parser ( f ParsedPattern )
407
401
parseConnective0 mkResult = do
408
402
sort <- braces parseSort
409
403
() <- parens $ pure ()
0 commit comments