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

feat(library/init/lean/ir/lirc): we should support only C external names without mangling

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-14 16:17:15 -07:00
parent f8bd816215
commit 59f9de720d
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/ir/extract_cpp.lean
View file

@ -345,7 +345,9 @@ d.foldl (λ s d, match d with
def emit_used_headers (env : environment) (external_names : fnid → option string) (d : list decl) : except_t format (state_t string id) unit :=
let used := collect_used d in
(used.mfor (λ fid, match env fid with
| some d := emit_header d.header >> emit ";\n" >> when (need_uncurry d) (emit_uncurry_header d >> emit ";\n")
| some d := do
unless (external_names fid = none) (emit "extern \"C\" "),
emit_header d.header >> emit ";\n" >> when (need_uncurry d) (emit_uncurry_header d >> emit ";\n")
| _ := return ())).run { external_names := external_names, ctx := mk_context, env := env }
end cpp

2
library/init/lean/ir/lirc.lean
View file

@ -21,7 +21,7 @@ def parse_input_aux : nat → list decl → fnid2string → parser (list decl ×
| (n+1) ds m :=
(eoi >> return (ds.reverse, m))
<|>
(do cid ← (do symbol "[", n ← lexeme $ cpp_identifier, symbol "]", return (some n)) <|> return none,
(do cid ← (do symbol "[", n ← lexeme $ c_identifier, symbol "]", return (some n)) <|> return none,
d ← parse_decl,
match cid with
| some cid := parse_input_aux n (d::ds) (m.insert d.name cid)