chore: style
This commit is contained in:
Leonardo de Moura
parent
2f46279d78
commit
bfe4f5e7d3
12 changed files with 524 additions and 583 deletions
|
|
@ -260,10 +260,9 @@ variable {β : Type u}
|
|||
| leaf vs => leaf <$> vs.mmap f
|
||||
|
||||
@[specialize] def mmap (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) :=
|
||||
do
|
||||
root ← mmapAux f t.root;
|
||||
tail ← t.tail.mmap f;
|
||||
pure { tail := tail, root := root, .. t }
|
||||
do root ← mmapAux f t.root;
|
||||
tail ← t.tail.mmap f;
|
||||
pure { tail := tail, root := root, .. t }
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -161,31 +161,29 @@ do s ← get;
|
|||
|
||||
/- Updates `map[k]` using the current set of `owned` variables. -/
|
||||
def updateParamMap (k : Key) : M Unit :=
|
||||
do
|
||||
s ← get;
|
||||
match s.map.find k with
|
||||
| some ps => do
|
||||
ps ← ps.mmap $ fun (p : Param) =>
|
||||
if p.borrow && s.owned.contains p.x.idx then do
|
||||
markModifiedParamMap; pure { borrow := false, .. p }
|
||||
else
|
||||
pure p;
|
||||
modify $ fun s => { map := s.map.insert k ps, .. s }
|
||||
| none => pure ()
|
||||
do s ← get;
|
||||
match s.map.find k with
|
||||
| some ps => do
|
||||
ps ← ps.mmap $ fun (p : Param) =>
|
||||
if p.borrow && s.owned.contains p.x.idx then do
|
||||
markModifiedParamMap; pure { borrow := false, .. p }
|
||||
else
|
||||
pure p;
|
||||
modify $ fun s => { map := s.map.insert k ps, .. s }
|
||||
| none => pure ()
|
||||
|
||||
def getParamInfo (k : Key) : M (Array Param) :=
|
||||
do
|
||||
s ← get;
|
||||
match s.map.find k with
|
||||
| some ps => pure ps
|
||||
| none =>
|
||||
match k with
|
||||
| (Key.decl fn) => do
|
||||
ctx ← read;
|
||||
match findEnvDecl ctx.env fn with
|
||||
| some decl => pure decl.params
|
||||
| none => pure Array.empty -- unreachable if well-formed input
|
||||
| _ => pure Array.empty -- unreachable if well-formed input
|
||||
do s ← get;
|
||||
match s.map.find k with
|
||||
| some ps => pure ps
|
||||
| none =>
|
||||
match k with
|
||||
| (Key.decl fn) => do
|
||||
ctx ← read;
|
||||
match findEnvDecl ctx.env fn with
|
||||
| some decl => pure decl.params
|
||||
| none => pure Array.empty -- unreachable if well-formed input
|
||||
| _ => pure Array.empty -- unreachable if well-formed input
|
||||
|
||||
/- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
|
||||
def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
|
||||
|
|
@ -218,12 +216,11 @@ xs.size.mfor $ fun i => do
|
|||
```
|
||||
-/
|
||||
def ownArgsIfParam (xs : Array Arg) : M Unit :=
|
||||
do
|
||||
ctx ← read;
|
||||
xs.mfor $ fun x =>
|
||||
match x with
|
||||
| Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x
|
||||
| _ => pure ()
|
||||
do ctx ← read;
|
||||
xs.mfor $ fun x =>
|
||||
match x with
|
||||
| Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x
|
||||
| _ => pure ()
|
||||
|
||||
def collectExpr (z : VarId) : Expr → M Unit
|
||||
| Expr.reset _ x => ownVar z *> ownVar x
|
||||
|
|
@ -300,10 +297,9 @@ partial def collectDecl : Decl → M Unit
|
|||
whileModifingParamMapAux x ()
|
||||
|
||||
def collectDecls (decls : Array Decl) : M ParamMap :=
|
||||
do
|
||||
whileModifingParamMap (decls.mfor collectDecl);
|
||||
s ← get;
|
||||
pure s.map
|
||||
do whileModifingParamMap (decls.mfor collectDecl);
|
||||
s ← get;
|
||||
pure s.map
|
||||
|
||||
def infer (env : Environment) (decls : Array Decl) : ParamMap :=
|
||||
(collectDecls decls { env := env }).run' { map := mkInitParamMap env decls }
|
||||
|
|
@ -311,11 +307,10 @@ def infer (env : Environment) (decls : Array Decl) : ParamMap :=
|
|||
end Borrow
|
||||
|
||||
def inferBorrow (decls : Array Decl) : CompilerM (Array Decl) :=
|
||||
do
|
||||
env ← getEnv;
|
||||
let decls := decls.map Decl.normalizeIds;
|
||||
let paramMap := Borrow.infer env decls;
|
||||
pure (Borrow.applyParamMap decls paramMap)
|
||||
do env ← getEnv;
|
||||
let decls := decls.map Decl.normalizeIds;
|
||||
let paramMap := Borrow.infer env decls;
|
||||
pure (Borrow.applyParamMap decls paramMap)
|
||||
|
||||
end IR
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -51,30 +51,29 @@ let ps := decl.params;
|
|||
|| ps.size > closureMaxArgs
|
||||
|
||||
def mkBoxedVersionAux (decl : Decl) : N Decl :=
|
||||
do
|
||||
let ps := decl.params;
|
||||
qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
|
||||
(newVDecls, xs) ← qs.size.mfold
|
||||
(fun i (r : Array FnBody × Array Arg) =>
|
||||
let (newVDecls, xs) := r;
|
||||
let p := ps.get! i;
|
||||
let q := qs.get! i;
|
||||
if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
|
||||
else do
|
||||
x ← mkFresh;
|
||||
pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
|
||||
(Array.empty, Array.empty);
|
||||
r ← mkFresh;
|
||||
let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
|
||||
body ←
|
||||
if !decl.resultType.isScalar then do {
|
||||
pure $ reshape newVDecls (FnBody.ret (Arg.var r))
|
||||
} else do {
|
||||
newR ← mkFresh;
|
||||
let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
|
||||
pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
|
||||
};
|
||||
pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
|
||||
do let ps := decl.params;
|
||||
qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
|
||||
(newVDecls, xs) ← qs.size.mfold
|
||||
(fun i (r : Array FnBody × Array Arg) =>
|
||||
let (newVDecls, xs) := r;
|
||||
let p := ps.get! i;
|
||||
let q := qs.get! i;
|
||||
if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
|
||||
else do
|
||||
x ← mkFresh;
|
||||
pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
|
||||
(Array.empty, Array.empty);
|
||||
r ← mkFresh;
|
||||
let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
|
||||
body ←
|
||||
if !decl.resultType.isScalar then do {
|
||||
pure $ reshape newVDecls (FnBody.ret (Arg.var r))
|
||||
} else do {
|
||||
newR ← mkFresh;
|
||||
let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
|
||||
pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
|
||||
};
|
||||
pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
|
||||
|
||||
def mkBoxedVersion (decl : Decl) : Decl :=
|
||||
(mkBoxedVersionAux decl).run' 1
|
||||
|
|
@ -181,37 +180,36 @@ else match xType with
|
|||
It is used when the expected type does not match `xType`.
|
||||
If `xType` is scalar, then we need to "box" it. Otherwise, we need to "unbox" it. -/
|
||||
def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr :=
|
||||
do
|
||||
optVal ← isExpensiveConstantValueBoxing x xType;
|
||||
match optVal with
|
||||
| some v => do
|
||||
ctx ← read;
|
||||
s ← get;
|
||||
/- Create auxiliary FnBody
|
||||
do optVal ← isExpensiveConstantValueBoxing x xType;
|
||||
match optVal with
|
||||
| some v => do
|
||||
ctx ← read;
|
||||
s ← get;
|
||||
/- Create auxiliary FnBody
|
||||
```
|
||||
let x_1 : xType := v;
|
||||
let x_2 : expectedType := Expr.box xType x_1;
|
||||
ret x_2
|
||||
```
|
||||
-/
|
||||
let body : FnBody :=
|
||||
FnBody.vdecl { idx := 1 } xType v $
|
||||
FnBody.vdecl { idx := 2 } expectedType (Expr.box xType { idx := 1 }) $
|
||||
FnBody.ret (mkVarArg { idx := 2 });
|
||||
match s.auxDeclCache.find body with
|
||||
| some v => pure v
|
||||
| none => do
|
||||
let auxName := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
|
||||
let auxConst := Expr.fap auxName Array.empty;
|
||||
let auxDecl := Decl.fdecl auxName Array.empty expectedType body;
|
||||
modify $ fun s => {
|
||||
auxDecls := s.auxDecls.push auxDecl,
|
||||
auxDeclCache := s.auxDeclCache.cons body auxConst,
|
||||
nextAuxId := s.nextAuxId + 1,
|
||||
.. s
|
||||
};
|
||||
pure auxConst
|
||||
| none => pure $ if xType.isScalar then Expr.box xType x else Expr.unbox x
|
||||
-/
|
||||
let body : FnBody :=
|
||||
FnBody.vdecl { idx := 1 } xType v $
|
||||
FnBody.vdecl { idx := 2 } expectedType (Expr.box xType { idx := 1 }) $
|
||||
FnBody.ret (mkVarArg { idx := 2 });
|
||||
match s.auxDeclCache.find body with
|
||||
| some v => pure v
|
||||
| none => do
|
||||
let auxName := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
|
||||
let auxConst := Expr.fap auxName Array.empty;
|
||||
let auxDecl := Decl.fdecl auxName Array.empty expectedType body;
|
||||
modify $ fun s => {
|
||||
auxDecls := s.auxDecls.push auxDecl,
|
||||
auxDeclCache := s.auxDeclCache.cons body auxConst,
|
||||
nextAuxId := s.nextAuxId + 1,
|
||||
.. s
|
||||
};
|
||||
pure auxConst
|
||||
| none => pure $ if xType.isScalar then Expr.box xType x else Expr.unbox x
|
||||
|
||||
@[inline] def castVarIfNeeded (x : VarId) (expected : IRType) (k : VarId → M FnBody) : M FnBody :=
|
||||
do xType ← getVarType x;
|
||||
|
|
|
|||
|
|
@ -58,16 +58,14 @@ def checkScalarVar (x : VarId) : M Unit :=
|
|||
checkVarType x IRType.isScalar
|
||||
|
||||
def checkFullApp (c : FunId) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
decl ← getDecl c;
|
||||
unless (ys.size == decl.params.size) (throw ("incorrect number of arguments to '" ++ toString c ++ "', " ++ toString ys.size ++ " provided, " ++ toString decl.params.size ++ " expected"));
|
||||
checkArgs ys
|
||||
do decl ← getDecl c;
|
||||
unless (ys.size == decl.params.size) (throw ("incorrect number of arguments to '" ++ toString c ++ "', " ++ toString ys.size ++ " provided, " ++ toString decl.params.size ++ " expected"));
|
||||
checkArgs ys
|
||||
|
||||
def checkPartialApp (c : FunId) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
decl ← getDecl c;
|
||||
unless (ys.size < decl.params.size) (throw ("too many arguments too partial application '" ++ toString c ++ "', num. args: " ++ toString ys.size ++ ", arity: " ++ toString decl.params.size));
|
||||
checkArgs ys
|
||||
do decl ← getDecl c;
|
||||
unless (ys.size < decl.params.size) (throw ("too many arguments too partial application '" ++ toString c ++ "', num. args: " ++ toString ys.size ++ ", arity: " ++ toString decl.params.size));
|
||||
checkArgs ys
|
||||
|
||||
def checkExpr (ty : IRType) : Expr → M Unit
|
||||
| Expr.pap f ys => checkPartialApp f ys *> checkObjType ty -- partial applications should always produce a closure object
|
||||
|
|
@ -124,11 +122,10 @@ def checkDecl : Decl → M Unit
|
|||
end Checker
|
||||
|
||||
def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
match Checker.checkDecl decl { env := env, decls := decls } with
|
||||
| Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg)
|
||||
| other => pure ()
|
||||
do env ← getEnv;
|
||||
match Checker.checkDecl decl { env := env, decls := decls } with
|
||||
| Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg)
|
||||
| other => pure ()
|
||||
|
||||
def checkDecls (decls : Array Decl) : CompilerM Unit :=
|
||||
decls.mfor (checkDecl decls)
|
||||
|
|
|
|||
|
|
@ -25,34 +25,33 @@ namespace Lean
|
|||
namespace IR
|
||||
|
||||
private def compileAux (decls : Array Decl) : CompilerM Unit :=
|
||||
do
|
||||
logDecls `init decls;
|
||||
checkDecls decls;
|
||||
decls ← elimDeadBranches decls;
|
||||
logDecls `elim_dead_branches decls;
|
||||
let decls := decls.map Decl.pushProj;
|
||||
logDecls `push_proj decls;
|
||||
let decls := decls.map Decl.insertResetReuse;
|
||||
logDecls `reset_reuse decls;
|
||||
let decls := decls.map Decl.elimDead;
|
||||
logDecls `elim_dead decls;
|
||||
let decls := decls.map Decl.simpCase;
|
||||
logDecls `simp_case decls;
|
||||
let decls := decls.map Decl.normalizeIds;
|
||||
decls ← inferBorrow decls;
|
||||
logDecls `borrow decls;
|
||||
decls ← explicitBoxing decls;
|
||||
logDecls `boxing decls;
|
||||
decls ← explicitRC decls;
|
||||
logDecls `rc decls;
|
||||
let decls := decls.map Decl.expandResetReuse;
|
||||
logDecls `expand_reset_reuse decls;
|
||||
let decls := decls.map Decl.pushProj;
|
||||
logDecls `push_proj decls;
|
||||
logDecls `result decls;
|
||||
checkDecls decls;
|
||||
addDecls decls;
|
||||
pure ()
|
||||
do logDecls `init decls;
|
||||
checkDecls decls;
|
||||
decls ← elimDeadBranches decls;
|
||||
logDecls `elim_dead_branches decls;
|
||||
let decls := decls.map Decl.pushProj;
|
||||
logDecls `push_proj decls;
|
||||
let decls := decls.map Decl.insertResetReuse;
|
||||
logDecls `reset_reuse decls;
|
||||
let decls := decls.map Decl.elimDead;
|
||||
logDecls `elim_dead decls;
|
||||
let decls := decls.map Decl.simpCase;
|
||||
logDecls `simp_case decls;
|
||||
let decls := decls.map Decl.normalizeIds;
|
||||
decls ← inferBorrow decls;
|
||||
logDecls `borrow decls;
|
||||
decls ← explicitBoxing decls;
|
||||
logDecls `boxing decls;
|
||||
decls ← explicitRC decls;
|
||||
logDecls `rc decls;
|
||||
let decls := decls.map Decl.expandResetReuse;
|
||||
logDecls `expand_reset_reuse decls;
|
||||
let decls := decls.map Decl.pushProj;
|
||||
logDecls `push_proj decls;
|
||||
logDecls `result decls;
|
||||
checkDecls decls;
|
||||
addDecls decls;
|
||||
pure ()
|
||||
|
||||
@[export lean_ir_compile]
|
||||
def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) :=
|
||||
|
|
@ -61,15 +60,14 @@ match (compileAux decls opts).run { env := env } with
|
|||
| EState.Result.error msg s => (s.log, Except.error msg)
|
||||
|
||||
def addBoxedVersionAux (decl : Decl) : CompilerM Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
if !ExplicitBoxing.requiresBoxedVersion env decl then pure ()
|
||||
else do
|
||||
let decl := ExplicitBoxing.mkBoxedVersion decl;
|
||||
let decls : Array Decl := #[decl];
|
||||
decls ← explicitRC decls;
|
||||
decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
|
||||
pure ()
|
||||
do env ← getEnv;
|
||||
if !ExplicitBoxing.requiresBoxedVersion env decl then pure ()
|
||||
else do
|
||||
let decl := ExplicitBoxing.mkBoxedVersion decl;
|
||||
let decls : Array Decl := #[decl];
|
||||
decls ← explicitRC decls;
|
||||
decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
|
||||
pure ()
|
||||
|
||||
-- Remark: we are ignoring the `Log` here. This should be fine.
|
||||
@[export lean_ir_add_boxed_version]
|
||||
|
|
|
|||
|
|
@ -93,96 +93,91 @@ def emitCInitName (n : Name) : M Unit :=
|
|||
toCInitName n >>= emit
|
||||
|
||||
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit :=
|
||||
do
|
||||
let ps := decl.params;
|
||||
when (ps.isEmpty && addExternForConsts) (emit "extern ");
|
||||
emit (toCType decl.resultType ++ " " ++ cppBaseName);
|
||||
unless (ps.isEmpty) $ do {
|
||||
emit "(";
|
||||
if ps.size > closureMaxArgs && isBoxedName decl.name then
|
||||
emit "lean_object**"
|
||||
else
|
||||
ps.size.mfor $ fun i => do {
|
||||
when (i > 0) (emit ", ");
|
||||
emit (toCType (ps.get! i).ty)
|
||||
};
|
||||
emit ")"
|
||||
};
|
||||
emitLn ";"
|
||||
do let ps := decl.params;
|
||||
when (ps.isEmpty && addExternForConsts) (emit "extern ");
|
||||
emit (toCType decl.resultType ++ " " ++ cppBaseName);
|
||||
unless (ps.isEmpty) $ do {
|
||||
emit "(";
|
||||
if ps.size > closureMaxArgs && isBoxedName decl.name then
|
||||
emit "lean_object**"
|
||||
else
|
||||
ps.size.mfor $ fun i => do {
|
||||
when (i > 0) (emit ", ");
|
||||
emit (toCType (ps.get! i).ty)
|
||||
};
|
||||
emit ")"
|
||||
};
|
||||
emitLn ";"
|
||||
|
||||
def emitFnDecl (decl : Decl) (addExternForConsts : Bool) : M Unit :=
|
||||
do
|
||||
cppBaseName ← toCName decl.name;
|
||||
emitFnDeclAux decl cppBaseName addExternForConsts
|
||||
do cppBaseName ← toCName decl.name;
|
||||
emitFnDeclAux decl cppBaseName addExternForConsts
|
||||
|
||||
def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit :=
|
||||
do
|
||||
let cName := mkSimpleName cNameStr;
|
||||
env ← getEnv;
|
||||
let extC := isExternC env decl.name;
|
||||
emitFnDeclAux decl cNameStr (!extC)
|
||||
do let cName := mkSimpleName cNameStr;
|
||||
env ← getEnv;
|
||||
let extC := isExternC env decl.name;
|
||||
emitFnDeclAux decl cNameStr (!extC)
|
||||
|
||||
def emitFnDecls : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
let decls := getDecls env;
|
||||
let modDecls : NameSet := decls.foldl (fun s d => s.insert d.name) {};
|
||||
let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {};
|
||||
let usedDecls := usedDecls.toList;
|
||||
usedDecls.mfor $ fun n => do
|
||||
decl ← getDecl n;
|
||||
match getExternNameFor env `c decl.name with
|
||||
| some cName => emitExternDeclAux decl cName
|
||||
| none => emitFnDecl decl (!modDecls.contains n)
|
||||
do env ← getEnv;
|
||||
let decls := getDecls env;
|
||||
let modDecls : NameSet := decls.foldl (fun s d => s.insert d.name) {};
|
||||
let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {};
|
||||
let usedDecls := usedDecls.toList;
|
||||
usedDecls.mfor $ fun n => do
|
||||
decl ← getDecl n;
|
||||
match getExternNameFor env `c decl.name with
|
||||
| some cName => emitExternDeclAux decl cName
|
||||
| none => emitFnDecl decl (!modDecls.contains n)
|
||||
|
||||
def emitMainFn : M Unit :=
|
||||
do
|
||||
d ← getDecl `main;
|
||||
match d with
|
||||
| Decl.fdecl f xs t b => do
|
||||
unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
|
||||
env ← getEnv;
|
||||
let usesLeanAPI := usesLeanNamespace env d;
|
||||
if usesLeanAPI then
|
||||
emitLn "void lean_initialize();"
|
||||
else
|
||||
emitLn "void lean_initialize_runtime_module();";
|
||||
emitLn "int main(int argc, char ** argv) {\nlean_object* w; lean_object* in;";
|
||||
if usesLeanAPI then
|
||||
emitLn "lean_initialize();"
|
||||
else
|
||||
emitLn "lean_initialize_runtime_module();";
|
||||
emitLn "w = lean_io_mk_world();";
|
||||
modName ← getModName;
|
||||
emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);");
|
||||
emitLns ["lean_io_mark_end_initialization();",
|
||||
"if (lean_io_result_is_ok(w)) {",
|
||||
"lean_init_task_manager();"];
|
||||
if xs.size == 2 then do {
|
||||
emitLns ["in = lean_box(0);",
|
||||
"int i = argc;",
|
||||
"while (i > 1) {",
|
||||
" lean_object* n;",
|
||||
" i--;",
|
||||
" n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
|
||||
" in = n;",
|
||||
"}"];
|
||||
emitLn ("w = " ++ leanMainFn ++ "(in, w);")
|
||||
} else do {
|
||||
emitLn ("w = " ++ leanMainFn ++ "(w);")
|
||||
};
|
||||
emitLn "}";
|
||||
emitLns ["if (lean_io_result_is_ok(w)) {",
|
||||
" int ret = lean_unbox(lean_io_result_get_value(w));",
|
||||
" lean_dec_ref(w);",
|
||||
" return ret;",
|
||||
"} else {",
|
||||
" lean_io_result_show_error(w);",
|
||||
" lean_dec_ref(w);",
|
||||
" return 1;",
|
||||
"}"];
|
||||
emitLn "}"
|
||||
| other => throw "function declaration expected"
|
||||
do d ← getDecl `main;
|
||||
match d with
|
||||
| Decl.fdecl f xs t b => do
|
||||
unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
|
||||
env ← getEnv;
|
||||
let usesLeanAPI := usesLeanNamespace env d;
|
||||
if usesLeanAPI then
|
||||
emitLn "void lean_initialize();"
|
||||
else
|
||||
emitLn "void lean_initialize_runtime_module();";
|
||||
emitLn "int main(int argc, char ** argv) {\nlean_object* w; lean_object* in;";
|
||||
if usesLeanAPI then
|
||||
emitLn "lean_initialize();"
|
||||
else
|
||||
emitLn "lean_initialize_runtime_module();";
|
||||
emitLn "w = lean_io_mk_world();";
|
||||
modName ← getModName;
|
||||
emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);");
|
||||
emitLns ["lean_io_mark_end_initialization();",
|
||||
"if (lean_io_result_is_ok(w)) {",
|
||||
"lean_init_task_manager();"];
|
||||
if xs.size == 2 then do {
|
||||
emitLns ["in = lean_box(0);",
|
||||
"int i = argc;",
|
||||
"while (i > 1) {",
|
||||
" lean_object* n;",
|
||||
" i--;",
|
||||
" n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
|
||||
" in = n;",
|
||||
"}"];
|
||||
emitLn ("w = " ++ leanMainFn ++ "(in, w);")
|
||||
} else do {
|
||||
emitLn ("w = " ++ leanMainFn ++ "(w);")
|
||||
};
|
||||
emitLn "}";
|
||||
emitLns ["if (lean_io_result_is_ok(w)) {",
|
||||
" int ret = lean_unbox(lean_io_result_get_value(w));",
|
||||
" lean_dec_ref(w);",
|
||||
" return ret;",
|
||||
"} else {",
|
||||
" lean_io_result_show_error(w);",
|
||||
" lean_dec_ref(w);",
|
||||
" return 1;",
|
||||
"}"];
|
||||
emitLn "}"
|
||||
| other => throw "function declaration expected"
|
||||
|
||||
def hasMainFn : M Bool :=
|
||||
do env ← getEnv;
|
||||
|
|
@ -193,28 +188,27 @@ def emitMainFnIfNeeded : M Unit :=
|
|||
mwhen hasMainFn emitMainFn
|
||||
|
||||
def emitFileHeader : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
modName ← getModName;
|
||||
emitLn "// Lean compiler output";
|
||||
emitLn ("// Module: " ++ toString modName);
|
||||
emit "// Imports:";
|
||||
env.imports.mfor $ fun m => emit (" " ++ toString m);
|
||||
emitLn "";
|
||||
emitLn "#include \"runtime/lean.h\"";
|
||||
emitLns [
|
||||
"#if defined(__clang__)",
|
||||
"#pragma clang diagnostic ignored \"-Wunused-parameter\"",
|
||||
"#pragma clang diagnostic ignored \"-Wunused-label\"",
|
||||
"#elif defined(__GNUC__) && !defined(__CLANG__)",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-parameter\"",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-label\"",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"",
|
||||
"#endif",
|
||||
"#ifdef __cplusplus",
|
||||
"extern \"C\" {",
|
||||
"#endif"
|
||||
]
|
||||
do env ← getEnv;
|
||||
modName ← getModName;
|
||||
emitLn "// Lean compiler output";
|
||||
emitLn ("// Module: " ++ toString modName);
|
||||
emit "// Imports:";
|
||||
env.imports.mfor $ fun m => emit (" " ++ toString m);
|
||||
emitLn "";
|
||||
emitLn "#include \"runtime/lean.h\"";
|
||||
emitLns [
|
||||
"#if defined(__clang__)",
|
||||
"#pragma clang diagnostic ignored \"-Wunused-parameter\"",
|
||||
"#pragma clang diagnostic ignored \"-Wunused-label\"",
|
||||
"#elif defined(__GNUC__) && !defined(__CLANG__)",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-parameter\"",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-label\"",
|
||||
"#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"",
|
||||
"#endif",
|
||||
"#ifdef __cplusplus",
|
||||
"extern \"C\" {",
|
||||
"#endif"
|
||||
]
|
||||
|
||||
def emitFileFooter : M Unit :=
|
||||
emitLns [
|
||||
|
|
@ -249,11 +243,10 @@ partial def declareVars : FnBody → Bool → M Bool
|
|||
| e, d => if e.isTerminal then pure d else declareVars e.body d
|
||||
|
||||
def emitTag (x : VarId) (xType : IRType) : M Unit :=
|
||||
do
|
||||
if xType.isObj then do
|
||||
emit "lean_obj_tag("; emit x; emit ")"
|
||||
else
|
||||
emit x
|
||||
do if xType.isObj then do
|
||||
emit "lean_obj_tag("; emit x; emit ")"
|
||||
else
|
||||
emit x
|
||||
|
||||
def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
|
||||
if alts.size != 2 then none
|
||||
|
|
@ -262,11 +255,10 @@ else match alts.get! 0 with
|
|||
| _ => none
|
||||
|
||||
def emitIf (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (tag : Nat) (t : FnBody) (e : FnBody) : M Unit :=
|
||||
do
|
||||
emit "if ("; emitTag x xType; emit " == "; emit tag; emitLn ")";
|
||||
emitBody t;
|
||||
emitLn "else";
|
||||
emitBody e
|
||||
do emit "if ("; emitTag x xType; emit " == "; emit tag; emitLn ")";
|
||||
emitBody t;
|
||||
emitLn "else";
|
||||
emitBody e
|
||||
|
||||
def emitCase (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (alts : Array Alt) : M Unit :=
|
||||
match isIf alts with
|
||||
|
|
@ -280,20 +272,18 @@ match isIf alts with
|
|||
emitLn "}"
|
||||
|
||||
def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit :=
|
||||
do
|
||||
emit $
|
||||
if checkRef then (if n == 1 then "lean_inc" else "lean_inc_n")
|
||||
else (if n == 1 then "lean_inc_ref" else "lean_inc_ref_n");
|
||||
emit "(" *> emit x;
|
||||
when (n != 1) (emit ", " *> emit n);
|
||||
emitLn ");"
|
||||
do emit $
|
||||
if checkRef then (if n == 1 then "lean_inc" else "lean_inc_n")
|
||||
else (if n == 1 then "lean_inc_ref" else "lean_inc_ref_n");
|
||||
emit "(" *> emit x;
|
||||
when (n != 1) (emit ", " *> emit n);
|
||||
emitLn ");"
|
||||
|
||||
def emitDec (x : VarId) (n : Nat) (checkRef : Bool) : M Unit :=
|
||||
do
|
||||
emit (if checkRef then "lean_dec" else "lean_dec_ref");
|
||||
emit "("; emit x;
|
||||
when (n != 1) (do emit ", "; emit n);
|
||||
emitLn ");"
|
||||
do emit (if checkRef then "lean_dec" else "lean_dec_ref");
|
||||
emit "("; emit x;
|
||||
when (n != 1) (do emit ", "; emit n);
|
||||
emitLn ");"
|
||||
|
||||
def emitDel (x : VarId) : M Unit :=
|
||||
do emit "lean_free_object("; emit x; emitLn ");"
|
||||
|
|
@ -315,26 +305,24 @@ def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit :=
|
|||
do emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
|
||||
|
||||
def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit :=
|
||||
do
|
||||
match t with
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| IRType.uint8 => emit "lean_ctor_set_uint8"
|
||||
| IRType.uint16 => emit "lean_ctor_set_uint16"
|
||||
| IRType.uint32 => emit "lean_ctor_set_uint32"
|
||||
| IRType.uint64 => emit "lean_ctor_set_uint64"
|
||||
| _ => throw "invalid instruction";
|
||||
emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
|
||||
do match t with
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| IRType.uint8 => emit "lean_ctor_set_uint8"
|
||||
| IRType.uint16 => emit "lean_ctor_set_uint16"
|
||||
| IRType.uint32 => emit "lean_ctor_set_uint32"
|
||||
| IRType.uint64 => emit "lean_ctor_set_uint64"
|
||||
| _ => throw "invalid instruction";
|
||||
emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
|
||||
|
||||
def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit :=
|
||||
do
|
||||
ps ← getJPParams j;
|
||||
unless (xs.size == ps.size) (throw "invalid goto");
|
||||
xs.size.mfor $ fun i => do {
|
||||
let p := ps.get! i;
|
||||
let x := xs.get! i;
|
||||
emit p.x; emit " = "; emitArg x; emitLn ";"
|
||||
};
|
||||
emit "goto "; emit j; emitLn ";"
|
||||
do ps ← getJPParams j;
|
||||
unless (xs.size == ps.size) (throw "invalid goto");
|
||||
xs.size.mfor $ fun i => do {
|
||||
let p := ps.get! i;
|
||||
let x := xs.get! i;
|
||||
emit p.x; emit " = "; emitArg x; emitLn ";"
|
||||
};
|
||||
emit "goto "; emit j; emitLn ";"
|
||||
|
||||
def emitLhs (z : VarId) : M Unit :=
|
||||
do emit z; emit " = "
|
||||
|
|
@ -350,43 +338,39 @@ else if ssize == 0 then emit "sizeof(size_t)*" *> emit usize
|
|||
else emit "sizeof(size_t)*" *> emit usize *> emit " + " *> emit ssize
|
||||
|
||||
def emitAllocCtor (c : CtorInfo) : M Unit :=
|
||||
do
|
||||
emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", ";
|
||||
emitCtorScalarSize c.usize c.ssize; emitLn ");"
|
||||
do emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", ";
|
||||
emitCtorScalarSize c.usize c.ssize; emitLn ");"
|
||||
|
||||
def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
|
||||
ys.size.mfor $ fun i => do
|
||||
emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get! i); emitLn ");"
|
||||
|
||||
def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
emitLhs z;
|
||||
if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
|
||||
emit "lean_box("; emit c.cidx; emitLn ");"
|
||||
else do
|
||||
emitAllocCtor c; emitCtorSetArgs z ys
|
||||
do emitLhs z;
|
||||
if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
|
||||
emit "lean_box("; emit c.cidx; emitLn ");"
|
||||
else do
|
||||
emitAllocCtor c; emitCtorSetArgs z ys
|
||||
|
||||
def emitReset (z : VarId) (n : Nat) (x : VarId) : M Unit :=
|
||||
do
|
||||
emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
|
||||
n.mfor $ fun i => do {
|
||||
emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
|
||||
};
|
||||
emit " "; emitLhs z; emit x; emitLn ";";
|
||||
emitLn "} else {";
|
||||
emit " lean_dec_ref("; emit x; emitLn ");";
|
||||
emit " "; emitLhs z; emitLn "lean_box(0);";
|
||||
emitLn "}"
|
||||
do emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
|
||||
n.mfor $ fun i => do {
|
||||
emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
|
||||
};
|
||||
emit " "; emitLhs z; emit x; emitLn ";";
|
||||
emitLn "} else {";
|
||||
emit " lean_dec_ref("; emit x; emitLn ");";
|
||||
emit " "; emitLhs z; emitLn "lean_box(0);";
|
||||
emitLn "}"
|
||||
|
||||
def emitReuse (z : VarId) (x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
emit "if (lean_is_scalar("; emit x; emitLn ")) {";
|
||||
emit " "; emitLhs z; emitAllocCtor c;
|
||||
emitLn "} else {";
|
||||
emit " "; emitLhs z; emit x; emitLn ";";
|
||||
when updtHeader (do emit " lean_ctor_set_tag("; emit z; emit ", "; emit c.cidx; emitLn ");");
|
||||
emitLn "}";
|
||||
emitCtorSetArgs z ys
|
||||
do emit "if (lean_is_scalar("; emit x; emitLn ")) {";
|
||||
emit " "; emitLhs z; emitAllocCtor c;
|
||||
emitLn "} else {";
|
||||
emit " "; emitLhs z; emit x; emitLn ";";
|
||||
when updtHeader (do emit " lean_ctor_set_tag("; emit z; emit ", "; emit c.cidx; emitLn ");");
|
||||
emitLn "}";
|
||||
emitCtorSetArgs z ys
|
||||
|
||||
def emitProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
|
||||
do emitLhs z; emit "lean_ctor_get("; emit x; emit ", "; emit i; emitLn ");"
|
||||
|
|
@ -395,40 +379,37 @@ def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
|
|||
do emitLhs z; emit "lean_ctor_get_usize("; emit x; emit ", "; emit i; emitLn ");"
|
||||
|
||||
def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit :=
|
||||
do
|
||||
emitLhs z;
|
||||
match t with
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| IRType.uint8 => emit "lean_ctor_get_uint8"
|
||||
| IRType.uint16 => emit "lean_ctor_get_uint16"
|
||||
| IRType.uint32 => emit "lean_ctor_get_uint32"
|
||||
| IRType.uint64 => emit "lean_ctor_get_uint64"
|
||||
| _ => throw "invalid instruction";
|
||||
emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
|
||||
do emitLhs z;
|
||||
match t with
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| IRType.uint8 => emit "lean_ctor_get_uint8"
|
||||
| IRType.uint16 => emit "lean_ctor_get_uint16"
|
||||
| IRType.uint32 => emit "lean_ctor_get_uint32"
|
||||
| IRType.uint64 => emit "lean_ctor_get_uint64"
|
||||
| _ => throw "invalid instruction";
|
||||
emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
|
||||
|
||||
def toStringArgs (ys : Array Arg) : List String :=
|
||||
ys.toList.map argToCString
|
||||
|
||||
def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
emitLhs z;
|
||||
decl ← getDecl f;
|
||||
match decl with
|
||||
| Decl.extern _ _ _ extData =>
|
||||
match mkExternCall extData `c (toStringArgs ys) with
|
||||
| some c => emit c *> emitLn ";"
|
||||
| none => throw ("failed to emit extern application '" ++ toString f ++ "'")
|
||||
| _ => do emitCName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";"
|
||||
do emitLhs z;
|
||||
decl ← getDecl f;
|
||||
match decl with
|
||||
| Decl.extern _ _ _ extData =>
|
||||
match mkExternCall extData `c (toStringArgs ys) with
|
||||
| some c => emit c *> emitLn ";"
|
||||
| none => throw ("failed to emit extern application '" ++ toString f ++ "'")
|
||||
| _ => do emitCName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";"
|
||||
|
||||
def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
|
||||
do
|
||||
decl ← getDecl f;
|
||||
let arity := decl.params.size;
|
||||
emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
|
||||
ys.size.mfor $ fun i => do {
|
||||
let y := ys.get! i;
|
||||
emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
|
||||
}
|
||||
do decl ← getDecl f;
|
||||
let arity := decl.params.size;
|
||||
emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
|
||||
ys.size.mfor $ fun i => do {
|
||||
let y := ys.get! i;
|
||||
emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
|
||||
}
|
||||
|
||||
def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit :=
|
||||
if ys.size > closureMaxArgs then do
|
||||
|
|
@ -449,15 +430,14 @@ def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit :=
|
|||
do emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");"
|
||||
|
||||
def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit :=
|
||||
do
|
||||
emitLhs z;
|
||||
match t with
|
||||
| IRType.usize => emit "lean_unbox_usize"
|
||||
| IRType.uint32 => emit "lean_unbox_uint32"
|
||||
| IRType.uint64 => emit "lean_unbox_uint64"
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| other => emit "lean_unbox";
|
||||
emit "("; emit x; emitLn ");"
|
||||
do emitLhs z;
|
||||
match t with
|
||||
| IRType.usize => emit "lean_unbox_usize"
|
||||
| IRType.uint32 => emit "lean_unbox_uint32"
|
||||
| IRType.uint64 => emit "lean_unbox_uint64"
|
||||
| IRType.float => throw "floats are not supported yet"
|
||||
| other => emit "lean_unbox";
|
||||
emit "("; emit x; emitLn ");"
|
||||
|
||||
def emitIsShared (z : VarId) (x : VarId) : M Unit :=
|
||||
do emitLhs z; emit "!lean_is_exclusive("; emit x; emitLn ");"
|
||||
|
|
@ -516,11 +496,10 @@ match v with
|
|||
| Expr.lit v => emitLit z t v
|
||||
|
||||
def isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool :=
|
||||
do
|
||||
ctx ← read;
|
||||
match v, b with
|
||||
| Expr.fap f _, FnBody.ret (Arg.var y) => pure $ f == ctx.mainFn && x == y
|
||||
| _, _ => pure false
|
||||
do ctx ← read;
|
||||
match v, b with
|
||||
| Expr.fap f _, FnBody.ret (Arg.var y) => pure $ f == ctx.mainFn && x == y
|
||||
| _, _ => pure false
|
||||
|
||||
def paramEqArg (p : Param) (x : Arg) : Bool :=
|
||||
match x with
|
||||
|
|
@ -610,40 +589,39 @@ emitJPs emitFnBody b;
|
|||
emitLn "}"
|
||||
|
||||
def emitDeclAux (d : Decl) : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
let (vMap, jpMap) := mkVarJPMaps d;
|
||||
adaptReader (fun (ctx : Context) => { jpMap := jpMap, .. ctx }) $ do
|
||||
unless (hasInitAttr env d.name) $
|
||||
match d with
|
||||
| Decl.fdecl f xs t b => do
|
||||
baseName ← toCName f;
|
||||
emit (toCType t); emit " ";
|
||||
if xs.size > 0 then do {
|
||||
emit baseName;
|
||||
emit "(";
|
||||
if xs.size > closureMaxArgs && isBoxedName d.name then
|
||||
emit "lean_object** _args"
|
||||
else
|
||||
xs.size.mfor $ fun i => do {
|
||||
when (i > 0) (emit ", ");
|
||||
let x := xs.get! i;
|
||||
emit (toCType x.ty); emit " "; emit x.x
|
||||
};
|
||||
emit ")"
|
||||
} else do {
|
||||
emit ("_init_" ++ baseName ++ "()")
|
||||
};
|
||||
emitLn " {";
|
||||
when (xs.size > closureMaxArgs && isBoxedName d.name) $
|
||||
xs.size.mfor $ fun i => do {
|
||||
let x := xs.get! i;
|
||||
emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
|
||||
};
|
||||
emitLn "_start:";
|
||||
adaptReader (fun (ctx : Context) => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b);
|
||||
emitLn "}"
|
||||
| _ => pure ()
|
||||
do env ← getEnv;
|
||||
let (vMap, jpMap) := mkVarJPMaps d;
|
||||
adaptReader (fun (ctx : Context) => { jpMap := jpMap, .. ctx }) $ do
|
||||
unless (hasInitAttr env d.name) $
|
||||
match d with
|
||||
| Decl.fdecl f xs t b => do
|
||||
baseName ← toCName f;
|
||||
emit (toCType t); emit " ";
|
||||
if xs.size > 0 then do {
|
||||
emit baseName;
|
||||
emit "(";
|
||||
if xs.size > closureMaxArgs && isBoxedName d.name then
|
||||
emit "lean_object** _args"
|
||||
else
|
||||
xs.size.mfor $ fun i => do {
|
||||
when (i > 0) (emit ", ");
|
||||
let x := xs.get! i;
|
||||
emit (toCType x.ty); emit " "; emit x.x
|
||||
};
|
||||
emit ")"
|
||||
} else do {
|
||||
emit ("_init_" ++ baseName ++ "()")
|
||||
};
|
||||
emitLn " {";
|
||||
when (xs.size > closureMaxArgs && isBoxedName d.name) $
|
||||
xs.size.mfor $ fun i => do {
|
||||
let x := xs.get! i;
|
||||
emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
|
||||
};
|
||||
emitLn "_start:";
|
||||
adaptReader (fun (ctx : Context) => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b);
|
||||
emitLn "}"
|
||||
| _ => pure ()
|
||||
|
||||
def emitDecl (d : Decl) : M Unit :=
|
||||
let d := d.normalizeIds;
|
||||
|
|
@ -652,63 +630,53 @@ catch
|
|||
(fun err => throw (err ++ "\ncompiling:\n" ++ toString d))
|
||||
|
||||
def emitFns : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
let decls := getDecls env;
|
||||
decls.reverse.mfor emitDecl
|
||||
do env ← getEnv;
|
||||
let decls := getDecls env;
|
||||
decls.reverse.mfor emitDecl
|
||||
|
||||
def emitDeclInit (d : Decl) : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
let n := d.name;
|
||||
if isIOUnitInitFn env n then do {
|
||||
emit "w = "; emitCName n; emitLn "(w);";
|
||||
emitLn "if (lean_io_result_is_error(w)) return w;"
|
||||
} else when (d.params.size == 0) $ do {
|
||||
match getInitFnNameFor env d.name with
|
||||
| some initFn => do {
|
||||
emit "w = "; emitCName initFn; emitLn "(w);";
|
||||
emitLn "if (lean_io_result_is_error(w)) return w;";
|
||||
emitCName n; emitLn " = lean_io_result_get_value(w);"
|
||||
}
|
||||
| _ => do {
|
||||
emitCName n; emit " = "; emitCInitName n; emitLn "();"
|
||||
};
|
||||
when d.resultType.isObj $ do {
|
||||
emit "lean_mark_persistent("; emitCName n; emitLn ");"
|
||||
}
|
||||
}
|
||||
do env ← getEnv;
|
||||
let n := d.name;
|
||||
if isIOUnitInitFn env n then do {
|
||||
emit "w = "; emitCName n; emitLn "(w);";
|
||||
emitLn "if (lean_io_result_is_error(w)) return w;"
|
||||
} else when (d.params.size == 0) $ do {
|
||||
match getInitFnNameFor env d.name with
|
||||
| some initFn => do {
|
||||
emit "w = "; emitCName initFn; emitLn "(w);";
|
||||
emitLn "if (lean_io_result_is_error(w)) return w;";
|
||||
emitCName n; emitLn " = lean_io_result_get_value(w);"
|
||||
}
|
||||
| _ => do { emitCName n; emit " = "; emitCInitName n; emitLn "();" };
|
||||
when d.resultType.isObj $ do {
|
||||
emit "lean_mark_persistent("; emitCName n; emitLn ");"
|
||||
}
|
||||
}
|
||||
|
||||
def emitInitFn : M Unit :=
|
||||
do
|
||||
env ← getEnv;
|
||||
modName ← getModName;
|
||||
env.imports.mfor $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
|
||||
emitLns [
|
||||
"static bool _G_initialized = false;",
|
||||
"lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
|
||||
"if (_G_initialized) return w;",
|
||||
"_G_initialized = true;",
|
||||
"if (lean_io_result_is_error(w)) return w;"
|
||||
];
|
||||
env.imports.mfor $ fun m => emitLns [
|
||||
"w = initialize_" ++ m.mangle "" ++ "(w);",
|
||||
"if (lean_io_result_is_error(w)) return w;"
|
||||
];
|
||||
let decls := getDecls env;
|
||||
decls.reverse.mfor emitDeclInit;
|
||||
emitLns [
|
||||
"return w;",
|
||||
"}"]
|
||||
do env ← getEnv;
|
||||
modName ← getModName;
|
||||
env.imports.mfor $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
|
||||
emitLns [
|
||||
"static bool _G_initialized = false;",
|
||||
"lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
|
||||
"if (_G_initialized) return w;",
|
||||
"_G_initialized = true;",
|
||||
"if (lean_io_result_is_error(w)) return w;"];
|
||||
env.imports.mfor $ fun m => emitLns [
|
||||
"w = initialize_" ++ m.mangle "" ++ "(w);",
|
||||
"if (lean_io_result_is_error(w)) return w;"];
|
||||
let decls := getDecls env;
|
||||
decls.reverse.mfor emitDeclInit;
|
||||
emitLns ["return w;", "}"]
|
||||
|
||||
def main : M Unit :=
|
||||
do
|
||||
emitFileHeader;
|
||||
emitFnDecls;
|
||||
emitFns;
|
||||
emitInitFn;
|
||||
emitMainFnIfNeeded;
|
||||
emitFileFooter
|
||||
do emitFileHeader;
|
||||
emitFnDecls;
|
||||
emitFns;
|
||||
emitInitFn;
|
||||
emitMainFnIfNeeded;
|
||||
emitFileFooter
|
||||
|
||||
end EmitC
|
||||
|
||||
|
|
|
|||
|
|
@ -239,24 +239,22 @@ and `z := reuse x ctor_i ws; F` is replaced with
|
|||
`set x i ws[i]` operations, and we replace `z` with `x` in `F`
|
||||
-/
|
||||
def mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
|
||||
do
|
||||
ctx ← read;
|
||||
let b := reuseToSet ctx x y b;
|
||||
releaseUnreadFields y mask b
|
||||
do ctx ← read;
|
||||
let b := reuseToSet ctx x y b;
|
||||
releaseUnreadFields y mask b
|
||||
|
||||
-- Expand `bs; x := reset[n] y; b`
|
||||
partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
|
||||
(bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody :=
|
||||
do
|
||||
let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
|
||||
let (bs, mask) := eraseProjIncFor n y bs;
|
||||
let bSlow := mkSlowPath x y mask b;
|
||||
bFast ← mkFastPath x y mask b;
|
||||
/- We only optimize recursively the fast. -/
|
||||
bFast ← mainFn bFast Array.empty;
|
||||
c ← mkFresh;
|
||||
let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
|
||||
pure $ reshape bs b
|
||||
do let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
|
||||
let (bs, mask) := eraseProjIncFor n y bs;
|
||||
let bSlow := mkSlowPath x y mask b;
|
||||
bFast ← mkFastPath x y mask b;
|
||||
/- We only optimize recursively the fast. -/
|
||||
bFast ← mainFn bFast Array.empty;
|
||||
c ← mkFresh;
|
||||
let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
|
||||
pure $ reshape bs b
|
||||
|
||||
partial def searchAndExpand : FnBody → Array FnBody → M FnBody
|
||||
| d@(FnBody.vdecl x t (Expr.reset n y) b), bs =>
|
||||
|
|
|
|||
|
|
@ -192,23 +192,22 @@ The state is initialized using `builtinTermElabTable`.
|
|||
The current implementation just uses the bultin elaborators.
|
||||
-/
|
||||
def mkElabAttribute {σ} [Inhabited σ] (attrName : Name) (kind : String) (builtinTable : IO.Ref σ) : IO (ElabAttribute σ) :=
|
||||
do
|
||||
ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
addImportedFn := fun es => do
|
||||
table ← builtinTable.get;
|
||||
-- TODO: populate table with `es`
|
||||
pure table,
|
||||
addEntryFn := fun (s : σ) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := attrName,
|
||||
descr := kind ++ " elaborator",
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
addImportedFn := fun es => do
|
||||
table ← builtinTable.get;
|
||||
-- TODO: populate table with `es`
|
||||
pure table,
|
||||
addEntryFn := fun (s : σ) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := attrName,
|
||||
descr := kind ++ " elaborator",
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
|
||||
abbrev TermElabAttribute := ElabAttribute TermElabTable
|
||||
def mkTermElabAttribute : IO TermElabAttribute :=
|
||||
|
|
@ -437,11 +436,10 @@ def localContext : Elab LocalContext :=
|
|||
do scope ← getScope; pure scope.lctx
|
||||
|
||||
def mkLocalDecl (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : Elab LocalDecl :=
|
||||
do
|
||||
idx ← mkFreshName;
|
||||
modifyGetScope $ fun scope =>
|
||||
let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi;
|
||||
(decl, { lctx := lctx, .. scope })
|
||||
do idx ← mkFreshName;
|
||||
modifyGetScope $ fun scope =>
|
||||
let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi;
|
||||
(decl, { lctx := lctx, .. scope })
|
||||
|
||||
def mkLambda (xs : Array Expr) (b : Expr) : Elab Expr :=
|
||||
do lctx ← localContext; pure $ lctx.mkLambda xs b
|
||||
|
|
@ -452,11 +450,10 @@ do lctx ← localContext; pure $ lctx.mkForall xs b
|
|||
def anonymousInstNamePrefix := `_inst
|
||||
|
||||
def mkAnonymousInstName : Elab Name :=
|
||||
do
|
||||
scope ← getScope;
|
||||
let n := anonymousInstNamePrefix.appendIndexAfter scope.nextInstIdx;
|
||||
modifyScope $ fun scope => { nextInstIdx := scope.nextInstIdx + 1, .. scope };
|
||||
pure n
|
||||
do scope ← getScope;
|
||||
let n := anonymousInstNamePrefix.appendIndexAfter scope.nextInstIdx;
|
||||
modifyScope $ fun scope => { nextInstIdx := scope.nextInstIdx + 1, .. scope };
|
||||
pure n
|
||||
|
||||
def rootNamespace := `_root_
|
||||
|
||||
|
|
@ -493,11 +490,10 @@ do s ← get;
|
|||
| none => throw (ElabException.other ("unknown namespace '" ++ toString n ++ "'"))
|
||||
|
||||
@[inline] def withNewScope {α} (x : Elab α) : Elab α :=
|
||||
do
|
||||
modify $ fun s => { scopes := s.scopes.head! :: s.scopes, .. s };
|
||||
a ← x;
|
||||
modify $ fun s => { scopes := s.scopes.tail!, .. s};
|
||||
pure a
|
||||
do modify $ fun s => { scopes := s.scopes.head! :: s.scopes, .. s };
|
||||
a ← x;
|
||||
modify $ fun s => { scopes := s.scopes.tail!, .. s};
|
||||
pure a
|
||||
|
||||
@[inline] def withInPattern {α} (x : Elab α) : Elab α :=
|
||||
withNewScope $ do
|
||||
|
|
|
|||
|
|
@ -98,50 +98,47 @@ nss.mforArgs $ fun ns => do
|
|||
addOpenDecl (OpenDecl.simple ns [])
|
||||
|
||||
def elabOpenOnly (n : SyntaxNode) : Elab Unit :=
|
||||
do
|
||||
let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let ids := n.getArg 2;
|
||||
ids.mforArgs $ fun idStx => do
|
||||
let id := idStx.getId;
|
||||
let declName := ns ++ id;
|
||||
env ← getEnv;
|
||||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit id declName)
|
||||
else
|
||||
logUnknownDecl idStx declName
|
||||
do let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let ids := n.getArg 2;
|
||||
ids.mforArgs $ fun idStx => do
|
||||
let id := idStx.getId;
|
||||
let declName := ns ++ id;
|
||||
env ← getEnv;
|
||||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit id declName)
|
||||
else
|
||||
logUnknownDecl idStx declName
|
||||
|
||||
def elabOpenHiding (n : SyntaxNode) : Elab Unit :=
|
||||
do
|
||||
let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let idsStx := n.getArg 2;
|
||||
env ← getEnv;
|
||||
ids : List Name ← idsStx.mfoldArgs (fun idStx ids => do
|
||||
let id := idStx.getId;
|
||||
let declName := ns ++ id;
|
||||
if env.contains declName then
|
||||
pure (id::ids)
|
||||
else do
|
||||
logUnknownDecl idStx declName;
|
||||
pure ids)
|
||||
[];
|
||||
addOpenDecl (OpenDecl.simple ns ids)
|
||||
do let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let idsStx := n.getArg 2;
|
||||
env ← getEnv;
|
||||
ids : List Name ← idsStx.mfoldArgs (fun idStx ids => do
|
||||
let id := idStx.getId;
|
||||
let declName := ns ++ id;
|
||||
if env.contains declName then
|
||||
pure (id::ids)
|
||||
else do
|
||||
logUnknownDecl idStx declName;
|
||||
pure ids)
|
||||
[];
|
||||
addOpenDecl (OpenDecl.simple ns ids)
|
||||
|
||||
def elabOpenRenaming (n : SyntaxNode) : Elab Unit :=
|
||||
do
|
||||
let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let rs := (n.getArg 2);
|
||||
rs.mforSepArgs $ fun stx => do
|
||||
let fromId := stx.getIdAt 0;
|
||||
let toId := stx.getIdAt 2;
|
||||
let declName := ns ++ fromId;
|
||||
env ← getEnv;
|
||||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit toId declName)
|
||||
else
|
||||
logUnknownDecl stx declName
|
||||
do let ns := n.getIdAt 0;
|
||||
ns ← resolveNamespace ns;
|
||||
let rs := (n.getArg 2);
|
||||
rs.mforSepArgs $ fun stx => do
|
||||
let fromId := stx.getIdAt 0;
|
||||
let toId := stx.getIdAt 2;
|
||||
let declName := ns ++ fromId;
|
||||
env ← getEnv;
|
||||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit toId declName)
|
||||
else
|
||||
logUnknownDecl stx declName
|
||||
|
||||
@[builtinCommandElab «open»] def elabOpen : CommandElab :=
|
||||
fun n => do
|
||||
|
|
@ -157,13 +154,12 @@ fun n => do
|
|||
elabOpenRenaming body
|
||||
|
||||
def addUniverse (idStx : Syntax) : Elab Unit :=
|
||||
do
|
||||
let id := idStx.getId;
|
||||
univs ← getUniverses;
|
||||
if univs.elem id then
|
||||
logError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
|
||||
else
|
||||
modifyScope $ fun scope => { univs := id :: scope.univs, .. scope }
|
||||
do let id := idStx.getId;
|
||||
univs ← getUniverses;
|
||||
if univs.elem id then
|
||||
logError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
|
||||
else
|
||||
modifyScope $ fun scope => { univs := id :: scope.univs, .. scope }
|
||||
|
||||
@[builtinCommandElab «universe»] def elabUniverse : CommandElab :=
|
||||
fun n => do
|
||||
|
|
|
|||
|
|
@ -201,19 +201,18 @@ fun n => do
|
|||
logErrorAndThrow n.val ("unknown identifier '" ++ toString id ++ "'")
|
||||
|
||||
def oldElaborate (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab Expr :=
|
||||
do
|
||||
p ← toPreTerm stx;
|
||||
scope ← getScope;
|
||||
s ← get;
|
||||
match oldElaborateAux s.env scope.options s.mctx scope.lctx (mkPreTypeAscriptionIfSome p expectedType) with
|
||||
| Except.error (some pos, fmt) => do
|
||||
ctx ← read;
|
||||
logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
|
||||
throw ElabException.silent
|
||||
| Except.error (none, fmt) => logErrorAndThrow stx (fmt.pretty scope.options)
|
||||
| Except.ok (env, mctx, e) => do
|
||||
modify $ fun s => { env := env, mctx := mctx, .. s };
|
||||
pure e
|
||||
do p ← toPreTerm stx;
|
||||
scope ← getScope;
|
||||
s ← get;
|
||||
match oldElaborateAux s.env scope.options s.mctx scope.lctx (mkPreTypeAscriptionIfSome p expectedType) with
|
||||
| Except.error (some pos, fmt) => do
|
||||
ctx ← read;
|
||||
logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
|
||||
throw ElabException.silent
|
||||
| Except.error (none, fmt) => logErrorAndThrow stx (fmt.pretty scope.options)
|
||||
| Except.ok (env, mctx, e) => do
|
||||
modify $ fun s => { env := env, mctx := mctx, .. s };
|
||||
pure e
|
||||
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -120,12 +120,11 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
|
|||
parseFileAux state msgs (stxs.push stx)
|
||||
|
||||
def parseFile (env : Environment) (fname : String) : IO Syntax :=
|
||||
do
|
||||
fname ← IO.realPath fname;
|
||||
contents ← IO.readTextFile fname;
|
||||
let ctx := mkParserContextCore env contents fname;
|
||||
let (stx, state, messages) := parseHeader env ctx;
|
||||
parseFileAux env ctx state messages #[stx]
|
||||
do fname ← IO.realPath fname;
|
||||
contents ← IO.readTextFile fname;
|
||||
let ctx := mkParserContextCore env contents fname;
|
||||
let (stx, state, messages) := parseHeader env ctx;
|
||||
parseFileAux env ctx state messages #[stx]
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -1346,20 +1346,19 @@ instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ a
|
|||
section
|
||||
set_option compiler.extract_closed false
|
||||
def mkTokenTableAttribute : IO TokenTableAttribute :=
|
||||
do
|
||||
ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnvExtension {
|
||||
name := `_tokens_,
|
||||
addImportedFn := fun es => mkImportedTokenTable es,
|
||||
addEntryFn := fun (s : TokenTable) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt "token table attribute" -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := `_tokens_,
|
||||
descr := "internal token table attribute",
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl }
|
||||
do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnvExtension {
|
||||
name := `_tokens_,
|
||||
addImportedFn := fun es => mkImportedTokenTable es,
|
||||
addEntryFn := fun (s : TokenTable) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt "token table attribute" -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := `_tokens_,
|
||||
descr := "internal token table attribute",
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl }
|
||||
end
|
||||
|
||||
@[init mkTokenTableAttribute]
|
||||
|
|
@ -1512,25 +1511,24 @@ We still need to:
|
|||
- Add support for scoped parser extensions.
|
||||
-/
|
||||
def registerParserAttribute (attrName : Name) (kind : String) (descr : String) (builtinTable : Option (IO.Ref ParsingTables) := none) : IO ParserAttribute :=
|
||||
do
|
||||
ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
addImportedFn := fun es => do
|
||||
table ← match builtinTable with
|
||||
| some table => table.get
|
||||
| none => pure {};
|
||||
do ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
addImportedFn := fun es => do
|
||||
table ← match builtinTable with
|
||||
| some table => table.get
|
||||
| none => pure {};
|
||||
-- TODO: populate table with `es`
|
||||
pure table,
|
||||
addEntryFn := fun (s : ParsingTables) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt "parser attribute" -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := attrName,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
pure table,
|
||||
addEntryFn := fun (s : ParsingTables) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => Array.empty, -- TODO
|
||||
statsFn := fun _ => fmt "parser attribute" -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := attrName,
|
||||
descr := descr,
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
|
||||
namespace ParserAttribute
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue