697f69020f
It is still broken since we apply attributes before we compile code. Recall that attributes such as `@[export]` and `@[extern]` must be applied before we compile code. On the other hand, any attribute `attrName` ``` @[attrName] def foo := ... ``` which creates auxiliary definitions that depend on `foo` must be applied AFTER we generate code for `foo`. Otherwise, we will fail to compile the auxiliary definition since we don't have code for `foo` yet. I will fix the issue above by allowing attributes to specify when they should be applied. I will start with only two options: before and after code compilation. In the future, we may need more options (e.g., before elaboration), but I don't see the need yet. cc @kha
118 lines
4.1 KiB
Text
118 lines
4.1 KiB
Text
/-
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import init.lean.level init.lean.kvmap
|
|
|
|
namespace Lean
|
|
|
|
inductive Literal
|
|
| natVal (val : Nat)
|
|
| strVal (val : String)
|
|
|
|
inductive BinderInfo
|
|
| default | implicit | strictImplicit | instImplicit | auxDecl
|
|
|
|
abbrev MData := KVMap
|
|
namespace MData
|
|
abbrev empty : MData := {KVMap .}
|
|
instance : HasEmptyc MData := ⟨empty⟩
|
|
end MData
|
|
|
|
/-
|
|
TODO(Leo): fix the `mvar` Constructor.
|
|
In Lean3 (and Lean4), we have two kinds of metavariables: regular and temporary.
|
|
The Type of regular metavariables is stored in the metavarContext.
|
|
The Type of temporary metavariables is stored in the metavar itself. This decision is legacy from Lean2.
|
|
Moreover, the `Name` in temporary metavariables are supposed to be (small) numerals. So,
|
|
we can store their assignment as an Array. Actually, it is a numeral with a hidden unique prefix.
|
|
The decision of storing the Type of the tmp metavar is also debatable.
|
|
For example, we can avoid this by have another Array with their types.
|
|
For regular metavariables, the `Expr` field is a dummy value.
|
|
|
|
We should have two different constructors:
|
|
`| mvar : Name → Expr` for regular metavariables
|
|
and
|
|
`| tmvar : Usize → Expr` for temporary metavariables
|
|
The `Usize` makes it clear that we can use arrays to store tmp metavar assignments and their types.
|
|
-/
|
|
inductive Expr
|
|
| bvar : Nat → Expr -- bound variables
|
|
| fvar : Name → Expr -- free variables
|
|
| mvar : Name → Expr → Expr -- (temporary) meta variables
|
|
| sort : Level → Expr -- Sort
|
|
| const : Name → List Level → Expr -- constants
|
|
| app : Expr → Expr → Expr -- application
|
|
| lam : Name → BinderInfo → Expr → Expr → Expr -- lambda abstraction
|
|
| pi : Name → BinderInfo → Expr → Expr → Expr -- Pi
|
|
| elet : Name → Expr → Expr → Expr → Expr -- let expressions
|
|
| lit : Literal → Expr -- literals
|
|
| mdata : MData → Expr → Expr -- metadata
|
|
| proj : Name → Nat → Expr → Expr -- projection
|
|
|
|
instance exprIsInhabited : Inhabited Expr :=
|
|
⟨Expr.sort Level.zero⟩
|
|
|
|
attribute [extern "lean_expr_mk_bvar"] Expr.bvar
|
|
attribute [extern "lean_expr_mk_fvar"] Expr.fvar
|
|
attribute [extern "lean_expr_mk_mvar"] Expr.mvar
|
|
attribute [extern "lean_expr_mk_sort"] Expr.sort
|
|
attribute [extern "lean_expr_mk_const"] Expr.const
|
|
attribute [extern "lean_expr_mk_app"] Expr.app
|
|
attribute [extern "lean_expr_mk_lambda"] Expr.lam
|
|
attribute [extern "lean_expr_mk_pi"] Expr.pi
|
|
attribute [extern "lean_expr_mk_let"] Expr.elet
|
|
attribute [extern "lean_expr_mk_lit"] Expr.lit
|
|
attribute [extern "lean_expr_mk_mdata"] Expr.mdata
|
|
attribute [extern "lean_expr_mk_proj"] Expr.proj
|
|
|
|
def mkApp (fn : Expr) (args : List Expr) : Expr :=
|
|
args.foldl Expr.app fn
|
|
|
|
def mkCApp (fn : Name) (args : List Expr) : Expr :=
|
|
mkApp (Expr.const fn []) args
|
|
|
|
namespace Expr
|
|
@[extern "lean_expr_hash"]
|
|
constant hash (n : @& Expr) : USize := default USize
|
|
|
|
instance : Hashable Expr := ⟨Expr.hash⟩
|
|
|
|
@[extern "lean_expr_dbg_to_string"]
|
|
constant dbgToString (e : @& Expr) : String := default String
|
|
|
|
@[extern "lean_expr_quick_lt"]
|
|
constant quickLt (a : @& Expr) (b : @& Expr) : Bool := default _
|
|
|
|
@[extern "lean_expr_lt"]
|
|
constant lt (a : @& Expr) (b : @& Expr) : Bool := default _
|
|
|
|
@[extern "lean_expr_eqv"]
|
|
constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
|
|
|
|
instance : HasBeq Expr := ⟨Expr.eqv⟩
|
|
|
|
end Expr
|
|
|
|
def mkConst (n : Name) (ls : List Level := []) : Expr :=
|
|
Expr.const n ls
|
|
|
|
def getAppFn : Expr → Expr
|
|
| (Expr.app f a) := getAppFn f
|
|
| e := e
|
|
|
|
def mkBinApp (f a b : Expr) :=
|
|
Expr.app (Expr.app f a) b
|
|
|
|
def mkBinCApp (f : Name) (a b : Expr) :=
|
|
mkBinApp (mkConst f) a b
|
|
|
|
def mkDecIsTrue (pred proof : Expr) :=
|
|
mkBinApp (Expr.const `Decidable.isTrue []) pred proof
|
|
|
|
def mkDecIsFalse (pred proof : Expr) :=
|
|
mkBinApp (Expr.const `Decidable.isFalse []) pred proof
|
|
|
|
end Lean
|