Skip to content

Commit

Permalink
crucible-syntax: Export helper for parsing assignments
Browse files Browse the repository at this point in the history
  • Loading branch information
langston-barrett committed Nov 8, 2023
1 parent 3daf9bb commit c111435
Showing 1 changed file with 22 additions and 14 deletions.
36 changes: 22 additions & 14 deletions crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ module Lang.Crucible.Syntax.Concrete
, BoundedNat(..)
, PosNat
, posNat
, someAssign
-- * Rules for pretty-printing language syntax
, printExpr
)
Expand Down Expand Up @@ -1935,26 +1936,33 @@ deriving instance Show (ACFG ext)

data Arg t = Arg AtomName Position (TypeRepr t)



arguments' :: forall m ext
. ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
=> m (Some (Ctx.Assignment Arg))
arguments' = call (go (Some Ctx.empty))
someAssign ::
forall m ext a.
( MonadSyntax Atomic m
, ?parserHooks :: ParserHooks ext
) =>
Text ->
m (Some a) ->
m (Some (Ctx.Assignment a))
someAssign desc sub = call (go (Some Ctx.empty))
where
go :: Some (Ctx.Assignment Arg) -> m (Some (Ctx.Assignment Arg))
go :: Some (Ctx.Assignment a) -> m (Some (Ctx.Assignment a))
go args@(Some prev) =
describe "argument list" $
describe desc $
(emptyList *> pure args) <|>
(depCons oneArg $
(depCons sub $
\(Some a) ->
go (Some $ Ctx.extend prev a))

where oneArg =
(describe "argument" $
located $
cons atomName (cons isType emptyList)) <&>
\(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)
arguments' :: forall m ext
. ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
=> m (Some (Ctx.Assignment Arg))
arguments' = someAssign "argument list" oneArg
where oneArg =
(describe "argument" $
located $
cons atomName (cons isType emptyList)) <&>
\(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)


saveArgs :: (MonadState (SyntaxState s) m, MonadError (ExprErr s) m)
Expand Down

0 comments on commit c111435

Please sign in to comment.