
  0 | module Idris.Syntax.Views
  1 | 
  2 | import Idris.Syntax
  3 | import Idris.Syntax.Builtin
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | data Arg' nm
  9 |    = Explicit FC (PTerm' nm)
 10 |    | Auto     FC (PTerm' nm)
 11 |    | Named    FC Name (PTerm' nm)
 12 | 
 13 | export
 14 | unArg : Arg' nm -> PTerm' nm
 15 | unArg (Explicit _ t) = t
 16 | unArg (Auto _ t) = t
 17 | unArg (Named _ _ t) = t
 18 | 
 19 | export
 20 | getFnArgs : (Name -> nm) -> PTerm' nm -> (PTerm' nm, List (Arg' nm))
 21 | getFnArgs embed fts = go fts [] where
 22 | 
 23 |   go : PTerm' nm -> List (Arg' nm) -> (PTerm' nm, List (Arg' nm))
 24 |   go (PApp fc f t) = go f . (Explicit fc t ::)
 25 |   go (PAutoApp fc f t) = go f . (Auto fc t ::)
 26 |   go (PNamedApp fc f n t) = go f . (Named fc n t ::)
 27 |   go (PBracketed fc f) = go f
 28 |   -- we don't care about the binder info here
 29 |   go (POp fc leftSide op r) =
 30 |     (PRef op.fc op.val.toName,) . (Explicit fc leftSide.val.getLhs ::) . (Explicit fc r ::)
 31 |   go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::)
 32 |   -- ambiguous, picking the type constructor here
 33 |   go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::)
 34 |   go (PDPair full fc l ty r)
 35 |     = (PRef fc $ embed dpairname,)
 36 |     . (Explicit fc l ::) . (Explicit fc ty ::) . (Explicit fc r ::)
 37 |   go f = (f,)
 38 | 
 39 | export
 40 | underPis : PTerm' nm -> (List (Maybe Name, Binder (PTerm' nm)), PTerm' nm)
 41 | underPis abs = go abs [] where
 42 | 
 43 |   go : PTerm' nm -> List (Maybe Name, Binder (PTerm' nm)) ->
 44 |        (List (Maybe Name, Binder (PTerm' nm)), PTerm' nm)
 45 |   go (PPi fc rig pinfo mn a b) = go b . ((mn, Pi fc rig pinfo a) ::)
 46 |   go (PBracketed fc abs) = go abs
 47 |   go abs = (, abs)
 48 | 
 49 | export
 50 | underLams : PTerm' nm -> (List (PTerm' nm, Binder (PTerm' nm)), PTerm' nm)
 51 | underLams fs = go fs [] where
 52 | 
 53 |   go : PTerm' nm -> List (PTerm' nm, Binder (PTerm' nm)) ->
 54 |        (List (PTerm' nm, Binder (PTerm' nm)), PTerm' nm)
 55 |   go (PBracketed fc f) = go f
 56 |   go (PLam fc rig pinfo pat a sc) = go sc . ((pat, Lam fc rig pinfo a) ::)
 57 |   go fs = (,fs)
 58 |