Method refactor

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2025_08_13_00
+ttcVersion = 2025_08_16_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/WithData.idr

@@ -34,7 +34,7 @@ public export
 WithArity : Type -> Type
 WithArity = AddMetadata Arity'
 
-||| Obtain totality information from the metadata
+||| Obtain arity information from the metadata
 export
 (.arity) :
     {n : Nat} ->
@@ -54,7 +54,7 @@ public export
 WithOpts : Type -> Type
 WithOpts = AddMetadata Opts'
 
-||| Obtain totality information from the metadata
+||| Obtain data options from the metadata
 export
 (.opts) :
     {n : Nat} ->
@@ -189,6 +189,13 @@ export
           WithData fields a -> WithFC Name
 (.name) = WithData.get "name" @{inRange}
 
+||| Extract the name out of the metadata.
+export
+(.nameVal) : {n : Nat} ->
+          (inRange : NameInRange "name" fields === Just (n, WithFC Name)) =>
+          WithData fields a -> Name
+(.nameVal) x = x.name.val
+
 ||| Attach name and file context information to a type
 public export
 WithName : Type -> Type

src/Idris/Desugar.idr

@@ -1195,7 +1195,7 @@ mutual
            let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'
 
            body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
-           pure [IPragma int.fc (maybe [tn] (\n => [tn, snd n]) conname)
+           pure [IPragma int.fc (maybe [tn] (\n => [tn, n.val]) conname)
                             (\nest, env =>
                               elabInterface int.fc vis env nest consb
                                             tn paramsb det conname
@@ -1291,8 +1291,8 @@ mutual
                                              (mkNamespace recName))
                                fields
            let _ = the (List $ List IField) fields'
-           let conname = maybe (mkConName tn) snd conname_in
-           whenJust (fst <$> conname_in) (addDocString conname)
+           let conname = maybe (mkConName tn) val conname_in
+           whenJust (get "doc" <$> conname_in) (addDocString conname)
            let _ = the Name conname
            pure [IRecord rec.fc (Just recName)
                          vis mbtot (Mk [rec.fc] $ MkImpRecord (Mk [NoFC tn] paramsb) (Mk [NoFC conname, opts] (concat fields')))]

src/Idris/Doc/String.idr

@@ -310,7 +310,7 @@ getDocsForName fc n config
     getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
     getMethDoc meth
         = do syn <- get Syn
-             let [nstr] = lookupName meth.name (defDocstrings syn)
+             let [nstr] = lookupName meth.name.val (defDocstrings syn)
                   | _ => pure []
              pure <$> showDoc methodsConfig nstr
 

src/Idris/Elab/Implementation.idr

@@ -52,7 +52,7 @@ bindConstraints fc p ((n, ty) :: rest) sc
 bindImpls : List (AddFC (ImpParameter' RawImp)) -> RawImp -> RawImp
 bindImpls [] ty = ty
 bindImpls (binder :: rest) sc
-    = IPi binder.fc binder.rig binder.val.info (Just binder.name.val) binder.val.boundType (bindImpls rest sc)
+    = IPi binder.fc binder.rig binder.val.info (Just binder.nameVal) binder.val.boundType (bindImpls rest sc)
 
 addDefaults : FC -> Name ->
               (params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
@@ -163,7 +163,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                  ++ "\n  specialised to: " ++ show ps
                  ++ "\n  and parents: " ++ show (parents cdata)
                  ++ "\n  using implicits: " ++ show impsp
-                 ++ "\n  and methods: " ++ show (methods cdata) ++ "\n"
+                 ++ "\n  and methods: " ++ show (map val (methods cdata)) ++ "\n"
                  ++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"
          logTerm "elab.implementation" 3 "Constructor type: " conty
          log "elab.implementation" 5 $ "Making implementation " ++ show impName
@@ -223,7 +223,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                let (body, missing)
                      = addDefaults vfc impName
                                       (zip (params cdata) ps)
-                                      (map (dropNS . name) (methods cdata))
+                                      (map (dropNS . (.nameVal)) (methods cdata))
                                       (defaults cdata) body_in
 
                log "elab.implementation" 5 $ "Added defaults: body is " ++ show body
@@ -243,7 +243,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                defs <- get Ctxt
                fns <- topMethTypes [] impName methImps impsp
                                       (implParams cdata) (params cdata)
-                                      (map name (methods cdata))
+                                      (map (.nameVal) (methods cdata))
                                       (methods cdata)
                traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
 
@@ -405,14 +405,14 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
     topMethType methupds impName methImps impsp imppnames pnames allmeths meth
         = do -- Get the specialised type by applying the method to the
              -- parameters
-             n <- inCurrentNS (methName meth.name)
+             n <- inCurrentNS (methName meth.nameVal)
              let varsList = toList vars
 
              -- Avoid any name clashes between parameters and method types by
              -- renaming IBindVars in the method types which appear in the
              -- parameters
              let upds' = !(traverse (applyCon impName) allmeths)
-             let mty_in = substNames varsList upds' meth.type
+             let mty_in = substNames varsList upds' meth.val
              let (upds, mty_in) = runState [] (renameIBinds impsp (findImplicits mty_in) mty_in)
              -- Finally update the method type so that implicits from the
              -- parameters are passed through to any earlier methods which
@@ -440,7 +440,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
              mty <- bindTypeNamesUsed ifc ibound varsList mbase
 
              log "elab.implementation" 3 $
-                     "Method " ++ show meth.name ++ " ==> " ++
+                     "Method " ++ show meth.nameVal ++ " ==> " ++
                      show n ++ " : " ++ show mty
              log "elab.implementation" 3 $ "    (initially " ++ show mty_in ++ ")"
              log "elab.implementation" 5 $ "Updates " ++ show methupds
@@ -453,7 +453,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                              else [(n, impsApply (IVar vfc n)
                                      (map (\x => (x, IBindVar vfc x)) ibinds))]
 
-             pure ((meth.name, n, upds, meth.count, meth.totalReq, mty), methupds')
+             pure ((meth.nameVal, n, upds, meth.rig, meth.totReq, mty), methupds')
 
     topMethTypes : List (Name, RawImp) ->
                    Name -> List (Name, RigCount, Maybe RawImp, RawImp) ->
@@ -537,18 +537,18 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                    Core ()
     addTransform iname ns meth
         = do log "elab.implementation" 3 $
-                     "Adding transform for " ++ show meth.name ++ " : " ++ show meth.type ++
+                     "Adding transform for " ++ show meth.nameVal ++ " : " ++ show meth.val ++
                      "\n\tfor " ++ show iname ++ " in " ++ show ns
-             let lhs = INamedApp vfc (IVar vfc meth.name)
+             let lhs = INamedApp vfc (IVar vfc meth.name.val)
                                      (UN $ Basic "__con")
                                      (IVar vfc iname)
-             let Just mname = lookup (dropNS meth.name) ns
+             let Just mname = lookup (dropNS meth.nameVal) ns
                  | Nothing => pure ()
              let rhs = IVar vfc mname
              log "elab.implementation" 5 $ show lhs ++ " ==> " ++ show rhs
              handleUnify
                  (processDecl [] nest env
-                     (ITransform vfc (UN $ Basic (show meth.name ++ " " ++ show iname)) lhs rhs))
+                     (ITransform vfc (UN $ Basic (show meth.nameVal ++ " " ++ show iname)) lhs rhs))
                  (\err =>
                      log "elab.implementation" 5 $ "Can't add transform " ++
                                 show lhs ++ " ==> " ++ show rhs ++

src/Idris/Elab/Interface.idr

@@ -68,26 +68,6 @@ getSig (IData _ _ _ (MkImpLater fc n ty))
 getSig _ = Nothing
 
 ------------------------------------------------------------------------
--- Declaration
-
-record Declaration where
-  constructor MkDeclaration
-  name   : Name
-  count  : RigCount
-  flags  : List FnOpt
-  isData : Bool
-  type   : RawImp
-
-sigToDecl : Signature -> Declaration
-sigToDecl sig = MkDeclaration
-  { name = sig.name.val
-  , count = sig.count
-  , flags = sig.flags
-  , isData = sig.isData
-  , type = sig.type
-  }
-
-------------------------------------------------------------------------
 
 
 -- TODO: Check all the parts of the body are legal
@@ -282,22 +262,18 @@ mkCon loc n
 updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  Name -> Name -> List Name -> List Name -> List RawImp ->
-                 List Declaration -> List (Name, List ImpClause) ->
+                 List Signature -> List (Name, List ImpClause) ->
                  Core ()
 updateIfaceSyn iname cn impps ps cs ms ds
     = do ms' <- traverse totMeth ms
          let info = MkIFaceInfo cn impps ps cs ms' ds
          update Syn { ifaces     $= addName iname info,
                       saveIFaces $= (iname :: ) }
  where
-    totMeth : Declaration -> Core Method
+    totMeth : Signature -> Core Method
     totMeth decl
         = do let treq = findTotality decl.flags
-             pure $ MkMethod { name = decl.name
-                             , count = decl.count
-                             , totalReq = treq
-                             , type = decl.type
-                             }
+             pure $ Mk [decl.name, decl.count, treq] decl.type
 
 -- Read the implicitly added parameters from an interface type, so that we
 -- know to substitute an implicit in when defining the implementation
@@ -319,27 +295,27 @@ elabInterface : {vars : _} ->
                 Name ->
                 (params : List (Name, (RigCount, RawImp))) ->
                 (dets : Maybe (List1 Name)) ->
-                (conName : Maybe (String, Name)) ->
+                (conName : Maybe (WithDoc $ AddFC Name)) ->
                 List ImpDecl ->
                 Core ()
 elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon body
     = do fullIName <- getFullName iname
          ns_iname <- inCurrentNS fullIName
-         let conName_in = maybe (mkCon vfc fullIName) snd mcon
+         let conName_in = maybe (mkCon vfc fullIName) val mcon
          -- Machine generated names need to be qualified when looking them up
          conName <- inCurrentNS conName_in
-         whenJust (fst <$> mcon) (addDocString conName)
+         whenJust (get "doc" <$> mcon) (addDocString conName)
          let meth_sigs = mapMaybe getSig body
-         let meth_decls = map sigToDecl meth_sigs
-         let meth_names = map name meth_decls
+         let meth_decls = meth_sigs
+         let meth_names = map (val . name) meth_decls
          let defaults = mapMaybe getDefault body
 
          elabAsData conName meth_names meth_sigs
          elabConstraintHints conName meth_names
          elabMethods conName meth_names meth_sigs
          ds <- traverse (elabDefault meth_decls) defaults
 
-         ns_meths <- traverse (\mt => do n <- inCurrentNS mt.name
+         ns_meths <- traverse (\mt => do n <- traverse inCurrentNS mt.name
                                          pure ({ name := n } mt)) meth_decls
          defs <- get Ctxt
          Just ty <- lookupTyExact ns_iname (gamma defs)
@@ -404,7 +380,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod
     -- Check that a default definition is correct. We just discard it here once
     -- we know it's okay, since we'll need to re-elaborate it for each
     -- instance, to specialise it
-    elabDefault : List Declaration ->
+    elabDefault : List Signature ->
                   (FC, List FnOpt, Name, List ImpClause) ->
                   Core (Name, List ImpClause)
     elabDefault tydecls (dfc, opts, n, cs)
@@ -414,7 +390,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod
              dn <- inCurrentNS dn_in
 
              (rig, dty) <-
-                       case findBy (\ d => d <$ guard (n == d.name)) tydecls of
+                       case findBy (\ d => d <$ guard (n == d.name.val)) tydecls of
                           Just d => pure (d.count, d.type)
                           Nothing => throw (GenericMsg dfc ("No method named " ++ show n ++ " in interface " ++ show iname))
 
@@ -423,15 +399,15 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod
              -- Substitute the method names with their top level function
              -- name, so they don't get implicitly bound in the name
              methNameMap <- traverse (\d =>
-                                do let n = d.name
+                                do let n = d.name.val
                                    cn <- inCurrentNS n
                                    pure (n, applyParams (IVar vdfc cn) paramNames))
                                tydecls
              let dty = bindPs params      -- bind parameters
                      $ bindIFace vdfc ity -- bind interface (?!)
                      $ substNames (toList vars) methNameMap dty
 
-             dty_imp <- bindTypeNames dfc [] (map name tydecls ++ toList vars) dty
+             dty_imp <- bindTypeNames dfc [] (map (val . name) tydecls ++ toList vars) dty
              log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
 
              let dtydecl = IClaim $ MkFCVal vdfc

src/Idris/Parser.idr

@@ -1664,12 +1664,12 @@ getVisibility (Just vis) (Left x :: xs)
    = fatalError "Multiple visibility modifiers"
 getVisibility v (_ :: xs) = getVisibility v xs
 
-recordConstructor : OriginDesc -> Rule (String, Name)
+recordConstructor : OriginDesc -> Rule (WithDoc $ AddFC Name)
 recordConstructor fname
   = do doc <- optDocumentation fname
        decorate fname Keyword $ exactIdent "constructor"
-       n <- mustWork $ decoratedDataConstructorName fname
-       pure (doc, n)
+       n <- fcBounds $ mustWork $ decoratedDataConstructorName fname
+       pure (doc :+ n)
 
 autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t)
 autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto"

src/Idris/Resugar.idr

@@ -522,7 +522,7 @@ mutual
       = do ps' <- traverse (traverse (traverse (toPTerm startPrec))) header.val
            fs' <- traverse toPField body.val
            pure (Just (MkFCVal fc $ PRecord "" vis mbtot
-                          (MkPRecord header.name.val (map toBinder ps') body.opts (Just ("", body.name.val)) fs')))
+                          (MkPRecord header.name.val (map toBinder ps') body.opts (Just (AddDef body.name)) fs')))
            where
              toBinder : ImpParameter' (PTerm' KindedName) -> PBinder' KindedName
              toBinder binder

src/Idris/Syntax.idr

@@ -402,7 +402,7 @@ mutual
        MkPRecord : (tyname : Name) ->
                    (params : List (PBinder' nm)) ->
                    (opts : List DataOpt) ->
-                   (conName : Maybe (String, Name)) ->
+                   (conName : Maybe (WithDoc $ AddFC Name)) ->
                    (decls : List (PField' nm)) ->
                    PRecordDecl' nm
        MkPRecordLater : (tyname : Name) ->
@@ -568,7 +568,7 @@ mutual
                     (doc : String) ->
                     (params : List (BasicMultiBinder' nm)) ->
                     (det : Maybe (List1 Name)) ->
-                    (conName : Maybe (String, Name)) ->
+                    (conName : Maybe (WithDoc $ AddFC Name)) ->
                     List (PDecl' nm) ->
                     PDeclNoFC' nm
        PImplementation : Visibility -> List PFnOpt -> Pass ->
@@ -1014,19 +1014,9 @@ covering
 Show IPTerm where
   showPrec = showPTermPrec rawName
 
-public export
-record Method where
-  constructor MkMethod
-  name     : Name
-  count    : RigCount
-  totalReq : Maybe TotalReq
-  type     : RawImp
-
-export
-covering
-Show Method where
-  show (MkMethod n c treq ty)
-    = "[" ++ show treq ++ "] " ++ show c ++ " " ++ show n ++ " : " ++ show ty
+public export 0
+Method : Type
+Method = WithName $ WithRig $ AddMetadata Tot' $ RawImp
 
 public export
 record IFaceInfo where

src/Idris/Syntax/TTC.idr

@@ -16,23 +16,6 @@ import Libraries.Data.StringMap
 
 %default covering
 
-
-export
-TTC Method where
-  toBuf (MkMethod nm c treq ty)
-      = do toBuf nm
-           toBuf c
-           toBuf treq
-           toBuf ty
-
-  fromBuf
-      = do nm <- fromBuf
-           c <- fromBuf
-           treq <- fromBuf
-           ty <- fromBuf
-           pure (MkMethod nm c treq ty)
-
-
 export
 TTC IFaceInfo where
   toBuf (MkIFaceInfo ic impps ps cs ms ds)