Calculate parameter positions in types

README.md

@@ -9,7 +9,11 @@ exceptions. The most notable user visible differences, which might cause Idris
 
 + Unbound implicit arguments are always erased, so it is a type error to
   attempt to pattern match on one.
-+ Simplified resolution of ambiguous names.
++ Simplified resolution of ambiguous names, which might mean you need to
+  explicitly disambiguate more often. As a general rule, Idris 2 will be able
+  to disambiguate between names which have different concrete return types
+  (such as data constructores), or which have different concrete argument
+  types (such as record projections).
 + Minor differences in the meaning of export modifiers `private`, `export`,
   and `public export`, which now refer to visibility of names from other
   *namespaces* rather than visibility from other *files*.

src/Core/Context.idr

@@ -57,8 +57,9 @@ Show Def where
       = show args ++ "; " ++ show ct
   show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a
   show (TCon t a ps ds ms cons) 
-      = "TyCon " ++ show t ++ " " ++ show a ++ " " ++ show cons
+      = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ 
-        ++ " with " ++ show ms
+        " constructors: " ++ show cons ++ 
+        " mutual with: " ++ show ms
   show (ExternDef arity) = "<external def with arith " ++ show arity ++ ">"
   show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
   show (Hole _ inv) = "Hole"
@@ -1261,18 +1262,88 @@ getNextTypeTag
          put Ctxt (record { nextTag $= (+1) } defs)
          pure (nextTag defs)
 
