diff --git a/.gitignore b/.gitignore index 9abe79ec70..dee600ba78 100644 --- a/.gitignore +++ b/.gitignore @@ -23,4 +23,5 @@ CMakeFiles/ doc/html make.deps src/emacs/dependencies -compile_commands.json \ No newline at end of file +compile_commands.json +*.idea diff --git a/library/.project b/library/.project index 2305ddbe7e..8a80bd4d59 100644 --- a/library/.project +++ b/library/.project @@ -1,3 +1,4 @@ + *.lean - flycheck*.lean - .#*.lean +- ffi.lean diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 06c689964e..24baef61a4 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -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 diff --git a/library/init/default.lean b/library/init/default.lean index 660262dfeb..7fcb420a1e 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -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, diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 0646a75153..95f3831a59 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -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 diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index c49054a16c..93f92173f7 100644 --- a/library/init/meta/name.lean +++ b/library/init/meta/name.lean @@ -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⟩ diff --git a/library/init/native/anf.lean b/library/init/native/anf.lean new file mode 100644 index 0000000000..fab41e67b1 --- /dev/null +++ b/library/init/native/anf.lean @@ -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 +} diff --git a/library/init/native/builtin.lean b/library/init/native/builtin.lean new file mode 100644 index 0000000000..04a8c3b822 --- /dev/null +++ b/library/init/native/builtin.lean @@ -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 diff --git a/library/init/native/cf.lean b/library/init/native/cf.lean new file mode 100644 index 0000000000..b0fede6371 --- /dev/null +++ b/library/init/native/cf.lean @@ -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 +} diff --git a/library/init/native/config.lean b/library/init/native/config.lean new file mode 100644 index 0000000000..92aa0f6c59 --- /dev/null +++ b/library/init/native/config.lean @@ -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 diff --git a/library/init/native/default.lean b/library/init/native/default.lean new file mode 100644 index 0000000000..6a19fe0ac8 --- /dev/null +++ b/library/init/native/default.lean @@ -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 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()); + -- -- *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 diff --git a/library/init/native/format.lean b/library/init/native/format.lean new file mode 100644 index 0000000000..b4a13ce0d4 --- /dev/null +++ b/library/init/native/format.lean @@ -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 " +| (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 diff --git a/library/init/native/internal.lean b/library/init/native/internal.lean new file mode 100644 index 0000000000..e25649b8c7 --- /dev/null +++ b/library/init/native/internal.lean @@ -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 diff --git a/library/init/native/ir.lean b/library/init/native/ir.lean new file mode 100644 index 0000000000..269d8ac408 --- /dev/null +++ b/library/init/native/ir.lean @@ -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 +-- | diff --git a/library/init/native/pass.lean b/library/init/native/pass.lean new file mode 100644 index 0000000000..5b521e7af3 --- /dev/null +++ b/library/init/native/pass.lean @@ -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 diff --git a/library/init/native/procedure.lean b/library/init/native/procedure.lean new file mode 100644 index 0000000000..45c0b5184f --- /dev/null +++ b/library/init/native/procedure.lean @@ -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 ⟩ diff --git a/library/init/native/result.lean b/library/init/native/result.lean new file mode 100644 index 0000000000..a76260cfa5 --- /dev/null +++ b/library/init/native/result.lean @@ -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 diff --git a/library/init/native/util.lean b/library/init/native/util.lean new file mode 100644 index 0000000000..3a539cbba6 --- /dev/null +++ b/library/init/native/util.lean @@ -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 diff --git a/library/system/io.lean b/library/system/io.lean index 0220dbf106..89415c83dc 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -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 := diff --git a/old_library/system/IO.lean b/old_library/system/IO.lean index 280ee7975d..27d33c3c7d 100644 --- a/old_library/system/IO.lean +++ b/old_library/system/IO.lean @@ -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 := diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 56e1c59382..e16c0183c6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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} $) add_subdirectory(library/compiler) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/native_compiler) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lean) set(LEAN_OBJS ${LEAN_OBJS} $) 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 $ ${LEAN_OBJS}) target_link_libraries(leanshared ${EXTRA_LIBS}) install(TARGETS leanshared DESTINATION lib) + install(TARGETS leanstatic DESTINATION lib) endif() add_subdirectory(shell) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9de0b4f6a5..e993ed7dfe 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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 parser::parse_kv_pairs() { + name_map 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()); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 1a5a137d60..027a22a696 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -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 parse_kv_pairs() override final; double parse_double(); bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); } diff --git a/src/init/init.cpp b/src/init/init.cpp index e5cbf3f63c..7dbdfbbc51 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -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(); diff --git a/src/library/abstract_parser.h b/src/library/abstract_parser.h index de639f5c3e..8c6d91412d 100644 --- a/src/library/abstract_parser.h +++ b/src/library/abstract_parser.h @@ -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 parse_kv_pairs() = 0; }; } diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index bdf4a138b5..96c8f90d3d 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -210,10 +210,59 @@ struct indices_attribute_data : public attr_data { } }; +struct key_value_data : public attr_data { + // generalize: name_map 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; /** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */ typedef typed_attribute indices_attribute; +template class typed_attribute; +/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */ +typedef typed_attribute key_value_attribute; + class user_attribute_ext { public: virtual name_map get_attributes(environment const & env); diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index c1bcd500ce..fad9cfca61 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -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) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index dfcaa771cc..a1ecf210f4 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -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); diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index c518106f46..26dbd107ea 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -24,6 +24,7 @@ void initialize_compiler_module() { initialize_simp_inductive(); initialize_vm_compiler(); } + void finalize_compiler_module() { finalize_vm_compiler(); finalize_simp_inductive(); diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 2b16f44dba..95376a841b 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -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 & args, unsigned bpz, name_map 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 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 const & m) { buffer args; expr fn = get_app_args(e, args); @@ -212,6 +227,8 @@ class vm_compiler_fn { emit(mk_sconstructor_instr(0)); } else if (optional 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 extern_names(environment const & env, buffer 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 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 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 code; vm_compiler_fn gen(new_env, code); diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index 905a683019..f1b56a0d54 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -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()); } diff --git a/src/library/io_state.h b/src/library/io_state.h index 4b8b6c4ee6..636dc579bb 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -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(); } diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 62738494f8..1186eb3c93 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -98,6 +98,8 @@ public: mod.m_env = optional(p.env()); + mod.m_opts = p.ios().get_options(); + mod.m_ok = parsed_ok; // TODO(gabriel): what should this be? return mod; diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index 24f8e96bd1..e490f39c5d 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -39,6 +39,7 @@ struct module_info { struct parse_result { optional m_env; + options m_opts; bool m_ok = false; std::string m_obj_code; diff --git a/src/library/native_compiler/CMakeLists.txt b/src/library/native_compiler/CMakeLists.txt new file mode 100644 index 0000000000..701fcb75fe --- /dev/null +++ b/src/library/native_compiler/CMakeLists.txt @@ -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) diff --git a/src/library/native_compiler/cpp_compiler.cpp b/src/library/native_compiler/cpp_compiler.cpp new file mode 100644 index 0000000000..7a0d04bf8b --- /dev/null +++ b/src/library/native_compiler/cpp_compiler.cpp @@ -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; + } +} diff --git a/src/library/native_compiler/cpp_compiler.h b/src/library/native_compiler/cpp_compiler.h new file mode 100644 index 0000000000..c3bc1eea65 --- /dev/null +++ b/src/library/native_compiler/cpp_compiler.h @@ -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 +#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 m_library_paths; + buffer m_include_paths; + buffer m_files; + buffer 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(); + +} diff --git a/src/library/native_compiler/cpp_emitter.cpp b/src/library/native_compiler/cpp_emitter.cpp new file mode 100644 index 0000000000..bec4320fd9 --- /dev/null +++ b/src/library/native_compiler/cpp_emitter.cpp @@ -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 +#include +#include +#include +#include "cpp_emitter.h" +#include "kernel/environment.h" + +namespace lean { + +void cpp_emitter::emit_headers() { + *this->m_output_stream << + "#include " << 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); +} + +} diff --git a/src/library/native_compiler/cpp_emitter.h b/src/library/native_compiler/cpp_emitter.h new file mode 100644 index 0000000000..44eac5acce --- /dev/null +++ b/src/library/native_compiler/cpp_emitter.h @@ -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 +#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); + }; +} diff --git a/src/library/native_compiler/extern.cpp b/src/library/native_compiler/extern.cpp new file mode 100644 index 0000000000..66ef14efe8 --- /dev/null +++ b/src/library/native_compiler/extern.cpp @@ -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(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(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() { +} +} diff --git a/src/library/native_compiler/extern.h b/src/library/native_compiler/extern.h new file mode 100644 index 0000000000..ee469e9cca --- /dev/null +++ b/src/library/native_compiler/extern.h @@ -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 +#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(); +} diff --git a/src/library/native_compiler/init_module.cpp b/src/library/native_compiler/init_module.cpp new file mode 100644 index 0000000000..12857ea75c --- /dev/null +++ b/src/library/native_compiler/init_module.cpp @@ -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(); +} +} diff --git a/src/library/native_compiler/init_module.h b/src/library/native_compiler/init_module.h new file mode 100644 index 0000000000..f20b0dc75f --- /dev/null +++ b/src/library/native_compiler/init_module.h @@ -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(); +} diff --git a/src/library/native_compiler/native_compiler.cpp b/src/library/native_compiler/native_compiler.cpp new file mode 100644 index 0000000000..74ac5c73da --- /dev/null +++ b/src/library/native_compiler/native_compiler.cpp @@ -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 +#include +#include +#include +#include + +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 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 fns) { + buffer in_lean_namespace; + buffer 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 & 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 & 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 const & procs) { + for (auto & p : procs) { + m_arity_map.insert(p.m_name, get_arity(p.m_code)); + } + } + + void populate_arity_map(buffer 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 native_include_paths() { + std::vector 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 native_library_paths() { + std::vector 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_fns, + buffer & procs, + native_compiler_mode mode) { + native_compiler_fn compiler(env); + + buffer 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 & 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 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(); + } + case vm_builtin_kind::CFun: { + auto arity = get_vm_builtin_arity(n); + return optional( + mk_lean_extern(internal_name, arity)); + } + case vm_builtin_kind::Cases: { + return optional( + mk_lean_extern(internal_name, 2u)); + } + } + } else { + return optional(); + } +} + +void populate_extern_fns( + environment const & env, + used_defs const & used, + buffer & 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 decls) { + std::cout << "compiled native module" << std::endl; + + // Preprocess the main function. + buffer all_procs; + buffer main_procs; + buffer 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 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 all_procs; + buffer main_procs; + buffer 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 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 & 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 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; +} +} diff --git a/src/library/native_compiler/native_compiler.h b/src/library/native_compiler/native_compiler.h new file mode 100644 index 0000000000..bc4718a5f1 --- /dev/null +++ b/src/library/native_compiler/native_compiler.h @@ -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 get_builtin(name const & n); + +enum native_compiler_mode { JIT, AOT }; +void native_compile(environment const & env, buffer> & procs, native_compiler_mode & mode); +void native_compile_binary(environment const & env, declaration const & d); +void native_compile_module(environment const & env, buffer 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(); +} diff --git a/src/library/native_compiler/options.cpp b/src/library/native_compiler/options.cpp new file mode 100644 index 0000000000..f58bd7bab7 --- /dev/null +++ b/src/library/native_compiler/options.cpp @@ -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; +} +}} diff --git a/src/library/native_compiler/options.h b/src/library/native_compiler/options.h new file mode 100644 index 0000000000..1ba80f1692 --- /dev/null +++ b/src/library/native_compiler/options.h @@ -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(); +}} diff --git a/src/library/native_compiler/used_defs.cpp b/src/library/native_compiler/used_defs.cpp new file mode 100644 index 0000000000..57c0de0fe5 --- /dev/null +++ b/src/library/native_compiler/used_defs.cpp @@ -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 +#include +#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 action) : m_env(env) { + this->m_used_names = name_set(); + this->m_names_to_process = std::vector(); + 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 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 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(); +} +} diff --git a/src/library/native_compiler/used_defs.h b/src/library/native_compiler/used_defs.h new file mode 100644 index 0000000000..38a49765d3 --- /dev/null +++ b/src/library/native_compiler/used_defs.h @@ -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 +#include +#include +#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 m_names_to_process; + environment const & m_env; + std::function 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 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(); + } +}; +} diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 528f3b3024..7fd2c3906a 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -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) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 2d7b29349f..32deb3fae9 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -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(); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 3641bb1663..abe6f5cafb 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ + #include #include #include @@ -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 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 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 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"); diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 04216e60cf..99a54f3078 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -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 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 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); diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 0f5ca3d215..a11b45ba08 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -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 & 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() { diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index acef1e36f9..9be84b791d 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -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() { diff --git a/src/library/vm/vm_native.cpp b/src/library/vm/vm_native.cpp new file mode 100644 index 0000000000..68ab8b5327 --- /dev/null +++ b/src/library/vm/vm_native.cpp @@ -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 +#include +#include +#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() { +} +} diff --git a/src/library/vm/vm_native.h b/src/library/vm/vm_native.h new file mode 100644 index 0000000000..d6bcdd74f5 --- /dev/null +++ b/src/library/vm/vm_native.h @@ -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(); +} diff --git a/src/shared/init.cpp b/src/shared/init.cpp index 95c7f227c8..3428b7dfbd 100644 --- a/src/shared/init.cpp +++ b/src/shared/init.cpp @@ -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; } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index cd83d7f778..8162559e26 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -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}) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index fafc9c6d23..13d5677c03 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -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 export_all_txt; optional doc; optional 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); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 906eda4a0b..912b35edde 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -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) diff --git a/src/util/dynamic_library.cpp b/src/util/dynamic_library.cpp new file mode 100644 index 0000000000..f432d44892 --- /dev/null +++ b/src/util/dynamic_library.cpp @@ -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 + +// 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 +#else +// Linux verison, dlfcn should be availble on this platform +#include +#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; +} + +} diff --git a/src/util/dynamic_library.h b/src/util/dynamic_library.h new file mode 100644 index 0000000000..8db43a23bf --- /dev/null +++ b/src/util/dynamic_library.h @@ -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 +#include + +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); +}; + +} diff --git a/src/util/executable.h b/src/util/executable.h new file mode 100644 index 0000000000..abbf35216c --- /dev/null +++ b/src/util/executable.h @@ -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 + +// 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; +} diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index f9ae5e4324..80869e08f9 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -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); diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 8b4408e42b..0881d20e03 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -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(); /** diff --git a/src/util/process.cpp b/src/util/process.cpp new file mode 100644 index 0000000000..d2df3b9497 --- /dev/null +++ b/src/util/process.cpp @@ -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 +#include +#include +#include +#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 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 + +} diff --git a/src/util/process.h b/src/util/process.h new file mode 100644 index 0000000000..5fe329c18e --- /dev/null +++ b/src/util/process.h @@ -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 +#include +#include "util/buffer.h" + +namespace lean { + +class process { + std::string m_proc_name; + buffer m_args; +public: + process(std::string exe_name); + process & arg(std::string arg_str); + void run(); +}; +} diff --git a/tests/lean/native_run/.gitignore b/tests/lean/native_run/.gitignore new file mode 100644 index 0000000000..3800da35d8 --- /dev/null +++ b/tests/lean/native_run/.gitignore @@ -0,0 +1,2 @@ +*.dSYM +*.cpp diff --git a/tests/lean/native_run/config.lean b/tests/lean/native_run/config.lean new file mode 100644 index 0000000000..e900c86a6d --- /dev/null +++ b/tests/lean/native_run/config.lean @@ -0,0 +1,4 @@ +-- set_option default configuration for tests +prelude +set_option pp.colors false +set_option pp.unicode true diff --git a/tests/lean/native_run/hello_world.lean b/tests/lean/native_run/hello_world.lean new file mode 100644 index 0000000000..6986a54ceb --- /dev/null +++ b/tests/lean/native_run/hello_world.lean @@ -0,0 +1,4 @@ +import system.IO + +definition main : IO unit := + put_str "Hello Lean!\n" diff --git a/tests/lean/native_run/hello_world.lean.expected.out b/tests/lean/native_run/hello_world.lean.expected.out new file mode 100644 index 0000000000..203765ffc5 --- /dev/null +++ b/tests/lean/native_run/hello_world.lean.expected.out @@ -0,0 +1 @@ +Hello Lean! diff --git a/tests/lean/native_run/test_single.sh b/tests/lean/native_run/test_single.sh new file mode 100755 index 0000000000..f1e46bd3f9 --- /dev/null +++ b/tests/lean/native_run/test_single.sh @@ -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