diff --git a/README.md b/README.md index 95d8b67..28c0b26 100644 --- a/README.md +++ b/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*. diff --git a/src/Core/Context.idr b/src/Core/Context.idr index e27e1fe..4879a0d 100644 --- a/src/Core/Context.idr +++ b/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 - ++ " with " ++ show ms + = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ + " constructors: " ++ show cons ++ + " mutual with: " ++ show ms show (ExternDef arity) = "" show (Builtin {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 -paramPos _ _ = [] -- TODO +-- If a name appears more than once in an argument list, only the first is +-- 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 -addData vars vis (MkData (MkCon dfc tyn arity tycon) datacons) + List Name -> Visibility -> Int -> DataDef -> Core Int +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) diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index 74bbdfc..2422ca8 100644 --- a/src/Core/Termination.idr +++ b/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 - = do tot <- getTotality loc n +checkPositive loc n_in + = do n <- toResolvedNames n_in + tot <- getTotality loc n case isTerminating tot of Unchecked => do (tot', cons) <- calcPositive loc n diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 95372f7..3fd53a6 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/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 - = do defs <- get Ctxt - -- TODO: Look up 'x' in nested names, when we have them - case defined x env of - Just _ => - if isNil args || notLHS mode - then pure $ orig - else pure $ IMustUnify fc "Name applied to arguments" orig - Nothing => - do est <- get EST - let prims = mapMaybe id - [!fromIntegerName, !fromStringName, !fromCharName] - case !(lookupCtxtName x (gamma defs)) of - [] => pure orig - [nalt] => pure $ mkAlt prims est nalt - nalts => pure $ IAlternative fc Unique - (map (mkAlt prims est) nalts) +expandAmbigName mode nest env orig args (IVar fc x) exp + = case lookup x (names nest) of + Just _ => pure orig + Nothing => do + defs <- get Ctxt + case defined x env of + Just _ => + if isNil args || notLHS mode + then pure $ orig + else pure $ IMustUnify fc "Name applied to arguments" orig + Nothing => + do est <- get EST + let prims = mapMaybe id + [!fromIntegerName, !fromStringName, !fromCharName] + case !(lookupCtxtName x (gamma defs)) of + [] => pure orig + [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 env orig +expandAmbigName mode nest env orig args (IApp fc f a) exp + = expandAmbigName mode nest env orig ((fc, Nothing, a) :: args) f exp -expandAmbigName mode env orig args (IImplicitApp fc f n a) exp - = expandAmbigName mode env orig +expandAmbigName mode nest env orig args (IImplicitApp fc f n a) exp + = 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 diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index be986a3..bc03b67 100644 --- a/src/TTImp/Elab/Term.idr +++ b/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 - -- TODO: insertLazy + tm <- expandAmbigName (elabMode elabinfo) nest env tm_in [] tm_in exp case elabMode elabinfo of InLHS _ => -- Don't expand implicit lambda on lhs checkImp rigc elabinfo nest env tm exp diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 5b0d5bb..43d34f7 100644 --- a/src/TTImp/ProcessData.idr +++ b/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