0 | ||| Some utilities for defining and manipulating TTImp values
  1 | ||| for writing elaborator scripts.
  2 | |||
  3 | ||| Some notes: Use quotes whenever possible:
  4 | |||
  5 | ||| Names can be quoted like so: `{ AName }, `{ In.Namespace.AName }.
  6 | ||| Both examples are of type Language.Reflection.TT.Name.
  7 | |||
  8 | ||| Expressions can be quoted like so: `(\x => x * x)
  9 | module Language.Reflection.Syntax
 10 |
 11 | import Data.String
 12 | import Data.List1
 13 | import Language.Reflection
 14 |
 15 | %default total
 16 |
 17 | --------------------------------------------------------------------------------
 18 | --          Names
 19 | --------------------------------------------------------------------------------
 20 |
 21 | public export
 22 | FromString Name where
 23 |   fromString s = run (split ('.' ==) s) []
 24 |
 25 |     where
 26 |       run : List1 String -> List String -> Name
 27 |       run (h ::: []) []        = UN $ Basic h
 28 |       run (h ::: []) ns        = NS (MkNS ns) (UN $ Basic h)
 29 |       run ll@(h ::: (y :: ys)) xs =
 30 |         run (assert_smaller ll $ y ::: ys) (h :: xs)
 31 |
 32 | export
 33 | Interpolation Name where
 34 |   interpolate = show
 35 |
 36 | ||| True if the given name ends on (`Basic $ UN "Nil")
 37 | public export
 38 | isNil : Name -> Bool
 39 | isNil (NS ns nm)         = isNil nm
 40 | isNil (UN $ Basic "Nil") = True
 41 | isNil _                  = False
 42 |
 43 | ||| True if the given name ends on (`Basic $ UN "Lin")
 44 | public export
 45 | isLin : Name -> Bool
 46 | isLin (NS ns nm)         = isLin nm
 47 | isLin (UN $ Basic "Lin") = True
 48 | isLin _                  = False
 49 |
 50 | ||| True if the given name ends on (`Basic $ UN "::")
 51 | public export
 52 | isCons : Name -> Bool
 53 | isCons (NS ns nm)        = isCons nm
 54 | isCons (UN $ Basic "::") = True
 55 | isCons _                 = False
 56 |
 57 | ||| True if the given name ends on (`Basic $ UN ":<")
 58 | public export
 59 | isSnoc : Name -> Bool
 60 | isSnoc (NS ns nm)        = isSnoc nm
 61 | isSnoc (UN $ Basic ":<") = True
 62 | isSnoc _                 = False
 63 |
 64 | ||| Takes a (probably fully qualified name) and generates a
 65 | ||| identifier from this without the dots.
 66 | |||
 67 | ||| Example : camelCase "Data.List1.List1" = "DataList1List1"
 68 | export
 69 | camelCase : Name -> String
 70 | camelCase = concat . split ('.' ==) . show
 71 |
 72 | ||| Convert a `Name` to a simple string dropping some of its context
 73 | ||| like its namespace (if any).
 74 | |||
 75 | ||| Use this to get access to a simple variable name or to print the
 76 | ||| un-prefixed name of a data- or type constructor.
 77 | export
 78 | nameStr : Name -> String
 79 | nameStr (UN $ Basic x)  = x
 80 | nameStr (UN $ Field x)  = x
 81 | nameStr (UN Underscore) = "_"
 82 | nameStr (NS _ x) = nameStr x
 83 | nameStr (MN x y) = x ++ show y
 84 | nameStr (DN _ x) = nameStr x
 85 | nameStr (Nested (x,y) n) = #"nested_\#{nameStr n}_\#{show x}_\#{show y}"#
 86 | nameStr (CaseBlock x n) = #"case_n_\#{show x}"#
 87 | nameStr (WithBlock x n) = #"with_n_\#{show x}"#
 88 |
 89 | ||| An interface for things with a `Name`.
 90 | |||
 91 | ||| This comes with several utility function strewn across this module
 92 | ||| for creating variables from names and printing a name as a string.
 93 | ||| All these make use of dot syntax, so they can be used like record
 94 | ||| projections.
 95 | public export
 96 | interface Named a where
 97 |   ||| Extract the `Name` from a value.
 98 |   |||
 99 |   ||| We call this `(.getName)` instead
100 |   ||| of just `(.name)`, because `name` is a commonly used record field name.
101 |   (.getName) : a -> Name
102 |
103 | public export %inline
104 | Named Name where
105 |   n.getName = n
106 |
107 | ||| Use `nameStr` to convert the name of a value to a simple string.
108 | public export %inline
109 | (.nameStr) : Named a => a -> String
110 | x.nameStr = nameStr x.getName
111 |
112 | --------------------------------------------------------------------------------
113 | --          Vars
114 | --------------------------------------------------------------------------------
115 |
116 | ||| Creates a variable from the given name
117 | |||
118 | ||| Names are best created using quotes: `{ AName },
119 | ||| `{ In.Namespacs.Name }.
120 | |||
121 | ||| Likewise, if the name is already known at the time of
122 | ||| writing, use quotes for defining variables directly: `(AName)
123 | public export %inline
124 | var : (name : Name) -> TTImp
125 | var = IVar EmptyFC
126 |
127 | ||| Creates a variable with the name of the given value.
128 | public export %inline
129 | (.nameVar) : Named a => a -> TTImp
130 | n.nameVar = var n.getName
131 |
132 | ||| Alias for `var . fromString`
133 | public export %inline
134 | varStr : String -> TTImp
135 | varStr = var . fromString
136 |
137 | ||| Binds a new variable, for instance in a pattern match.
138 | |||
139 | ||| This is an alias for `IBindVar EmptyFC`.
140 | public export %inline
141 | bindVar : Name -> TTImp
142 | bindVar = IBindVar EmptyFC
143 |
144 | ||| Bind a named value to a variable. This uses `nameStr` for
145 | ||| the variable's name.
146 | public export %inline
147 | (.bindVar) : Named a => a -> TTImp
148 | x.bindVar = bindVar x.getName
149 |
150 | ||| Implicit value bound if unsolved
151 | |||
152 | ||| This is an alias for `Implicit EmptyFC True`
153 | public export %inline
154 | implicitTrue : TTImp
155 | implicitTrue = Implicit EmptyFC True
156 |
157 | ||| Implicitly typed value unbound if unsolved
158 | |||
159 | ||| This is an alias for `Implicit EmptyFC False`
160 | public export %inline
161 | implicitFalse : TTImp
162 | implicitFalse = Implicit EmptyFC False
163 |
164 | ||| Primitive values.
165 | |||
166 | ||| This is an alias for `IPrimVal EmptyFC`
167 | public export %inline
168 | primVal : (c : Constant) -> TTImp
169 | primVal = IPrimVal EmptyFC
170 |
171 | ||| Creates a string constant from a named value. Uses
172 | ||| `nameStr` to convert the name to a string.
173 | public export %inline
174 | (.namePrim) : Named a => a -> TTImp
175 | x.namePrim = primVal $ Str x.nameStr
176 |
177 | ||| The type `Type`.
178 | |||
179 | ||| This is an alias for `IType EmptyFC`.
180 | public export %inline
181 | type :  TTImp
182 | type = IType EmptyFC
183 |
184 | ||| A named hole.
185 | |||
186 | ||| This is an alias for `IHole EmptyFC`.
187 | public export %inline
188 | hole :  String -> TTImp
189 | hole = IHole EmptyFC
190 |
191 | ||| Tries to extract a variable name from a `TTImp`.
192 | |||
193 | ||| Returns `Nothing` if not an `IVar`.
194 | public export
195 | unVar : TTImp -> Maybe Name
196 | unVar (IVar _ n) = Just n
197 | unVar _          = Nothing
198 |
199 | ||| Proof search
200 | |||
201 | ||| This is an alias for `ISearch EmptyFC`
202 | public export %inline
203 | iSearch : (depth : Nat) -> TTImp
204 | iSearch = ISearch EmptyFC
205 |
206 | --------------------------------------------------------------------------------
207 | --          Application
208 | --------------------------------------------------------------------------------
209 |
210 | ||| Function application.
211 | |||
212 | ||| This is an alias for `IApp EmptyFC`.
213 | |||
214 | ||| Example: ```app (var "Just") (var "x")```
215 | |||          is equivalent to `(Just x)
216 | public export %inline
217 | app : (fun, arg : TTImp) -> TTImp
218 | app = IApp EmptyFC
219 |
220 | export
221 | unApp : TTImp -> (TTImp,List TTImp)
222 | unApp = run []
223 |
224 |   where
225 |     run : List TTImp -> TTImp -> (TTImp,List TTImp)
226 |     run xs (IApp _ y z) = run (z :: xs) y
227 |     run xs t            = (t,xs)
228 |
229 | ||| Applies a list of variables to a function.
230 | |||
231 | ||| See `appNames` for an example
232 | public export %inline
233 | appAll : Name -> List TTImp -> TTImp
234 | appAll fun = foldl app (var fun)
235 |
236 | ||| Applies a list of variable names to a function.
237 | |||
238 | ||| Example: appNames "either" ["f","g","val"]
239 | |||          is equivalent to ~(either f g val)
240 | public export %inline
241 | appNames : (fun : Name) -> (args : List Name) -> TTImp
242 | appNames fun = appAll fun . map var
243 |
244 | ||| Binds a list of parameters to a data constructor in
245 | ||| a pattern match.
246 | |||
247 | ||| Example: bindAll "MkPair" ["a","b"]
248 | |||          is the same as `(MkPair a b)
249 | public export %inline
250 | bindAll : (fun : Name) -> (args : List Name) -> TTImp
251 | bindAll fun = appAll fun . map bindVar
252 |
253 | ||| Alias for `IBindHere EmptyFC`
254 | public export %inline
255 | bindHere : (mode : BindMode) -> (val : TTImp) -> TTImp
256 | bindHere = IBindHere EmptyFC
257 |
258 | ||| Alias for `IMustUnify EmptyFC`
259 | public export %inline
260 | mustUnify : (reason : DotReason) -> (val : TTImp) -> TTImp
261 | mustUnify = IMustUnify EmptyFC
262 |
263 | ||| Alias for `IAs EmptyFC EmptyFC`
264 | public export %inline
265 | iAs : (side : UseSide) -> (name : Name) -> (val : TTImp) -> TTImp
266 | iAs = IAs EmptyFC EmptyFC
267 |
268 | ||| Applying an auto-implicit.
269 | |||
270 | ||| This is an alias for `IAutoApp EmptyFC`.
271 | |||
272 | ||| Example: `autoApp (var "traverse") (var "MyApp")`
273 | |||          is equivalent to `(traverse @{MyApp})
274 | public export %inline
275 | autoApp : (fun, arg : TTImp) -> TTImp
276 | autoApp = IAutoApp EmptyFC
277 |
278 | ||| Infix version of `autoApp`
279 | public export %inline
280 | (.@) : TTImp -> TTImp -> TTImp
281 | (.@) = autoApp
282 |
283 | ||| Application in a `with` expression
284 | |||
285 | ||| This is an alias for `IWithApp EmptyFC`.
286 | public export %inline
287 | withApp : (fun, arg : TTImp) -> TTImp
288 | withApp = IWithApp EmptyFC
289 |
290 | ||| Named function application.
291 | |||
292 | ||| This is an alias for `INamedApp EmptyFC`.
293 | |||
294 | ||| Example: `namedApp (var "traverse") "f" (var "MyApp")`
295 | |||          is equivalent to `(traverse {f = MyApp})
296 | public export %inline
297 | namedApp : (fun : TTImp) -> (name : Name) -> (arg : TTImp) -> TTImp
298 | namedApp = INamedApp EmptyFC
299 |
300 | ||| Catch-all pattern match on a data constructor.
301 | |||
302 | ||| Example: `bindAny "Person"`
303 | |||          is the same as `(Person {})
304 | ||| ```
305 | public export %inline
306 | bindAny : Named a => a -> TTImp
307 | bindAny n = namedApp n.nameVar (UN Underscore) implicitTrue
308 |
309 | ||| Alias for `IAlternative EmptyFC`
310 | public export %inline
311 | alternative : (tpe : AltType) -> (alts : List TTImp) -> TTImp
312 | alternative = IAlternative EmptyFC
313 |
314 | --------------------------------------------------------------------------------
315 | --          Function Arguments
316 | --------------------------------------------------------------------------------
317 |
318 | ||| A function argument, typically extracted from pi-types or used
319 | ||| to define pi-types.
320 | public export
321 | record Arg where
322 |   constructor MkArg
323 |   count  : Count
324 |   piInfo : PiInfo TTImp
325 |   name   : Maybe Name
326 |   type   : TTImp
327 |
328 | ||| Creates an explicit unnamed argument of the given type.
329 | public export %inline
330 | arg : TTImp -> Arg
331 | arg = MkArg MW ExplicitArg Nothing
332 |
333 | ||| Creates an explicit, unnamed, zero-quantity
334 | ||| argument of the given type.
335 | public export %inline
336 | erasedArg : TTImp -> Arg
337 | erasedArg = MkArg M0 ExplicitArg Nothing
338 |
339 | ||| Creates an explicit argument of the given name
340 | ||| to be used in a lambda.
341 | public export %inline
342 | lambdaArg : Named a => a -> Arg
343 | lambdaArg n = MkArg MW ExplicitArg (Just n.getName) implicitFalse
344 |
345 | ||| Creates an erased implicit argument of the given name.
346 | public export %inline
347 | erasedImplicit : Named a => a -> Arg
348 | erasedImplicit n = MkArg M0 ImplicitArg (Just n.getName) implicitFalse
349 |
350 | ||| True if the given argument is an explicit argument.
351 | public export
352 | isExplicit : Arg -> Bool
353 | isExplicit (MkArg _ ExplicitArg _ _) = True
354 | isExplicit (MkArg _ _           _ _) = False
355 |
356 | ||| True if the given argument has quantity zero.
357 | public export
358 | isErased : Arg -> Bool
359 | isErased (MkArg M0 _ _ _) = True
360 | isErased _                = False
361 |
362 | ||| True if the given argument is explicit and does not have
363 | ||| quantity zero.
364 | public export
365 | isExplicitUnerased : Arg -> Bool
366 | isExplicitUnerased (MkArg M1 ExplicitArg _ _) = True
367 | isExplicitUnerased (MkArg MW ExplicitArg _ _) = True
368 | isExplicitUnerased _                          = False
369 |
370 | ||| Extracts the arguments from a function type.
371 | export
372 | unPi : TTImp -> (List Arg, TTImp)
373 | unPi (IPi _ c p n at rt) = mapFst (MkArg c p n at ::) $ unPi rt
374 | unPi tpe                 = ([],tpe)
375 |
376 | ||| Extracts the arguments from a lambda.
377 | export
378 | unLambda : TTImp -> (List Arg, TTImp)
379 | unLambda (ILam _ c p n at rt) = mapFst (MkArg c p n at ::) $ unLambda rt
380 | unLambda tpe                  = ([],tpe)
381 |
382 | --------------------------------------------------------------------------------
383 | --          Lambdas
384 | --------------------------------------------------------------------------------
385 |
386 | ||| Defines an anonymous function (lambda).
387 | |||
388 | ||| This passes the fields of `Arg` to `ILam EmptyFC`
389 | public export
390 | lam : (arg : Arg) -> (lamTy : TTImp) -> TTImp
391 | lam (MkArg c p n t) = ILam EmptyFC c p n t
392 |
393 | --------------------------------------------------------------------------------
394 | --          Function Types
395 | --------------------------------------------------------------------------------
396 |
397 | ||| Defines a function type.
398 | |||
399 | ||| This passes the fields of `Arg` to `IPi EmptyFC`
400 | public export
401 | pi : (arg : Arg) -> (retTy : TTImp) -> TTImp
402 | pi (MkArg c p n t) = IPi EmptyFC c p n t
403 |
404 | ||| Defines a function type taking the given arguments.
405 | public export %inline
406 | piAll : TTImp -> List Arg -> TTImp
407 | piAll res = foldr pi res
408 |
409 | ||| Defines a function type taking implicit arguments of the
410 | ||| given names.
411 | public export %inline
412 | piAllImplicit : TTImp -> List Name -> TTImp
413 | piAllImplicit res = piAll res . map erasedImplicit
414 |
415 | ||| Defines a function type taking the given auto-implicit arguments.
416 | public export
417 | piAllAuto : TTImp -> List TTImp -> TTImp
418 | piAllAuto res = piAll res . map (MkArg MW AutoImplicit Nothing)
419 |
420 | --------------------------------------------------------------------------------
421 | --          Pattern Matching
422 | --------------------------------------------------------------------------------
423 |
424 | ||| An impossible clause in a pattern match.
425 | |||
426 | ||| This is an alias for `ImpossibleClause EmptyFC`.
427 | public export %inline
428 | impossibleClause : (lhs : TTImp) -> Clause
429 | impossibleClause = ImpossibleClause EmptyFC
430 |
431 | ||| A pattern clause consisting of the left-hand and
432 | ||| right-hand side of the pattern arrow "=>".
433 | |||
434 | ||| This is an alias for `PatClause EmptyFC`.
435 | public export %inline
436 | patClause : (lhs : TTImp) -> (rhs : TTImp) -> Clause
437 | patClause = PatClause EmptyFC
438 |
439 | ||| A with clause.
440 | |||
441 | ||| This is an alias for `WithClause EmptyFC`.
442 | public export %inline
443 | withClause :
444 |      (lhs     : TTImp)
445 |   -> (rig     : Count)
446 |   -> (wval    : TTImp)
447 |   -> (prf     : Maybe (Count, Name))
448 |   -> (flags   : List WithFlag)
449 |   -> (clauses : List Clause)
450 |   -> Clause
451 | withClause = WithClause EmptyFC
452 |
453 | ||| A case expression.
454 | |||
455 | ||| This is an alias for `ICase EmptyFC []`.
456 | public export %inline
457 | iCase : (sc : TTImp) -> (ty : TTImp) -> (clauses : List Clause) -> TTImp
458 | iCase = ICase EmptyFC []
459 |
460 | ||| "as"-pattern.
461 | |||
462 | ||| This is an alias for `IAs EmptyFC UseLeft`.
463 | public export %inline
464 | as : Name -> TTImp -> TTImp
465 | as = IAs EmptyFC EmptyFC UseLeft
466 |
467 | --------------------------------------------------------------------------------
468 | --          Function Declarations
469 | --------------------------------------------------------------------------------
470 |
471 | ||| Named type.
472 | |||
473 | ||| This is an alias for `MkTyp EmptyFC`.
474 | public export %inline
475 | mkTy : (name : Name) -> (type : TTImp) -> ITy
476 | mkTy = MkTy EmptyFC . MkFCVal EmptyFC
477 |
478 | ||| Type declaration of a function.
479 | |||
480 | ||| `claim c v opts n tp` is an alias for
481 | ||| `IClaim EmptyFC c v opts (MkTy EmptyFC n tp)`.
482 | public export %inline
483 | claim :
484 |      (count : Count)
485 |   -> (vis   : Visibility)
486 |   -> (opts  : List FnOpt)
487 |   -> (name  : Name)
488 |   -> (type  : TTImp)
489 |   -> Decl
490 | claim c v opts n tp = IClaim $ MkFCVal EmptyFC $ MkIClaimData c v opts (mkTy n tp)
491 |
492 | ||| `simpleClaim v n t` is an alias for `claim MW v [] (mkTy n t)`
493 | public export %inline
494 | simpleClaim : Visibility -> Name -> TTImp -> Decl
495 | simpleClaim v = claim MW v []
496 |
497 | ||| Alias for `simpleClaim Public`
498 | public export %inline
499 | public' : Name -> TTImp -> Decl
500 | public' = simpleClaim Public
501 |
502 | ||| Alias for `simpleClaim Private``
503 | public export %inline
504 | private' : Name -> TTImp -> Decl
505 | private' = simpleClaim Private
506 |
507 | ||| Alias for `simpleClaim Export`
508 | public export %inline
509 | export' : Name -> TTImp -> Decl
510 | export' = simpleClaim Export
511 |
512 | ||| `directHint v` is an alias for `claim MW v [Hint True]`
513 | public export %inline
514 | directHint : Visibility -> Name -> TTImp -> Decl
515 | directHint v = claim MW v [Hint True]
516 |
517 | ||| `interfaceHint v opts` is an alias for `claim MW v (Hint False :: opts)`
518 | public export %inline
519 | interfaceHintOpts : Visibility -> List FnOpt -> Name -> TTImp -> Decl
520 | interfaceHintOpts v opts = claim MW v (Hint False :: opts)
521 |
522 | ||| `interfaceHint v` is an alias for `claim MW v [Hint False]`
523 | public export %inline
524 | interfaceHint : Visibility -> Name -> TTImp -> Decl
525 | interfaceHint v = claim MW v [Hint False]
526 |
527 | ||| Function definition (implementation)
528 | |||
529 | ||| This is an alias for `IDef EmptyFC`.
530 | public export %inline
531 | def : Name -> List Clause -> Decl
532 | def = IDef EmptyFC
533 |
534 | --------------------------------------------------------------------------------
535 | --          Local Defs and Let
536 | --------------------------------------------------------------------------------
537 |
538 | ||| Let bindings.
539 | |||
540 | ||| This is an alias for `ILet EmptyFC`.
541 | public export %inline
542 | iLet :
543 |      (count : Count)
544 |   -> (name  : Name)
545 |   -> (type  : TTImp)
546 |   -> (val   : TTImp)
547 |   -> (scope : TTImp)
548 |   -> TTImp
549 | iLet = ILet EmptyFC EmptyFC
550 |
551 | ||| Local definitions
552 | |||
553 | ||| This is an alias for `ILocal EmptyFC`.
554 | public export %inline
555 | local : (decls : List Decl) -> (scope : TTImp) -> TTImp
556 | local = ILocal EmptyFC
557 |
558 | ||| Field updates
559 | |||
560 | ||| This is an alias for `IUpdate EmptyFC`.
561 | public export %inline
562 | update : (updates : List IFieldUpdate) -> (arg : TTImp) -> TTImp
563 | update = IUpdate EmptyFC
564 |
565 | --------------------------------------------------------------------------------
566 | --          Data Declarations
567 | --------------------------------------------------------------------------------
568 |
569 | ||| Data declaration.
570 | |||
571 | ||| This merges constructors `IData` and `MkData`.
572 | public export
573 | iData :
574 |      (vis   : Visibility)
575 |   -> (name  : Name)
576 |   -> (tycon : TTImp)
577 |   -> (opts  : List DataOpt)
578 |   -> (cons  : List ITy)
579 |   -> Decl
580 | iData v n tycon opts cons =
581 |   IData EmptyFC (specified v) Nothing (MkData EmptyFC n (Just tycon) opts cons)
582 |
583 | ||| Data claim.
584 | |||
585 | ||| This merges constructors `IData` and `MkLater`.
586 | public export
587 | iDataLater :
588 |      (vis   : Visibility)
589 |   -> (name  : Name)
590 |   -> (tycon : TTImp)
591 |   -> Decl
592 | iDataLater v n tycon =
593 |   IData EmptyFC (specified v) Nothing (MkLater EmptyFC n tycon)
594 |
595 | ||| Simple data declaration of type `Type` (no options, no parameters,
596 | ||| no indices).
597 | |||
598 | ||| `simpleData v n` is an alias for `iData v n type []`.
599 | public export %inline
600 | simpleData : Visibility -> Name -> (cons : List ITy) -> Decl
601 | simpleData v n = iData v n type []
602 |
603 | ||| Alias for `simpleData Public`
604 | public export %inline
605 | simpleDataPublic : Name -> (cons : List ITy) -> Decl
606 | simpleDataPublic = simpleData Public
607 |
608 | ||| Alias for `simpleData Export`
609 | public export %inline
610 | simpleDataExport : Name -> (cons : List ITy) -> Decl
611 | simpleDataExport = simpleData Export
612 |
613 | --------------------------------------------------------------------------------
614 | --          Rewrite
615 | --------------------------------------------------------------------------------
616 |
617 | ||| Alias for `IRewrite EmptyFC`
618 | public export %inline
619 | iRewrite : (eq,scope : TTImp) -> TTImp
620 | iRewrite = IRewrite EmptyFC
621 |
622 | --------------------------------------------------------------------------------
623 | --          Laziness
624 | --------------------------------------------------------------------------------
625 |
626 | ||| Alias for `IDelayed EmptyFC`
627 | public export %inline
628 | iDelayed : (reason : LazyReason) -> (arg : TTImp) -> TTImp
629 | iDelayed = IDelayed EmptyFC
630 |
631 | ||| Alias for `IDelay EmptyFC`
632 | public export %inline
633 | iDelay : (arg : TTImp) -> TTImp
634 | iDelay = IDelay EmptyFC
635 |
636 | ||| Alias for `IForce EmptyFC`
637 | public export %inline
638 | iForce : (arg : TTImp) -> TTImp
639 | iForce = IForce EmptyFC
640 |
641 | --------------------------------------------------------------------------------
642 | --          Quotation
643 | --------------------------------------------------------------------------------
644 |
645 | ||| Alias for `IQuote EmptyFC`
646 | public export %inline
647 | quote : TTImp -> TTImp
648 | quote = IQuote EmptyFC
649 |
650 | ||| Alias for `IQuoteName EmptyFC`
651 | public export %inline
652 | quoteName : Name -> TTImp
653 | quoteName = IQuoteName EmptyFC
654 |
655 | ||| Alias for `IQuoteDecl EmptyFC`
656 | public export %inline
657 | quoteDecl : List Decl -> TTImp
658 | quoteDecl = IQuoteDecl EmptyFC
659 |
660 | ||| Alias for `IUnquote EmptyFC`
661 | public export %inline
662 | unquote : TTImp -> TTImp
663 | unquote = IUnquote EmptyFC
664 |
665 | --------------------------------------------------------------------------------
666 | --          Recursion
667 | --------------------------------------------------------------------------------
668 |
669 |
670 | ||| Checks if one of the given names makes an appearance in the
671 | ||| given type.
672 | export
673 | rec : List Name -> (tpe : TTImp) -> Bool
674 | rec nms (IVar fc nm1)        = nm1 `elem` nms
675 | rec nms (IApp fc s t)        = rec nms s || rec nms t
676 | rec nms (INamedApp fc s _ t) = rec nms s || rec nms t
677 | rec nms (IAutoApp fc s t)    = rec nms s || rec nms t
678 | rec nms (IDelayed _ LLazy t) = rec nms t
679 | rec nms t                    = False
680 |
681 | ||| Prefixes the given expression with `assert_total`, if
682 | ||| one of the names listed makes an appearance in the given type.
683 | export
684 | assertIfRec : List Name -> (tpe : TTImp) -> (expr : TTImp) -> TTImp
685 | assertIfRec nms tpe expr =
686 |   if rec nms tpe then var "assert_total" `app` expr else expr
687 |
688 | --------------------------------------------------------------------------------
689 | --          Elab Utils
690 | --------------------------------------------------------------------------------
691 |
692 | ||| Constructs a `TTImp` from the given arguments, which
693 | ||| wraps them in unqualified list constructors.
694 | |||
695 | ||| For instance, `listOf [var "x", var "y"]` generates
696 | ||| an expression corresponding to `x :: y :: Nil`
697 | public export %inline
698 | listOf : Foldable t => t TTImp -> TTImp
699 | listOf = foldr (\e,acc => `(~(e) :: ~(acc))) `( Nil )
700 |
701 | private errMsg : Name -> List (Name,TTImp) -> String
702 | errMsg n [] = show n ++ " is not in scope."
703 | errMsg n xs =
704 |   let rest := concat $ intersperse ", " $ map (show . fst) xs
705 |    in show n ++ " is not unique: " ++ rest
706 |
707 | lookupRefinedName : Elaboration m => (prev : List (Name, TTImp)) -> Name -> m (Name, TTImp)
708 | lookupRefinedName prev n = case !(getType n) of
709 |   [p] => pure p
710 |   []  => fail $ errMsg n prev
711 |   ps  => fail $ errMsg n ps
712 |
713 | ||| Looks up a name in the current namespace.
714 | export
715 | lookupName : Elaboration m => Name -> m (Name, TTImp)
716 | lookupName n = do
717 |   pairs <- getType n
718 |   case pairs of
719 |     [p] => pure p
720 |     ps  => case n of
721 |              UN _ => inCurrentNS n >>= lookupRefinedName ps
722 |              _    => fail $ errMsg n ps
723 |