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