[ re #1944 ] Allow toplevel aliases (#1952)

* [ re #1944 ] Allow simple toplevel aliases
* [ done ] toplevel aliases with arguments
* [ fix ] weird nonsensical test case
* [ fix ] golden test files

src/Core/Context.idr

@@ -824,10 +824,11 @@ getFieldNames ctxt recNS
 
 -- Find similar looking names in the context
 export
-getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String)
+getSimilarNames : {auto c : Ref Ctxt Defs} ->
+                   Name -> Core (Maybe (String, List (Name, Nat)))
 getSimilarNames nm = case show <$> userNameRoot nm of
-  Nothing => pure []
-  Just str => if length str <= 1 then pure [] else
+  Nothing => pure Nothing
+  Just str => if length str <= 1 then pure (Just (str, [])) else
     let threshold : Nat := max 1 (assert_total (divNat (length str) 3))
         test : Name -> IO (Maybe Nat) := \ nm => do
             let (Just str') = show <$> userNameRoot nm
@@ -836,9 +837,14 @@ getSimilarNames nm = case show <$> userNameRoot nm of
             pure (dist <$ guard (dist <= threshold))
     in do defs <- get Ctxt
           kept <- coreLift $ mapMaybeM test (resolvedAs (gamma defs))
-          let sorted = sortBy (\ x, y => compare (snd x) (snd y)) $ toList kept
-          let roots = mapMaybe (showNames nm str . fst) sorted
-          pure (nub roots)
+          pure $ Just (str, toList kept)
+
+export
+showSimilarNames : Name -> String -> List (Name, Nat) -> List String
+showSimilarNames nm str kept
+  = let sorted = sortBy (\ x, y => compare (snd x) (snd y)) kept
+        roots  = mapMaybe (showNames nm str . fst) sorted
+    in nub roots
 
   where
 
@@ -854,7 +860,9 @@ getSimilarNames nm = case show <$> userNameRoot nm of
 maybeMisspelling : {auto c : Ref Ctxt Defs} ->
                    Error -> Name -> Core a
 maybeMisspelling err nm = do
-  candidates <- getSimilarNames nm
+  Just (str, kept) <- getSimilarNames nm
+    | Nothing => throw err
+  let candidates = showSimilarNames nm str kept
   case candidates of
     [] => throw err
     (x::xs) => throw (MaybeMisspelling err (x ::: xs))

src/Core/Options/Log.idr

@@ -70,6 +70,7 @@ knownTopics = [
     ("declare.data.constructor", Nothing),
     ("declare.data.parameters", Nothing),
     ("declare.def", Nothing),
+    ("declare.def.alias", Nothing),
     ("declare.def.clause", Nothing),
     ("declare.def.clause.impossible", Nothing),
     ("declare.def.clause.with", Nothing),

src/TTImp/Interactive/CaseSplit.idr

@@ -231,15 +231,10 @@ updateArg allvars var con (IAs fc nameFC s n p)
     = updateArg allvars var con p
 updateArg allvars var con tm = pure $ Implicit (getFC tm) True
 
-data ArgType
-    = Explicit FC RawImp
-    | Auto     FC RawImp
-    | Named    FC Name RawImp
-
 update : {auto c : Ref Ctxt Defs} ->
          List Name -> -- all the variable names
          (var : Name) -> (con : Name) ->
-         ArgType -> Core ArgType
+         Arg -> Core Arg
 update allvars var con (Explicit fc arg)
     = pure $ Explicit fc !(updateArg allvars var con arg)
 update allvars var con (Auto fc arg)
@@ -247,21 +242,6 @@ update allvars var con (Auto fc arg)
 update allvars var con (Named fc n arg)
     = pure $ Named fc n !(updateArg allvars var con arg)
 
-getFnArgs : RawImp -> List ArgType -> (RawImp, List ArgType)
-getFnArgs (IApp fc tm a) args
-    = getFnArgs tm (Explicit fc a :: args)
-getFnArgs (IAutoApp fc tm a) args
-    = getFnArgs tm (Auto fc a :: args)
-getFnArgs (INamedApp fc tm n a) args
-    = getFnArgs tm (Named fc n a :: args)
-getFnArgs tm args = (tm, args)
-
-apply : RawImp -> List ArgType -> RawImp
-apply f (Explicit fc a :: args) = apply (IApp fc f a) args
-apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
-apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
-apply f [] = f
-
 -- Return a new LHS to check, replacing 'var' with an application of 'con'
 -- Also replace any variables with '_' to allow elaboration to
 -- expand them

src/TTImp/ProcessDef.idr

@@ -24,6 +24,7 @@ import TTImp.Impossible
 import TTImp.PartialEval
 import TTImp.TTImp
 import TTImp.TTImp.Functor
+import TTImp.ProcessType
 import TTImp.Unelab
 import TTImp.Utils
 import TTImp.WithClause
@@ -889,6 +890,65 @@ warnUnreachable : {auto c : Ref Ctxt Defs} ->
 warnUnreachable (MkClause env lhs rhs)
     = recordWarning (UnreachableClause (getLoc lhs) env lhs)
 
+isAlias : RawImp -> Maybe ((FC, Name)                -- head symbol
+                          , List (FC, (FC, String))) -- pattern variables
+isAlias lhs
+  = do let (hd, apps) = getFnArgs lhs []
+       hd <- isIVar hd
+       args <- traverse (isExplicit >=> bitraverse pure isIBindVar) apps
+       pure (hd, args)
+
+lookupOrAddAlias : {vars : _} ->
+                   {auto m : Ref MD Metadata} ->
+                   {auto c : Ref Ctxt Defs} ->
+                   {auto u : Ref UST UState} ->
+                   List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
+                   Name -> List ImpClause -> Core (Maybe GlobalDef)
+lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)]
+  = do defs <- get Ctxt
+       log "declare.def.alias" 20 $ "Looking at \{show cl}"
+       Nothing <- lookupCtxtExact n (gamma defs)
+         | Just gdef => pure (Just gdef)
+       -- No prior declaration:
+       --   1) check whether it has the shape of an alias
+       let Just (hd, args) = isAlias lhs
+         | Nothing => pure Nothing
+       --   2) check whether it could be a misspelling
+       log "declare.def" 5 $
+         "Missing type declaration for the alias "
+         ++ show n
+         ++ ". Checking first whether it is a misspelling."
+       [] <- do -- get the candidates
+                Just (str, kept) <- getSimilarNames n
+                   | Nothing => pure []
+                -- only keep the ones that haven't been defined yet
+                decls <- for kept $ \ (cand, weight) => do
+                    Just gdef <- lookupCtxtExact cand (gamma defs)
+                      | Nothing => pure Nothing -- should be impossible
+                    let None = definition gdef
+                      | _ => pure Nothing
+                    pure (Just (cand, weight))
+                pure $ showSimilarNames n str $ catMaybes decls
+          | (x :: xs) => throw (MaybeMisspelling (NoDeclaration fc n) (x ::: xs))
+       --   3) declare an alias
+       log "declare.def" 5 "Not a misspelling: go ahead and declare it!"
+       processType eopts nest env fc top Public []
+          $ MkImpTy fc fc n $ holeyType (map snd args)
+       defs <- get Ctxt
+       lookupCtxtExact n (gamma defs)
+
+  where
+    holeyType : List (FC, String) -> RawImp
+    holeyType [] = Implicit fc False
+    holeyType ((xfc, x) :: xs)
+      = let xfc = virtualiseFC xfc in
+        IPi xfc top Explicit (Just (UN $ Basic x)) (Implicit xfc False)
+      $ holeyType xs
+
+lookupOrAddAlias _ _ _ fc n _
+  = do defs <- get Ctxt
+       lookupCtxtExact n (gamma defs)
+
 export
 processDef : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
