diff options
| author | Alasdair Armstrong | 2017-11-08 15:06:13 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-08 15:06:13 +0000 |
| commit | 2def55466c941aa8d4b933ecd93a7d3eb739fce8 (patch) | |
| tree | 8c68136ab787dca5aea4aaf8d352c3730285a136 /language | |
| parent | e43324b207b13d7e4094e2561b4e4a84c76e1299 (diff) | |
Allow for different extern names for different backends
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/language/l2.ott b/language/l2.ott index 13feac23..09b950b8 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -695,9 +695,6 @@ exp :: 'E_' ::= % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn % the expi and the result are both of type vector of 'a - | [ num1 = exp1 , ... , numn = expn opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }} -% num1 .. numn must be a consecutive list of naturals - % we pick [ ] not { } for vector literals for consistency with their % array-like access syntax, in contrast to the C which has funny % syntax for array literals. We don't have to preserve [ ] for lists @@ -956,20 +953,16 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} -% | let typschm pat = exp :: :: val_explicit -% {{ com let, explicit type ($[[pat]]$ must be total)}} -% at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here | let pat = exp :: :: val {{ com let, implicit type ($[[pat]]$ must be total)}} val_spec {{ ocaml 'a val_spec }} :: 'VS_' ::= {{ ocaml VS_aux of val_spec_aux * 'a annot }} - | val_spec_aux :: :: aux - + | val_spec_aux :: :: aux val_spec_aux :: 'VS_' ::= - {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * string option * bool }} + {{ com value type specification }} + {{ ocaml VS_val_spec of typschm * id * (string -> string) option * bool }} | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} |