From 917fa74366fd129e954382bd76fc1891d1aff814 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 1 Apr 2022 14:19:53 -0400 Subject: [PATCH] doc: docstrings for decls and attributes Co-authored-by: Sebastian Ullrich --- src/Lean/Attributes.lean | 1 + src/Lean/CoreM.lean | 10 ++++++ src/Lean/Declaration.lean | 62 ++++++++++++++++++++++---------- src/Lean/Elab/DeclModifiers.lean | 3 ++ src/Lean/ResolveName.lean | 49 +++++++++++++++++++++++-- 5 files changed, 103 insertions(+), 22 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 3d88eb4e1a..4ed5757294 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -35,6 +35,7 @@ instance : ToString AttributeKind where | AttributeKind.scoped => "scoped" structure AttributeImpl extends AttributeImplCore where + /-- This is run when the attribute is applied to a declaration `decl`. `stx` is the syntax of the attribute including arguments. -/ add (decl : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased" deriving Inhabited diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 6e59a4e013..1df51fc914 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -31,6 +31,7 @@ structure Cache where instLevelValue : InstantiateLevelCache := {} deriving Inhabited +/-- State for the CoreM monad. -/ structure State where env : Environment nextMacroScope : MacroScope := firstFrontendMacroScope + 1 @@ -39,6 +40,7 @@ structure State where cache : Cache := {} deriving Inhabited +/-- Context for the CoreM monad. -/ structure Context where options : Options := {} currRecDepth : Nat := 0 @@ -50,6 +52,14 @@ structure Context where maxHeartbeats : Nat := getMaxHeartbeats options currMacroScope : MacroScope := firstFrontendMacroScope +/-- CoreM is a monad for manipulating the Lean environment. +It is the base monad for `MetaM`. +The main features it provides are: +- name generator state +- environment state +- Lean options context +- the current open namespace +-/ abbrev CoreM := ReaderT Context <| StateRefT State (EIO Exception) -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index d01bc64e40..d1c0eba660 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -192,13 +192,23 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool A series of checks are performed by the kernel to check whether a `inductiveDecls` is valid or not. -/ structure InductiveVal extends ConstantVal where - numParams : Nat -- Number of parameters - numIndices : Nat -- Number of indices - all : List Name -- List of all (including this one) inductive datatypes in the mutual declaration containing this one - ctors : List Name -- List of all constructors for this inductive datatype - isRec : Bool -- `true` Iff it is recursive + /-- Number of parameters. A parameter is an argument to the defined type that is fixed over constructors. -/ + numParams : Nat + /-- Number of indices. An index is an argument that varies over constructors. + + An example of this is the `n : Nat` argument in the vector constructor `cons : α → Vector α n → Vector α (n+1)` -/ + numIndices : Nat + /-- List of all (including this one) inductive datatypes in the mutual declaration containing this one -/ + all : List Name + /-- List of the names of the constructors for this inductive datatype. -/ + ctors : List Name + /-- `true` when recursive (that is, the inductive type appears as an argument in a constructor). -/ + isRec : Bool + /-- Whether the definition is flagged as unsafe. -/ isUnsafe : Bool isReflexive : Bool + /-- An inductive definition `T` is nested when there is a constructor with an argument `x : F T`, + where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...). -/ isNested : Bool deriving Inhabited @@ -226,10 +236,14 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length structure ConstructorVal extends ConstantVal where - induct : Name -- Inductive Type this Constructor is a member of - cidx : Nat -- Constructor index (i.e., Position in the inductive declaration) - numParams : Nat -- Number of parameters in inductive datatype `induct` - numFields : Nat -- Number of fields (i.e., arity - nparams) + /-- Inductive type this constructor is a member of -/ + induct : Name + /-- Constructor index (i.e., Position in the inductive declaration) -/ + cidx : Nat + /-- Number of parameters in inductive datatype. -/ + numParams : Nat + /-- Number of fields (i.e., arity - nparams) -/ + numFields : Nat isUnsafe : Bool deriving Inhabited @@ -249,19 +263,29 @@ def mkConstructorValEx (name : Name) (levelParams : List Name) (type : Expr) (in /-- Information for reducing a recursor -/ structure RecursorRule where - ctor : Name -- Reduction rule for this Constructor - nfields : Nat -- Number of fields (i.e., without counting inductive datatype parameters) - rhs : Expr -- Right hand side of the reduction rule + /-- Reduction rule for this Constructor -/ + ctor : Name + /-- Number of fields (i.e., without counting inductive datatype parameters) -/ + nfields : Nat + /-- Right hand side of the reduction rule -/ + rhs : Expr deriving Inhabited structure RecursorVal extends ConstantVal where - all : List Name -- List of all inductive datatypes in the mutual declaration that generated this recursor - numParams : Nat -- Number of parameters - numIndices : Nat -- Number of indices - numMotives : Nat -- Number of motives - numMinors : Nat -- Number of minor premises - rules : List RecursorRule -- A reduction for each Constructor - k : Bool -- It supports K-like reduction + /-- List of all inductive datatypes in the mutual declaration that generated this recursor -/ + all : List Name + /-- Number of parameters -/ + numParams : Nat + /-- Number of indices -/ + numIndices : Nat + /-- Number of motives -/ + numMotives : Nat + /-- Number of minor premises -/ + numMinors : Nat + /-- A reduction for each Constructor -/ + rules : List RecursorRule + /-- It supports K-like reduction -/ + k : Bool isUnsafe : Bool deriving Inhabited diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 08d758ffe6..864f125098 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -26,6 +26,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] (declName if env.contains declName then throwError "a non-private declaration '{declName}' has already been declared" +/-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/ inductive Visibility where | regular | «protected» | «private» deriving Inhabited @@ -35,10 +36,12 @@ instance : ToString Visibility := ⟨fun | Visibility.«private» => "private" | Visibility.«protected» => "protected"⟩ +/-- Whether a declaration is default, partial or nonrec. -/ inductive RecKind where | «partial» | «nonrec» | default deriving Inhabited +/-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/ structure Modifiers where docString? : Option String := none visibility : Visibility := Visibility.regular diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 62818f0046..173530704f 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -141,7 +141,7 @@ def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDec | OpenDecl.simple ns [] :: ds => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds | _ :: ds => resolveNamespaceUsingOpenDecls env n ds -/- +/-- Given a name `id` try to find namespace it refers to. The resolution procedure works as follows 1- If `id` is in the scope of `namespace` commands the namespace `s_1. ... . s_n`, then return `s_1 . ... . s_i ++ n` if it is the name of an existing namespace. We search "backwards". @@ -170,7 +170,7 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where getCurrNamespace := liftM (m:=m) getCurrNamespace getOpenDecls := liftM (m:=m) getOpenDecls -/- +/-- Given a name `n`, return a list of possible interpretations. Each interpretation is a pair `(declName, fieldList)`, where `declName` is the name of a declaration in the current environment, and `fieldList` are @@ -187,6 +187,7 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where - `resolveGlobalName x` => `[(Foo.x, [])]` - `resolveGlobalName x.y` => `[(Foo.x.y, [])]` - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]` + After `open Foo open Boo`, we have - `resolveGlobalName x` => `[(Foo.x, []), (Boo.x, [])]` - `resolveGlobalName x.y` => `[(Foo.x.y, [])]` @@ -195,12 +196,14 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id + def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) : m Name := do match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with | some ns => return ns | none => throwError s!"unknown namespace '{id}'" -/-- +/-- Given a name `n`, return a list of possible interpretations for global constants. + Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/ def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do @@ -216,6 +219,27 @@ def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] | [c] => pure c | _ => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}" +/-- Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved +constant names that it could be refering to based on the currently open namespaces. +This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax +because `Syntax` objects may have names that have already been resolved. + +## Example: +``` +def Boo.x := 1 +def Foo.x := 2 +def Foo.x.y := 3 +``` +After `open Foo`, we have +- `resolveGlobalConst x` => `[Foo.x]` +- `resolveGlobalConst x.y` => `[Foo.x.y]` +- `resolveGlobalConst x.z.w` => error: unknown constant + +After `open Foo open Boo`, we have +- `resolveGlobalConst x` => `[Foo.x, Boo.x]` +- `resolveGlobalConst x.y` => `[Foo.x.y]` +- `resolveGlobalConst x.z.w` => error: unknown constant +-/ def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m (List Name) | stx@(Syntax.ident _ _ n pre) => do let pre := pre.filterMap fun (n, fields) => if fields.isEmpty then some n else none @@ -225,6 +249,25 @@ def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m return pre | stx => throwErrorAt stx s!"expected identifier" +/-- Interpret the syntax `n` as an identifier for a global constant, and return a resolved +constant name. If there are multiple possible interpretations it will throw. + +## Example: +``` +def Boo.x := 1 +def Foo.x := 2 +def Foo.x.y := 3 +``` +After `open Foo`, we have +- `resolveGlobalConstNoOverload x` => `Foo.x` +- `resolveGlobalConstNoOverload x.y` => `Foo.x.y` +- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant + +After `open Foo open Boo`, we have +- `resolveGlobalConstNoOverload x` => error: ambiguous identifier +- `resolveGlobalConstNoOverload x.y` => `Foo.x.y` +- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant +-/ def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do let cs ← resolveGlobalConst id match cs with