@@ -899,8 +959,8 @@ processDef : {vars : _} ->
 processDef opts nest env fc n_in cs_in
     = do n <- inCurrentNS n_in
          defs <- get Ctxt
-         Just gdef <- lookupCtxtExact n (gamma defs)
-              | Nothing => noDeclaration fc n
+         Just gdef <- lookupOrAddAlias opts nest env fc n cs_in
+           | Nothing => noDeclaration fc n
          let None = definition gdef
               | _ => throw (AlreadyDefined fc n)
          let ty = type gdef

src/TTImp/TTImp.idr

@@ -732,6 +732,16 @@ definedInBlock ns decls =
     defName ns (IPragma pns _) = map (expandNS ns) pns
     defName _ _ = []
 
+export
+isIVar : RawImp' nm -> Maybe (FC, nm)
+isIVar (IVar fc v) = Just (fc, v)
+isIVar _ = Nothing
+
+export
+isIBindVar : RawImp' nm -> Maybe (FC, String)
+isIBindVar (IBindVar fc v) = Just (fc, v)
+isIBindVar _ = Nothing
+
 export
 getFC : RawImp' nm -> FC
 getFC (IVar x _) = x
@@ -785,6 +795,53 @@ namespace ImpDecl
   getFC (ILog _) = EmptyFC
   getFC (IBuiltin fc _ _) = fc
 
