Allow pre-declarations without an expression for topdefs

it allows for better splitting between metadata and code (even if the type has
to be repeated at the moment)
This commit is contained in:
Louis Gesbert 2023-12-01 10:44:37 +01:00
parent 14cbe07d18
commit 0d5759d99c
2 changed files with 12 additions and 8 deletions

View File

@ -1307,7 +1307,10 @@ let process_topdef
| Some (eopt0, ty0), eopt -> (
let err msg =
Message.raise_multispanned_error
[None, Mark.get ty0; None, Mark.get typ]
[
None, Mark.get (TopdefName.get_info id);
None, Mark.get def.S.topdef_name;
]
(msg ^^ " for %a") TopdefName.format id
in
if not (Type.equal ty0 typ) then err "Conflicting type definitions"

View File

@ -699,13 +699,14 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
{ ctxt with local = { ctxt.local with typedefs } }
| ScopeUse _ -> ctxt
| Topdef def ->
let name, pos = def.topdef_name in
Option.iter
(fun use ->
raise_already_defined_error (TopdefName.get_info use) name pos
"toplevel definition")
(Ident.Map.find_opt name ctxt.local.topdefs);
let uid = TopdefName.fresh ctxt.local.path def.topdef_name in
let name, _ = def.topdef_name in
let uid =
match Ident.Map.find_opt name ctxt.local.topdefs with
| None -> TopdefName.fresh ctxt.local.path def.topdef_name
| Some uid -> uid
(* Topdef declaration may appear multiple times as long as their types
match and only one contains an expression defining it *)
in
let topdefs = Ident.Map.add name uid ctxt.local.topdefs in
{ ctxt with local = { ctxt.local with topdefs } }