0 | -- Computing the parameters
  1 |
  2 | module Core.Context.Data
  3 |
  4 | import Core.Context.Log
  5 | import Core.Normalise
  6 |
  7 | import Libraries.Data.NatSet
  8 | import Libraries.Data.WithDefault
  9 |
 10 | %default covering
 11 |
 12 | -- If a name appears more than once in an argument list, only the first is
 13 | -- considered a parameter
 14 | dropReps : List (Maybe (Term vars)) -> List (Maybe (Term vars))
 15 | dropReps [] = []
 16 | dropReps {vars} (Just (Local fc r x p) :: xs)
 17 |     = Just (Local fc r x p) :: assert_total (dropReps (map toNothing xs))
 18 |   where
 19 |     toNothing : Maybe (Term vars) -> Maybe (Term vars)
 20 |     toNothing tm@(Just (Local _ _ v' _))
 21 |         = if x == v' then Nothing else tm
 22 |     toNothing tm = tm
 23 | dropReps (x :: xs) = x :: dropReps xs
 24 |
 25 | updateParams : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
 26 |                Maybe (List (Maybe (Term vars))) ->
 27 |                   -- arguments to the type constructor which could be
 28 |                   -- parameters
 29 |                   -- Nothing, as an argument, means this argument can't
 30 |                   -- be a parameter position
 31 |                List (Term vars) ->
 32 |                   -- arguments to an application
 33 |                Core (List (Maybe (Term vars)))
 34 | updateParams Nothing args = dropReps <$> traverse couldBeParam args
 35 |   where
 36 |     couldBeParam : Term vars -> Core (Maybe (Term vars))
 37 |     couldBeParam tm = pure $ case !(etaContract tm) of
 38 |       Local fc r v p => Just (Local fc r v p)
 39 |       _ => Nothing
 40 | updateParams (Just args) args' = pure $ dropReps $ zipWith mergeArg args args'
 41 |   where
 42 |     mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
 43 |     mergeArg (Just (Local fc r x p)) (Local _ _ y _)
 44 |         = if x == y then Just (Local fc r x p) else Nothing
 45 |     mergeArg _ _ = Nothing
 46 |
 47 | getPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
 48 |         Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
 49 |         Core (Maybe (List (Maybe (Term vars))))
 50 | getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
 51 |       = do scPs <- getPs (map (map (map weaken)) acc) tyn sc
 52 |            pure $ map (map (>>= \ tm => shrink tm (Drop Refl))) scPs
 53 | getPs acc tyn tm
 54 |     = case getFnArgs tm of
 55 |            (Ref _ _ n, args) =>
 56 |               if n == tyn
 57 |                  then Just <$> updateParams acc args
 58 |                  else pure acc
 59 |            _ => pure acc
 60 |
 61 | toPos : Maybe (List (Maybe a)) -> NatSet
 62 | toPos Nothing = NatSet.empty
 63 | toPos (Just ns) = justPos 0 ns NatSet.empty
 64 |   where
 65 |     justPos : Nat -> List (Maybe a) -> NatSet -> NatSet
 66 |     justPos i [] acc = acc
 67 |     justPos i (Just x :: xs) acc = justPos (1 + i) xs (insert i acc)
 68 |     justPos i (Nothing :: xs) acc = justPos (1 + i) xs acc
 69 |
 70 | getConPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
 71 |            Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
 72 |            Core NatSet
 73 | getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
 74 |     = do bacc <- getPs acc tyn ty
 75 |          getConPs (map (map (map weaken)) bacc) tyn sc
 76 | getConPs acc tyn (Bind _ x (Let _ _ v ty) sc)
 77 |     = getConPs acc tyn (subst v sc)
 78 | getConPs acc tyn tm = toPos <$> getPs acc tyn tm
 79 |
 80 | paramPos : {auto _ : Ref Ctxt Defs} -> Name -> (dcons : List ClosedTerm) ->
 81 |            Core (Maybe NatSet)
 82 | paramPos tyn [] = pure Nothing -- no constructor!
 83 | paramPos tyn dcons = do
 84 |   candidates <- traverse (getConPs Nothing tyn) dcons
 85 |   pure $ Just $ NatSet.intersectAll candidates
 86 |
 87 | export
 88 | addData : {auto c : Ref Ctxt Defs} ->
 89 |           Scope -> Visibility -> Int -> DataDef -> Core Int
 90 | addData vars vis tidx (MkData con datacons)
 91 |     = do defs <- get Ctxt
 92 |          let tyName = con.name.val
 93 |          let allPos = NatSet.allLessThan con.arity
 94 |          -- In case there are no constructors, all the positions are parameter positions!
 95 |          let paramPositions = fromMaybe allPos !(paramPos (Resolved tidx) (map val datacons))
 96 |          log "declare.data.parameters" 20 $
 97 |             "Positions of parameters for datatype" ++ show tyName ++
 98 |             ": " ++ show paramPositions
 99 |          let tydef = newDef con.fc tyName top vars con.val (specified vis)
100 |                             (TCon con.arity
101 |                                   paramPositions
102 |                                   allPos
103 |                                   defaultFlags [] (Just $ map (.name.val) datacons) Nothing)
104 |          (idx, gam') <- addCtxt tyName tydef (gamma defs)
105 |          gam'' <- addDataConstructors 0 datacons gam'
106 |          put Ctxt ({ gamma := gam'' } defs)
107 |          pure idx
108 |   where
109 |     conVisibility : Visibility -> Visibility
110 |     conVisibility Export = Private
111 |     conVisibility x = x
112 |
113 |     addDataConstructors : (tag : Int) -> List Constructor ->
114 |                           Context -> Core Context
115 |     addDataConstructors tag [] gam = pure gam
116 |     addDataConstructors tag (con :: cs) gam
117 |         = do let conName = con.name.val
118 |              let condef = newDef con.fc conName top vars con.val (specified $ conVisibility vis) (DCon tag con.arity Nothing)
119 |              -- Check 'n' is undefined
120 |              Nothing <- lookupCtxtExact conName gam
121 |                  | Just gdef => throw (AlreadyDefined con.fc conName)
122 |              (idx, gam') <- addCtxt conName condef gam
123 |              addDataConstructors (tag + 1) cs gam'
124 |