-paramPos : Name -> (dcons : List ClosedTerm) -> List Nat
+-- If a name appears more than once in an argument list, only the first is
-paramPos _ _ = [] -- TODO
+-- considered a parameter
+dropReps : List (Maybe (Term vars)) -> List (Maybe (Term vars))
+dropReps [] = []
+dropReps {vars} (Just (Local fc r x p) :: xs)
+    = Just (Local fc r x p) :: assert_total (dropReps (map toNothing xs))
+  where
+    toNothing : Maybe (Term vars) -> Maybe (Term vars)
+    toNothing tm@(Just (Local _ _ v' _))
+        = if x == v' then Nothing else tm
+    toNothing tm = tm
+dropReps (x :: xs) = x :: dropReps xs
+
+updateParams : Maybe (List (Maybe (Term vars))) ->
+                  -- arguments to the type constructor which could be
+                  -- parameters
+                  -- Nothing, as an argument, means this argument can't
+                  -- be a parameter position
+               List (Term vars) ->
+                  -- arguments to an application
+               List (Maybe (Term vars))
+updateParams Nothing args = dropReps $ map couldBeParam args
+  where
+    couldBeParam : Term vars -> Maybe (Term vars)
+    couldBeParam (Local fc r v p) = Just (Local fc r v p)
+    couldBeParam _ = Nothing
+updateParams (Just args) args' = dropReps $ zipWith mergeArg args args'
+  where
+    mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
+    mergeArg (Just (Local fc r x p)) (Local _ _ y _)
+        = if x == y then Just (Local fc r x p) else Nothing
+    mergeArg _ _ = Nothing
+
+getPs : Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
+        Maybe (List (Maybe (Term vars)))
+getPs acc tyn (Bind _ x (Pi _ _ ty) sc)
+      = let scPs = getPs (map (map (map weaken)) acc) tyn sc in
+            map (map shrink) scPs
+  where
+    shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
+    shrink Nothing = Nothing
+    shrink (Just tm) = shrinkTerm tm (DropCons SubRefl)
+getPs acc tyn tm
+    = case getFnArgs tm of
+           (Ref _ _ n, args) => 
+              if n == tyn
+                 then Just (updateParams acc args)
+                 else acc
+           _ => acc
+
+toPos : Maybe (List (Maybe a)) -> List Nat
+toPos Nothing = []
+toPos (Just ns) = justPos 0 ns
+  where
+    justPos : Nat -> List (Maybe a) -> List Nat
+    justPos i [] = []
+    justPos i (Just x :: xs) = i :: justPos (1 + i) xs
+    justPos i (Nothing :: xs) = justPos (1 + i) xs
+
+getConPs : Maybe (List (Maybe (Term vars))) -> Name -> Term vars -> List Nat
+getConPs acc tyn (Bind _ x (Pi _ _ ty) sc)
+    = let bacc = getPs acc tyn ty in
+          getConPs (map (map (map weaken)) bacc) tyn sc
+getConPs acc tyn tm = toPos (getPs acc tyn tm)
+
+combinePos : Eq a => List (List a) -> List a
+combinePos [] = []
+combinePos (xs :: xss) = filter (\x => all (elem x) xss) xs
+
+paramPos : Name -> (dcons : List ClosedTerm) ->
+           List Nat
+paramPos tyn dcons = combinePos (map (getConPs Nothing tyn) dcons)
 
 export
 addData : {auto c : Ref Ctxt Defs} ->
-					List Name -> Visibility -> DataDef -> Core Int
+					List Name -> Visibility -> Int -> DataDef -> Core Int
-addData vars vis (MkData (MkCon dfc tyn arity tycon) datacons)
+addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
     = do defs <- get Ctxt 
          tag <- getNextTypeTag 
          let tydef = newDef dfc tyn RigW vars tycon vis 
                             (TCon tag arity 
-                                  (paramPos tyn (map type datacons))
+                                  (paramPos (Resolved tidx) (map type datacons))
                                   (allDet arity)
                                   [] (map name datacons))
          (idx, gam') <- addCtxt tyn tydef (gamma defs)

src/Core/Termination.idr

@@ -513,8 +513,9 @@ calcPositive loc n
 export
 checkPositive : {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> Core Terminating
-checkPositive loc n 
+checkPositive loc n_in
-    = do tot <- getTotality loc n
+    = do n <- toResolvedNames n_in
+         tot <- getTotality loc n
          case isTerminating tot of
               Unchecked =>
                   do (tot', cons) <- calcPositive loc n

src/TTImp/Elab/Ambiguity.idr

@@ -18,31 +18,33 @@ import TTImp.TTImp
 export
 expandAmbigName : {auto c : Ref Ctxt Defs} ->
                   {auto e : Ref EST (EState vars)} ->
-                  ElabMode -> Env Term vars -> RawImp -> 
+                  ElabMode -> NestedNames vars -> Env Term vars -> RawImp -> 
                   List (FC, Maybe (Maybe Name), RawImp) -> 
                   RawImp -> Maybe (Glued vars) -> Core RawImp
-expandAmbigName (InLHS _) env orig args (IBindVar fc n) exp
+expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp
     = do est <- get EST
          if n `elem` lhsPatVars est
             then pure $ IMustUnify fc "Non linear pattern variable" orig
             else pure $ orig
-expandAmbigName mode env orig args (IVar fc x) exp
+expandAmbigName mode nest env orig args (IVar fc x) exp
-    = do defs <- get Ctxt
+   = case lookup x (names nest) of
-         -- TODO: Look up 'x' in nested names, when we have them
+          Just _ => pure orig
-         case defined x env of
+          Nothing => do
-              Just _ => 
+             defs <- get Ctxt
-                if isNil args || notLHS mode 
+             case defined x env of
-                   then pure $ orig
+                  Just _ => 
-                   else pure $ IMustUnify fc "Name applied to arguments" orig
+                    if isNil args || notLHS mode 
-              Nothing => 
+                       then pure $ orig
-                 do est <- get EST
+                       else pure $ IMustUnify fc "Name applied to arguments" orig
-                    let prims = mapMaybe id 
+                  Nothing => 
-                                  [!fromIntegerName, !fromStringName, !fromCharName]
+                     do est <- get EST
-                    case !(lookupCtxtName x (gamma defs)) of
+                        let prims = mapMaybe id 
-                         [] => pure orig
+                                      [!fromIntegerName, !fromStringName, !fromCharName]
-                         [nalt] => pure $ mkAlt prims est nalt
+                        case !(lookupCtxtName x (gamma defs)) of
-                         nalts => pure $ IAlternative fc Unique 
+                             [] => pure orig
-                                                (map (mkAlt prims est) nalts)
+                             [nalt] => pure $ mkAlt prims est nalt
+                             nalts => pure $ IAlternative fc Unique 
+                                                    (map (mkAlt prims est) nalts)
   where
     buildAlt : RawImp -> List (FC, Maybe (Maybe Name), RawImp) -> 
                RawImp
@@ -88,13 +90,13 @@ expandAmbigName mode env orig args (IVar fc x) exp
     notLHS (InLHS _) = False
     notLHS _ = True
 
-expandAmbigName mode env orig args (IApp fc f a) exp
+expandAmbigName mode nest env orig args (IApp fc f a) exp
-    = expandAmbigName mode env orig 
+    = expandAmbigName mode nest env orig 
                       ((fc, Nothing, a) :: args) f exp
-expandAmbigName mode env orig args (IImplicitApp fc f n a) exp
+expandAmbigName mode nest env orig args (IImplicitApp fc f n a) exp
-    = expandAmbigName mode env orig 
+    = expandAmbigName mode nest env orig 
                       ((fc, Just n, a) :: args) f exp
-expandAmbigName elabmode env orig args tm exp = pure orig
+expandAmbigName elabmode nest env orig args tm exp = pure orig
 
 stripDelay : Defs -> NF vars -> NF vars
 stripDelay defs (NDelayed fc r t) = t

src/TTImp/Elab/Term.idr

@@ -199,8 +199,7 @@ TTImp.Elab.Check.check rigc elabinfo nest env tm@(IUpdate fc fs rec) exp
 TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp 
     = do defs <- get Ctxt
          est <- get EST
-         tm <- expandAmbigName (elabMode elabinfo) env tm_in [] tm_in exp
+         tm <- expandAmbigName (elabMode elabinfo) nest env tm_in [] tm_in exp
-         -- TODO: insertLazy
          case elabMode elabinfo of
               InLHS _ => -- Don't expand implicit lambda on lhs
                  checkImp rigc elabinfo nest env tm exp

src/TTImp/ProcessData.idr

@@ -183,7 +183,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          cons <- traverse (checkCon eopts nest env cvis (Resolved tidx)) cons_raw
 
          let ddef = MkData (MkCon dfc n arity fullty) cons
-         addData vars vis ddef
+         addData vars vis tidx ddef
 
          -- Type is defined mutually with every data type undefined at the
          -- point it was declared, and every data type undefined right now