
  0 | module Idris.Parser.Let
  1 | 
  2 | import Idris.Syntax
  3 | import Libraries.Text.Bounded
  4 | 
  5 | import Data.Either
  6 | import Data.List1
  7 | 
  8 | %default total
  9 | 
 10 | ------------------------------------------------------------------------
 11 | -- Types
 12 | 
 13 | -- `let ... in ...` is used for two different notions:
 14 | -- * pattern-matching let binders to locally take an expression apart
 15 | -- * Local definitions that can be recursive
 16 | 
 17 | public export
 18 | record LetBinder where
 19 |   constructor MkLetBinder
 20 |   letUsage     : RigCount
 21 |   letPattern   : PTerm
 22 |   letBoundType : PTerm
 23 |   letBoundTerm : PTerm
 24 |   letUnhappy   : List PClause
 25 | 
 26 | public export
 27 | LetDecl : Type
 28 | LetDecl = List PDecl
 29 | 
 30 | ------------------------------------------------------------------------
 31 | -- Let-binding functions
 32 | 
 33 | letFactory : (List (WithBounds LetBinder) -> a -> a) ->
 34 |              (WithBounds LetDecl -> a -> a) ->
 35 |              List1 (WithBounds (Either LetBinder LetDecl)) ->
 36 |              a -> a
 37 | letFactory letBind letDeclare blocks scope = foldr mkLet scope groups where
 38 | 
 39 |   LetBlock : Type
 40 |   LetBlock = Either (List1 (WithBounds LetBinder)) (List1 (WithBounds LetDecl))
 41 | 
 42 |   groups : List LetBlock
 43 |   groups = compress (forget $ map (\ b => bimap (<$ b) (<$ b) b.val) blocks)
 44 | 
 45 |   mkLet : LetBlock -> a -> a
 46 |   mkLet (Left  letBinds) = letBind (forget letBinds)
 47 |   mkLet (Right letDecls) =
 48 |     let bounds = mergeBounds (head letDecls) (last letDecls)
 49 |     in letDeclare (concatMap val letDecls <$ bounds)
 50 | 
 51 | export
 52 | mkLets : OriginDesc ->
 53 |          List1 (WithBounds (Either LetBinder LetDecl)) ->
 54 |          PTerm -> PTerm
 55 | mkLets origin = letFactory buildLets
 56 |   (\ decls, scope => PLocal (virtualiseFC $ boundToFC origin decls) decls.val scope)
 57 | 
 58 |   where
 59 | 
 60 |     buildLets : List (WithBounds LetBinder) -> PTerm -> PTerm
 61 |     buildLets [] sc = sc
 62 |     buildLets (b :: rest) sc
 63 |       = let (MkLetBinder rig pat ty val alts) = b.val
 64 |             fc = virtualiseFC $ boundToFC origin b
 65 |         in PLet fc rig pat ty val (buildLets rest sc) alts
 66 | 
 67 | export
 68 | mkDoLets : OriginDesc ->
 69 |            List1 (WithBounds (Either LetBinder LetDecl)) ->
 70 |            List PDo
 71 | mkDoLets origin lets = letFactory
 72 |     (\ binds, rest => buildDoLets binds ++ rest)
 73 |     (\ decls, rest => DoLetLocal (boundToFC origin decls) decls.val :: rest)
 74 |     lets
 75 |     []
 76 | 
 77 |   where
 78 | 
 79 |     buildDoLets : List (WithBounds LetBinder) -> List PDo
 80 |     buildDoLets [] = []
 81 |     buildDoLets (b :: rest) = let fc = boundToFC origin b in case b.val of
 82 |       (MkLetBinder rig (PRef fc' (UN un)) ty val []) =>
 83 |          (if isPatternVariable un
 84 |             then DoLet fc fc' (UN un) rig ty val
 85 |             else DoLetPat fc (PRef fc' (UN un)) ty val []
 86 |          ) :: buildDoLets rest
 87 |       (MkLetBinder rig (PImplicit fc') ty val []) =>
 88 |         DoLet fc fc' (UN Underscore) rig ty val :: buildDoLets rest
 89 |       (MkLetBinder rig pat ty val alts) =>
 90 |         DoLetPat fc pat ty val alts :: buildDoLets rest
 91 |