diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ec9aaa6..411e7fc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -6,6 +6,8 @@ beyond work on the language core, are (in no particular order): * CI integration. * Documentation string support (at the REPL and IDE mode). +* Generating HTML documentation from documentation strings (and possibly other + formations) * A better REPL, including: - `it` and `:let` - readline and tab completion diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index a6a3884..2283995 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -38,15 +38,29 @@ expandAmbigName mode nest env orig args (IVar fc x) exp else pure $ IMustUnify fc "Name applied to arguments" orig Nothing => do est <- get EST - let prims = mapMaybe id - [!fromIntegerName, !fromStringName, !fromCharName] + fi <- fromIntegerName + si <- fromStringName + ci <- fromCharName + let prims = mapMaybe id [fi, si, ci] let primApp = isPrimName prims x case !(lookupCtxtName x (gamma defs)) of [] => pure orig [nalt] => pure $ mkAlt primApp est nalt - nalts => pure $ IAlternative fc Unique + nalts => pure $ IAlternative fc (uniqType fi si ci x args) (map (mkAlt primApp est) nalts) where + -- If there's multiple alternatives and all else fails, resort to using + -- the primitive directly + uniqType : Maybe Name -> Maybe Name -> Maybe Name -> Name -> + List (FC, Maybe (Maybe Name), RawImp) -> AltType + uniqType (Just fi) _ _ n [(_, _, IPrimVal fc (BI x))] + = UniqueDefault (IPrimVal fc (BI x)) + uniqType _ (Just si) _ n [(_, _, IPrimVal fc (Str x))] + = UniqueDefault (IPrimVal fc (Str x)) + uniqType _ _ (Just ci) n [(_, _, IPrimVal fc (Ch x))] + = UniqueDefault (IPrimVal fc (Ch x)) + uniqType _ _ _ _ _ = Unique + buildAlt : RawImp -> List (FC, Maybe (Maybe Name), RawImp) -> RawImp buildAlt f [] = f