diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 9161ecfcb56..af4f19ed2ba 100644 --- a/src/Core/Binary.idr +++ b/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 () diff --git a/src/Core/WithData.idr b/src/Core/WithData.idr index 1701e2eecd2..64483f57313 100644 --- a/src/Core/WithData.idr +++ b/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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index a1a90914d77..7fa14e4827f 100644 --- a/src/Idris/Desugar.idr +++ b/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')))] diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index bbe4a2892f7..9012f3c9ce9 100644 --- a/src/Idris/Doc/String.idr +++ b/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 diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 9751f6ee732..aebba49e42d 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/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 ++ diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 50bd4dd3901..a75e50953ef 100644 --- a/src/Idris/Elab/Interface.idr +++ b/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,7 +262,7 @@ 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 @@ -290,14 +270,10 @@ updateIfaceSyn iname 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,19 +295,19 @@ 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 @@ -339,7 +315,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod 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,7 +399,7 @@ 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 @@ -431,7 +407,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod $ 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 diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f1c5aad520e..b83f6636c12 100644 --- a/src/Idris/Parser.idr +++ b/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" diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index f346928b053..bbdaec1b411 100644 --- a/src/Idris/Resugar.idr +++ b/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 diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index fae1f96612c..0ee2b7ff979 100644 --- a/src/Idris/Syntax.idr +++ b/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 diff --git a/src/Idris/Syntax/TTC.idr b/src/Idris/Syntax/TTC.idr index bc46054fc94..b04b8b25078 100644 --- a/src/Idris/Syntax/TTC.idr +++ b/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)