+public export
+data Arg' nm
+   = Explicit FC (RawImp' nm)
+   | Auto     FC (RawImp' nm)
+   | Named    FC Name (RawImp' nm)
+
+public export
+Arg : Type
+Arg = Arg' Name
+
+public export
+IArg : Type
+IArg = Arg' KindedName
+
+export
+isExplicit : Arg' nm -> Maybe (FC, RawImp' nm)
+isExplicit (Explicit fc t) = Just (fc, t)
+isExplicit _ = Nothing
+
+export
+unIArg : Arg' nm -> RawImp' nm
+unIArg (Explicit _ t) = t
+unIArg (Auto _ t) = t
+unIArg (Named _ _ t) = t
+
+export
+Show nm => Show (Arg' nm) where
+  show (Explicit fc t) = show t
+  show (Auto fc t) = "@{" ++ show t ++ "}"
+  show (Named fc n t) = "{" ++ show n ++ " = " ++ show t ++ "}"
+
+export
+getFnArgs : RawImp' nm -> List (Arg' nm) -> (RawImp' nm, List (Arg' nm))
+getFnArgs (IApp fc f arg) args = getFnArgs f (Explicit fc arg :: args)
+getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
+getFnArgs (IAutoApp fc f arg) args = getFnArgs f (Auto fc arg :: args)
+getFnArgs tm args = (tm, args)
+
+-- TODO: merge these definitions
+namespace Arg
+  export
+  apply : RawImp' nm -> List (Arg' nm) -> RawImp' nm
+  apply f (Explicit fc a :: args) = apply (IApp fc f a) args
+  apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
+  apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
+  apply f [] = f
+
 export
 apply : RawImp' nm -> List (RawImp' nm) -> RawImp' nm
 apply f [] = f

src/TTImp/Unelab.idr

@@ -32,27 +32,6 @@ used idx (TDelay _ _ _ tm) = used idx tm
 used idx (TForce _ _ tm) = used idx tm
 used idx _ = False
 
-data IArg
-   = Exp FC IRawImp
-   | Auto FC IRawImp
-   | Named FC Name IRawImp
-
-unIArg : IArg -> IRawImp
-unIArg (Exp _ t) = t
-unIArg (Auto _ t) = t
-unIArg (Named _ _ t) = t
-
-Show IArg where
-  show (Exp fc t) = show t
-  show (Auto fc t) = "@{" ++ show t ++ "}"
-  show (Named fc n t) = "{" ++ show n ++ " = " ++ show t ++ "}"
-
-getFnArgs : IRawImp -> List IArg -> (IRawImp, List IArg)
-getFnArgs (IApp fc f arg) args = getFnArgs f (Exp fc arg :: args)
-getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
-getFnArgs (IAutoApp fc f arg) args = getFnArgs f (Auto fc arg :: args)
-getFnArgs tm args = (tm, args)
-
 data UnelabMode
      = Full
      | NoSugar Bool -- uniqify names
@@ -116,7 +95,7 @@ mutual
       mkCase : List (vs ** (Env Term vs, Term vs, Term vs)) ->
                Nat -> Nat -> List IArg -> Core IRawImp
       mkCase pats (S k) dropped (_ :: args) = mkCase pats k (S dropped) args
-      mkCase pats Z dropped (Exp fc tm :: _)
+      mkCase pats Z dropped (Explicit fc tm :: _)
           = do pats' <- traverse (mkClause fc dropped) pats
                pure $ ICase fc tm (Implicit fc False) pats'
       mkCase _ _ _ _ = pure orig
@@ -154,7 +133,7 @@ mutual
     where
       apply : IRawImp -> List IArg -> IRawImp
       apply tm [] = tm
-      apply tm (Exp fc a :: args) = apply (IApp fc tm a) args
+      apply tm (Explicit fc a :: args) = apply (IApp fc tm a) args
       apply tm (Auto fc a :: args) = apply (IAutoApp fc tm a) args
       apply tm (Named fc n a :: args) = apply (INamedApp fc tm n a) args
 

tests/Main.idr

@@ -41,7 +41,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic046", "basic047",             "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
-       "basic061", "basic062",
+       "basic061", "basic062", "basic063",
        "interpolation001", "interpolation002", "interpolation003"]
 
 idrisTestsCoverage : TestPool

tests/idris2/basic063/NoDeclaration.idr

@@ -0,0 +1,23 @@
+module NoDeclaration
+
+identity : (a : Type) -> a -> a
+identity _ x = x
+
+idNat = identity Nat
+
+double = (S 1 *)
+
+test : idNat (double 3) === 6
+test = Refl
+
+unwords : List String -> String
+unwords [] = ""
+unwords [x] = x
+unwords (x::xs) = x ++ " " ++ unwords xs
+
+helloWorld = unwords ["hello", "world"]
+
+test' : NoDeclaration.helloWorld === "hello world"
+test' = Refl
+
+cat x y = unwords [x, show {ty = Nat} y]

