0 | module Idris.Syntax
   1 |
   2 | import public Core.Context
   3 | import public Core.Context.Log
   4 | import public Core.Normalise
   5 | import public Core.Options
   6 |
   7 | import TTImp.TTImp
   8 |
   9 | import Data.SortedMap
  10 | import Data.String
  11 |
  12 | import public Idris.Syntax.Pragmas
  13 |
  14 | import Libraries.Data.ANameMap
  15 | import Libraries.Data.NameMap
  16 | import Libraries.Data.String.Extra
  17 | import Libraries.Data.WithDefault
  18 | import Libraries.Text.PrettyPrint.Prettyprinter
  19 |
  20 | %default covering
  21 |
  22 | public export
  23 | data OpStr' nm = OpSymbols nm | Backticked nm
  24 |
  25 | -- Left: backticked, Right: operator symbols
  26 | export
  27 | opNameToEither : OpStr' nm -> Either nm nm
  28 | opNameToEither (Backticked nm) = Left nm
  29 | opNameToEither (OpSymbols nm) = Right nm
  30 |
  31 | export
  32 | Functor OpStr' where
  33 |   map f (OpSymbols x) = OpSymbols (f x)
  34 |   map f (Backticked x) = Backticked (f x)
  35 |
  36 | export
  37 | Foldable OpStr' where
  38 |   foldr f i (OpSymbols x) = f x i
  39 |   foldr f i (Backticked x) = f x i
  40 |
  41 | export
  42 | traverseOp : (fn : Functor f) => (a -> f b) -> OpStr' a -> f (OpStr' b)
  43 | traverseOp f (OpSymbols x) = map OpSymbols (f x)
  44 | traverseOp f (Backticked x) = map Backticked (f x)
  45 |
  46 |
  47 | public export
  48 | Show nm => Show (OpStr' nm) where
  49 |   show (OpSymbols nm) = show nm
  50 |   show (Backticked nm) = "`\{show nm}`"
  51 |
  52 | public export
  53 | (.toName) : OpStr' nm -> nm
  54 | (.toName) (OpSymbols nm) = nm
  55 | (.toName) (Backticked nm) = nm
  56 |
  57 | public export
  58 | OpStr : Type
  59 | OpStr = OpStr' Name
  60 |
  61 | public export
  62 | data HidingDirective = HideName Name
  63 |                      | HideFixity Fixity Name
  64 |
  65 | -------------------------------------------------------------------------------
  66 |
  67 | mutual
  68 |
  69 |   ||| Source language as produced by the parser
  70 |   public export
  71 |   PTerm : Type
  72 |   PTerm = PTerm' Name
  73 |
  74 |   ||| Internal PTerm
  75 |   ||| Source language as produced by the unelaboration of core Terms
  76 |   ||| KindedNames carry extra information about the nature of the variable
  77 |   public export
  78 |   IPTerm : Type
  79 |   IPTerm = PTerm' KindedName
  80 |
  81 |   ||| The full high level source language
  82 |   ||| This gets desugared to RawImp (TTImp.TTImp),
  83 |   ||| then elaborated to Term (Core.TT)
  84 |   public export
  85 |   data PTerm' : Type -> Type where
  86 |        -- Direct (more or less) translations to RawImp
  87 |
  88 |        PRef : FC -> nm -> PTerm' nm
  89 |        NewPi : WithFC (PBinderScope' nm) -> PTerm' nm
  90 |        Forall : WithFC (List1 (WithFC Name), PTerm' nm) -> PTerm' nm
  91 |
  92 |        PPi : FC -> RigCount -> PiInfo (PTerm' nm) -> Maybe Name ->
  93 |              (argTy : PTerm' nm) -> (retTy : PTerm' nm) -> PTerm' nm
  94 |        PLam : FC -> RigCount -> PiInfo (PTerm' nm) -> (pat : PTerm' nm) ->
  95 |               (argTy : PTerm' nm) -> (scope : PTerm' nm) -> PTerm' nm
  96 |        PLet : FC -> RigCount -> (pat : PTerm' nm) ->
  97 |               (nTy : PTerm' nm) -> (nVal : PTerm' nm) -> (scope : PTerm' nm) ->
  98 |               (alts : List (PClause' nm)) -> PTerm' nm
  99 |        PCase : FC -> List (PFnOpt' nm) -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
 100 |        PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm
 101 |        PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm
 102 |        PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 103 |        PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 104 |        PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm
 105 |        PAutoApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 106 |
 107 |        PDelayed : FC -> LazyReason -> PTerm' nm -> PTerm' nm
 108 |        PDelay : FC -> PTerm' nm -> PTerm' nm
 109 |        PForce : FC -> PTerm' nm -> PTerm' nm
 110 |
 111 |        PSearch : FC -> (depth : Nat) -> PTerm' nm
 112 |        PPrimVal : FC -> Constant -> PTerm' nm
 113 |        PQuote : FC -> PTerm' nm -> PTerm' nm
 114 |        PQuoteName : FC -> Name -> PTerm' nm
 115 |        PQuoteDecl : FC -> List (PDecl' nm) -> PTerm' nm
 116 |        PUnquote : FC -> PTerm' nm -> PTerm' nm
 117 |        PRunElab : FC -> PTerm' nm -> PTerm' nm
 118 |        PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm' nm
 119 |        PType : FC -> PTerm' nm
 120 |        PAs : FC -> (nameFC : FC) -> Name -> (pattern : PTerm' nm) -> PTerm' nm
 121 |        PDotted : FC -> PTerm' nm -> PTerm' nm
 122 |        PImplicit : FC -> PTerm' nm
 123 |        PInfer : FC -> PTerm' nm
 124 |
 125 |        -- Operators
 126 |
 127 |        POp : (full : FC) ->
 128 |              (lhsInfo : WithFC (OperatorLHSInfo (PTerm' nm))) ->
 129 |              WithFC (OpStr' nm) -> (rhs : PTerm' nm) -> PTerm' nm
 130 |        PPrefixOp : (full : FC) -> WithFC (OpStr' nm) -> PTerm' nm -> PTerm' nm
 131 |        PSectionL : (full : FC) -> WithFC (OpStr' nm) -> PTerm' nm -> PTerm' nm
 132 |        PSectionR : (full : FC) -> PTerm' nm -> WithFC (OpStr' nm) -> PTerm' nm
 133 |        PEq : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 134 |        PBracketed : FC -> PTerm' nm -> PTerm' nm
 135 |
 136 |        -- Syntactic sugar
 137 |        PString : FC -> (hashtag : Nat) -> List (PStr' nm) -> PTerm' nm
 138 |        PMultiline : FC -> (hashtag : Nat) -> (indent : Nat) -> List (List (PStr' nm)) -> PTerm' nm
 139 |        PDoBlock : FC -> Maybe Namespace -> List (PDo' nm) -> PTerm' nm
 140 |        PBang : FC -> PTerm' nm -> PTerm' nm
 141 |        PIdiom : FC -> Maybe Namespace -> PTerm' nm -> PTerm' nm
 142 |        PList : (full, nilFC : FC) -> List (FC, PTerm' nm) -> PTerm' nm
 143 |                                         -- ^   v location of the conses/snocs
 144 |        PSnocList : (full, nilFC : FC) -> SnocList ((FC, PTerm' nm)) -> PTerm' nm
 145 |        PPair : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 146 |        PDPair : (full, opFC : FC) -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
 147 |        PUnit : FC -> PTerm' nm
 148 |        PIfThenElse : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
 149 |        PComprehension : FC -> PTerm' nm -> List (PDo' nm) -> PTerm' nm
 150 |        PRewrite : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
 151 |        -- A list range [x,y..z]
 152 |        PRange : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> PTerm' nm
 153 |        -- A stream range [x,y..]
 154 |        PRangeStream : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm
 155 |        -- r.x.y
 156 |        PPostfixApp : FC -> PTerm' nm -> List (FC, Name) -> PTerm' nm
 157 |        -- .x.y
 158 |        PPostfixAppPartial : FC -> List (FC, Name) -> PTerm' nm
 159 |
 160 |        -- Debugging
 161 |        PUnifyLog : FC -> LogLevel -> PTerm' nm -> PTerm' nm
 162 |
 163 |        -- with-disambiguation
 164 |        PWithUnambigNames : FC -> List (FC, Name) -> PTerm' nm -> PTerm' nm
 165 |
 166 |   export
 167 |   getPTermLoc : PTerm' nm -> FC
 168 |   getPTermLoc (PRef fc _) = fc
 169 |   getPTermLoc (NewPi x) = x.fc
 170 |   getPTermLoc (Forall x) = x.fc
 171 |   getPTermLoc (PPi fc _ _ _ _ _) = fc
 172 |   getPTermLoc (PLam fc _ _ _ _ _) = fc
 173 |   getPTermLoc (PLet fc _ _ _ _ _ _) = fc
 174 |   getPTermLoc (PCase fc _ _ _) = fc
 175 |   getPTermLoc (PLocal fc _ _) = fc
 176 |   getPTermLoc (PUpdate fc _) = fc
 177 |   getPTermLoc (PApp fc _ _) = fc
 178 |   getPTermLoc (PWithApp fc _ _) = fc
 179 |   getPTermLoc (PAutoApp fc _ _) = fc
 180 |   getPTermLoc (PNamedApp fc _ _ _) = fc
 181 |   getPTermLoc (PDelayed fc _ _) = fc
 182 |   getPTermLoc (PDelay fc _) = fc
 183 |   getPTermLoc (PForce fc _) = fc
 184 |   getPTermLoc (PSearch fc _) = fc
 185 |   getPTermLoc (PPrimVal fc _) = fc
 186 |   getPTermLoc (PQuote fc _) = fc
 187 |   getPTermLoc (PQuoteName fc _) = fc
 188 |   getPTermLoc (PQuoteDecl fc _) = fc
 189 |   getPTermLoc (PUnquote fc _) = fc
 190 |   getPTermLoc (PRunElab fc _) = fc
 191 |   getPTermLoc (PHole fc _ _) = fc
 192 |   getPTermLoc (PType fc) = fc
 193 |   getPTermLoc (PAs fc _ _ _) = fc
 194 |   getPTermLoc (PDotted fc _) = fc
 195 |   getPTermLoc (PImplicit fc) = fc
 196 |   getPTermLoc (PInfer fc) = fc
 197 |   getPTermLoc (POp fc _ _ _) = fc
 198 |   getPTermLoc (PPrefixOp fc _ _) = fc
 199 |   getPTermLoc (PSectionL fc _ _) = fc
 200 |   getPTermLoc (PSectionR fc _ _) = fc
 201 |   getPTermLoc (PEq fc _ _) = fc
 202 |   getPTermLoc (PBracketed fc _) = fc
 203 |   getPTermLoc (PString fc _ _) = fc
 204 |   getPTermLoc (PMultiline fc _ _ _) = fc
 205 |   getPTermLoc (PDoBlock fc _ _) = fc
 206 |   getPTermLoc (PBang fc _) = fc
 207 |   getPTermLoc (PIdiom fc _ _) = fc
 208 |   getPTermLoc (PList fc _ _) = fc
 209 |   getPTermLoc (PSnocList fc _ _) = fc
 210 |   getPTermLoc (PPair fc _ _) = fc
 211 |   getPTermLoc (PDPair fc _ _ _ _) = fc
 212 |   getPTermLoc (PUnit fc) = fc
 213 |   getPTermLoc (PIfThenElse fc _ _ _) = fc
 214 |   getPTermLoc (PComprehension fc _ _) = fc
 215 |   getPTermLoc (PRewrite fc _ _) = fc
 216 |   getPTermLoc (PRange fc _ _ _) = fc
 217 |   getPTermLoc (PRangeStream fc _ _) = fc
 218 |   getPTermLoc (PPostfixApp fc _ _) = fc
 219 |   getPTermLoc (PPostfixAppPartial fc _) = fc
 220 |   getPTermLoc (PUnifyLog fc _ _) = fc
 221 |   getPTermLoc (PWithUnambigNames fc _ _) = fc
 222 |
 223 |   public export
 224 |   PFieldUpdate : Type
 225 |   PFieldUpdate = PFieldUpdate' Name
 226 |
 227 |   public export
 228 |   data PFieldUpdate' : Type -> Type where
 229 |        PSetField : (path : List String) -> PTerm' nm -> PFieldUpdate' nm
 230 |        PSetFieldApp : (path : List String) -> PTerm' nm -> PFieldUpdate' nm
 231 |
 232 |   public export
 233 |   PDo : Type
 234 |   PDo = PDo' Name
 235 |
 236 |   public export
 237 |   data PDo' : Type -> Type where
 238 |        DoExp : FC -> PTerm' nm -> PDo' nm
 239 |        DoBind : FC -> (nameFC : FC) -> Name -> RigCount -> Maybe (PTerm' nm) -> PTerm' nm -> PDo' nm
 240 |        DoBindPat : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> List (PClause' nm) -> PDo' nm
 241 |        DoLet : FC -> (lhs : FC) -> Name -> RigCount -> PTerm' nm -> PTerm' nm -> PDo' nm
 242 |        DoLetPat : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
 243 |        DoLetLocal : FC -> List (PDecl' nm) -> PDo' nm
 244 |        DoRewrite : FC -> PTerm' nm -> PDo' nm
 245 |
 246 |   public export
 247 |   PStr : Type
 248 |   PStr = PStr' Name
 249 |
 250 |   public export
 251 |   data PStr' : Type -> Type where
 252 |        StrLiteral : FC -> String -> PStr' nm
 253 |        StrInterp : FC -> PTerm' nm -> PStr' nm
 254 |
 255 |   public export
 256 |   PlainMultiBinder : Type
 257 |   PlainMultiBinder = PlainMultiBinder' Name
 258 |
 259 |   ||| A plain binder without information about its use
 260 |   ||| plainBinder := name ':' term
 261 |   public export
 262 |   PlainMultiBinder' : (nm : Type) -> Type
 263 |   PlainMultiBinder' nm = List1 (WithName (PTerm' nm))
 264 |
 265 |   public export
 266 |   PlainBinder : Type
 267 |   PlainBinder = PlainBinder' Name
 268 |
 269 |   ||| A plain binder without information about its use
 270 |   ||| plainBinder := name ':' term
 271 |   public export
 272 |   PlainBinder' : (nm : Type) -> Type
 273 |   PlainBinder' nm  = WithName (PTerm' nm)
 274 |
 275 |   public export
 276 |   BasicMultiBinder : Type
 277 |   BasicMultiBinder = BasicMultiBinder' Name
 278 |
 279 |   ||| A binder with quantity information attached
 280 |   ||| basicBinder := qty plainBinder
 281 |   public export
 282 |   record BasicMultiBinder' (nm : Type) where
 283 |     constructor MkBasicMultiBinder
 284 |     rig : RigCount
 285 |     names : List1 (WithFC Name)
 286 |     type : PTerm' nm
 287 |
 288 |   public export
 289 |   PBinder : Type
 290 |   PBinder = PBinder' Name
 291 |
 292 |   ||| A binder with information about how it is binding
 293 |   ||| pbinder := '{' basicBinder '}'
 294 |   |||          | '{' auto basicBinder '}'
 295 |   |||          | '{' default term basicBinder '}'
 296 |   |||          | '(' basicBinder ')'
 297 |   public export
 298 |   record PBinder' (nm : Type) where
 299 |     constructor MkPBinder
 300 |     info : PiInfo (PTerm' nm)
 301 |     bind : BasicMultiBinder' nm
 302 |
 303 |   public export
 304 |   PBinderScope : Type
 305 |   PBinderScope = PBinderScope' Name
 306 |
 307 |   public export
 308 |   record PBinderScope' (nm : Type) where
 309 |     constructor MkPBinderScope
 310 |     binder : PBinder' nm
 311 |     scope : PTerm' nm
 312 |
 313 |   public export
 314 |   MkFullBinder : PiInfo (PTerm' nm) -> RigCount -> WithFC Name -> PTerm' nm -> PBinder' nm
 315 |   MkFullBinder info rig x y = MkPBinder info (MkBasicMultiBinder rig (singleton x) y)
 316 |
 317 |   export
 318 |   getLoc : PDo' nm -> FC
 319 |   getLoc (DoExp fc _) = fc
 320 |   getLoc (DoBind fc _ _ _ _ _) = fc
 321 |   getLoc (DoBindPat fc _ _ _ _) = fc
 322 |   getLoc (DoLet fc _ _ _ _ _) = fc
 323 |   getLoc (DoLetPat fc _ _ _ _) = fc
 324 |   getLoc (DoLetLocal fc _) = fc
 325 |   getLoc (DoRewrite fc _) = fc
 326 |
 327 |   export
 328 |   papply : FC -> PTerm' nm -> List (PTerm' nm) -> PTerm' nm
 329 |   papply fc f [] = f
 330 |   papply fc f (a :: as) = papply fc (PApp fc f a) as
 331 |
 332 |   export
 333 |   applyArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm
 334 |   applyArgs f [] = f
 335 |   applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args
 336 |
 337 |   export
 338 |   applyWithArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm
 339 |   applyWithArgs f [] = f
 340 |   applyWithArgs f ((fc, a) :: args) = applyWithArgs (PWithApp fc f a) args
 341 |
 342 |   public export
 343 |   PTypeDecl : Type
 344 |   PTypeDecl = PTypeDecl' Name
 345 |
 346 |   public export
 347 |   record PTypeDeclData' (nm : Type) where
 348 |       constructor MkPTy
 349 |       -- List of names and their associated documentation
 350 |       -- If no documentation is provided the first projection is `""`
 351 |       names : List1 (String, WithFC Name)
 352 |       doc: String
 353 |       type : PTerm' nm -- probably need `WithFC` here to fix #3408
 354 |
 355 |   public export
 356 |   PTypeDecl' : Type -> Type
 357 |   PTypeDecl' nm = WithFC (PTypeDeclData' nm)
 358 |
 359 |   export
 360 |   (.nameList) : PTypeDecl' nm -> List Name
 361 |   (.nameList) = forget . map (val . snd) . names . val
 362 |
 363 |   public export
 364 |   PDataDecl : Type
 365 |   PDataDecl = PDataDecl' Name
 366 |
 367 |   public export
 368 |   data PDataDecl' : Type -> Type where
 369 |        MkPData : FC -> (tyname : Name) ->
 370 |                  -- if we have already declared the type earlier using `MkPLater`,
 371 |                  -- we are allowed to leave the telescope out here
 372 |                  (tycon : Maybe (PTerm' nm)) ->
 373 |                  (opts : List DataOpt) ->
 374 |                  (datacons : List (PTypeDecl' nm)) -> PDataDecl' nm
 375 |        MkPLater : FC -> (tyname : Name) -> (tycon : PTerm' nm) -> PDataDecl' nm
 376 |
 377 |   public export
 378 |   data PRecordDecl' : Type -> Type where
 379 |        MkPRecord : (tyname : Name) ->
 380 |                    (params : List (PBinder' nm)) ->
 381 |                    (opts : List DataOpt) ->
 382 |                    (conName : Maybe (WithDoc $ AddFC Name)) ->
 383 |                    (decls : List (PField' nm)) ->
 384 |                    PRecordDecl' nm
 385 |        MkPRecordLater : (tyname : Name) ->
 386 |                         (params : List (PBinder' nm)) ->
 387 |                         PRecordDecl' nm
 388 |
 389 |   export
 390 |   getPDataDeclLoc : PDataDecl' nm -> FC
 391 |   getPDataDeclLoc (MkPData fc _ _ _ _) = fc
 392 |   getPDataDeclLoc (MkPLater fc _ _) = fc
 393 |
 394 |   public export
 395 |   PWithProblem : Type
 396 |   PWithProblem = PWithProblem' Name
 397 |
 398 |
 399 |   public export
 400 |   record PWithProblem' (nm : Type) where
 401 |     constructor MkPWithProblem
 402 |     withRigCount : RigCount
 403 |     withRigValue : PTerm' nm
 404 |     withRigProof : Maybe (RigCount, Name) -- This ought to be a `Basic` username
 405 |
 406 |   public export
 407 |   PClause : Type
 408 |   PClause = PClause' Name
 409 |
 410 |   public export
 411 |   data PClause' : Type -> Type where
 412 |        MkPatClause : FC -> (lhs : PTerm' nm) -> (rhs : PTerm' nm) ->
 413 |                      (whereblock : List (PDecl' nm)) -> PClause' nm
 414 |        MkWithClause : FC -> (lhs : PTerm' nm) -> List1 (PWithProblem' nm) ->
 415 |                       List WithFlag -> List (PClause' nm) -> PClause' nm
 416 |        MkImpossible : FC -> (lhs : PTerm' nm) -> PClause' nm
 417 |
 418 |   export
 419 |   getPClauseLoc : PClause -> FC
 420 |   getPClauseLoc (MkPatClause fc _ _ _) = fc
 421 |   getPClauseLoc (MkWithClause fc _ _ _ _) = fc
 422 |   getPClauseLoc (MkImpossible fc _) = fc
 423 |
 424 |   public export
 425 |   data Directive : Type where
 426 |        Hide : HidingDirective -> Directive
 427 |        Unhide : Name -> Directive
 428 |        Logging : Maybe LogLevel -> Directive
 429 |        LazyOn : Bool -> Directive
 430 |        UnboundImplicits : Bool -> Directive
 431 |        AmbigDepth : Nat -> Directive
 432 |        TotalityDepth: Nat -> Directive
 433 |        PairNames : Name -> Name -> Name -> Directive
 434 |        RewriteName : Name -> Name -> Directive
 435 |        PrimInteger : Name -> Directive
 436 |        PrimString : Name -> Directive
 437 |        PrimChar : Name -> Directive
 438 |        PrimDouble : Name -> Directive
 439 |        PrimTTImp : Name -> Directive
 440 |        PrimName : Name -> Directive
 441 |        PrimDecls : Name -> Directive
 442 |        CGAction : String -> String -> Directive
 443 |        Names : Name -> List String -> Directive
 444 |        StartExpr : PTerm' nm -> Directive
 445 |        Overloadable : Name -> Directive
 446 |        Extension : LangExt -> Directive
 447 |        DefaultTotality : TotalReq -> Directive
 448 |        PrefixRecordProjections : Bool -> Directive
 449 |        AutoImplicitDepth : Nat -> Directive
 450 |        NFMetavarThreshold : Nat -> Directive
 451 |        SearchTimeout : Integer -> Directive
 452 |        -- There is no nm on Directive
 453 |        ForeignImpl : Name -> List PTerm -> Directive
 454 |
 455 |   public export
 456 |   RecordField' : Type -> Type
 457 |   RecordField' nm = WithDoc $ WithRig $ WithNames $ PiBindData (PTerm' nm)
 458 |
 459 |   public export
 460 |   PField : Type
 461 |   PField = PField' Name
 462 |
 463 |   public export
 464 |   PField' : Type -> Type
 465 |   PField' nm = AddFC (RecordField' nm)
 466 |
 467 |   public export
 468 |   0 PRecordDeclLet : Type
 469 |   PRecordDeclLet = PRecordDeclLet' Name
 470 |
 471 |   public export
 472 |   data PRecordDeclLet' : Type -> Type where
 473 |     RecordClaim : WithFC (PClaimData' nm) -> PRecordDeclLet' nm
 474 |     RecordClause : WithFC (PClause' nm) -> PRecordDeclLet' nm
 475 |
 476 |   -- For noting the pass we're in when desugaring a mutual block
 477 |   -- TODO: Decide whether we want mutual blocks!
 478 |   public export
 479 |   data Pass = Single | AsType | AsDef
 480 |
 481 |   export
 482 |   Eq Pass where
 483 |     Single == Single = True
 484 |     AsType == AsType = True
 485 |     AsDef == AsDef = True
 486 |     _ == _ = False
 487 |
 488 |   export
 489 |   typePass : Pass -> Bool
 490 |   typePass p = p == Single || p == AsType
 491 |
 492 |   export
 493 |   defPass : Pass -> Bool
 494 |   defPass p = p == Single || p == AsDef
 495 |
 496 |   public export
 497 |   PFnOpt : Type
 498 |   PFnOpt = PFnOpt' Name
 499 |
 500 |   public export
 501 |   data PFnOpt' : Type -> Type where
 502 |        IFnOpt : FnOpt' nm -> PFnOpt' nm
 503 |        PForeign : List (PTerm' nm) -> PFnOpt' nm
 504 |        PForeignExport : List (PTerm' nm) -> PFnOpt' nm
 505 |
 506 |   public export
 507 |   PClaimData : Type
 508 |   PClaimData = PClaimData' Name
 509 |
 510 |   public export
 511 |   record PClaimData' (nm : Type) where
 512 |     constructor MkPClaim
 513 |     qty : RigCount
 514 |     vis : Visibility
 515 |     opts : List (PFnOpt' nm)
 516 |     type : PTypeDecl' nm
 517 |
 518 |   public export
 519 |   record PFixityData where
 520 |     constructor MkPFixityData
 521 |     exportModifier : WithDefault Visibility Export
 522 |     binding : BindingModifier
 523 |     fixity : Fixity
 524 |     precedence : Nat
 525 |     operators : List1 OpStr
 526 |
 527 |   public export
 528 |   PDecl : Type
 529 |   PDecl = PDecl' Name
 530 |
 531 |   public export
 532 |   data PDeclNoFC' : Type -> Type where
 533 |        PClaim : PClaimData' nm -> PDeclNoFC' nm
 534 |        PDef : List (PClause' nm) -> PDeclNoFC' nm
 535 |        PData : (doc : String) -> WithDefault Visibility Private ->
 536 |                Maybe TotalReq -> PDataDecl' nm -> PDeclNoFC' nm
 537 |        PParameters : Either (List1 (PlainBinder' nm))
 538 |                             (List1 (PBinder' nm)) ->
 539 |                      List (PDecl' nm) -> PDeclNoFC' nm
 540 |        PUsing : List (Maybe Name, PTerm' nm) ->
 541 |                 List (PDecl' nm) -> PDeclNoFC' nm
 542 |        PInterface : WithDefault Visibility Private ->
 543 |                     (constraints : List (Maybe Name, PTerm' nm)) ->
 544 |                     Name ->
 545 |                     (doc : String) ->
 546 |                     (params : List (BasicMultiBinder' nm)) ->
 547 |                     (det : Maybe (List1 Name)) ->
 548 |                     (conName : Maybe (WithDoc $ AddFC Name)) ->
 549 |                     List (PDecl' nm) ->
 550 |                     PDeclNoFC' nm
 551 |        PImplementation : Visibility -> List PFnOpt -> Pass ->
 552 |                          (implicits : List (AddFC (ImpParameter' (PTerm' nm)))) ->
 553 |                          (constraints : List (Maybe Name, PTerm' nm)) ->
 554 |                          Name ->
 555 |                          (params : List (PTerm' nm)) ->
 556 |                          (implName : Maybe Name) ->
 557 |                          (nusing : List Name) ->
 558 |                          Maybe (List (PDecl' nm)) ->
 559 |                          PDeclNoFC' nm
 560 |        PRecord : (doc : String) ->
 561 |                  WithDefault Visibility Private ->
 562 |                  Maybe TotalReq ->
 563 |                  PRecordDecl' nm ->
 564 |                  PDeclNoFC' nm
 565 |
 566 |        -- TODO: PPostulate
 567 |        -- TODO: POpen (for opening named interfaces)
 568 |        ||| PFail is a failing block. The string must appear as a
 569 |        ||| substring of the error message raised when checking the block.
 570 |        PFail : Maybe String -> List (PDecl' nm) -> PDeclNoFC' nm
 571 |
 572 |        PMutual : List (PDecl' nm) -> PDeclNoFC' nm
 573 |        PFixity : PFixityData -> PDeclNoFC' nm
 574 |        PNamespace : Namespace -> List (PDecl' nm) -> PDeclNoFC' nm
 575 |        PTransform : String -> PTerm' nm -> PTerm' nm -> PDeclNoFC' nm
 576 |        PRunElabDecl : PTerm' nm -> PDeclNoFC' nm
 577 |        PDirective : Directive -> PDeclNoFC' nm
 578 |        PBuiltin : BuiltinType -> Name -> PDeclNoFC' nm
 579 |
 580 |   public export
 581 |   PDeclNoFC : Type
 582 |   PDeclNoFC = PDeclNoFC' Name
 583 |
 584 |   public export
 585 |   PDecl' : Type -> Type
 586 |   PDecl' x = WithFC (PDeclNoFC' x)
 587 |
 588 |   export
 589 |   getPDeclLoc : PDecl' nm -> FC
 590 |   getPDeclLoc x = x.fc
 591 |
 592 | export
 593 | isStrInterp : PStr -> Maybe FC
 594 | isStrInterp (StrInterp fc _) = Just fc
 595 | isStrInterp (StrLiteral {}) = Nothing
 596 |
 597 | export
 598 | isStrLiteral : PStr -> Maybe (FC, String)
 599 | isStrLiteral (StrInterp {}) = Nothing
 600 | isStrLiteral (StrLiteral fc str) = Just (fc, str)
 601 |
 602 | export
 603 | isPDef : PDecl -> Maybe (WithFC (List PClause))
 604 | isPDef (MkWithData fc (PDef cs)) = Just (MkWithData fc cs)
 605 | isPDef _ = Nothing
 606 |
 607 |
 608 | definedInData : PDataDecl -> List Name
 609 | definedInData (MkPData _ n _ _ cons) = n :: concatMap (.nameList) cons
 610 | definedInData (MkPLater _ n _) = [n]
 611 |
 612 | export
 613 | definedIn : List PDeclNoFC -> List Name
 614 | definedIn [] = []
 615 | definedIn (PClaim claim :: ds) = claim.type.nameList ++ definedIn ds
 616 | definedIn (PData _ _ _ d :: ds) = definedInData d ++ definedIn ds
 617 | definedIn (PParameters _ pds :: ds) = definedIn (map val pds) ++ definedIn ds
 618 | definedIn (PUsing _ pds :: ds) = definedIn (map val pds) ++ definedIn ds
 619 | definedIn (PNamespace _ ns :: ds) = definedIn (map val ns) ++ definedIn ds
 620 | definedIn (_ :: ds) = definedIn ds
 621 |
 622 | public export
 623 | data REPLEval : Type where
 624 |      EvalTC : REPLEval -- Evaluate as if part of the typechecker
 625 |      NormaliseAll : REPLEval -- Normalise everything (default)
 626 |      Execute : REPLEval -- Evaluate then pass to an executer
 627 |      Scheme : REPLEval -- Use the scheme evaluator
 628 |
 629 | export
 630 | Show REPLEval where
 631 |   show EvalTC = "typecheck"
 632 |   show NormaliseAll = "normalise"
 633 |   show Execute = "execute"
 634 |   show Scheme = "scheme"
 635 |
 636 | export
 637 | Pretty Void REPLEval where
 638 |   pretty EvalTC = pretty "typecheck"
 639 |   pretty NormaliseAll = pretty "normalise"
 640 |   pretty Execute = pretty "execute"
 641 |   pretty Scheme = pretty "scheme"
 642 |
 643 | public export
 644 | data REPLOpt : Type where
 645 |      ShowImplicits : Bool -> REPLOpt
 646 |      ShowNamespace : Bool -> REPLOpt
 647 |      ShowMachineNames : Bool -> REPLOpt
 648 |      ShowTypes : Bool -> REPLOpt
 649 |      EvalMode : REPLEval -> REPLOpt
 650 |      Editor : String -> REPLOpt
 651 |      CG : String -> REPLOpt
 652 |      Profile : Bool -> REPLOpt
 653 |      EvalTiming : Bool -> REPLOpt
 654 |
 655 | export
 656 | Show REPLOpt where
 657 |   show (ShowImplicits impl) = "showimplicits = " ++ show impl
 658 |   show (ShowNamespace ns) = "shownamespace = " ++ show ns
 659 |   show (ShowMachineNames mn) = "showmachinenames = " ++ show mn
 660 |   show (ShowTypes typs) = "showtypes = " ++ show typs
 661 |   show (EvalMode mod) = "eval = " ++ show mod
 662 |   show (Editor editor) = "editor = " ++ show editor
 663 |   show (CG str) = "cg = " ++ str
 664 |   show (Profile p) = "profile = " ++ show p
 665 |   show (EvalTiming p) = "evaltiming = " ++ show p
 666 |
 667 | export
 668 | Pretty Void REPLOpt where
 669 |   pretty (ShowImplicits impl) = "showimplicits" <++> equals <++> pretty (show impl)
 670 |   pretty (ShowNamespace ns) = "shownamespace" <++> equals <++> pretty (show ns)
 671 |   pretty (ShowMachineNames mn) = "showmachinenames" <++> equals <++> pretty (show mn)
 672 |   pretty (ShowTypes typs) = "showtypes" <++> equals <++> pretty (show typs)
 673 |   pretty (EvalMode mod) = "eval" <++> equals <++> pretty mod
 674 |   pretty (Editor editor) = "editor" <++> equals <++> pretty editor
 675 |   pretty (CG str) = "cg" <++> equals <++> pretty str
 676 |   pretty (Profile p) = "profile" <++> equals <++> pretty (show p)
 677 |   pretty (EvalTiming p) = "evaltiming" <++> equals <++> pretty (show p)
 678 |
 679 | public export
 680 | data EditCmd : Type where
 681 |      TypeAt : Int -> Int -> Name -> EditCmd
 682 |      CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
 683 |      AddClause : Bool -> Int -> Name -> EditCmd
 684 |      Refine : Bool -> Int -> (hole : Name) -> (expr : PTerm) -> EditCmd
 685 |      Intro : Bool -> Int -> (hole : Name) -> EditCmd
 686 |      ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
 687 |      ExprSearchNext : EditCmd
 688 |      GenerateDef : Bool -> Int -> Name -> Nat -> EditCmd
 689 |      GenerateDefNext : EditCmd
 690 |      MakeLemma : Bool -> Int -> Name -> EditCmd
 691 |      MakeCase : Bool -> Int -> Name -> EditCmd
 692 |      MakeWith : Bool -> Int -> Name -> EditCmd
 693 |
 694 | public export
 695 | data BracketType
 696 |   = IdiomBrackets
 697 |   | NameQuote
 698 |   | TermQuote
 699 |   | DeclQuote
 700 |
 701 | public export
 702 | data DocDirective : Type where
 703 |   ||| A reserved keyword
 704 |   Keyword : String -> DocDirective
 705 |   ||| A reserved symbol
 706 |   Symbol  : String -> DocDirective
 707 |   ||| A type of brackets
 708 |   Bracket : BracketType -> DocDirective
 709 |   ||| An arbitrary PTerm
 710 |   APTerm  : PTerm -> DocDirective
 711 |   ||| A module name
 712 |   AModule : ModuleIdent -> DocDirective
 713 |
 714 | public export
 715 | data HelpType : Type where
 716 |   GenericHelp : HelpType
 717 |   DetailedHelp : (details : String) -> HelpType
 718 |
 719 | public export
 720 | data REPLCmd : Type where
 721 |      NewDefn : List PDecl -> REPLCmd
 722 |      Eval : PTerm -> REPLCmd
 723 |      Check : PTerm -> REPLCmd
 724 |      CheckWithImplicits : PTerm -> REPLCmd
 725 |      PrintDef : PTerm -> REPLCmd
 726 |      Reload : REPLCmd
 727 |      Load : String -> REPLCmd
 728 |      ImportMod : ModuleIdent -> REPLCmd
 729 |      Edit : REPLCmd
 730 |      Compile : PTerm -> String -> REPLCmd
 731 |      Exec : PTerm -> REPLCmd
 732 |      Help : HelpType -> REPLCmd
 733 |      TypeSearch : PTerm -> REPLCmd
 734 |      FuzzyTypeSearch : PTerm -> REPLCmd
 735 |      DebugInfo : Name -> REPLCmd
 736 |      SetOpt : REPLOpt -> REPLCmd
 737 |      GetOpts : REPLCmd
 738 |      CGDirective : String -> REPLCmd
 739 |      CD : String -> REPLCmd
 740 |      CWD: REPLCmd
 741 |      Missing : Name -> REPLCmd
 742 |      Total : Name -> REPLCmd
 743 |      Doc : DocDirective -> REPLCmd
 744 |      Browse : Namespace -> REPLCmd
 745 |      SetLog : Maybe LogLevel -> REPLCmd
 746 |      SetConsoleWidth : Maybe Nat -> REPLCmd
 747 |      SetColor : Bool -> REPLCmd
 748 |      Metavars : REPLCmd
 749 |      Editing : EditCmd -> REPLCmd
 750 |      RunShellCommand : String -> REPLCmd
 751 |      ShowVersion : REPLCmd
 752 |      Quit : REPLCmd
 753 |      NOP : REPLCmd
 754 |      ImportPackage : String -> REPLCmd
 755 |
 756 | public export
 757 | record Import where
 758 |   constructor MkImport
 759 |   loc : FC
 760 |   reexport : Bool
 761 |   path : ModuleIdent
 762 |   nameAs : Namespace
 763 |
 764 | export
 765 | Show Import where
 766 |   show (MkImport loc reexport path nameAs)
 767 |     = unwords $ catMaybes
 768 |       [ Just "import"
 769 |       , "public" <$ guard reexport
 770 |       , Just (show path)
 771 |       , ("as " ++ show nameAs) <$ guard (miAsNamespace path /= nameAs)
 772 |       ]
 773 |
 774 | public export
 775 | record Module where
 776 |   constructor MkModule
 777 |   headerLoc : FC
 778 |   moduleNS : ModuleIdent
 779 |   imports : List Import
 780 |   documentation : String
 781 |   decls : List PDecl
 782 |
 783 | parameters {0 nm : Type} (toName : nm -> Name)
 784 |
 785 |   showAlt : PClause' nm -> String
 786 |   showDo : PDo' nm -> String
 787 |   showPStr : PStr' nm -> String
 788 |   showUpdate : PFieldUpdate' nm -> String
 789 |   showPTermPrec : Prec -> PTerm' nm -> String
 790 |   showOpPrec : Prec -> OpStr' nm -> String
 791 |   showPBinder : Prec -> PBinder' nm -> String
 792 |   showBasicMultiBinder : BasicMultiBinder' nm -> String
 793 |
 794 |   showPTerm : PTerm' nm -> String
 795 |   showPTerm = showPTermPrec Open
 796 |
 797 |   showAlt (MkPatClause _ lhs rhs _) =
 798 |     " | " ++ showPTerm lhs ++ " => " ++ showPTerm rhs ++ ";"
 799 |   showAlt (MkWithClause _ lhs wps flags cs) = " | <<with alts not possible>>;"
 800 |   showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;"
 801 |
 802 |   showDo (DoExp _ tm) = showPTerm tm
 803 |   showDo (DoBind _ _ n rig (Just ty) tm) = showCount rig ++ show n ++ " : " ++ showPTerm ty ++ " <- " ++ showPTerm tm
 804 |   showDo (DoBind _ _ n rig _ tm) = showCount rig ++ show n ++ " <- " ++ showPTerm tm
 805 |   showDo (DoBindPat _ l (Just ty) tm alts)
 806 |       = showPTerm l ++ " : " ++ showPTerm ty ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts
 807 |   showDo (DoBindPat _ l _ tm alts)
 808 |       = showPTerm l ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts
 809 |   showDo (DoLet _ _ l rig _ tm) = "let " ++ show l ++ " = " ++ showPTerm tm
 810 |   showDo (DoLetPat _ l _ tm alts)
 811 |       = "let " ++ showPTerm l ++ " = " ++ showPTerm tm ++ concatMap showAlt alts
 812 |   showDo (DoLetLocal _ ds)
 813 |       -- We'll never see this when displaying a normal form...
 814 |       = "let { << definitions >>  }"
 815 |   showDo (DoRewrite _ rule)
 816 |       = "rewrite " ++ showPTerm rule
 817 |
 818 |   showPStr (StrLiteral _ str) = show str
 819 |   showPStr (StrInterp _ tm) = showPTerm tm
 820 |
 821 |   showUpdate (PSetField p v) = showSep "." p ++ " = " ++ showPTerm v
 822 |   showUpdate (PSetFieldApp p v) = showSep "." p ++ " $= " ++ showPTerm v
 823 |
 824 |   showBasicMultiBinder (MkBasicMultiBinder rig names type)
 825 |         = "\{showCount rig} \{showNames}: \{showPTerm type}"
 826 |         where
 827 |           showNames : String
 828 |           showNames = concat $ intersperse ", " $ map (show . val) (forget names)
 829 |
 830 |   showPBinder d (MkPBinder Implicit bind) = "{\{showBasicMultiBinder bind}}"
 831 |   showPBinder d (MkPBinder Explicit bind) = "(\{showBasicMultiBinder bind})"
 832 |   showPBinder d (MkPBinder AutoImplicit bind) = "{auto \{showBasicMultiBinder bind}}"
 833 |   showPBinder d (MkPBinder (DefImplicit x) bind) = "{default \{showPTerm x} \{ showBasicMultiBinder bind}}"
 834 |
 835 |   showPTermPrec d (PRef _ n) = showPrec d (toName n)
 836 |   showPTermPrec d (Forall (MkWithData _ (names, scope)))
 837 |         = "forall " ++ concat (intersperse ", " (map (show . val) (forget names))) ++ " . " ++ showPTermPrec d scope
 838 |   showPTermPrec d (NewPi (MkWithData _ (MkPBinderScope binder scope)))
 839 |         = showPBinder d binder ++ " -> "  ++ showPTermPrec d scope
 840 |   showPTermPrec d (PPi _ rig Explicit Nothing arg ret)
 841 |         = showPTermPrec d arg ++ " -> " ++ showPTermPrec d ret
 842 |   showPTermPrec d (PPi _ rig Explicit (Just n) arg ret)
 843 |         = "(" ++ showCount rig ++ showPrec d n
 844 |          ++ " : " ++ showPTermPrec d arg ++ ") -> "
 845 |          ++ showPTermPrec d ret
 846 |   showPTermPrec d (PPi _ rig Implicit Nothing arg ret) -- shouldn't happen
 847 |         = "{" ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> "
 848 |           ++ showPTermPrec d ret
 849 |   showPTermPrec d (PPi _ rig Implicit (Just n) arg ret)
 850 |         = "{" ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
 851 |   showPTermPrec d (PPi _ top AutoImplicit Nothing arg ret)
 852 |         = showPTermPrec d arg ++ " => " ++ showPTermPrec d ret
 853 |   showPTermPrec d (PPi _ rig AutoImplicit (Just n) arg ret)
 854 |         = "{auto " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
 855 |   showPTermPrec d (PPi _ rig (DefImplicit t) Nothing arg ret) -- shouldn't happen
 856 |         = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
 857 |   showPTermPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret)
 858 |         = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
 859 |   showPTermPrec d (PLam _ rig _ n (PImplicit _) sc)
 860 |         = "\\" ++ showCount rig ++ showPTermPrec d n ++ " => " ++ showPTermPrec d sc
 861 |   showPTermPrec d (PLam _ rig _ n ty sc)
 862 |         = "\\" ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " => " ++ showPTermPrec d sc
 863 |   showPTermPrec d (PLet _ rig n (PImplicit _) val sc alts)
 864 |         = "let " ++ showCount rig ++ showPTermPrec d n ++ " = " ++ showPTermPrec d val ++ " in " ++ showPTermPrec d sc
 865 |   showPTermPrec d (PLet _ rig n ty val sc alts)
 866 |         = "let " ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " = "
 867 |                  ++ showPTermPrec d val ++ concatMap showAlt alts ++
 868 |                  " in " ++ showPTermPrec d sc
 869 |   showPTermPrec _ (PCase _ _ tm cs)
 870 |         = "case " ++ showPTerm tm ++ " of { " ++
 871 |             showSep " ; " (map showCase cs) ++ " }"
 872 |       where
 873 |         showCase : PClause' nm -> String
 874 |         showCase (MkPatClause _ lhs rhs _) = showPTerm lhs ++ " => " ++ showPTerm rhs
 875 |         showCase (MkWithClause _ lhs _ flags _) = " | <<with alts not possible>>"
 876 |         showCase (MkImpossible _ lhs) = showPTerm lhs ++ " impossible"
 877 |   showPTermPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form...
 878 |         = "let { << definitions >>  } in " ++ showPTermPrec d sc
 879 |   showPTermPrec d (PUpdate _ fs)
 880 |         = "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
 881 |   showPTermPrec d (PApp _ f a) =
 882 |       let catchall : Lazy String := showPTermPrec App f ++ " " ++ showPTermPrec App a in
 883 |       case f of
 884 |         PRef _ n =>
 885 |           if isJust (isRF (toName n))
 886 |           then showPTermPrec App a ++ " " ++ showPTermPrec App f
 887 |           else catchall
 888 |         _ => catchall
 889 |   showPTermPrec d (PWithApp _ f a) = showPTermPrec d f ++ " | " ++ showPTermPrec d a
 890 |   showPTermPrec d (PAutoApp _ f a)
 891 |         = showPTermPrec d f ++ " @{" ++ showPTermPrec d a ++ "}"
 892 |   showPTermPrec d (PDelayed _ LInf ty)
 893 |         = showParens (d >= App) $ "Inf " ++ showPTermPrec App ty
 894 |   showPTermPrec d (PDelayed _ _ ty)
 895 |         = showParens (d >= App) $ "Lazy " ++ showPTermPrec App ty
 896 |   showPTermPrec d (PDelay _ tm)
 897 |         = showParens (d >= App) $ "Delay " ++ showPTermPrec App tm
 898 |   showPTermPrec d (PForce _ tm)
 899 |         = showParens (d >= App) $ "Force " ++ showPTermPrec App tm
 900 |   showPTermPrec d (PNamedApp _ f n (PRef _ a))
 901 |         = if n == (toName a)
 902 |              then showPTermPrec d f ++ " {" ++ showPrec d n ++ "}"
 903 |              else showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d (toName a) ++ "}"
 904 |   showPTermPrec d (PNamedApp _ f n a)
 905 |         = showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPTermPrec d a ++ "}"
 906 |   showPTermPrec _ (PSearch {}) = "%search"
 907 |   showPTermPrec d (PQuote _ tm) = "`(" ++ showPTermPrec d tm ++ ")"
 908 |   showPTermPrec d (PQuoteName _ n) = "`{" ++ showPrec d n ++ "}"
 909 |   showPTermPrec d (PQuoteDecl _ tm) = "`[ <<declaration>> ]"
 910 |   showPTermPrec d (PUnquote _ tm) = "~(" ++ showPTermPrec d tm ++ ")"
 911 |   showPTermPrec d (PRunElab _ tm) = "%runElab " ++ showPTermPrec d tm
 912 |   showPTermPrec d (PPrimVal _ c) = showPrec d c
 913 |   showPTermPrec _ (PHole _ _ n) = "?" ++ n
 914 |   showPTermPrec _ (PType _) = "Type"
 915 |   showPTermPrec d (PAs _ _ n p) = showPrec d n ++ "@" ++ showPTermPrec d p
 916 |   showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p
 917 |   showPTermPrec _ (PImplicit _) = "_"
 918 |   showPTermPrec _ (PInfer _) = "?"
 919 |   showPTermPrec d (POp _ (MkWithData _ $ NoBinder left) op right)
 920 |         = showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right
 921 |   showPTermPrec d (POp _ (MkWithData _ $ BindType nm left) op right)
 922 |         = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")"
 923 |   showPTermPrec d (POp _ (MkWithData _ $ BindExpr nm left) op right)
 924 |         = "(" ++ showPTermPrec d nm ++ " := " ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")"
 925 |   showPTermPrec d (POp _ (MkWithData _ $ BindExplicitType nm ty left) op right)
 926 |         = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d ty ++ ":=" ++ showPTermPrec d left ++ " " ++ showOpPrec d op.val ++ " " ++ showPTermPrec d right ++ ")"
 927 |   showPTermPrec d (PPrefixOp _ op x) = showOpPrec d op.val ++ showPTermPrec d x
 928 |   showPTermPrec d (PSectionL _ op x) = "(" ++ showOpPrec d op.val ++ " " ++ showPTermPrec d x ++ ")"
 929 |   showPTermPrec d (PSectionR _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op.val ++ ")"
 930 |   showPTermPrec d (PEq fc l r) = showPTermPrec d l ++ " = " ++ showPTermPrec d r
 931 |   showPTermPrec d (PBracketed _ tm) = "(" ++ showPTermPrec d tm ++ ")"
 932 |   showPTermPrec d (PString _ _ xs) = join " ++ " $ showPStr <$> xs
 933 |   showPTermPrec d (PMultiline _ _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")"
 934 |   showPTermPrec d (PDoBlock _ ns ds)
 935 |         = "do " ++ showSep " ; " (map showDo ds)
 936 |   showPTermPrec d (PBang _ tm) = "!" ++ showPTermPrec d tm
 937 |   showPTermPrec d (PIdiom _ Nothing tm) = "[|" ++ showPTermPrec d tm ++ "|]"
 938 |   showPTermPrec d (PIdiom _ (Just ns) tm) = show ns ++ ".[|" ++ showPTermPrec d tm ++ "|]"
 939 |   showPTermPrec d (PList _ _ xs)
 940 |         = "[" ++ showSep ", " (map (showPTermPrec d . snd) xs) ++ "]"
 941 |   showPTermPrec d (PSnocList _ _ xs)
 942 |         = "[<" ++ showSep ", " (map (showPTermPrec d . snd) (xs <>> [])) ++ "]"
 943 |   showPTermPrec d (PPair _ l r) = "(" ++ showPTermPrec d l ++ ", " ++ showPTermPrec d r ++ ")"
 944 |   showPTermPrec d (PDPair _ _ l (PImplicit _) r) = "(" ++ showPTermPrec d l ++ " ** " ++ showPTermPrec d r ++ ")"
 945 |   showPTermPrec d (PDPair _ _ l ty r) = "(" ++ showPTermPrec d l ++ " : " ++ showPTermPrec d ty ++
 946 |                                  " ** " ++ showPTermPrec d r ++ ")"
 947 |   showPTermPrec _ (PUnit _) = "()"
 948 |   showPTermPrec d (PIfThenElse _ x t e) = "if " ++ showPTermPrec d x ++ " then " ++ showPTermPrec d t ++
 949 |                                  " else " ++ showPTermPrec d e
 950 |   showPTermPrec d (PComprehension _ ret es)
 951 |         = "[" ++ showPTermPrec d (dePure ret) ++ " | " ++
 952 |                  showSep ", " (map (showDo . deGuard) es) ++ "]"
 953 |       where
 954 |         dePure : PTerm' nm -> PTerm' nm
 955 |         dePure tm@(PApp _ (PRef _ n) arg)
 956 |             = if dropNS (toName n) == UN (Basic "pure") then arg else tm
 957 |         dePure tm = tm
 958 |
 959 |         deGuard : PDo' nm -> PDo' nm
 960 |         deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg))
 961 |             = if dropNS (toName n) == UN (Basic "guard") then DoExp fc arg else tm
 962 |         deGuard tm = tm
 963 |   showPTermPrec d (PRewrite _ rule tm)
 964 |         = "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm
 965 |   showPTermPrec d (PRange _ start Nothing end)
 966 |         = "[" ++ showPTermPrec d start ++ " .. " ++ showPTermPrec d end ++ "]"
 967 |   showPTermPrec d (PRange _ start (Just next) end)
 968 |         = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. " ++ showPTermPrec d end ++ "]"
 969 |   showPTermPrec d (PRangeStream _ start Nothing)
 970 |         = "[" ++ showPTermPrec d start ++ " .. ]"
 971 |   showPTermPrec d (PRangeStream _ start (Just next))
 972 |         = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. ]"
 973 |   showPTermPrec d (PUnifyLog _ _ tm) = showPTermPrec d tm
 974 |   showPTermPrec d (PPostfixApp fc rec fields)
 975 |         = showPTermPrec d rec ++ concatMap (\n => "." ++ show n) fields
 976 |   showPTermPrec d (PPostfixAppPartial fc fields)
 977 |         = concatMap (\n => "." ++ show n) fields
 978 |   showPTermPrec d (PWithUnambigNames fc ns rhs)
 979 |         = "with " ++ show ns ++ " " ++ showPTermPrec d rhs
 980 |
 981 |   showOpPrec d (OpSymbols op) = showPrec d (toName op)
 982 |   showOpPrec d (Backticked op) = "`\{showPrec d (toName op)}`"
 983 |
 984 | export
 985 | covering
 986 | Show PTerm where
 987 |   showPrec = showPTermPrec id
 988 |
 989 | export
 990 | covering
 991 | Show IPTerm where
 992 |   showPrec = showPTermPrec rawName
 993 |
 994 | public export 0
 995 | Method : Type
 996 | Method = WithName $ WithRig $ AddMetadata Tot' $ RawImp
 997 |
 998 | public export
 999 | record IFaceInfo where
1000 |   constructor MkIFaceInfo
1001 |   iconstructor : Name
1002 |   implParams : List Name
1003 |   params : List Name
1004 |   parents : List RawImp
1005 |   methods : List Method
1006 |      -- ^ name, whether a data method, and desugared type (without constraint)
1007 |   defaults : List (Name, List ImpClause)
1008 |
1009 | -- If you update this, update 'extendSyn' in Desugar to keep it up to date
1010 | -- when reading imports
1011 | public export
1012 | record SyntaxInfo where
1013 |   constructor MkSyntax
1014 |   ||| Operators fixities as a map from their names to their fixity,
1015 |   ||| precedence, and the file context where that fixity was defined.
1016 |   fixities : ANameMap FixityInfo
1017 |   -- info about modules
1018 |   saveMod : List ModuleIdent -- current module name
1019 |   modDocstrings : SortedMap ModuleIdent String
1020 |   modDocexports : SortedMap ModuleIdent (List Import) -- keeping the imports that happen to be reexports
1021 |   -- info about interfaces
1022 |   saveIFaces : List Name -- interfaces defined in current session, to save
1023 |                          -- to ttc
1024 |   ifaces : ANameMap IFaceInfo
1025 |   -- info about definitions
1026 |   saveDocstrings : NameMap () -- names defined in current session
1027 |   defDocstrings : ANameMap String
1028 |   bracketholes : List Name -- hole names in argument position (so need
1029 |                            -- to be bracketed when solved)
1030 |                            -- TODO: use Set instead List
1031 |   usingImpl : List (Maybe Name, RawImp)
1032 |   startExpr : RawImp
1033 |   holeNames : List String -- hole names in the file
1034 |
1035 | export
1036 | prefixes : SyntaxInfo -> ANameMap (FC, Nat)
1037 | prefixes = fromList
1038 |     . map (\(name, fx)=> (name, fx.fc, fx.precedence))
1039 |     . filter ((== Prefix) . fix . snd)
1040 |     . toList
1041 |     . fixities
1042 |
1043 | export
1044 | infixes : SyntaxInfo -> ANameMap (FC, Fixity, Nat)
1045 | infixes = fromList
1046 |     . map (\(nm, fx) => (nm, fx.fc, fx.fix, fx.precedence))
1047 |     . filter ((/= Prefix) . fix . snd)
1048 |     . toList
1049 |     . fixities
1050 |
1051 | HasNames IFaceInfo where
1052 |   full gam iface
1053 |       = do -- coreLift $ printLn (iconstructor iface)
1054 |            -- coreLift $ printLn (methods iface)
1055 |            pure iface
1056 |
1057 |   resolved gam iface = pure iface
1058 |
1059 | HasNames a => HasNames (ANameMap a) where
1060 |   full gam nmap
1061 |       = insertAll empty (toList nmap)
1062 |     where
1063 |       insertAll : ANameMap a -> List (Name, a) -> Core (ANameMap a)
1064 |       insertAll ms [] = pure ms
1065 |       insertAll ms ((k, v) :: ns)
1066 |           = insertAll (addName !(full gam k) !(full gam v) ms) ns
1067 |
1068 |   resolved gam nmap
1069 |       = insertAll empty (toList nmap)
1070 |     where
1071 |       insertAll : ANameMap a -> List (Name, a) -> Core (ANameMap a)
1072 |       insertAll ms [] = pure ms
1073 |       insertAll ms ((k, v) :: ns)
1074 |           = insertAll (addName !(resolved gam k) !(resolved gam v) ms) ns
1075 |
1076 | export
1077 | HasNames SyntaxInfo where
1078 |   full gam syn
1079 |       = pure $ { ifaces := !(full gam (ifaces syn))
1080 |                , bracketholes := !(traverse (full gam) (bracketholes syn))
1081 |                } syn
1082 |   resolved gam syn
1083 |       = pure $ { ifaces := !(resolved gam (ifaces syn))
1084 |                , bracketholes := !(traverse (resolved gam) (bracketholes syn))
1085 |                } syn
1086 |
1087 | export
1088 | initSyntax : SyntaxInfo
1089 | initSyntax
1090 |     = MkSyntax initFixities
1091 |                []
1092 |                empty
1093 |                empty
1094 |                []
1095 |                empty
1096 |                initSaveDocStrings
1097 |                initDocStrings
1098 |                []
1099 |                []
1100 |                (IVar EmptyFC (UN $ Basic "main"))
1101 |                []
1102 |
1103 |   where
1104 |
1105 |
1106 |     initFixities : ANameMap FixityInfo
1107 |     initFixities = fromList
1108 |       [ (UN $ Basic "-", MkFixityInfo EmptyFC Export NotBinding Prefix 10)
1109 |       , (UN $ Basic "negate", MkFixityInfo EmptyFC Export NotBinding Prefix 10) -- for documentation purposes
1110 |       , (UN $ Basic "=", MkFixityInfo EmptyFC Export NotBinding Infix 0)
1111 |       ]
1112 |
1113 |     initDocStrings : ANameMap String
1114 |     initDocStrings = empty
1115 |
1116 |     initSaveDocStrings : NameMap ()
1117 |     initSaveDocStrings = empty
1118 |
1119 | -- A label for Syntax info in the global state
1120 | export
1121 | data Syn : Type where
1122 |
1123 | export
1124 | withSyn : {auto s : Ref Syn SyntaxInfo} -> Core a -> Core a
1125 | withSyn = wrapRef Syn (\_ => pure ())
1126 |
1127 | -- Add a list of reexports for a module name
1128 | export
1129 | addModDocInfo : {auto s : Ref Syn SyntaxInfo} ->
1130 |                 ModuleIdent -> String -> List Import ->
1131 |                 Core ()
1132 | addModDocInfo mi doc reexpts
1133 |     = update Syn { saveMod $= (mi ::)
1134 |                  , modDocexports $= insert mi reexpts
1135 |                  , modDocstrings $= insert mi doc }
1136 |
1137 | ||| Remove a fixity from the context
1138 | export
1139 | removeFixity :
1140 |   {auto s : Ref Syn SyntaxInfo} -> FC -> Fixity -> Name -> Core ()
1141 | removeFixity loc _ key = do
1142 |   fixityInfo <- fixities <$> get Syn
1143 |   if isJust $ lookupExact key fixityInfo
1144 |      then -- When the fixity is found, simply remove it
1145 |        update Syn ({ fixities $= removeExact key })
1146 |      else -- When the fixity is not found, find close matches
1147 |        let fixityNames : List Name = map fst (toList fixityInfo)
1148 |            closeNames = !(filterM (coreLift . closeMatch key) fixityNames)
1149 |            sameName : List Name = fst <$> lookupName (dropAllNS key) fixityInfo
1150 |            similarNamespaces = nub (closeNames ++ sameName)
1151 |        in if null similarNamespaces
1152 |              then
1153 |                throw $ GenericMsg loc "Fixity \{show key} not found"
1154 |              else
1155 |                throw $ GenericMsgSol loc "Fixity \{show key} not found" "Did you mean"
1156 |                  $ map printFixityHide similarNamespaces
1157 |   where
1158 |     printFixityHide : Name -> String
1159 |     printFixityHide nm = "%hide \{show nm}"
1160 |
1161 | ||| Return all fixity declarations for an operator name
1162 | export
1163 | getFixityInfo : {auto s : Ref Syn SyntaxInfo} -> String -> Core (List (Name, FixityInfo))
1164 | getFixityInfo nm = do
1165 |   syn <- get Syn
1166 |   pure $ lookupName (UN $ Basic nm) (fixities syn)
1167 |
1168 | export
1169 | covering
1170 | Show PTypeDecl where
1171 |   show pty = unwords [show pty.nameList, ":", show pty.val.type]
1172 |
1173 | export
1174 | covering
1175 | Show PClause where
1176 |   show (MkPatClause _ lhs rhs []) = unwords [ show lhs, "=", show rhs ]
1177 |   show (MkPatClause {}) = "MkPatClause"
1178 |   show (MkWithClause {}) = "MkWithClause"
1179 |   show (MkImpossible _ lhs) = unwords [ show lhs, "impossible" ]
1180 |
1181 | export
1182 | covering
1183 | Show PClaimData where
1184 |   show (MkPClaim rig _ _ sig) = showCount rig ++ show sig
1185 |
1186 | -- TODO: finish writing this instance
1187 | export
1188 | covering
1189 | Show PDeclNoFC where
1190 |   show (PClaim pclaim) = show pclaim
1191 |   show (PDef cls) = unlines (show <$> cls)
1192 |   show (PData {}) = "PData"
1193 |   show (PParameters {}) = "PParameters"
1194 |   show (PUsing {}) = "PUsing"
1195 |   show (PInterface {}) = "PInterface"
1196 |   show (PImplementation {}) = "PImplementation"
1197 |   show (PRecord {}) = "PRecord"
1198 |   show (PFail mstr ds) = unlines (unwords ("failing" :: maybe [] (pure . show) mstr) :: (show . val <$> ds))
1199 |   show (PMutual {}) = "PMutual"
1200 |   show (PFixity {}) = "PFixity"
1201 |   show (PNamespace {}) = "PNamespace"
1202 |   show (PTransform {}) = "PTransform"
1203 |   show (PRunElabDecl {}) = "PRunElabDecl"
1204 |   show (PDirective {}) = "PDirective"
1205 |   show (PBuiltin {}) = "PBuiltin"
1206 |
1207 |