max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(*): C++ code generator

Browse source 
in progress move of Lean.native to init
This commit is contained in:
Jared Roesch 2016-12-05 16:11:41 -08:00 • committed by Leonardo de Moura
parent d5372e770f
commit e65d90ac79
73 changed files with 3434 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -23,4 +23,5 @@ CMakeFiles/
doc/html
make.deps
src/emacs/dependencies
compile_commands.json
compile_commands.json
*.idea

1
library/.project
View file

@ -1,3 +1,4 @@
+ *.lean
- flycheck*.lean
- .#*.lean
- ffi.lean

5
library/init/data/list/basic.lean
View file

@ -111,6 +111,11 @@ def dropn : ℕ → list α → list α
| (succ n) [] := []
| (succ n) (x::r) := dropn n r
def taken : ℕ → list α → list α
| 0 a := []
| (succ n) [] := []
| (succ n) (x :: r) := x :: taken n r
definition foldl (f : α → β → α) : α → list β → α
| a [] := a
| a (b :: l) := foldl (f a b) l

1
library/init/default.lean
View file

@ -7,6 +7,7 @@ prelude
import init.core init.logic init.category init.data.basic
import init.propext init.funext init.category.combinators init.function init.classical
import init.util init.coe init.wf init.meta init.algebra init.data
import init.native
def debugger.attr : user_attribute :=
{ name := `breakpoint,

4
library/init/meta/expr.lean
View file

@ -28,6 +28,7 @@ meta instance : inhabited expr :=
⟨expr.sort level.zero⟩
meta constant expr.mk_macro (d : macro_def) : list expr → expr
meta constant expr.macro_def_name (d : macro_def) : name
meta def expr.mk_var (n : nat) : expr :=
expr.var (unsigned.of_nat n)
@ -82,6 +83,9 @@ meta constant expr.lower_vars : expr → nat → nat → expr
/- (copy_pos_info src tgt) copy position information from src to tgt. -/
meta constant expr.copy_pos_info : expr → expr → expr
meta constant expr.is_internal_cnstr : expr → option unsigned
meta constant expr.get_nat_value : expr → option nat
namespace expr
open decidable

17
library/init/meta/name.lean
View file

@ -36,12 +36,23 @@ def name.get_prefix : name → name
| (mk_string s p) := p
| (mk_numeral s p) := p
def name.to_string : name → string
definition name.to_string_with_sep (sep : string) : name → string
| anonymous := "[anonymous]"
| (mk_string s anonymous) := s
| (mk_numeral v anonymous) := to_string v
| (mk_string s n) := name.to_string n ++ "." ++ s
| (mk_numeral v n) := name.to_string n ++ "." ++ to_string v
| (mk_string s n) := name.to_string_with_sep n ++ sep ++ s
| (mk_numeral v n) := name.to_string_with_sep n ++ sep ++ to_string v
private def name.components' : name -> list name
| anonymous := []
| (mk_string s n) := mk_string s anonymous :: name.components' n
| (mk_numeral v n) := mk_numeral v anonymous :: name.components' n
def name.components (n : name) : list name :=
list.reverse (name.components' n)
definition name.to_string : name → string :=
name.to_string_with_sep "."
instance : has_to_string name :=
⟨name.to_string⟩

133
library/init/native/anf.lean Normal file
View file

@ -0,0 +1,133 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.format
import init.meta.expr
import init.data.string
import init.category.state
import init.native.internal
import init.native.ir
import init.native.format
import init.native.builtin
import init.native.util
import init.native.pass
import init.native.config
open native
@[reducible] meta def binding :=
(name × expr × expr)
@[reducible] meta def anf_state :=
(list (list binding) × nat)
@[reducible] meta def anf_monad :=
state anf_state
meta def trace_anf (s : string) : anf_monad unit :=
trace s (fun u, return u)
private meta def let_bind (n : name) (ty : expr) (e : expr) : anf_monad unit := do
scopes ← state.read,
match scopes with
| ([], _) := return ()
| ((s :: ss), count) := state.write $ (((n, ty, e) :: s) :: ss, count)
end
private meta def mk_let : list binding → expr → expr
| [] body := body
| ((n, ty, val) :: es) body :=
mk_let es (expr.elet n ty val (expr.abstract body (mk_local n)))
private meta def mk_let_in_current_scope (body : expr) : anf_monad expr := do
(scopes, _) ← state.read,
match scopes with
| [] := pure $ body
| (top :: _) := return $ mk_let top body
end
private meta def enter_scope (action : anf_monad expr) : anf_monad expr := do
(scopes, count) ← state.read,
state.write ([] :: scopes, count),
result ← action,
bound_result ← mk_let_in_current_scope result,
state.write (scopes, count),
return bound_result
private meta def fresh_name : anf_monad name := do
(ss, count) ← state.read,
-- need to replace this with unique prefix as per our earlier conversation
n ← pure $ name.mk_numeral (unsigned.of_nat count) `_anf_,
state.write (ss, count + 1),
return n
-- Hoist a set of expressions above the result of the callback
-- function.
meta def hoist
(anf : expr → anf_monad expr)
(kont : list name → anf_monad expr) : list expr → anf_monad expr
| [] := kont []
| es := do
ns ← monad.for es $ (fun x, do
value ← anf x,
fresh ← fresh_name,
let_bind fresh mk_neutral_expr value,
return fresh),
kont ns
private meta def anf_constructor (head : expr) (args : list expr) (anf : expr → anf_monad expr) : anf_monad expr :=
hoist anf (fun args', return $ mk_call head (list.map mk_local args')) args
private meta def anf_call (head : expr) (args : list expr) (anf : expr → anf_monad expr) : anf_monad expr := do
hoist anf (fun ns, match ns with
-- need to think about how to refactor this, we should get at least one back from here always
-- this case should never happen
| [] := return head
| (head' :: args') := return $ mk_call (mk_local head') (list.map mk_local args')
end) (head :: args)
private meta def anf_case (action : expr → anf_monad expr) (e : expr) : anf_monad expr := do
under_lambda fresh_name (fun e', enter_scope (action e')) e
private meta def anf_cases_on (head : expr) (args : list expr) (anf : expr → anf_monad expr) : anf_monad expr := do
match args with
| [] := return $ mk_call head []
| (scrut :: cases) := do
scrut' ← anf scrut,
cases' ← monad.mapm (anf_case anf) cases,
return $ mk_call head (scrut' :: cases')
end
-- stop deleting this, not sure why I keep removing this line of code
open application_kind
private meta def anf' : expr → anf_monad expr
| (expr.elet n ty val body) := do
fresh ← fresh_name,
val' ← anf' val,
let_bind fresh ty val',
anf' (expr.instantiate_vars body [mk_local fresh])
| (expr.app f arg) := do
let fn := expr.get_app_fn (expr.app f arg),
args := expr.get_app_args (expr.app f arg)
in match app_kind fn with
| cases := anf_cases_on fn args anf'
| constructor := anf_constructor fn args anf'
| other := anf_call fn args anf'
end
| e := return e
private meta def init_state : anf_state :=
([], 0)
private meta def anf_transform (conf : config) (e : expr) : expr :=
prod.fst $ (under_lambda fresh_name (enter_scope ∘ anf') e) init_state
meta def anf : pass := {
name := "anf",
transform := fun conf proc, procedure.map_body (fun e, anf_transform conf e) proc
}

14
library/init/native/builtin.lean Normal file
View file

@ -0,0 +1,14 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.name
inductive builtin
| cfun : name → nat → builtin
| cases : name → nat → builtin
| vm : name → builtin
meta constant native.get_builtin : name → option builtin

85
library/init/native/cf.lean Normal file
View file

@ -0,0 +1,85 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.format
import init.meta.expr
import init.data.string
import init.category.state
import init.native.ir
import init.native.format
import init.native.builtin
import init.native.util
import init.native.pass
import init.native.procedure
import init.native.internal
import init.native.config
open native
namespace cf
@[reducible] meta def cf_state :=
config × nat
@[reducible] meta def cf_monad :=
state cf_state
meta def when_debug (action : cf_monad unit) : cf_monad unit := do
(config, _) ← state.read,
if config.debug config
then action
else return ()
-- point at the code where you can't synthesize?
-- the error behavior here seems bad if you replace the unit
-- with `u`
meta def trace_cf (s : string) : cf_monad unit :=
when_debug (trace s (fun u, return ()))
meta def fresh_name : cf_monad name := do
(config, count) ← state.read,
-- need to replace this with unique prefix as per our earlier conversation
n ← pure $ name.mk_numeral (unsigned.of_nat count) `_anf_,
state.write (config, count + 1),
return n
private meta def cf_case (action : expr → cf_monad expr) (e : expr) : cf_monad expr := do
under_lambda fresh_name (fun e', action e') e
private meta def cf_cases_on (head : expr) (args : list expr) (cf : expr → cf_monad expr) : cf_monad expr :=
match args with
| [] := return $ mk_call head []
| (scrut :: cases) := do
trace_cf "inside cases on",
cases' ← monad.mapm (cf_case cf) cases,
return $ mk_call head (scrut :: cases')
end
meta def cf' : expr → cf_monad expr
| (expr.elet n ty val body) :=
expr.elet n ty val <$> (cf' body)
| (expr.app f arg) := do
trace_cf "processing app",
let fn := expr.get_app_fn (expr.app f arg),
args := expr.get_app_args (expr.app f arg)
in if is_cases_on fn
then cf_cases_on fn args cf'
else return (mk_call (expr.const `native_compiler.return []) [(expr.app f arg)])
| e := return $ expr.app (expr.const `native_compiler.return []) e
meta def init_state : config → cf_state :=
fun c, (c, 0)
end cf
private meta def cf_transform (conf : config) (e : expr) : expr :=
prod.fst $ (under_lambda cf.fresh_name cf.cf' e) (cf.init_state conf)
meta def cf : pass := {
name := "control_flow",
transform := fun conf proc, procedure.map_body (fun e, cf_transform conf e) proc
}

15
library/init/native/config.lean Normal file
View file

@ -0,0 +1,15 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.data.bool.basic
namespace native
-- eventually expose all the options here
record config :=
(debug : bool)
end native

616
library/init/native/default.lean Normal file
View file

@ -0,0 +1,616 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.format
import init.meta.expr
import init.category.state
import init.data.string
import init.data.list.instances
import init.native.ir
import init.native.format
import init.native.internal
import init.native.anf
import init.native.cf
import init.native.pass
import init.native.util
import init.native.config
import init.native.result
namespace native
inductive error
| string : string → error
| many : list error → error
meta def error.to_string : error → string
| (error.string s) := s
| (error.many es) := to_string $ list.map error.to_string es
meta def arity_map : Type :=
rb_map name nat
meta def get_arity : expr → nat
| (expr.lam _ _ _ body) := 1 + get_arity body
| _ := 0
@[reducible] def ir_result (A : Type*) :=
native.result error A
meta def mk_arity_map : list (name × expr) → arity_map
| [] := rb_map.mk name nat
| ((n, body) :: rest) := rb_map.insert (mk_arity_map rest) n (get_arity body)
@[reducible] meta def ir_compiler_state :=
(config × arity_map × nat)
@[reducible] meta def ir_compiler (A : Type) :=
native.resultT (state ir_compiler_state) error A
meta def lift {A} (action : state ir_compiler_state A) : ir_compiler A :=
⟨fmap (fun (a : A), native.result.ok a) action⟩
meta def trace_ir (s : string) : ir_compiler unit := do
(conf, map, counter) ← lift $ state.read,
if config.debug conf
then trace s (fun u, return ())
else return ()
-- An `exotic` monad combinator that accumulates errors.
meta def run {M E A} (res : native.resultT M E A) : M (native.result E A) :=
match res with
| ⟨action⟩ := action
end
meta def sequence_err : list (ir_compiler format) → ir_compiler (list format × list error)
| [] := return ([], [])
| (action :: remaining) :=
⟨ fun s,
match (run (sequence_err remaining)) s with
| (native.result.err e, s') := (native.result.err e, s)
| (native.result.ok (res, errs), s') :=
match (run action) s' with
| (native.result.err e, s'') := (native.result.ok (res, e :: errs), s'')
| (native.result.ok v, s'') := (native.result.ok (v :: res, errs), s'')
end
end
⟩
-- meta lemma sequence_err_always_ok :
-- forall xs v s s', sequence_err xs s = native.result.ok (v, s') := sorry
meta def lift_result {A} (action : ir_result A) : ir_compiler A :=
⟨fun s, (action, s)⟩
-- TODO: fix naming here
private meta def take_arguments' : expr → list name → (list name × expr)
| (expr.lam n _ _ body) ns := take_arguments' body (n :: ns)
| e' ns := (ns, e')
meta def fresh_name : ir_compiler name := do
(conf, map, counter) ← lift state.read,
let fresh := name.mk_numeral (unsigned.of_nat counter) `native._ir_compiler_
in do
lift $ state.write (conf, map, counter + 1),
return fresh
meta def take_arguments (e : expr) : ir_compiler (list name × expr) :=
let (arg_names, body) := take_arguments' e [] in do
fresh_names ← monad.mapm (fun x, fresh_name) arg_names,
let locals := list.map mk_local fresh_names in
return $ (fresh_names, expr.instantiate_vars body (list.reverse locals))
-- meta def lift_state {A} (action : state arity_map A) : ir_compiler A :=
-- fun (s : arity_map), match action s with
-- | (a, s) := (return a, s)
-- end
meta def mk_error {T} : string → ir_compiler T :=
fun s, do
trace_ir "CREATEDERROR",
lift_result (native.result.err $ error.string s)
meta def lookup_arity (n : name) : ir_compiler nat := do
(_, map, counter) ← lift state.read,
if n = `nat.cases_on
then pure 2
else
match rb_map.find map n with
| option.none := mk_error $ "could not find arity for: " ++ to_string n
| option.some n := return n
end
meta def mk_nat_literal (n : nat) : ir_compiler ir.expr :=
return (ir.expr.lit $ ir.literal.nat n)
def repeat {A : Type} : nat → A → list A
| 0 _ := []
| (n + 1) a := a :: repeat n a
def zip {A B : Type} : list A → list B → list (A × B)
| [] [] := []
| [] (y :: ys) := []
| (x :: xs) [] := []
| (x :: xs) (y :: ys) := (x, y) :: zip xs ys
private def upto' : ℕ → list ℕ
| 0 := []
| (n + 1) := n :: upto' n
def upto (n : ℕ) : list ℕ :=
list.reverse $ upto' n
def label {A : Type} (xs : list A) : list (nat × A) :=
zip (upto (list.length xs)) xs
-- lemma label_size_eq :
-- forall A (xs : list A),
-- list.length (label xs) = list.length xs :=
-- begin
-- intros,
-- induction xs,
-- apply sorry
-- apply sorry
-- end
-- HELPERS --
meta def assert_name : ir.expr → ir_compiler name
| (ir.expr.locl n) := lift_result $ native.result.ok n
| e := mk_error $ "expected name found: " ++ to_string (format_cpp.expr e)
meta def assert_expr : ir.stmt → ir_compiler ir.expr
| (ir.stmt.e exp) := return exp
| s := mk_error ("internal invariant violated, found: " ++ (to_string (format_cpp.stmt s)))
meta def mk_call (head : name) (args : list ir.expr) : ir_compiler ir.expr :=
let args'' := list.map assert_name args
in do
args' ← monad.sequence args'',
return (ir.expr.call head args')
meta def mk_under_sat_call (head : name) (args : list ir.expr) : ir_compiler ir.expr :=
let args'' := list.map assert_name args in do
args' ← monad.sequence args'',
return $ ir.expr.mk_native_closure head args'
meta def bind_value_with_ty (val : ir.expr) (ty : ir.ty) (body : name → ir_compiler ir.stmt) : ir_compiler ir.stmt := do
fresh ← fresh_name,
ir.stmt.letb fresh ty val <$> (body fresh)
meta def bind_value (val : ir.expr) (body : name → ir_compiler ir.stmt) : ir_compiler ir.stmt :=
bind_value_with_ty val ir.ty.object body
-- not in love with this --solution-- hack, revisit
meta def compile_local (n : name) : ir_compiler name :=
return $ (mk_str_name "_$local$_" (name.to_string_with_sep "_" n))
meta def mk_invoke (loc : name) (args : list ir.expr) : ir_compiler ir.expr :=
let args'' := list.map assert_name args
in do
args' ← monad.sequence args'',
loc' ← compile_local loc,
lift_result (native.result.ok $ ir.expr.invoke loc' args')
meta def mk_over_sat_call (head : name) (fst snd : list ir.expr) : ir_compiler ir.expr :=
let fst' := list.map assert_name fst,
snd' := list.map assert_name snd in do
args' ← monad.sequence fst',
args'' ← monad.sequence snd',
fresh ← fresh_name,
locl ← compile_local fresh,
invoke ← ir.stmt.e <$> (mk_invoke fresh (fmap ir.expr.locl args'')),
return $ ir.expr.block (ir.stmt.seq [
ir.stmt.letb locl ir.ty.object (ir.expr.call head args') ir.stmt.nop,
invoke
])
meta def is_return (n : name) : bool :=
decidable.to_bool $ `native_compiler.return = n
meta def compile_call (head : name) (arity : nat) (args : list ir.expr) : ir_compiler ir.expr := do
trace_ir $ "compile_call: " ++ (to_string head),
if list.length args = arity
then mk_call head args
else if list.length args < arity
then mk_under_sat_call head args
else mk_over_sat_call head (list.taken arity args) (list.dropn arity args)
meta def mk_object (arity : unsigned) (args : list ir.expr) : ir_compiler ir.expr :=
let args'' := list.map assert_name args
in do args' ← monad.sequence args'',
lift_result (native.result.ok $ ir.expr.mk_object (unsigned.to_nat arity) args')
meta def one_or_error (args : list expr) : ir_compiler expr :=
match args with
| ((h : expr) :: []) := lift_result $ native.result.ok h
| _ := mk_error "internal invariant violated, should only have one argument"
end
meta def panic (msg : string) : ir_compiler ir.expr :=
return $ ir.expr.panic msg
-- END HELPERS --
meta def bind_case_fields' (scrut : name) : list (nat × name) → ir.stmt → ir_compiler ir.stmt
| [] body := return body
| ((n, f) :: fs) body := do
loc ← compile_local f,
ir.stmt.letb f ir.ty.object (ir.expr.project scrut n) <$> (bind_case_fields' fs body)
meta def bind_case_fields (scrut : name) (fs : list name) (body : ir.stmt) : ir_compiler ir.stmt :=
bind_case_fields' scrut (label fs) body
meta def mk_cases_on (case_name scrut : name) (cases : list (nat × ir.stmt)) (default : ir.stmt) : ir.stmt :=
ir.stmt.seq [
ir.stmt.letb `ctor_index ir.ty.int (ir.expr.call `cidx [scrut]) ir.stmt.nop,
ir.stmt.switch `ctor_index cases default
]
meta def compile_cases (action : expr → ir_compiler ir.stmt) (scrut : name)
: list (nat × expr) → ir_compiler (list (nat × ir.stmt))
| [] := return []
| ((n, body) :: cs) := do
(fs, body') ← take_arguments body,
body'' ← action body',
cs' ← compile_cases cs,
case ← bind_case_fields scrut fs body'',
return $ (n, case) :: cs'
meta def compile_cases_on_to_ir_expr
(case_name : name)
(cases : list expr)
(action : expr → ir_compiler ir.stmt) : ir_compiler ir.expr := do
default ← panic "default case should never be reached",
match cases with
| [] := mk_error $ "found " ++ to_string case_name ++ "applied to zero arguments"
| (h :: cs) := do
ir_scrut ← action h >>= assert_expr,
ir.expr.block <$> bind_value ir_scrut (fun scrut, do
cs' ← compile_cases action scrut (label cs),
return (mk_cases_on case_name scrut cs' (ir.stmt.e default)))
end
meta def bind_builtin_case_fields' (scrut : name) : list (nat × name) → ir.stmt → ir_compiler ir.stmt
| [] body := return body
| ((n, f) :: fs) body := do
loc ← compile_local f,
ir.stmt.letb loc ir.ty.object (ir.expr.project scrut n) <$> (bind_builtin_case_fields' fs body)
meta def bind_builtin_case_fields (scrut : name) (fs : list name) (body : ir.stmt) : ir_compiler ir.stmt :=
bind_builtin_case_fields' scrut (label fs) body
meta def compile_builtin_cases (action : expr → ir_compiler ir.stmt) (scrut : name)
: list (nat × expr) → ir_compiler (list (nat × ir.stmt))
| [] := return []
| ((n, body) :: cs) := do
(fs, body') ← take_arguments body,
body'' ← action body',
cs' ← compile_builtin_cases cs,
case ← bind_builtin_case_fields scrut fs body'',
return $ (n, case) :: cs'
meta def in_lean_ns (n : name) : name :=
mk_simple_name ("lean::" ++ name.to_string_with_sep "_" n)
meta def mk_builtin_cases_on (case_name scrut : name) (cases : list (nat × ir.stmt)) (default : ir.stmt) : ir.stmt :=
-- replace `ctor_index with a generated name
ir.stmt.seq [
ir.stmt.letb `buffer ir.ty.object_buffer ir.expr.uninitialized ir.stmt.nop,
ir.stmt.letb `ctor_index ir.ty.int (ir.expr.call (in_lean_ns case_name) [scrut, `buffer]) ir.stmt.nop,
ir.stmt.switch `ctor_index cases default
]
meta def compile_builtin_cases_on_to_ir_expr
(case_name : name)
(cases : list expr)
(action : expr → ir_compiler ir.stmt) : ir_compiler ir.expr := do
default ← panic "default case should never be reached",
match cases with
| [] := mk_error $ "found " ++ to_string case_name ++ "applied to zero arguments"
| (h :: cs) := do
ir_scrut ← action h >>= assert_expr,
ir.expr.block <$> bind_value ir_scrut (fun scrut, do
cs' ← compile_builtin_cases action scrut (label cs),
return (mk_builtin_cases_on case_name scrut cs' (ir.stmt.e default)))
end
meta def mk_is_simple (scrut : name) : ir.expr :=
ir.expr.call `is_simple [scrut]
meta def mk_is_zero (n : name) : ir.expr :=
ir.expr.equals (ir.expr.raw_int 0) (ir.expr.locl n)
meta def mk_cidx (obj : name) : ir.expr :=
ir.expr.call `cidx [obj]
-- we should add applicative brackets
meta def mk_simple_nat_cases_on (scrut : name) (zero_case succ_case : ir.stmt) : ir_compiler ir.stmt :=
bind_value_with_ty (mk_cidx scrut) (ir.ty.name `int) (fun cidx,
bind_value_with_ty (mk_is_zero cidx) (ir.ty.name `bool) (fun is_zero,
pure $ ir.stmt.ite is_zero zero_case succ_case))
meta def mk_mpz_nat_cases_on (scrut : name) (zero_case succ_case : ir.stmt) : ir_compiler ir.stmt :=
ir.stmt.e <$> panic "mpz"
meta def mk_nat_cases_on (scrut : name) (zero_case succ_case : ir.stmt) : ir_compiler ir.stmt :=
bind_value_with_ty (mk_is_simple scrut) (ir.ty.name `bool) (fun is_simple,
ir.stmt.ite is_simple <$>
mk_simple_nat_cases_on scrut zero_case succ_case <*>
mk_mpz_nat_cases_on scrut zero_case succ_case)
meta def assert_two_cases (cases : list expr) : ir_compiler (expr × expr) :=
match cases with
| c1 :: c2 :: _ := return (c1, c2)
| _ := mk_error "nat.cases_on should have exactly two cases"
end
meta def mk_vm_nat (n : name) : ir.expr :=
ir.expr.call (in_lean_ns `mk_vm_simple) [n]
meta def compile_succ_case (action : expr → ir_compiler ir.stmt) (scrut : name) (succ_case : expr) : ir_compiler ir.stmt := do
(fs, body') ← take_arguments succ_case,
body'' ← action body',
match fs with
| pred :: _ := do
loc ← compile_local pred,
fresh ← fresh_name,
bind_value_with_ty (mk_cidx scrut) (ir.ty.name `int) (fun cidx,
bind_value_with_ty (ir.expr.sub (ir.expr.locl cidx) (ir.expr.raw_int 1)) (ir.ty.name `int) (fun sub,
pure $ ir.stmt.letb loc ir.ty.object (mk_vm_nat sub) body''
))
| _ := mk_error "compile_succ_case too many fields"
end
meta def compile_nat_cases_on_to_ir_expr
(case_name : name)
(cases : list expr)
(action : expr → ir_compiler ir.stmt) : ir_compiler ir.expr :=
match cases with
| [] := mk_error $ "found " ++ to_string case_name ++ "applied to zero arguments"
| (h :: cs) := do
ir_scrut ← action h >>= assert_expr,
(zero_case, succ_case) ← assert_two_cases cs,
trace_ir (to_string zero_case),
trace_ir (to_string succ_case),
ir.expr.block <$> bind_value ir_scrut (fun scrut, do
zc ← action zero_case,
sc ← compile_succ_case action scrut succ_case,
mk_nat_cases_on scrut zc sc
)
end
-- this→emit_indented("if (is_simple(");
-- action(scrutinee);
-- this→emit_string("))");
-- this→emit_block([&] () {
-- this→emit_indented("if (cidx(");
-- action(scrutinee);
-- this→emit_string(") == 0) ");
-- this→emit_block([&] () {
-- action(zero_case);
-- *this→m_output_stream << ";\n";
-- });
-- this→emit_string("else ");
-- this→emit_block([&] () {
-- action(succ_case);
-- *this→m_output_stream << ";\n";
-- });
-- });
-- this→emit_string("else ");
-- this→emit_block([&] () {
-- this→emit_indented("if (to_mpz(");
-- action(scrutinee);
-- this→emit_string(") == 0) ");
-- this→emit_block([&] () {
-- action(zero_case);
-- *this→m_output_stream << ";\n";
-- });
-- this→emit_string("else ");
-- this→emit_block([&] () {
-- action(succ_case);
-- });
-- });
-- this code isnt' great working around the semi-functional frontend
meta def compile_expr_app_to_ir_expr
(head : expr)
(args : list expr)
(action : expr → ir_compiler ir.stmt) : ir_compiler ir.expr := do
trace_ir (to_string head ++ to_string args),
if expr.is_constant head = bool.tt
then (if is_return (expr.const_name head)
then do
rexp ← one_or_error args,
(ir.expr.block ∘ ir.stmt.return) <$> ((action rexp) >>= assert_expr)
else if is_nat_cases_on (expr.const_name head)
then compile_nat_cases_on_to_ir_expr (expr.const_name head) args action
else match is_internal_cnstr head with
| option.some n := do
args' ← monad.sequence $ list.map (fun x, action x >>= assert_expr) args,
mk_object n args'
| option.none := match is_internal_cases head with
| option.some n := compile_cases_on_to_ir_expr (expr.const_name head) args action
| option.none := match get_builtin (expr.const_name head) with
| option.some builtin :=
match builtin with
| builtin.vm n := mk_error "vm"
| builtin.cfun n arity := do
args' ← monad.sequence $ list.map (fun x, action x >>= assert_expr) args,
compile_call n arity args'
| builtin.cases n arity :=
compile_builtin_cases_on_to_ir_expr (expr.const_name head) args action
end
| option.none := do
args' ← monad.sequence $ list.map (fun x, action x >>= assert_expr) args,
arity ← lookup_arity (expr.const_name head),
compile_call (expr.const_name head) arity args'
end
end end)
else if expr.is_local_constant head
then do
args' ← monad.sequence $ list.map (fun x, action x >>= assert_expr) args,
mk_invoke (expr.local_uniq_name head) args'
else (mk_error ("unsupported call position" ++ (to_string head)))
meta def compile_expr_macro_to_ir_expr (e : expr) : ir_compiler ir.expr :=
match native.get_nat_value e with
| option.none := mk_error "unsupported macro"
| option.some n := mk_nat_literal n
end
meta def compile_expr_to_ir_expr (action : expr → ir_compiler ir.stmt): expr → ir_compiler ir.expr
| (expr.const n ls) :=
match native.is_internal_cnstr (expr.const n ls) with
| option.none :=
-- TODO, do I need to case on arity here? I should probably always emit a call
match get_builtin n with
| option.some (builtin.cfun n' arity) :=
compile_call n arity []
| _ :=
if n = "_neutral_"
then (pure $ ir.expr.mk_object 0 [])
else do
arity ← lookup_arity n,
compile_call n arity []
end
| option.some arity := pure $ ir.expr.mk_object (unsigned.to_nat arity) []
end
| (expr.var i) := mk_error "there should be no bound variables in compiled terms"
| (expr.sort _) := mk_error "found sort"
| (expr.mvar _ _) := mk_error "unexpected meta-variable in expr"
| (expr.local_const n _ _ _) := ir.expr.locl <$> compile_local n
| (expr.app f x) :=
let head := expr.get_app_fn (expr.app f x),
args := expr.get_app_args (expr.app f x)
in compile_expr_app_to_ir_expr head args action
| (expr.lam _ _ _ _) := mk_error "found lam"
| (expr.pi _ _ _ _) := mk_error "found pi"
| (expr.elet n _ v body) := mk_error "internal error: can not translate let binding into a ir_expr"
| (expr.macro d sz args) := compile_expr_macro_to_ir_expr (expr.macro d sz args)
meta def compile_expr_to_ir_stmt : expr → ir_compiler ir.stmt
| (expr.pi _ _ _ _) := mk_error "found pi, should not be translating a Pi for any reason (yet ...)"
| (expr.elet n _ v body) := do
n' ← compile_local n,
v' ← compile_expr_to_ir_expr compile_expr_to_ir_stmt v,
-- this is a scoping fail, we need to fix how we compile locals
body' ← compile_expr_to_ir_stmt (expr.instantiate_vars body [mk_local n]),
-- not the best solution, here need to think hard about how to prevent thing, more aggressive anf?
match v' with
| ir.expr.block stmt := return (ir.stmt.seq [ir.stmt.letb n' ir.ty.object ir.expr.uninitialized ir.stmt.nop, body'])
| _ := return (ir.stmt.letb n' ir.ty.object v' body')
end
| e' := ir.stmt.e <$> compile_expr_to_ir_expr compile_expr_to_ir_stmt e'
meta def compile_defn_to_ir (decl_name : name) (args : list name) (body : expr) : ir_compiler ir.defn := do
body' ← compile_expr_to_ir_stmt body,
let params := (zip args (repeat (list.length args) (ir.ty.ref ir.ty.object))) in
pure (ir.defn.mk decl_name params ir.ty.object body')
def unwrap_or_else {T R : Type} : ir_result T → (T → R) → (error → R) → R
| (native.result.err e) f err := err e
| (native.result.ok t) f err := f t
meta def replace_main (n : name) : name :=
if n = `main
then "___lean__main"
else n
meta def trace_expr (e : expr) : ir_compiler unit :=
trace ("trace_expr: " ++ to_string e) (fun u, return ())
meta def compile_defn (decl_name : name) (e : expr) : ir_compiler format :=
let arity := get_arity e in do
(args, body) ← take_arguments e,
ir ← compile_defn_to_ir (replace_main decl_name) args body,
return $ format_cpp.defn ir
meta def compile' : list (name × expr) → list (ir_compiler format)
| [] := []
| ((n, e) :: rest) := do
let decl := (fun d, d ++ format.line ++ format.line) <$> compile_defn n e
in decl :: (compile' rest)
meta def format_error : error → format
| (error.string s) := to_fmt s
| (error.many es) := format_concat (list.map format_error es)
meta def mk_lean_name (n : name) : ir.expr :=
ir.expr.constructor (in_lean_ns `name) (name.components n)
meta def emit_declare_vm_builtins : list (name × expr) → ir_compiler (list ir.stmt)
| [] := return []
| ((n, body) :: es) := do
vm_name ← pure $ (mk_lean_name n),
tail ← emit_declare_vm_builtins es,
fresh ← fresh_name,
let cpp_name := in_lean_ns `name,
single_binding := ir.stmt.seq [
ir.stmt.letb fresh (ir.ty.name cpp_name) vm_name ir.stmt.nop,
ir.stmt.e $ ir.expr.assign `env (ir.expr.call `add_native [`env, fresh, replace_main n])
] in return $ single_binding :: tail
meta def emit_main (procs : list (name × expr)) : ir_compiler ir.defn := do
builtins ← emit_declare_vm_builtins procs,
arity ← lookup_arity `main,
vm_simple_obj ← fresh_name,
call_main ← compile_call "___lean__main" arity [ir.expr.locl vm_simple_obj],
return (ir.defn.mk `main [] ir.ty.int $ ir.stmt.seq ([
ir.stmt.e $ ir.expr.call (in_lean_ns `initialize) [],
ir.stmt.letb `env (ir.ty.name (in_lean_ns `environment)) ir.expr.uninitialized ir.stmt.nop
] ++ builtins ++ [
ir.stmt.letb `ios (ir.ty.name (in_lean_ns `io_state)) (ir.expr.call (in_lean_ns `get_global_ios) []) ir.stmt.nop,
ir.stmt.letb `opts (ir.ty.name (in_lean_ns `options)) (ir.expr.call (in_lean_ns `get_options_from_ios) [`ios]) ir.stmt.nop,
ir.stmt.letb `S (ir.ty.name (in_lean_ns `vm_state)) (ir.expr.constructor (in_lean_ns `vm_state) [`env, `opts]) ir.stmt.nop,
ir.stmt.letb `scoped (ir.ty.name (in_lean_ns `scope_vm_state)) (ir.expr.constructor (in_lean_ns `scope_vm_state) [`S]) ir.stmt.nop,
ir.stmt.e $ ir.expr.assign `g_env (ir.expr.address_of `env),
ir.stmt.letb vm_simple_obj ir.ty.object (ir.expr.mk_object 0 []) ir.stmt.nop,
ir.stmt.e call_main
]))
-- -- call_mains
-- -- buffer<expr> args;
-- -- auto unit = mk_neutral_expr();
-- -- args.push_back(unit);
-- -- // Make sure to invoke the C call machinery since it is non-deterministic
-- -- // which case we enter here.
-- -- compile_to_c_call(main_fn, args, 0, name_map<unsigned>());
-- -- *this→m_output_stream << ";\n return 0;\n}" << std::endl;
-- ]
meta def unzip {A B} : list (A × B) → (list A × list B)
| [] := ([], [])
| ((x, y) :: rest) :=
let (xs, ys) := unzip rest
in (x :: xs, y :: ys)
meta def configuration : ir_compiler config := do
(conf, _, _) ← lift $ state.read,
pure conf
meta def apply_pre_ir_passes (procs : list procedure) (conf : config) : list procedure :=
run_passes conf [anf, cf] procs
meta def driver (procs : list (name × expr)) : ir_compiler (list format × list error) := do
procs' ← apply_pre_ir_passes procs <$> configuration,
(fmt_decls, errs) ← sequence_err (compile' procs'),
main ← emit_main procs',
return (format_cpp.defn main :: fmt_decls, errs)
meta def compile (conf : config) (procs : list (name × expr)) : format :=
let arities := mk_arity_map procs in
-- Put this in a combinator or something ...
match run (driver procs) (conf, arities, 0) with
| (native.result.err e, s) := error.to_string e
| (native.result.ok (decls, errs), s) :=
if list.length errs = 0
then format_concat decls
else format_error (error.many errs)
end
-- meta def compile (procs : list (name))
end native

167
library/init/native/format.lean Normal file
View file

@ -0,0 +1,167 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.name
import init.meta.format
import init.function
import init.native.ir
def intersperse {A : Type} (elem : A) : list A → list A
| [] := []
| (x :: []) := [x]
| (x :: xs) := x :: elem :: intersperse xs
meta def format_concat : list format → format
| [] := format.nil
| (f :: fs) := f ++ format_concat fs
meta def comma_sep (items : list format) : format :=
format_concat
(intersperse (format.of_string "," ++ format.space) items)
namespace format_cpp
meta def mangle_name (n : name) : format :=
to_fmt $ name.to_string_with_sep "_" n
private meta def mk_constructor_args : list name → list format
| [] := []
| (n :: ns) := mangle_name n :: mk_constructor_args ns
private meta def mk_constructor
(arity : nat)
(fs : list name) : format :=
"lean::mk_vm_constructor(" ++ to_fmt arity ++ "," ++
(format.bracket "{" "}" (comma_sep $ mk_constructor_args fs)) ++ ")"
private meta def mk_call (symbol : name) (args : list name) : format :=
mangle_name symbol ++ (format.bracket "(" ")" (comma_sep $ list.map mangle_name args))
meta def literal : ir.literal → format
| (ir.literal.nat n) := to_fmt "lean::mk_vm_nat(" ++ to_fmt n ++ ")"
meta def format_local (n : name) : format :=
to_fmt (name.to_string_with_sep "_" n)
meta def string_lit (s : string) : format :=
format.bracket "\"" "\"" (to_fmt s)
meta def block (body : format) : format :=
format.bracket "{" "}" (format.nest 4 (format.line ++ body) ++ format.line)
meta def expr' (action : ir.stmt → format) : ir.expr → format
| (ir.expr.call f xs) := mk_call f xs
| (ir.expr.mk_object n fs) :=
if n = 0
-- Over time I should remove these special case functions,
-- and just use the def language of the IR.
then to_fmt "lean::mk_vm_simple(0)"
else mk_constructor n fs
| (ir.expr.global n) :=
mk_call n []
| (ir.expr.locl n) :=
mangle_name n
| (ir.expr.lit l) :=
literal l
| (ir.expr.block s) :=
block (action s)
-- project really should only work for like fields/primtive arrays, this is a temporary hack
| (ir.expr.project obj n) :=
"cfield(" ++ (mangle_name obj) ++ ", " ++ (to_fmt n) ++ ")"
| (ir.expr.panic err_msg) :=
to_fmt "throw std::runtime_error(" ++ string_lit err_msg ++ ");"
| (ir.expr.mk_native_closure n args) :=
"lean::mk_native_closure(*g_env, lean::name({\"" ++ name.to_string_with_sep "\", \"" n ++ "\"})" ++ "," ++
format.bracket "{" "}" (comma_sep (list.map format_local args)) ++ ")"
| (ir.expr.invoke n args) :=
"lean::invoke(" ++ name.to_string_with_sep "_" n ++ ", " ++
(comma_sep (list.map format_local args)) ++ ")"
| (ir.expr.uninitialized) := ";"
| (ir.expr.assign n val) := mangle_name n ++ " = " ++ expr' val
| (ir.expr.constructor _ _) := "NYI"
| (ir.expr.address_of e) := "& " ++ mangle_name e ++ ";"
| (ir.expr.equals e1 e2) := expr' e1 ++ " == " ++ expr' e2
| (ir.expr.raw_int n) := to_string n
| (ir.expr.sub e1 e2) :=
expr' e1 ++ " - " ++ expr' e2
meta def default_case (body : format) : format :=
to_fmt "default:" ++ block body
meta def case (action : ir.stmt → format) : (nat × ir.stmt) → format
| (n, s) := "case " ++ to_fmt n ++ ":" ++ block (action s ++ format.line ++ "break;" ++ format.line)
meta def cases (action : ir.stmt → format) : list (nat × ir.stmt) → format
| [] := format.nil
| (c :: cs) := case action c ++ cases cs
meta def ty : ir.ty → format
| ir.ty.object := format.of_string "lean::vm_obj "
| (ir.ty.ref T) := ty T ++ format.of_string " const & "
| (ir.ty.mut_ref T) := ty T ++ format.of_string " &"
| (ir.ty.tag _ _) := format.of_string "an_error"
| (ir.ty.int) := "int "
| (ir.ty.object_buffer) := "lean::buffer<lean::vm_obj> "
| (ir.ty.name n) := to_fmt n ++ format.space
meta def parens (inner : format) : format :=
format.bracket "(" ")" inner
meta def stmt : ir.stmt → format
| (ir.stmt.e e) := expr' stmt e ++ ";"
| (ir.stmt.return e) :=
format.of_string "return" ++
format.space ++
expr' stmt e ++ format.of_string ";"
| (ir.stmt.letb n t ir.expr.uninitialized nop) :=
ty t ++ (mangle_name n) ++ to_fmt ";" ++ format.line
-- type checking should establish that these two types are equal
| (ir.stmt.letb n t (ir.expr.constructor ty_name args) nop) :=
-- temporary hack, need to think about how to model this better
if ty_name = "lean::name"
then let ctor_args := comma_sep (list.map (string_lit ∘ to_string) args) in
ty t ++ (mangle_name n) ++ " = lean::name({" ++ ctor_args ++ "})" ++ to_fmt ";" ++ format.line
else let ctor_args := parens $ comma_sep (list.map mangle_name args) in
ty t ++ (mangle_name n) ++ ctor_args ++ to_fmt ";" ++ format.line
| (ir.stmt.letb n t v body) :=
ty t ++ (mangle_name n) ++ (to_fmt " = ") ++ (expr' stmt v) ++ to_fmt ";" ++
format.line ++ stmt body
| (ir.stmt.switch scrut cs default) :=
(to_fmt "switch (") ++ (mangle_name scrut) ++ (to_fmt ")") ++
(block (format.line ++ cases stmt cs ++ default_case (stmt default)))
| ir.stmt.nop := format.of_string ";"
| (ir.stmt.ite cond tbranch fbranch) :=
"if (" ++ mangle_name cond ++ ") {" ++ format.line ++
stmt tbranch ++ format.line ++
"} else {" ++ format.line ++
stmt fbranch ++ format.line ++
"}" ++ format.line
| (ir.stmt.seq cs) :=
format_concat (list.map (fun c, stmt c ++ format.line) cs)
meta def expr := expr' stmt
meta def format_param (param : name × ir.ty) :=
ty (prod.snd param) ++
format.space ++
to_fmt (name.to_string_with_sep "_" (mk_str_name "_$local$_" (name.to_string_with_sep "_" (prod.fst param))))
meta def format_argument_list (tys : list (name × ir.ty)) : format :=
format.bracket "(" ")" (comma_sep (list.map format_param tys))
-- meta_def format_prototypes ()
meta def defn (d : ir.defn) : format :=
match d with
| ir.defn.mk n arg_tys ret_ty body :=
let body := stmt body in
(ty ret_ty) ++ format.space ++ (mangle_name n) ++
(format_argument_list arg_tys) ++ format.space ++
(format.bracket "{" "}" $ format.nest 4 (format.line ++ body) ++ format.line)
end
end format_cpp

16
library/init/native/internal.lean Normal file
View file

@ -0,0 +1,16 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.expr
import init.meta.format
-- builtin stuff
meta constant native.is_internal_cnstr : expr → option unsigned
meta constant native.is_internal_cases : expr → option unsigned
meta constant native.is_internal_proj : expr → option unsigned
meta constant native.get_nat_value : expr → option nat
meta constant native.dump_format : string → format → nat

108
library/init/native/ir.lean Normal file
View file

@ -0,0 +1,108 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.name
namespace ir
inductive tag_ty
| mk
inductive ty
| object : ty
| ref : ty → ty
| mut_ref : ty → ty
| tag : tag_ty → ty → ty
-- these are temporary
| int : ty
| object_buffer : ty
| name : name → ty
inductive literal
| nat : nat → literal
-- inductive value : Type
-- | name : name → value
-- | lit : literal → value
-- TODO: eventually model ty.object, mk_object, project, etc in the IR itself
mutual inductive expr, stmt
with expr : Type
| call : name → list name → expr
| global : name → expr
| lit : literal → expr
| mk_object : nat → list name → expr
| locl : name → expr
| block : stmt → expr
| project : name → nat → expr
| panic : string → expr
| mk_native_closure : name → list name → expr
| invoke : name → list name → expr
| assign : name → expr → expr
| uninitialized : expr
| constructor : name → list name → expr
| address_of : name → expr
-- hack for now, do in secon pass clean up
| equals : expr → expr → expr
| sub : expr → expr → expr
| raw_int : nat → expr
-- | value : value → expr
with stmt : Type
| ite : name → stmt → stmt → stmt
| switch : name → list (nat × stmt) → stmt → stmt
| letb : name → ty → expr → stmt → stmt
| e : expr → stmt
-- use a list here
| seq : list stmt → stmt
| return : expr → stmt
| nop : stmt
inductive defn
| mk : name → list (name × ty) → ty → stmt → defn
inductive decl
| mk : name → list (name × ty) → ty → decl
inductive item
| defn : defn → item
| decl : decl → item
end ir
-- def map (K V : Type) : Type :=
-- list (K × V)
-- def lookup {K V} (key : K) (map : map K V) : option V :=
-- sorry
-- def context :=
-- map name ir_decl
-- inductive value
-- | int : nat → value
-- def local_context :=
-- map name ir_expr
-- def call_fn (ctxt : context) (local_cx : local_context) (fn_name : name) (args : list name) : option ir_expr :=
-- sorry
-- -- We fix the global context during evaluation.
-- inductive step_expr (ctxt : context) : local_context → ir_expr → value → Prop
-- | call :
-- forall n args local_cx retval,
-- call_fn ctxt local_cx n args = option.some retval →
-- step_expr local_cx (ir_expr.call n args) retval
-- | local_name :
-- forall n e local_cx retval,
-- lookup n local_cx = option.some e →
-- step_expr local_cx n e
-- inductive step_stmt : context → local_context → ir_stmt → ir_stmt → Prop
-- | nop : forall ctxt local_ctxt,
-- step_stmt ctxt local_ctxt nop nop
-- |

53
library/init/native/pass.lean Normal file
View file

@ -0,0 +1,53 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.expr
import init.meta.format
import init.native.internal
import init.native.procedure
import init.native.config
namespace native
meta structure pass :=
(name : string)
(transform : config → procedure → procedure)
meta def file_name_for_dump (p : pass) :=
(pass.name p)
-- Unit functions get optimized away, need to talk to Leo about this one.
meta def run_pass (conf : config) (p : pass) (proc : procedure) : (format × procedure × format) :=
let result := pass.transform p conf proc in
(to_string proc, result, to_string result)
meta def collect_dumps {A : Type} : list (format × A × format) → format × list A × format
| [] := (format.nil, [], format.nil)
| ((pre, body, post) :: fs) :=
let (pre', bodies, post') := collect_dumps fs
in (pre ++ format.line ++ format.line ++ pre',
body :: bodies,
post ++ format.line ++ format.line ++ post')
meta def inner_loop_debug (conf : config) (p : pass) (es : list procedure) : list procedure :=
let (pre, bodies, post) := collect_dumps (list.map (fun e, run_pass conf p e) es) in
match native.dump_format (file_name_for_dump p ++ ".pre") pre with
| n := match native.dump_format (file_name_for_dump p ++ ".post") post with
| m := if n = m then bodies else bodies
end
end
meta def inner_loop (conf : config) (p : pass) (es : list procedure) : list procedure :=
if config.debug conf
then inner_loop_debug conf p es
else list.map (fun proc, pass.transform p conf proc) es
meta def run_passes (conf : config) (passes : list pass) (procs : list procedure) : list procedure :=
list.foldl (fun pass procs, inner_loop conf procs pass) procs passes
end native

21
library/init/native/procedure.lean Normal file
View file

@ -0,0 +1,21 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.name
import init.meta.expr
meta def procedure :=
name × expr
meta def procedure.to_string : procedure → string
| (n, e) := "def " ++ to_string n ++ " := \n" ++ to_string e
meta def procedure.map_body (f : expr → expr) : procedure → procedure
| (n, e) := (n, f e)
meta instance : has_to_string procedure :=
⟨ procedure.to_string ⟩

73
library/init/native/result.lean Normal file
View file

@ -0,0 +1,73 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.category.applicative
import init.category.functor
import init.category.monad
import init.logic
import init.function
namespace native
inductive result (E : Type) (R : Type) : Type
| err {} : E → result
| ok {} : R → result
-- TODO: elaborator is still underway, eventually clean these up, hacking around elab bugs
def unwrap_or {E T : Type} : result E T → T → T
| (result.err _) default := default
| (result.ok t) _ := t
def result.map : Π {E : Type} {T : Type} {U : Type}, (T → U) → result E T → result E U
| E T U f (result.err e) := result.err e
| E T U f (result.ok t) := result.ok (f t)
def result.and_then {E T U : Type} : result E T → (T → result E U) → result E U
| (result.err e) _ := result.err e
| (result.ok t) f := f t
instance result_functor (E : Type) : functor (result E) := functor.mk (@result.map E)
def result.seq {E T U : Type} : result E (T → U) → result E T → result E U
| f t := result.and_then f (fun f', result.and_then t (fun t', result.ok (f' t')))
instance result_applicative (E : Type) : applicative (result E) :=
applicative.mk (@result.map E) (@result.ok E) (@result.seq E)
instance result_monad (E : Type) : monad (result E) :=
monad.mk (@result.map E) (@result.ok E) (@result.and_then E)
inductive resultT (M : Type → Type) (E : Type) (A : Type) : Type
| run : M (result E A) → resultT
section resultT
variable {M : Type → Type}
def resultT.map [functor : functor M] {E : Type} {A B : Type} : (A → B) → resultT M E A → resultT M E B
| f (resultT.run action) := resultT.run (@functor.map M functor _ _ (result.map f) action)
def resultT.pure [monad : monad M] {E A : Type} (x : A) : resultT M E A :=
resultT.run $ return (result.ok x)
def resultT.and_then [monad : monad M] {E A B : Type} : resultT M E A → (A → resultT M E B) → resultT M E B
| (resultT.run action) f := resultT.run (do
res_a ← action,
-- a little ugly with this match
(match res_a with
| native.result.err e := return (native.result.err e)
| native.result.ok a := let (resultT.run actionB) := f a in actionB
end : M (result E B)))
instance resultT_functor [f : functor M] (E : Type) : functor (resultT M E) :=
functor.mk (@resultT.map M f E)
-- Should we unify functor and monad like haskell?
instance resultT_monad [f : functor M] [m : monad M] (E : Type) : monad (resultT M E) :=
monad.mk (@resultT.map M f E) (@resultT.pure M m E) (@resultT.and_then M m E)
end resultT
end native

67
library/init/native/util.lean Normal file
View file

@ -0,0 +1,67 @@
/-
Copyright (c) 2016 Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jared Roesch
-/
prelude
import init.meta.format
import init.meta.expr
import init.data.string
import init.category.state
import init.native.result
import init.native.internal
import init.native.builtin
meta def is_nat_cases_on (n : name) : bool :=
decidable.to_bool $ `nat.cases_on = n
meta def is_cases_on (head : expr) : bool :=
if is_nat_cases_on (expr.const_name head)
then bool.tt
else
match native.is_internal_cases head with
| option.some _ := bool.tt
| option.none :=
match native.get_builtin (expr.const_name head) with
| option.some b :=
match b with
| builtin.cases _ _ := bool.tt
| _ := bool.ff
end
| option.none := bool.ff
end
end
meta definition mk_local (n : name) : expr :=
expr.local_const n n binder_info.default (expr.const n [])
meta def mk_neutral_expr : expr :=
expr.const `_neutral_ []
meta def mk_call : expr → list expr → expr
| head [] := head
| head (e :: es) := mk_call (expr.app head e) es
-- really need to get out of the meta language so I can prove things, I should just have a unit test lemma
meta def under_lambda {M} [monad M] (fresh_name : M name) (action : expr -> M expr) : expr → M expr
| (expr.lam n bi ty body) := do
fresh ← fresh_name,
body' ← under_lambda $ expr.instantiate_var body (mk_local fresh),
return $ expr.lam n bi ty (expr.abstract body' (mk_local fresh))
| e := action e
inductive application_kind
| cases
| constructor
| other
-- I like this pattern of hiding the annoying C++ interfaces
-- behind more typical FP constructs so we can do case analysis instead.
meta def app_kind (head : expr) : application_kind :=
if is_cases_on head
then application_kind.cases
else match native.is_internal_cnstr head with
| some _ := application_kind.constructor
| none := application_kind.other
end

3
library/system/io.lean
View file

@ -13,6 +13,9 @@ constant put_str : string → io unit
constant put_nat : nat → io unit
constant get_line : io string
def put_str_ln {A} [has_to_string A] (s : A) : io unit :=
put_str $ #"\n" :: (to_string s)
meta constant format.print_using : format → options → io unit
meta definition format.print (fmt : format) : io unit :=

9
old_library/system/IO.lean
View file

@ -3,6 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
-/
constant {u} IO : Type u → Type u
constant functorIO : functor IO
constant monadIO : monad IO
@ -13,6 +14,14 @@ constant put_str : string → IO unit
constant put_nat : nat → IO unit
constant get_line : IO string
constant forever : IO unit -> IO unit
definition put_str_ln (x : string) : IO unit :=
put_str ('\n' :: x)
definition print_str {A : Type} [str : has_to_string A] (a : A) : IO unit :=
put_str_ln (to_string a)
meta_constant format.print_using : format → options → IO unit
meta_definition format.print (fmt : format) : IO unit :=

41
src/CMakeLists.txt
View file

@ -236,6 +236,14 @@ else()
set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
endif()
# DL
set(EXTRA_LIBS ${EXTRA_LIBS} dl)
# TRACK_MEMORY_USAGE
if(TRACK_MEMORY_USAGE)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_TRACK_MEMORY")
endif()
# jemalloc
if(JEMALLOC)
find_package(Jemalloc)
@ -249,20 +257,20 @@ if(JEMALLOC)
endif()
# tcmalloc
if(NOT "${JEMALLOC_FOUND}")
if(TCMALLOC)
find_package(Tcmalloc)
if(${TCMALLOC_FOUND})
set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
message(STATUS "Using tcmalloc.")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D HAS_TCMALLOC")
else()
message(STATUS "Failed to find tcmalloc, using standard malloc.")
endif()
else()
message(STATUS "Using standard malloc.")
endif()
endif()
# if(NOT "${JEMALLOC_FOUND}")
# if(TCMALLOC)
# find_package(Tcmalloc)
# if(${TCMALLOC_FOUND})
# set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
# message(STATUS "Using tcmalloc.")
# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D HAS_TCMALLOC")
# else()
# message(STATUS "Failed to find tcmalloc, using standard malloc.")
# endif()
# else()
# message(STATUS "Using standard malloc.")
# endif()
# endif()
# Readline
if(READLINE)
@ -340,6 +348,8 @@ add_subdirectory(library/vm)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:vm>)
add_subdirectory(library/compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
add_subdirectory(library/native_compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:native_compiler>)
add_subdirectory(frontends/lean)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lean_frontend>)
add_subdirectory(frontends/smt2)
@ -354,7 +364,7 @@ set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ft
if(EMSCRIPTEN)
set(LEAN_LIBRARY_TYPE SHARED)
else()
set(LEAN_LIBRARY_TYPE STATIC)
set(LEAN_LIBRARY_TYPE STATIC)
endif()
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
target_link_libraries(leanstatic ${EXTRA_LIBS})
@ -369,6 +379,7 @@ if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
add_library(leanshared SHARED shared/init.cpp $<TARGET_OBJECTS:api> ${LEAN_OBJS})
target_link_libraries(leanshared ${EXTRA_LIBS})
install(TARGETS leanshared DESTINATION lib)
install(TARGETS leanstatic DESTINATION lib)
endif()
add_subdirectory(shell)

26
src/frontends/lean/parser.cpp
View file

@ -672,6 +672,32 @@ unsigned parser::get_small_nat() {
return val.get_unsigned_int();
}
std::string parser::parse_string_lit() {
std::string v = get_str_val();
next();
return v;
}
name_map<std::string> parser::parse_kv_pairs() {
name_map<std::string> pairs;
return pairs;
// check_token_next(get_lparen_tk(), "invalid attribute options, '(' expected");
// bool comma = false;
// while (!p.curr_is_token(get_rparen_tk())) {
// p.next();
// if (comma) {
// check_token_next(get_comma_tk(), "invalid attribute options, ',' expected");
// } else {
// comma = true;
// }
//
// std::string k = parse_string_lit();
// std::cout << "parsed: " << k << std::endl;
// }
// check_token_next(get_rparen_tk(), "invalid attribute options, ')' expected");
// return pairs;
}
unsigned parser::parse_small_nat() {
if (!curr_is_numeral())
throw parser_error("(small) natural number expected", pos());

2
src/frontends/lean/parser.h
View file

@ -323,6 +323,8 @@ public:
unsigned get_small_nat();
virtual unsigned parse_small_nat() override final;
virtual std::string parse_string_lit() override final;
virtual name_map<std::string> parse_kv_pairs() override final;
double parse_double();
bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); }

4
src/init/init.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "library/constructions/init_module.h"
#include "library/equations_compiler/init_module.h"
#include "library/inductive_compiler/init_module.h"
#include "library/native_compiler/init_module.h"
#include "library/print.h"
#include "library/vm/init_module.h"
#include "library/compiler/init_module.h"
@ -38,6 +39,7 @@ void initialize() {
initialize_vm_core_module();
initialize_library_module();
initialize_compiler_module();
initialize_native_compiler_module();
initialize_tactic_module();
initialize_constructions_module();
initialize_equations_compiler_module();
@ -46,6 +48,7 @@ void initialize() {
initialize_frontend_smt2_module();
initialize_vm_module();
}
void finalize() {
run_thread_finalizers();
finalize_vm_module();
@ -55,6 +58,7 @@ void finalize() {
finalize_equations_compiler_module();
finalize_constructions_module();
finalize_tactic_module();
finalize_native_compiler_module();
finalize_compiler_module();
finalize_library_module();
finalize_vm_core_module();

2
src/library/abstract_parser.h
View file

@ -33,5 +33,7 @@ public:
virtual void next() = 0;
virtual unsigned parse_small_nat() = 0;
virtual std::string parse_string_lit() = 0;
virtual name_map<std::string> parse_kv_pairs() = 0;
};
}

49
src/library/attribute_manager.h
View file

@ -210,10 +210,59 @@ struct indices_attribute_data : public attr_data {
}
};
struct key_value_data : public attr_data {
// generalize: name_map<std::string> m_pairs;
std::string m_symbol;
std::string m_library;
virtual unsigned hash() const override {
// unsigned h = 0;
// // This isn't right ..., well maybe? I don't really know.
// // Rust's Hash trait is super good at this.
// m_pairs.for_each([&] (name const & n, std::string const & value) {
// h += n.hash();
// // h += ::lean::hash_str(value, h);
// });
return 0;
}
void write(serializer & s) const {
s << m_symbol;
s << m_library;
}
void read(deserializer & d) {
std::string m_symbol, m_library;
d >> m_symbol;
d >> m_library;
}
void parse(abstract_parser & p) override {
std::cout << "in extern parser" << std::endl;
std::string n = p.parse_string_lit();
std::string l = p.parse_string_lit();
std::cout << "link symbol: " << n << std::endl;
std::cout << "library symbol: " << l << std::endl;
this->m_symbol = n;
this->m_library = l;
}
virtual void print(std::ostream & out) override {
out << "external";
// for (auto p : m_idxs) {
// out << " " << p + 1;
// }
}
};
template class typed_attribute<indices_attribute_data>;
/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
typedef typed_attribute<indices_attribute_data> indices_attribute;
template class typed_attribute<key_value_data>;
/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
typedef typed_attribute<key_value_data> key_value_attribute;
class user_attribute_ext {
public:
virtual name_map<attribute_ptr> get_attributes(environment const & env);

3
src/library/compiler/CMakeLists.txt
View file

@ -1,4 +1,5 @@
add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess.cpp
compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp
lambda_lifting.cpp simp_inductive.cpp nat_value.cpp vm_compiler.cpp init_module.cpp)
lambda_lifting.cpp simp_inductive.cpp nat_value.cpp
vm_compiler.cpp init_module.cpp)

1
src/library/compiler/erase_irrelevant.cpp
View file

@ -175,6 +175,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
name const & I_name = rec_name.get_prefix();
if (I_name == get_false_name())
return *g_unreachable_expr;
/* This preprocessing step assumes that recursive recursors have already been eliminated */
lean_assert(!is_recursive_datatype(env(), I_name));
unsigned nparams = *inductive::get_num_params(env(), I_name);

1
src/library/compiler/init_module.cpp
View file

@ -24,6 +24,7 @@ void initialize_compiler_module() {
initialize_simp_inductive();
initialize_vm_compiler();
}
void finalize_compiler_module() {
finalize_vm_compiler();
finalize_simp_inductive();

44
src/library/compiler/vm_compiler.cpp
View file

@ -22,6 +22,12 @@ Author: Leonardo de Moura
#include "library/compiler/preprocess.h"
#include "library/compiler/comp_irrelevant.h"
/* These are used for loading external native dependencies in the virtual
machine.
*/
#include "library/native_compiler/extern.h"
#include "library/native_compiler/used_defs.h"
namespace lean {
class vm_compiler_fn {
environment m_env;
@ -199,6 +205,15 @@ class vm_compiler_fn {
emit_apply_instr(args.size() - 1);
}
void compile_external(name const & n, buffer<expr> & args, unsigned bpz, name_map<unsigned> const & m) {
// Not sure if this is the best approach, trying to lazy load the required
// dynamic libraries.
std::cout << "external compile" << n << std::endl;
optional<vm_decl> decl = get_vm_decl(m_env, n);
lean_assert(decl);
compile_global(*decl, args.size(), args.data(), bpz, m);
}
void compile_fn_call(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
buffer<expr> args;
expr fn = get_app_args(e, args);
@ -212,6 +227,8 @@ class vm_compiler_fn {
emit(mk_sconstructor_instr(0));
} else if (optional<vm_decl> decl = get_vm_decl(m_env, const_name(fn))) {
compile_global(*decl, args.size(), args.data(), bpz, m);
} else if (has_extern_attribute(m_env, const_name(fn))) {
compile_external(const_name(fn), args, bpz, m);
} else {
throw_unknown_constant(const_name(fn));
}
@ -337,11 +354,38 @@ public:
}
};
buffer<name> extern_names(environment const & env, buffer<procedure> const & procs) {
used_defs live_names(env, [&] (declaration const & d) {
live_names.names_in_decl(d);
});
for (auto p : procs) {
live_names.names_in_preprocessed_body(p.m_code);
}
buffer<name> extern_ns;
live_names.m_used_names.for_each([&] (name const & n) {
if (has_extern_attribute(env, n)) {
std::cout << "found external to load: " << n << std::endl;
extern_ns.push_back(n);
}
});
return extern_ns;
}
static environment vm_compile(environment const & env, buffer<procedure> const & procs) {
environment new_env = env;
for (auto const & p : procs) {
new_env = reserve_vm_index(new_env, p.m_name, p.m_code);
}
// Load all the external functions required by this compilation.
auto ns = extern_names(env, procs);
for (auto n : ns) {
new_env = load_external_fn(new_env, n);
}
for (auto const & p : procs) {
buffer<vm_instr> code;
vm_compiler_fn gen(new_env, code);

4
src/library/io_state.cpp
View file

@ -92,6 +92,10 @@ char const * formatted_exception::what() const noexcept {
return r.c_str();
}
options const & get_options_from_ios(io_state const & ios) {
return ios.get_options();
}
void initialize_io_state() {
g_dummy_ios = new io_state(mk_print_formatter_factory());
}

2
src/library/io_state.h
View file

@ -79,6 +79,8 @@ public:
~scope_global_ios();
};
options const & get_options_from_ios(io_state const & ios);
void initialize_io_state();
void finalize_io_state();
}

2
src/library/module_mgr.cpp
View file

@ -98,6 +98,8 @@ public:
mod.m_env = optional<environment>(p.env());
mod.m_opts = p.ios().get_options();
mod.m_ok = parsed_ok; // TODO(gabriel): what should this be?
return mod;

1
src/library/module_mgr.h
View file

@ -39,6 +39,7 @@ struct module_info {
struct parse_result {
optional<environment> m_env;
options m_opts;
bool m_ok = false;
std::string m_obj_code;

2
src/library/native_compiler/CMakeLists.txt Normal file
View file

@ -0,0 +1,2 @@
add_library(native_compiler OBJECT init_module.cpp native_compiler.cpp
cpp_emitter.cpp options.cpp used_defs.cpp cpp_compiler.cpp extern.cpp)

108
src/library/native_compiler/cpp_compiler.cpp Normal file
View file

@ -0,0 +1,108 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include "cpp_compiler.h"
#include "util/process.h"
namespace lean {
cpp_compiler & cpp_compiler::link(std::string lib) {
m_link.push_back(lib);
return *this;
}
cpp_compiler & cpp_compiler::library_path(std::string lib_path) {
m_library_paths.push_back(lib_path);
return *this;
}
cpp_compiler & cpp_compiler::include_path(std::string include_path) {
m_include_paths.push_back(include_path);
return *this;
}
cpp_compiler & cpp_compiler::debug(bool on) {
m_debug = on;
return *this;
}
cpp_compiler & cpp_compiler::file(std::string file_path) {
m_files.push_back(file_path);
return *this;
}
cpp_compiler::cpp_compiler() : m_library_paths(), m_include_paths(), m_files(), m_link(), m_debug(false) {}
cpp_compiler & cpp_compiler::shared_library(bool on) {
m_shared = on;
return *this;
}
cpp_compiler & cpp_compiler::pic(bool on) {
m_pic = on;
return * this;
}
void cpp_compiler::run() {
process p("g++");
p.arg("-std=c++11");
if (m_pic) {
p.arg("-fPIC");
}
if (m_shared) {
p.arg("-shared");
}
// Add all the library paths.
for (auto include_path : m_include_paths) {
std::string arg("-I");
arg += include_path;
p.arg(arg);
}
// Add all the link paths.
for (auto link_path : m_library_paths) {
std::string arg("-L");
arg += link_path;
p.arg(arg);
}
// Add all the files
for (auto file_path : m_files) {
p.arg(file_path);
}
// Add all the link arguments.
for (auto link: m_link) {
std::string arg("-l");
arg += link;
p.arg(arg);
}
if (m_debug) {
p.arg("-g");
}
p.run();
}
// Setup a compiler for building executables.
cpp_compiler mk_executable_compiler() {
cpp_compiler gpp;
gpp.link(LEAN_STATIC_LIB);
return gpp;
}
// Setup a compiler for building dynamic libraries.
cpp_compiler mk_shared_compiler() {
cpp_compiler gpp;
gpp.link(LEAN_SHARED_LIB);
gpp.pic(true);
gpp.shared_library(true);
return gpp;
}
}

47
src/library/native_compiler/cpp_compiler.h Normal file
View file

@ -0,0 +1,47 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <iostream>
#include "unistd.h"
#include "kernel/environment.h"
#include "kernel/expr.h"
namespace lean {
#define LEAN_STATIC_LIB "leanstatic"
#define LEAN_SHARED_LIB "leanshared"
class cpp_compiler {
buffer<std::string> m_library_paths;
buffer<std::string> m_include_paths;
buffer<std::string> m_files;
buffer<std::string> m_link;
bool m_debug;
bool m_shared;
bool m_pic;
public:
cpp_compiler & link(std::string lib);
cpp_compiler & library_path(std::string lib_path);
cpp_compiler & include_path(std::string include_path);
cpp_compiler & debug(bool on);
cpp_compiler & shared_library(bool on);
cpp_compiler & pic(bool on);
cpp_compiler & file(std::string file_path);
cpp_compiler();
void run();
};
// Setup a compiler for building executables.
cpp_compiler mk_executable_compiler();
// Setup a compiler for building dynamic libraries.
cpp_compiler mk_shared_compiler();
}

91
src/library/native_compiler/cpp_emitter.cpp Normal file
View file

@ -0,0 +1,91 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include <fstream>
#include <iostream>
#include <iomanip>
#include <utility>
#include "cpp_emitter.h"
#include "kernel/environment.h"
namespace lean {
void cpp_emitter::emit_headers() {
*this->m_output_stream <<
"#include <iostream>" << std::endl <<
"#include \"util/numerics/mpz.h\"" << std::endl <<
"#include \"library/vm/vm_io.h\"" << std::endl <<
"#include \"library/vm/vm.h\"" << std::endl <<
"#include \"library/io_state.h\"" << std::endl <<
"#include \"init/init.h\"" << std::endl << std::endl <<
"static lean::environment * g_env = nullptr;" << std::endl << std::endl;
}
void cpp_emitter::indent() {
this->m_width += 4;
}
void cpp_emitter::unindent() {
this->m_width -= 4;
}
void cpp_emitter::mangle_name(name const & n) {
if (n == name("main")) {
*this->m_output_stream << "___lean__main";
} else if (n.is_anonymous()) {
*this->m_output_stream << "anon_name?";
} else if (n.is_string()) {
auto s = n.to_string("_");
*this->m_output_stream << s;
} else if (n.is_numeral()) {
auto s = n.to_string("_");
*this->m_output_stream << "__lean_nv_" << s;
} else {
lean_unreachable();
}
}
void cpp_emitter::emit_declare_vm_builtin(name const & n) {
emit_indented("env = add_native(env, lean::name({");
*this->m_output_stream << "\"" << n.to_string("\" , \"") << "\"}), ";
mangle_name(n);
*this->m_output_stream << ");\n";
}
void cpp_emitter::emit_prototype(name const & n, unsigned arity) {
*this->m_output_stream << "lean::vm_obj ";
mangle_name(n);
auto comma = false;
*this->m_output_stream << "(";
for (unsigned i = 0; i < arity; i++) {
if (comma) {
*this->m_output_stream << ", ";
} else {
comma = true;
}
*this->m_output_stream << "lean::vm_obj const &";
}
*this->m_output_stream << ");" << std::endl;
}
void cpp_emitter::emit_string(const char * str) {
*this->m_output_stream << str;
}
void cpp_emitter::emit_indented(const char * str) {
this->m_output_stream->width(this->m_width);
*this->m_output_stream << str;
this->m_output_stream->width(0);
}
void cpp_emitter::emit_indented_line(const char * str) {
this->m_output_stream->width(this->m_width);
*this->m_output_stream << str << std::endl;
this->m_output_stream->width(this->m_width);
}
}

50
src/library/native_compiler/cpp_emitter.h Normal file
View file

@ -0,0 +1,50 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <iostream>
#include "kernel/environment.h"
#include "kernel/expr.h"
namespace lean {
static const char * LEAN_OBJ_TYPE = "lean::vm_obj";
// static const char * LEAN_ERR = "lean::runtime_error";
class cpp_emitter {
int m_width;
public:
std::fstream * m_output_stream;
cpp_emitter(std::string path) : m_width(0), m_output_stream(nullptr) {
this->m_output_stream =
new std::fstream(path.c_str(), std::ios_base::out);
}
~cpp_emitter() {
this->m_output_stream->flush();
this->m_output_stream->close();
delete this->m_output_stream;
}
void emit_headers();
void indent();
void unindent();
void emit_name(name const & n) {
this->emit_string("name({\"");
this->emit_string(n.to_string("\"}, {\"").c_str());
this->emit_string("\"})");
}
void emit_prototype(name const & n, unsigned arity);
void emit_indented(const char * str);
void emit_string(const char * str);
void emit_indented_line(const char * str);
void mangle_name(name const & n);
void emit_declare_vm_builtin(name const & n);
};
}

32
src/library/native_compiler/extern.cpp Normal file
View file

@ -0,0 +1,32 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include "library/attribute_manager.h"
namespace lean {
bool has_extern_attribute(environment const & env, name const & d) {
return has_attribute(env, "extern", d);
}
std::string library_name(environment const & env, name const & d) {
auto attr = static_cast<key_value_attribute const &>(get_attribute(env, "extern"));
auto data = attr.get(env, d);
return data->m_library;
}
std::string symbol_name(environment const & env, name const & d) {
auto attr = static_cast<key_value_attribute const &>(get_attribute(env, "extern"));
auto data = attr.get(env, d);
return data->m_symbol;
}
void initialize_extern_attribute() {
register_system_attribute(key_value_attribute("extern", "mark a constant as external to Lean"));
}
void finalize_extern_attribute() {
}
}

17
src/library/native_compiler/extern.h Normal file
View file

@ -0,0 +1,17 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <string>
#include "kernel/environment.h"
namespace lean {
bool has_extern_attribute(environment const & env, name const & d);
std::string library_name(environment const & env, name const & d);
std::string symbol_name(environment const & env, name const & d);
void initialize_extern_attribute();
void finalize_extern_attribute();
}

20
src/library/native_compiler/init_module.cpp Normal file
View file

@ -0,0 +1,20 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include "library/native_compiler/native_compiler.h"
#include "library/native_compiler/extern.h"
namespace lean {
void initialize_native_compiler_module() {
initialize_native_compiler();
initialize_extern_attribute();
}
void finalize_native_compiler_module() {
finalize_extern_attribute();
finalize_native_compiler();
}
}

11
src/library/native_compiler/init_module.h Normal file
View file

@ -0,0 +1,11 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
namespace lean {
void initialize_native_compiler_module();
void finalize_native_compiler_module();
}

516
src/library/native_compiler/native_compiler.cpp Normal file
View file

@ -0,0 +1,516 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch and Leonardo de Moura
*/
#include "util/fresh_name.h"
#include "util/sstream.h"
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/trace.h"
#include "library/annotation.h"
#include "library/vm/vm.h"
#include "library/vm/optimize.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_format.h"
#include "library/util.h"
#include "library/compiler/simp_inductive.h"
#include "library/compiler/erase_irrelevant.h"
#include "library/compiler/nat_value.h"
#include "library/compiler/preprocess.h"
#include "library/native_compiler/native_compiler.h"
#include "library/native_compiler/options.h"
#include "library/native_compiler/cpp_compiler.h"
#include "library/native_compiler/extern.h"
#include "library/compiler/vm_compiler.h"
#include "library/module.h"
#include "library/vm/vm.h"
#include "cpp_emitter.h"
#include "used_defs.h"
#include "util/lean_path.h"
// #include "util/executable.h"
#include <sys/types.h>
#include <sys/stat.h>
#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
static std::string* g_lean_install_path;
namespace lean {
expr mk_local(name const & n) {
return ::lean::mk_local(n, mk_neutral_expr());
}
// Helper functions for setting up the install path on boot-up.
void initialize_install_path() {
// 8 is the size of the string bin/lean which we want to remove from
// the installed version of Lean.
auto path = get_exe_location();
g_lean_install_path = new std::string(path.substr(0, path.size() - 8));
}
std::string get_install_path() {
return *g_lean_install_path;
}
extern_fn mk_lean_extern(name n, unsigned arity) {
return extern_fn(true, n, arity);
}
extern_fn mk_extern(name n, unsigned arity) {
return extern_fn(false, n, arity);
}
class native_compiler_fn {
public:
environment m_env;
cpp_emitter m_emitter;
native_compiler_mode m_mode;
name_map<unsigned> m_arity_map;
public:
native_compiler_fn(environment const & env):
m_env(env), m_emitter(cpp_emitter(std::string("out.cpp"))) {}
void emit_headers() {
this->m_emitter.emit_headers();
}
// Not the most effcient, need to do two loops.
void emit_prototypes(buffer<extern_fn> fns) {
buffer<extern_fn> in_lean_namespace;
buffer<extern_fn> rest;
for (auto fn : fns) {
if (fn.m_in_lean_namespace) {
in_lean_namespace.push_back(fn);
} else {
rest.push_back(fn);
}
}
this->m_emitter.emit_string("namespace lean {\n");
for (auto fn : in_lean_namespace) {
auto np = get_vm_builtin_internal_name(fn.m_name);
if (np && get_vm_builtin_kind(fn.m_name) == vm_builtin_kind::Cases) {
auto np = get_vm_builtin_internal_name(fn.m_name);
lean_assert(np);
this->m_emitter.emit_string("unsigned ");
this->m_emitter.mangle_name(fn.m_name);
this->m_emitter.emit_string("(lean::vm_obj const & o, lean::buffer<lean::vm_obj> & data);\n");
} else {
this->m_emitter.emit_prototype(fn.m_name, fn.m_arity);
}
}
this->m_emitter.emit_string("}\n\n");
// We should be really generating things with C linkage to make
// interfacing with non-cpp stuff possible.
// this->m_emitter.emit_string("extern \"C\" {\n");
for (auto fn : rest) {
if (get_vm_builtin_cases_idx(m_env, fn.m_name)) {
auto np = get_vm_builtin_internal_name(fn.m_name);
lean_assert(np);
this->m_emitter.emit_string("unsigned ");
this->m_emitter.mangle_name(fn.m_name);
this->m_emitter.emit_string("(lean::vm_obj const & o, lean::buffer<lean::vm_obj> & data);\n");
} else {
this->m_emitter.emit_prototype(fn.m_name, fn.m_arity);
}
}
// this->m_emitter.emit_string("}\n\n");
}
unsigned get_arity(expr e) {
unsigned r = 0;
while (is_lambda(e)) {
r++;
e = binding_body(e);
}
return r;
}
void emit_prototype(name const & n, expr e) {
this->m_emitter.emit_prototype(n, get_arity(e));
}
void populate_arity_map(buffer<procedure> const & procs) {
for (auto & p : procs) {
m_arity_map.insert(p.m_name, get_arity(p.m_code));
}
}
void populate_arity_map(buffer<extern_fn> const & procs) {
for (auto & p : procs) {
m_arity_map.insert(p.m_name, p.m_arity);
}
}
};
// Returns the path to the Lean library based on the standard search path,
// and provided options.
std::vector<std::string> native_include_paths() {
std::vector<std::string> paths;
auto conf = native::get_config();
auto native_include_path = std::string(conf.m_native_include_path);
// std::cout << native_include_path << std::endl;
// // TODO: support general path parsing here
if (native_include_path.compare("") == 0) {
// Finally look in the default path.
paths.push_back(get_install_path() + "include/lean_ext");
} else {
paths.push_back(native_include_path);
}
return paths;
}
std::vector<std::string> native_library_paths() {
std::vector<std::string> paths;
auto conf = native::get_config();
auto native_library_path = std::string(conf.m_native_library_path);
// // TODO: support general path parsing here
if (native_library_path.compare("") == 0) {
// Finally look in the default path.
paths.push_back(get_install_path() + "lib");
} else {
paths.push_back(native_library_path);
}
return paths;
}
// Constructs a compiler with the native configuation options applied.
cpp_compiler compiler_with_native_config(native_compiler_mode mode) {
cpp_compiler gpp;
if (mode == native_compiler_mode::AOT) {
gpp = mk_executable_compiler();
} else {
gpp = mk_shared_compiler();
}
auto conf = native::get_config();
auto include_paths = native_include_paths();
auto library_paths = native_library_paths();
// Setup include paths
for (auto path : include_paths) {
gpp.include_path(path);
}
for (auto path : library_paths) {
gpp.library_path(path);
}
// Have g++ emit debug information.
if (conf.m_native_emit_dwarf) {
gpp.debug(true);
}
return gpp;
}
void add_shared_dependencies(cpp_compiler & compiler) {
compiler.link("gmp")
.link("pthread")
.link("mpfr");
}
/* This function constructs a config value located in library/native/config.lean */
vm_obj mk_lean_native_config() {
auto native_conf = native::get_config();
// native_conf.display(std::cout);
std::cout << native_conf.m_native_dump << std::endl;
if (native_conf.m_native_dump == std::string("")) {
return mk_vm_simple(0);
} else {
return mk_vm_simple(1);
}
}
void native_compile(environment const & env,
buffer<extern_fn> & extern_fns,
buffer<procedure> & procs,
native_compiler_mode mode) {
native_compiler_fn compiler(env);
buffer<name> ns;
compiler.populate_arity_map(procs);
compiler.populate_arity_map(extern_fns);
// Emit the header includes.
compiler.emit_headers();
// Emit externs (currently only works for builtins).
compiler.emit_prototypes(extern_fns);
for (auto & p : procs) {
compiler.emit_prototype(p.m_name, p.m_code);
}
// First we convert for Lean ...
vm_obj procs_list = mk_vm_simple(0);
for (auto & p : procs) {
auto tuple = mk_vm_constructor(0, { to_obj(p.m_name), to_obj(p.m_code) });
procs_list = mk_vm_constructor(1, { tuple, procs_list });
}
vm_state S(env, get_global_ios().get_options());
scope_vm_state scoped(S);
// std::cout << "About to compile" << std::endl;
auto compiler_name = name({"native", "compile"});
auto cc = mk_native_closure(env, compiler_name, {});
auto conf = mk_lean_native_config();
vm_obj result = S.invoke(cc, conf, procs_list);
auto fmt = to_format(result);
std::string fn = (sstream() << fmt << "\n\n").str();
compiler.m_emitter.emit_string(fn.c_str());
// For now just close this, then exit.
compiler.m_emitter.m_output_stream->close();
// Get a compiler with the config specified by native options, placed
// in the correct mode.
auto gpp = compiler_with_native_config(mode);
// Add all the shared link dependencies.
add_shared_dependencies(gpp);
gpp.file("out.cpp")
.run();
}
void native_preprocess(environment const & env, declaration const & d, buffer<procedure> & procs) {
lean_trace(name({"compiler", "native"}),
tout() << "native_preprocess:" << d.get_name() << "\n";);
// Run the normal preprocessing and optimizations.
preprocess(env, d, procs);
}
bool is_internal_decl(declaration const & d) {
auto n = d.get_name();
return (n == name("_neutral_") ||
n == name({"native_compiler", "return"}) ||
is_internal_cnstr(mk_constant(n)) ||
is_internal_cases(mk_constant(n)) ||
is_internal_proj(mk_constant(n)));
}
optional<extern_fn> get_builtin(name const & n) {
auto internal_name = get_vm_builtin_internal_name(n);
if (internal_name) {
switch (get_vm_builtin_kind(n)) {
case vm_builtin_kind::VMFun: {
return optional<extern_fn>();
}
case vm_builtin_kind::CFun: {
auto arity = get_vm_builtin_arity(n);
return optional<extern_fn>(
mk_lean_extern(internal_name, arity));
}
case vm_builtin_kind::Cases: {
return optional<extern_fn>(
mk_lean_extern(internal_name, 2u));
}
}
} else {
return optional<extern_fn>();
}
}
void populate_extern_fns(
environment const & env,
used_defs const & used,
buffer<extern_fn> & extern_fns, bool is_library)
{
used.m_used_names.for_each([&] (name const & n) {
if (auto builtin = get_builtin(n)) {
// std::cout << "extern fn: " << n << std::endl;
extern_fns.push_back(mk_lean_extern(n, builtin.value().m_arity));
} else if (has_extern_attribute(env, n)) {
extern_fns.push_back(mk_extern(n, 0));
} else if (is_library) {
extern_fns.push_back(mk_extern(n, 0));
}
});
}
void native_compile_module(environment const & env, buffer<declaration> decls) {
std::cout << "compiled native module" << std::endl;
// Preprocess the main function.
buffer<procedure> all_procs;
buffer<procedure> main_procs;
buffer<extern_fn> extern_fns;
// Compute the live set of names, we attach a callback that will be
// invoked for every declaration encountered.
used_defs used_names(env, [&] (declaration const & d) {
buffer<procedure> procs;
// The the name is an internal decl we should not add it to the live set.
if (is_internal_decl(d)) {
return;
// We should skip it if its a bulitin, or a builtin_cases on.
} else if (auto p = get_builtin(d.get_name())) {
return;
// extern_fns.push_back(p.value());
} else if (auto p = get_vm_builtin_cases_idx(env, d.get_name())) {
return;
} else if (has_extern_attribute(env, d.get_name())) {
lean_unreachable()
} else {
native_preprocess(env, d, procs);
for (auto pair : procs) {
used_names.names_in_expr(pair.m_code);
all_procs.push_back(pair);
}
}
});
// We then loop over the set of procs produced by preprocessing the
// main function, we transitively collect all names.
for (auto decl : decls) {
used_names.names_in_decl(decl);
}
// We now need to collect every function we are choosing to
// declare as external. We emit an extern decl for every
// function that exists in the Lean namespace, and then
// an extern decl for every other function, since the
// symbols must be visible to other shared libraries
// when loading them.
populate_extern_fns(env, used_names, extern_fns, true);
// Finally we assert that there are no more unprocessed declarations.
lean_assert(used_names.stack_is_empty());
native_compile(env, extern_fns, all_procs, native_compiler_mode::JIT);
}
void native_compile_binary(environment const & env, declaration const & d) {
lean_trace(name("native_compile"),
tout() << "main_fn: " << d.get_name() << "\n";);
lean_trace(name("native_compiler"),
tout() << "main_body: " << d.get_value() << "\n";);
// Preprocess the main function.
buffer<procedure> all_procs;
buffer<procedure> main_procs;
buffer<extern_fn> extern_fns;
native_preprocess(env, d, main_procs);
// Compute the live set of names, we attach a callback that will be
// invoked for every declaration encountered.
used_defs used_names(env, [&] (declaration const & d) {
buffer<procedure> procs;
if (is_internal_decl(d)) {
return;
} else if (auto p = get_builtin(d.get_name())) {
return;
// extern_fns.push_back(p.value());
} else if (auto p = get_vm_builtin_cases_idx(env, d.get_name())) {
return;
} else {
native_preprocess(env, d, procs);
for (auto pair : procs) {
used_names.names_in_expr(pair.m_code);
all_procs.push_back(pair);
}
}
});
// We then loop over the set of procs produced by preprocessing the
// main function, we transitively collect all names.
for (auto pair : main_procs) {
all_procs.push_back(pair);
used_names.names_in_preprocessed_body(pair.m_code);
}
populate_extern_fns(env, used_names, extern_fns, false);
// Finally we assert that there are no more unprocessed declarations.
lean_assert(used_names.stack_is_empty());
native_compile(env, extern_fns, all_procs, native_compiler_mode::AOT);
}
// +void decls_to_native_compile(environment const & env, buffer<declaration> & decls) {
// + // module_ext const & ext = get_extension(env);
// + //
// + // // Collect all the declarations that should be compiled from this
// + // // module.
// + // for (auto decl_name : ext.m_module_decls) {
// + // auto decl = env.get(decl_name);
// + // if (is_noncomputable(env, decl_name) ||
// + // !decl.is_definition() ||
// + // is_vm_builtin_function(decl_name)) {
// + // continue;
// + // } else {
// + // std::cout << decl.get_name() << std::endl;
// + // decls.push_back(decl);
// + // }
// + // }
// +}
void native_compile_module(environment const & env) {
buffer<declaration> decls;
// TODO: bring this code back
// decls_to_native_compile(env, decls);
native_compile_module(env, decls);
}
// Setup for the storage of native modules to .olean files.
static std::string *g_native_module_key = nullptr;
static void native_module_reader(
deserializer & d,
environment & env) {
name fn;
d >> fn;
std::cout << "reading native module from meta-data: " << fn << std::endl;
// senv.update([&](environment const & env) -> environment {
// vm_decls ext = get_extension(env);
// // ext.update(fn, code_sz, code.data());
// // return update(env, ext);
// return
// });
}
environment set_native_module_path(environment & env, name const & n) {
return module::add(env, *g_native_module_key, [=] (environment const & e, serializer & s) {
std::cout << "writing out" << n << std::endl;
s << n;
native_compile_module(e);
});
}
void initialize_native_compiler() {
native::initialize_options();
initialize_install_path();
register_trace_class({"compiler", "native"});
register_trace_class({"compiler", "native", "preprocess"});
register_trace_class({"compiler", "native", "cpp_compiler"});
g_native_module_key = new std::string("native_module_path");
register_module_object_reader(*g_native_module_key, native_module_reader);
}
void finalize_native_compiler() {
native::finalize_options();
delete g_native_module_key;
}
}

36
src/library/native_compiler/native_compiler.h Normal file
View file

@ -0,0 +1,36 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include "kernel/environment.h"
namespace lean {
void initialize_install_path();
std::string get_install_path();
struct extern_fn {
bool m_in_lean_namespace;
name m_name;
unsigned m_arity;
extern_fn(bool in_lean_namespace, name n, unsigned arity) :
m_in_lean_namespace(in_lean_namespace), m_name(n), m_arity(arity) {}
};
optional<extern_fn> get_builtin(name const & n);
enum native_compiler_mode { JIT, AOT };
void native_compile(environment const & env, buffer<pair<name, expr>> & procs, native_compiler_mode & mode);
void native_compile_binary(environment const & env, declaration const & d);
void native_compile_module(environment const & env, buffer<declaration> decls);
void native_compile_module(environment const & env);
// void native_aot_compile(environment const & env, config & conf, declaration const & main);
// void native_compile_file(environment const & env, config & conf, declaration const & main);
environment set_native_module_path(environment & env, name const & n);
void initialize_native_compiler();
void finalize_native_compiler();
}

129
src/library/native_compiler/options.cpp Normal file
View file

@ -0,0 +1,129 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch, and Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "library/native_compiler/options.h"
#ifndef LEAN_DEFAULT_NATIVE_LIBRARY_PATH
#define LEAN_DEFAULT_NATIVE_LIBRARY_PATH ""
#endif
#ifndef LEAN_DEFAULT_NATIVE_MAIN_FN
#define LEAN_DEFAULT_NATIVE_MAIN_FN "main"
#endif
#ifndef LEAN_DEFAULT_NATIVE_INCLUDE_PATH
#define LEAN_DEFAULT_NATIVE_INCLUDE_PATH ""
#endif
#ifndef LEAN_DEFAULT_NATIVE_EMIT_DWARF
#define LEAN_DEFAULT_NATIVE_EMIT_DWARF false
#endif
#ifndef LEAN_DEFAULT_NATIVE_DYNAMIC
#define LEAN_DEFAULT_NATIVE_DYNAMIC false
#endif
#ifndef LEAN_DEFAULT_NATIVE_DUMP
#define LEAN_DEFAULT_NATIVE_DUMP ""
#endif
namespace lean {
namespace native {
/* Options */
static name * g_native_library_path = nullptr;
static name * g_native_main_fn = nullptr;
static name * g_native_include_path = nullptr;
static name * g_native_emit_dwarf = nullptr;
static name * g_native_dynamic = nullptr;
static name * g_native_dump = nullptr;
char const * get_native_library_path(options const & o) {
return o.get_string(*g_native_library_path, LEAN_DEFAULT_NATIVE_LIBRARY_PATH);
}
char const * get_native_main_fn(options const & o) {
return o.get_string(*g_native_main_fn, LEAN_DEFAULT_NATIVE_MAIN_FN);
}
char const * get_native_include_path(options const & o) {
return o.get_string(*g_native_include_path, LEAN_DEFAULT_NATIVE_INCLUDE_PATH);
}
bool get_native_emit_dwarf(options const & o) {
return o.get_bool(*g_native_emit_dwarf, LEAN_DEFAULT_NATIVE_EMIT_DWARF);
}
bool get_native_dynamic(options const & o) {
return o.get_bool(*g_native_dynamic, LEAN_DEFAULT_NATIVE_DYNAMIC);
}
char const * get_native_dump(options const & o) {
return o.get_string(*g_native_dump, LEAN_DEFAULT_NATIVE_DUMP);
}
config::config(options const & o) {
m_native_library_path = get_native_library_path(o);
m_native_main_fn = get_native_main_fn(o);
m_native_include_path = get_native_include_path(o);
m_native_emit_dwarf = get_native_emit_dwarf(o);
m_native_dynamic = get_native_dynamic(o);
m_native_dump = get_native_dump(o);
}
void config::display(std::ostream & os) {
os << "native.library_path = " << m_native_library_path << std::endl;
}
LEAN_THREAD_PTR(config, g_native_config);
scope_config::scope_config(options const & o):
m_old(g_native_config),
m_config(o) {
g_native_config = &m_config;
}
scope_config::~scope_config() {
g_native_config = m_old;
}
config & get_config() {
lean_assert(g_native_config);
return *g_native_config;
}
void initialize_options() {
g_native_library_path = new name{"native", "library_path"};
g_native_main_fn = new name{"native", "main"};
g_native_include_path = new name{"native", "include_path"};
g_native_emit_dwarf = new name{"native", "emit_dwarf"};
g_native_dynamic = new name{"native", "dynamic"};
g_native_dump = new name{"native", "dump"};
register_string_option(*native::g_native_library_path, LEAN_DEFAULT_NATIVE_LIBRARY_PATH,
"(native_compiler) path used to search for native libraries, including liblean");
register_string_option(*native::g_native_main_fn, LEAN_DEFAULT_NATIVE_MAIN_FN,
"(native_compiler) definition used as the program entry point");
register_string_option(*native::g_native_include_path, LEAN_DEFAULT_NATIVE_INCLUDE_PATH,
"(native_compiler) path used to search for native headers, for example those included with Lean");
register_bool_option(*native::g_native_emit_dwarf, LEAN_DEFAULT_NATIVE_EMIT_DWARF,
"(native_compiler) flag controls whether dwarf debugging information is generated for the emitted code");
register_bool_option(*native::g_native_dynamic, LEAN_DEFAULT_NATIVE_DYNAMIC,
"(native_compiler) flag controls whether to use dynamic linking");
register_string_option(*native::g_native_dump, LEAN_DEFAULT_NATIVE_DUMP,
"(native_compiler) flag controls whether the native compiler dumps terms before and after every pass");
}
void finalize_options() {
delete g_native_library_path;
delete g_native_main_fn;
delete g_native_include_path;
delete g_native_emit_dwarf;
delete g_native_dynamic;
delete g_native_dump;
}
}}

38
src/library/native_compiler/options.h Normal file
View file

@ -0,0 +1,38 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch, and Leonardo de Moura
*/
#pragma once
#include "util/sexpr/options.h"
namespace lean {
namespace native {
/** \brief Native compiler configuration object. */
struct config {
char const * m_native_library_path;
char const * m_native_include_path;
char const * m_native_main_fn;
bool m_native_emit_dwarf;
bool m_native_dynamic;
char const * m_native_dump;
config(options const & o);
void display(std::ostream & os);
};
struct scope_config {
config * m_old;
config m_config;
public:
scope_config(options const & o);
~scope_config();
};
config & get_config();
void initialize_options();
void finalize_options();
}}

136
src/library/native_compiler/used_defs.cpp Normal file
View file

@ -0,0 +1,136 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include <iostream>
#include <utility>
#include "used_defs.h"
#include "kernel/environment.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "kernel/type_checker.h"
#include "library/compiler/nat_value.h"
#include "util/name.h"
#include "util/name_set.h"
namespace lean {
used_defs::used_defs(environment const & env, std::function<void(declaration const &)> action) : m_env(env) {
this->m_used_names = name_set();
this->m_names_to_process = std::vector<name>();
this->m_action = action;
}
// Add a name to the live name set, marking
// marking it as seen, and queuing it to be processed.
void used_defs::add_name(name const & n) {
if (!this->m_used_names.contains(n)) {
this->m_used_names.insert(n);
this->m_names_to_process.push_back(n);
}
}
void used_defs::empty_stack() {
while (!this->m_names_to_process.empty()) {
auto n = this->m_names_to_process.back();
this->m_names_to_process.pop_back();
// Is a definition and not a synthetic compiler name.
auto d = this->m_env.find(n);
if (d && d.value().is_definition()) {
m_action(d.value());
}
}
}
void used_defs::names_in_decl(declaration const & d) {
// Start with the name of the current decl,
// we then will collect, the set of names in
// the body, and push them on to the stack to
// be processed, we will repeat this until,
// the stack is empty.
this->add_name(d.get_name());
// Finally we need to recursively process the
// remaining definitions to full compute the
// working set.
this->empty_stack();
lean_assert(this->m_names_to_process.empty());
}
void used_defs::names_in_expr(expr const & e) {
// std::cout << "exp: " << e << std::endl;
if (is_nat_value(e)) { return; }
switch (e.kind()) {
case expr_kind::Local: case expr_kind::Meta:
break;
case expr_kind::Var:
// std::cout << "var: " << e << std::endl;
break;
case expr_kind::Sort:
break;
case expr_kind::Constant: {
auto n = const_name(e);
if (n == name({"nat", "cases_on"})) { return; }
if (auto d = this->m_env.find(n)) {
this->names_in_decl(d.value());
}
break;
}
case expr_kind::Macro: {
type_checker tc(m_env);
if (!is_nat_value(e)) {
auto expanded_macro = tc.expand_macro(e);
// std::cout << e << std::endl;
if (expanded_macro) {
lean_assert(expanded_macro);
names_in_expr(expanded_macro.value());
} else {
/* Do nothing? what is the right behavior here */
}
}
break;
}
case expr_kind::Lambda:
case expr_kind::Pi: {
buffer<expr> ls;
auto ex = e;
while (is_binding(ex)) {
expr d = instantiate_rev(binding_domain(ex), ls.size(), ls.data());
// this->names_in_expr(d);
auto n = mk_fresh_name(); // (name const & prefix, unsigned k);
expr l = mk_local(n, binding_name(ex), d, binding_info(ex));
ls.push_back(l);
ex = binding_body(ex);
}
ex = instantiate_rev(ex, ls.size(), ls.data());
this->names_in_expr(ex);
break;
}
case expr_kind::App: {
buffer<expr> args;
auto fn = get_app_args(e, args);
this->names_in_expr(fn);
for (auto arg : args) {
this->names_in_expr(arg);
}
break;
}
case expr_kind::Let:
auto v = let_value(e);
auto body = let_body(e);
this->names_in_expr(v);
this->names_in_expr(body);
break;
}
}
void used_defs::names_in_preprocessed_body(expr const & e) {
names_in_expr(e);
empty_stack();
}
}

44
src/library/native_compiler/used_defs.h Normal file
View file

@ -0,0 +1,44 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <iostream>
#include <utility>
#include <vector>
#include "used_defs.h"
#include "kernel/environment.h"
#include "kernel/inductive/inductive.h"
#include "library/compiler/erase_irrelevant.h"
#include "util/name.h"
#include "util/name_set.h"
namespace lean {
struct used_defs {
name_set m_used_names;
std::vector<name> m_names_to_process;
environment const & m_env;
std::function<void(declaration const &)> m_action;
// Need a stack and a HashSet
// Rough algorithm
// For each name, check to see if its
// in the set, if not push it on to the stack,
// when done processing the main fucntion,
// invoke this procedure with the first item
// from the stack, and repeat until the stack
// is empty.
used_defs(environment const & env, std::function<void(declaration const &)>);
void names_in_decl(declaration const & d);
void names_in_expr(expr const & e);
void names_in_preprocessed_body(expr const & e);
void add_name(name const & n);
void empty_stack();
bool stack_is_empty() {
return m_names_to_process.empty();
}
};
}

3
src/library/vm/CMakeLists.txt
View file

@ -1,3 +1,4 @@
add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp init_module.cpp)
vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp init_module.cpp
vm_native.cpp)

3
src/library/vm/init_module.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "library/vm/vm_expr.h"
#include "library/vm/vm_pexpr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_native.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_environment.h"
@ -35,6 +36,7 @@ void initialize_vm_core_module() {
initialize_vm_expr();
initialize_vm_pexpr();
initialize_vm_list();
initialize_vm_native();
initialize_vm_exceptional();
initialize_vm_task();
initialize_vm_declaration();
@ -45,6 +47,7 @@ void finalize_vm_core_module() {
finalize_vm_declaration();
finalize_vm_task();
finalize_vm_exceptional();
finalize_vm_native();
finalize_vm_list();
finalize_vm_pexpr();
finalize_vm_expr();

66
src/library/vm/vm.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include <algorithm>
#include <vector>
@ -25,6 +26,9 @@ Author: Leonardo de Moura
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_expr.h"
#include "library/normalize.h"
#include "util/dynamic_library.h"
#include "library/native_compiler/extern.h"
#ifndef LEAN_DEFAULT_PROFILER
#define LEAN_DEFAULT_PROFILER false
@ -74,6 +78,10 @@ vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * data) {
return mk_vm_composite(vm_obj_kind::Constructor, cidx, sz, data);
}
vm_obj mk_vm_constructor(unsigned cidx, std::initializer_list<vm_obj const> args) {
return mk_vm_constructor(cidx, args.size(), args.begin());
}
vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1) {
return mk_vm_constructor(cidx, 1, &o1);
}
@ -93,6 +101,14 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm
return mk_vm_constructor(cidx, 4, args);
}
vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args) {
return mk_native_closure(env, n, args.size(), args.begin());
}
vm_obj mk_native_closure(environment const & env, name const & n, unsigned sz, vm_obj const * data) {
return get_vm_state().get_constant(n);
}
vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
}
@ -2590,8 +2606,16 @@ unsigned get_vm_builtin_arity(name const & fn) {
lean_unreachable();
}
void* get_extern_symbol(
std::string library_name,
std::string extern_name) {
dynamic_library library(library_name);
return library.symbol(extern_name);
}
static std::string * g_vm_monitor_key = nullptr;
static environment vm_monitor_register_core(environment const & env, name const & d) {
expr const & type = env.get(d).get_type();
if (!is_app_of(type, get_vm_monitor_name(), 1))
@ -2606,6 +2630,46 @@ environment vm_monitor_register(environment const & env, name const & d) {
return module::add(new_env, *g_vm_monitor_key, [=](environment const &, serializer & s) { s << d; });
}
environment load_external_fn(environment & env, name const & extern_n) {
try {
std::string lib_name = library_name(env, extern_n);
std::string symbol = symbol_name(env, extern_n);
dynamic_library *library = new dynamic_library(lib_name);
auto code = library->symbol(symbol);
lean_assert(code);
// Calculate the arity of the declared symbol.
unsigned arity = 1; // We always take at least one argument, because we are in the IO monad.
auto ty = normalize(env, env.get(extern_n).get_type(), true);
while (is_binding(ty)) {
ty = binding_body(ty);
arity += 1;
}
std::cout << arity << std::endl;
switch (arity) {
case 0: lean_unreachable();
case 1: return add_native(env, extern_n, (vm_cfunction_1)code);
case 2: return add_native(env, extern_n, (vm_cfunction_2)code);
case 3: return add_native(env, extern_n, (vm_cfunction_3)code);
case 4: return add_native(env, extern_n, (vm_cfunction_4)code);
case 5: return add_native(env, extern_n, (vm_cfunction_5)code);
case 6: return add_native(env, extern_n, (vm_cfunction_6)code);
case 7: return add_native(env, extern_n, (vm_cfunction_7)code);
case 8: return add_native(env, extern_n, (vm_cfunction_8)code);
default:
lean_unreachable();
// buffer<vm_obj> args;
// to_cbuffer(fn, args);
// args.push_back(a1);
// return to_fnN(d)(args.size(), args.data());
}
} catch (dynamic_linking_exception e) {
std::cout << e.what() << std::endl;
throw e;
}
}
static void vm_monitor_reader(deserializer & d, environment & env) {
name n;
d >> n;
@ -2634,7 +2698,7 @@ void finalize_vm_core() {
void initialize_vm() {
g_ext = new vm_decls_reg();
g_may_update_vm_builtins = false;
// g_may_update_vm_builtins = false;
g_vm_reserve_key = new std::string("VMR");
g_vm_code_key = new std::string("VMC");
g_vm_monitor_key = new std::string("VMMonitor");

6
src/library/vm/vm.h
View file

@ -141,11 +141,14 @@ small_object_allocator & get_vm_allocator();
// Constructors
vm_obj mk_vm_simple(unsigned cidx);
vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * args);
vm_obj mk_vm_constructor(unsigned cidx, std::initializer_list<vm_obj const> args);
vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &);
vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &);
vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
vm_obj mk_native_closure(environment const & env, name const & n, unsigned sz, vm_obj const * args);
vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args);
vm_obj mk_vm_closure(unsigned cidx, vm_obj const &);
vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &);
vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
@ -826,6 +829,9 @@ vm_builtin_kind get_vm_builtin_kind(name const & fn);
\pre is_vm_builtin_function(fn) && get_vm_builtin_kind(fn) == vm_builtin_kind::CFun */
unsigned get_vm_builtin_arity(name const & fn);
environment load_external_fn(environment & env, name const & extern_n);
// void* get_extern_symbol(std::string library_name, std::string extern_name);
/** \brief Invoke closure \c fn with the given arguments. These procedures are meant to be use by
C++ generated/extracted code. */
vm_obj invoke(vm_obj const & fn, vm_obj const & a1);

54
src/library/vm/vm_expr.cpp
View file

@ -24,6 +24,8 @@ Author: Leonardo de Moura
#include "library/vm/vm_option.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_list.h"
#include "library/compiler/simp_inductive.h"
#include "library/compiler/nat_value.h"
namespace lean {
struct vm_macro_definition : public vm_external {
@ -147,6 +149,10 @@ vm_obj expr_macro_arg(vm_obj const & m, vm_obj const & i) {
return to_obj(macro_arg(to_expr(m), to_unsigned(i)));
}
vm_obj expr_macro_def_name(vm_obj const & d) {
return to_obj(to_macro_definition(d).get_name());
}
static unsigned g_expr_macro_arg_fun_idx = -1;
unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
@ -323,6 +329,49 @@ vm_obj expr_copy_pos_info(vm_obj const & src, vm_obj const & tgt) {
return to_obj(copy_tag(to_expr(src), copy(to_expr(tgt))));
}
vm_obj expr_is_internal_cnstr(vm_obj const & e) {
auto opt_unsigned = is_internal_cnstr(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_is_internal_proj(vm_obj const & e) {
auto opt_unsigned = is_internal_proj(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_is_internal_cases(vm_obj const & e) {
auto opt_unsigned = is_internal_cases(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_get_nat_value(vm_obj const & o) {
expr e = to_expr(o);
if (is_nat_value(e)) {
auto n = mk_vm_nat(get_nat_value_value(e));
return mk_vm_constructor(1, { n });
} else {
return mk_vm_simple(0);
}
}
// TODO(Leo): move to a different file
vm_obj vm_mk_nat_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_nat_val_ne_proof(to_expr(a), to_expr(b)));
@ -361,6 +410,7 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN("_expr_macro_arg", expr_macro_arg);
DECLARE_VM_BUILTIN(name({"expr", "macro"}), expr_macro);
DECLARE_VM_BUILTIN(name({"expr", "mk_macro"}), expr_mk_macro);
DECLARE_VM_BUILTIN(name({"expr", "macro_def_name"}), expr_macro_def_name);
DECLARE_VM_BUILTIN(name({"expr", "has_decidable_eq"}), expr_has_decidable_eq);
DECLARE_VM_BUILTIN(name({"expr", "alpha_eqv"}), expr_alpha_eqv);
DECLARE_VM_BUILTIN(name({"expr", "to_string"}), expr_to_string);
@ -388,6 +438,10 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"), vm_mk_fin_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"), vm_mk_char_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof);
// Not sure if we should expose these or what?
DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr);
DECLARE_VM_BUILTIN(name({"expr", "get_nat_value"}), expr_get_nat_value);
}
void finalize_vm_expr() {

9
src/library/vm/vm_io.cpp
View file

@ -33,10 +33,19 @@ vm_obj get_line(vm_obj const &) {
return to_obj(str);
}
vm_obj forever (vm_obj const & action, vm_obj const &) {
while (true) {
invoke(action, mk_vm_simple(0));
}
return mk_vm_simple(0);
}
void initialize_vm_io() {
DECLARE_VM_BUILTIN("put_str", put_str);
DECLARE_VM_BUILTIN("put_nat", put_nat);
DECLARE_VM_BUILTIN("get_line", get_line);
DECLARE_VM_BUILTIN("forever", forever);
}
void finalize_vm_io() {

114
src/library/vm/vm_native.cpp Normal file
View file

@ -0,0 +1,114 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include <string>
#include <iostream>
#include <fstream>
#include "library/vm/vm.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_format.h"
#include "library/native_compiler/native_compiler.h"
#include "library/compiler/simp_inductive.h"
#include "library/compiler/nat_value.h"
namespace lean {
vm_obj native_is_internal_cnstr(vm_obj const & e) {
auto opt_unsigned = is_internal_cnstr(to_expr(e));
if (opt_unsigned) {
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj native_is_internal_cases(vm_obj const & e) {
auto opt_unsigned = is_internal_cases(to_expr(e));
if (opt_unsigned) {
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj native_is_internal_proj(vm_obj const & e) {
auto opt_unsigned = is_internal_proj(to_expr(e));
if (opt_unsigned) {
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj native_get_nat_value(vm_obj const & o) {
expr e = to_expr(o);
if (is_nat_value(e)) {
auto n = mk_vm_nat(get_nat_value_value(e));
return mk_vm_constructor(1, { n });
} else {
return mk_vm_simple(0);
}
}
vm_obj native_get_builtin(vm_obj const & o) {
name n = to_name(o);
if (!get_vm_builtin_internal_name(n)) {
return mk_vm_none();
}
switch (get_vm_builtin_kind(n)) {
case vm_builtin_kind::VMFun: {
name internal_name = name(get_vm_builtin_internal_name(n));
auto b = mk_vm_constructor(2, { to_obj(internal_name) });
return mk_vm_some(b);
}
case vm_builtin_kind::CFun: {
auto efn = *get_builtin(n);
auto pair = mk_vm_constructor(0, { to_obj(efn.m_name), mk_vm_simple(efn.m_arity) });
return mk_vm_some(pair);
}
case vm_builtin_kind::Cases: {
auto efn = *get_builtin(n);
auto pair = mk_vm_constructor(1, { to_obj(efn.m_name), mk_vm_simple(efn.m_arity) });
return mk_vm_some(pair);
}
default:
return mk_vm_none();
}
}
vm_obj native_dump_format(vm_obj const & string_obj, vm_obj const & format_obj) {
auto file_path = to_string(string_obj);
auto fmt = to_format(format_obj);
std::fstream dump_file(file_path, std::ios_base::out);
pretty(dump_file, 80, true, fmt);
dump_file.close();
return mk_vm_nat(0);
}
void initialize_vm_native() {
// Not sure if we should expose ese or what?
DECLARE_VM_BUILTIN(name({"native", "is_internal_cnstr"}), native_is_internal_cnstr);
DECLARE_VM_BUILTIN(name({"native", "is_internal_cases"}), native_is_internal_cases);
DECLARE_VM_BUILTIN(name({"native", "is_internal_proj"}), native_is_internal_proj);
DECLARE_VM_BUILTIN(name({"native", "get_nat_value"}), native_get_nat_value);
DECLARE_VM_BUILTIN(name({"native", "get_builtin"}), native_get_builtin);
DECLARE_VM_BUILTIN(name({"native", "dump_format"}), native_dump_format);
}
void finalize_vm_native() {
}
}

12
src/library/vm/vm_native.h Normal file
View file

@ -0,0 +1,12 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
namespace lean {
void initialize_vm_native();
void finalize_vm_native();
}

2
src/shared/init.cpp
View file

@ -7,5 +7,5 @@ Author: Leonardo de Moura
#include "init/init.h"
namespace lean {
// automatic initialization for the shared library
initializer g_init;
// initializer g_init;
}

8
src/shell/CMakeLists.txt
View file

@ -170,6 +170,14 @@ FOREACH(T ${LEANSLOWTESTS})
set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
ENDFOREACH(T)
file(GLOB LEANNATIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/native_run/*.lean")
FOREACH(T ${LEANNATIVETESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leannativetest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/native_run"
COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
ENDFOREACH(T)
# # LEAN DOCS
# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
# FOREACH(T ${LEANDOCS})

33
src/shell/lean.cpp
View file

@ -43,6 +43,9 @@ Author: Leonardo de Moura
#include "frontends/lean/opt_cmd.h"
#include "frontends/smt2/parser.h"
#include "frontends/lean/json.h"
#include "library/native_compiler/options.h"
#include "library/native_compiler/native_compiler.h"
#include "library/trace.h"
#include "init/init.h"
#include "shell/simple_pos_info_provider.h"
#include "shell/leandoc.h"
@ -121,6 +124,7 @@ static struct option g_long_options[] = {
{"threads", required_argument, 0, 'j'},
{"quiet", no_argument, 0, 'q'},
{"deps", no_argument, 0, 'd'},
{"compile", optional_argument, 0, 'C'},
#if defined(LEAN_SERVER)
{"json", no_argument, 0, 'J'},
{"server", optional_argument, 0, 'S'},
@ -167,6 +171,8 @@ options set_config_option(options const & opts, char const * in) {
case lean::IntOption:
case lean::UnsignedOption:
return opts.update(opt, atoi(val.c_str()));
case lean::StringOption:
return opts.update(opt, val);
default:
throw lean::exception(lean::sstream() << "invalid -D parameter, configuration option '" << opt
<< "' cannot be set in the command line, use set_option command");
@ -250,6 +256,8 @@ int main(int argc, char ** argv) {
bool make_mode = false;
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1;
bool smt2 = false;
bool compile = false;
bool export_native_objects = false;
bool only_deps = false;
unsigned num_threads = 0;
#if defined(LEAN_MULTI_THREAD)
@ -263,6 +271,7 @@ int main(int argc, char ** argv) {
optional<std::string> export_all_txt;
optional<std::string> doc;
optional<std::string> server_in;
std::string native_output;
while (true) {
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
if (c == -1)
@ -292,6 +301,13 @@ int main(int argc, char ** argv) {
case 'm':
make_mode = true;
break;
case 'n':
native_output = optarg;
export_native_objects = true;
break;
case 'C':
compile = true;
break;
case 'r':
doc = optarg;
break;
@ -488,11 +504,28 @@ int main(int argc, char ** argv) {
}
}
// Options appear to be empty, pretty sure I'm making a mistake here.
if (compile && !mods.empty()) {
auto final_env = *mods.front().second->m_result.get().m_env;
auto final_opts = mods.front().second->m_result.get().m_opts;
type_context tc(final_env, final_opts);
lean::scope_trace_env scope2(final_env, final_opts, tc);
lean::native::scope_config scoped_native_config(
final_opts);
native_compile_binary(final_env, final_env.get(lean::name("main")));
}
// if (!mods.empty() && export_native_objects) {
// // this code is now broken
// env = lean::set_native_module_path(env, lean::name(native_output));
// }
if (export_txt && !mods.empty()) {
exclusive_file_lock export_lock(*export_txt);
std::ofstream out(*export_txt);
export_module_as_lowtext(out, *mods.front().second->m_result.get().m_env);
}
if (export_all_txt && !mods.empty()) {
exclusive_file_lock export_lock(*export_all_txt);
std::ofstream out(*export_all_txt);

2
src/util/CMakeLists.txt
View file

@ -4,4 +4,4 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp
stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp
bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp
utf8.cpp name_map.cpp list_fn.cpp null_ostream.cpp file_lock.cpp
small_object_allocator.cpp subscripted_name_set.cpp)
small_object_allocator.cpp subscripted_name_set.cpp dynamic_library.cpp process.cpp)

60
src/util/dynamic_library.cpp Normal file
View file

@ -0,0 +1,60 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include <string>
// Interacting with dynamic linking is *not* cross-platform, this is my first
// attempt at supporting all platforms.
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
void dlopen(const char * file, int mode) {
// TODO: add windows support
throw std::runtime_error("Windows does not currently have support for dynamically loading object files");
}
#elif defined(__APPLE__)
// OSX version, dlfcn should be availble on this platform
#include <dlfcn.h>
#else
// Linux verison, dlfcn should be availble on this platform
#include <dlfcn.h>
#endif
#include "dynamic_library.h"
namespace lean {
dynamic_library::dynamic_library(std::string library_path):
m_name(library_path), m_handle(nullptr) {
m_handle = dlopen(library_path.c_str(), RTLD_LAZY | RTLD_GLOBAL);
// Check to see if an error occured while performing dynamic linking.
if (!m_handle) {
auto last_error_msg = dlerror();
throw dynamic_linking_exception(std::string(last_error_msg));
}
}
dynamic_library::~dynamic_library() {
auto err = dlclose(m_handle);
if (err != 0) {
auto last_error_msg = dlerror();
throw dynamic_linking_exception(std::string(last_error_msg));
}
}
dynamic_symbol dynamic_library::symbol(std::string name) {
auto sym = dlsym(m_handle, name.c_str());
if (sym == nullptr) {
auto last_error_msg = dlerror();
throw dynamic_linking_exception(std::string(last_error_msg));
}
return sym;
}
}

31
src/util/dynamic_library.h Normal file
View file

@ -0,0 +1,31 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <string>
#include <stdexcept>
namespace lean {
class dynamic_linking_exception : public std::runtime_error {
public:
dynamic_linking_exception(std::string msg) : std::runtime_error(msg) {}
};
typedef void* dynamic_symbol;
class dynamic_library {
std::string m_name;
std::string m_path;
void * m_handle;
public:
dynamic_library(std::string library_path);
~dynamic_library();
dynamic_symbol symbol(std::string name);
};
}

20
src/util/executable.h Normal file
View file

@ -0,0 +1,20 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jay Freeman (Saurik), Jared Roesch
*/
#include <mach-o/dyld.h>
// TODO: this must be platform specific code
std::string executable() {
uint32_t size(0);
lean_assert(_NSGetExecutablePath(NULL, &size) == -1);
std::string path;
path.resize(size);
lean_assert(_NSGetExecutablePath(&path[0], &size) != -1);
lean_assert(path.back() == '\0');
path.resize(strlen(path.c_str()));
return path;
}

6
src/util/lean_path.cpp
View file

@ -53,7 +53,7 @@ static char g_path_sep = ';';
static char g_path_alt_sep = ':';
static char g_sep = '\\';
static char g_bad_sep = '/';
static std::string get_exe_location() {
std::string get_exe_location() {
HMODULE hModule = GetModuleHandleW(NULL);
WCHAR path[MAX_PATH];
GetModuleFileNameW(hModule, path, MAX_PATH);
@ -69,7 +69,7 @@ bool is_path_sep(char c) { return c == g_path_sep || c == g_path_alt_sep; }
static char g_path_sep = ':';
static char g_sep = '/';
static char g_bad_sep = '\\';
static std::string get_exe_location() {
std::string get_exe_location() {
char buf1[PATH_MAX];
char buf2[PATH_MAX];
uint32_t bufsize = PATH_MAX;
@ -89,7 +89,7 @@ bool is_path_sep(char c) { return c == g_path_sep; }
static char g_path_sep = ':';
static char g_sep = '/';
static char g_bad_sep = '\\';
static std::string get_exe_location() {
std::string get_exe_location() {
char path[PATH_MAX];
char dest[PATH_MAX];
memset(dest, 0, PATH_MAX);

3
src/util/lean_path.h
View file

@ -19,6 +19,9 @@ public:
/** \brief Initialize the lean_path */
void init_lean_path();
std::string get_exe_location();
/** \brief Return the LEAN_PATH string */
char const * get_lean_path();
/**

62
src/util/process.cpp Normal file
View file

@ -0,0 +1,62 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#include <fstream>
#include <iostream>
#include <iomanip>
#include <utility>
#include "util/process.h"
#include "util/buffer.h"
#include "unistd.h"
#include "sys/wait.h"
namespace lean {
// TODO(jroesch): make this cross platform
process::process(std::string n): m_proc_name(n), m_args() {
m_args.push_back(m_proc_name);
}
process & process::arg(std::string a) {
m_args.push_back(a);
return *this;
}
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
void process::run() {
throw std::runtime_error("process::run not supported on Windows")
}
#else
void process::run() {
int pid = fork();
if (pid == 0) {
buffer<char*> pargs;
for (auto arg : m_args) {
auto str = new char[arg.size() + 1];
arg.copy(str, arg.size());
str[arg.size()] = '\0';
pargs.push_back(str);
}
pargs.data()[pargs.size()] = NULL;
auto err = execvp(pargs.data()[0], pargs.data());
if (err < 0) {
throw std::runtime_error("executing process failed: ...");
}
} else if (pid == -1) {
throw std::runtime_error("forking process failed: ...");
} else {
int status;
waitpid(pid, &status, 0);
}
}
#endif
}

23
src/util/process.h Normal file
View file

@ -0,0 +1,23 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jared Roesch
*/
#pragma once
#include <iostream>
#include <string>
#include "util/buffer.h"
namespace lean {
class process {
std::string m_proc_name;
buffer<std::string> m_args;
public:
process(std::string exe_name);
process & arg(std::string arg_str);
void run();
};
}

2
tests/lean/native_run/.gitignore vendored Normal file
View file

@ -0,0 +1,2 @@
*.dSYM
*.cpp

4
tests/lean/native_run/config.lean Normal file
View file

@ -0,0 +1,4 @@
-- set_option default configuration for tests
prelude
set_option pp.colors false
set_option pp.unicode true

4
tests/lean/native_run/hello_world.lean Normal file
View file

@ -0,0 +1,4 @@
import system.IO
definition main : IO unit :=
put_str "Hello Lean!\n"

1
tests/lean/native_run/hello_world.lean.expected.out Normal file
View file

@ -0,0 +1 @@
Hello Lean!

63
tests/lean/native_run/test_single.sh Executable file
View file

@ -0,0 +1,63 @@
#!/usr/bin/env bash
if [ $# -ne 3 -a $# -ne 2 ]; then
echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
exit 1
fi
ulimit -s 8192
LEAN=$1
export LEAN_PATH=../../../library:.
export HLEAN_PATH=../../../hott:.
export LIBRARY=../../../build/debug
export INCLUDE=../../../src
if [ $# -ne 3 ]; then
INTERACTIVE=no
else
INTERACTIVE=$3
fi
f=$2
if [ ${f: -6} == ".hlean" ]; then
CONFIG="config.hlean"
else
CONFIG="config.lean"
fi
echo "-- testing $f"
"$LEAN" --compile $CONFIG "$f" -D native.library_path="$LIBRARY" -D native.include_path="$INCLUDE" &> "$f.compile.out"
# Currently we always produce a file named a.out, it looks like the first command isn't running
# and then it crashes when it can't find a.out
./a.out &> "$f.produced.out.1"
sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" | sed "/warning: using 'sorry'/d" > "$f.produced.out"
rm -f "$f.produced.out.1"
rm -f "$f.compile.out"
rm -f a.out
if test -f "$f.expected.out"; then
if diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"; then
echo "-- checked"
exit 0
else
echo "ERROR: file $f.produced.out does not match $f.expected.out"
if [ $INTERACTIVE == "yes" ]; then
meld "$f.produced.out" "$f.expected.out"
if diff -I "executing external script" "$f.produced.out" "$f.expected.out"; then
echo "-- mismath was fixed"
fi
else
diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"
fi
exit 1
fi
else
echo "ERROR: file $f.expected.out does not exist"
if [ $INTERACTIVE == "yes" ]; then
read -p "copy $f.produced.out (y/n)? "
if [ $REPLY == "y" ]; then
cp -- "$f.produced.out" "$f.expected.out"
echo "-- copied $f.produced.out --> $f.expected.out"
fi
fi
exit 1
fi