tests/idris2/basic063/expected

@@ -0,0 +1,7 @@
+1/1: Building NoDeclaration (NoDeclaration.idr)
+NoDeclaration> NoDeclaration.idNat : Nat -> Nat
+NoDeclaration> NoDeclaration.double : Nat -> Nat
+NoDeclaration> NoDeclaration.helloWorld : String
+NoDeclaration> NoDeclaration.cat : String -> Nat -> String
+NoDeclaration> 
+Bye for now!

tests/idris2/basic063/input

@@ -0,0 +1,5 @@
+:t idNat
+:t double
+:t helloWorld
+:t cat
+:q

tests/idris2/basic063/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner NoDeclaration.idr < input

tests/idris2/error016/expected

@@ -8,7 +8,7 @@ Issue1230:9:1--9:15
  8 | mkRec2 : R
  9 | myRec2 = MkR 3
      ^^^^^^^^^^^^^^
-Did you mean any of: mkRec2, or myRec1?
+Did you mean: mkRec2?
 Main> Error: Undefined name nap. 
 
 (Interactive):1:4--1:7

tests/idris2/import002/expected

@@ -11,14 +11,13 @@ Test:5:9--5:12
  5 | thing : Nat -> Nat
              ^^^
 
-Error: No type declaration for Test.thing.
+Error: While processing right hand side of thing. Undefined name plus. 
 
-Test:6:1--6:28
+Test:6:19--6:23
  2 | 
  3 | import Mult
  4 | 
  5 | thing : Nat -> Nat
  6 | thing x = mult x (plus x x)
-     ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+                       ^^^^
 
-Test> Bye for now!

tests/idris2/import002/run

@@ -1,4 +1,3 @@
 rm -rf build
 
-echo ':q' | $1 --no-color --console-width 0 --no-banner --no-prelude Test.idr
-
+$1 --no-color --console-width 0 --no-banner --no-prelude --check Test.idr

tests/idris2/reg003/expected

@@ -1,70 +1,24 @@
 1/1: Building Holes (Holes.idr)
-Error: While processing type of Vect_ext. Undefined name ~=~. 
+Warning: Unreachable clause: f True
 
-Holes:4:64--4:85
- 1 | import Data.Vect
- 2 | import Data.Fin
- 3 | 
- 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
-                                                                    ^^^^^^^^^^^^^^^^^^^^^
-
-Error: While processing type of Weird. Undefined name ~=~. 
-
-Holes:7:26--7:31
- 3 | 
- 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
- 5 |   -> v = w
- 6 | 
- 7 | Weird : (v: Vect n a) -> v = v
-                              ^^^^^
-
-Error: No type declaration for Main.Weird.
-
-Holes:8:1--8:41
- 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
- 5 |   -> v = w
- 6 | 
- 7 | Weird : (v: Vect n a) -> v = v
- 8 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
-     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-Error: While processing type of f. Undefined name Bool. 
-
-Holes:10:5--10:9
- 06 | 
- 07 | Weird : (v: Vect n a) -> v = v
- 08 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
- 09 | 
- 10 | f : Bool -> Nat
-          ^^^^
-
-Error: No type declaration for Main.f.
-
-Holes:11:1--11:11
- 07 | Weird : (v: Vect n a) -> v = v
+Holes:12:1--12:7
  08 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
  09 | 
  10 | f : Bool -> Nat
  11 | f True = 0
-      ^^^^^^^^^^
+ 12 | f True = ?help
+      ^^^^^^
 
-Main> Error: Undefined name help. 
-
-(Interactive):1:4--1:8
- 1 | :t help
-        ^^^^
-
-Main> Error: Undefined name hole0. 
-
-(Interactive):1:4--1:9
- 1 | :t hole0
-        ^^^^^
-
-Main> Error: Undefined name hole1. 
-
-(Interactive):1:4--1:9
- 1 | :t hole1
-        ^^^^^
-
-Main> Unknown name hole1
+Main> Main.help : Nat
+Main>  0 a : Type
+ 0 n : Nat
+   v : Vect n a
+------------------------------
+hole0 : Vect n a
+Main>  0 a : Type
+ 0 n : Nat
+   v : Vect n a
+------------------------------
+hole1 : Vect n a
+Main> v
 Main> Bye for now!

tests/idris2/reg003/run

@@ -1,4 +1,3 @@
 rm -rf build
 
-$1 --no-color --console-width 0 --no-banner --no-prelude Holes.idr < input
-
+$1 --no-color --console-width 0 --no-banner Holes.idr < input