summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml2
-rw-r--r--src/ocaml_backend.ml5
-rw-r--r--src/parse_ast.ml2
-rw-r--r--src/parser.mly16
-rw-r--r--src/parser2.mly30
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/pretty_print_lem_ast.ml3
-rw-r--r--src/pretty_print_sail.ml3
-rw-r--r--src/pretty_print_sail2.ml9
-rw-r--r--src/type_check.ml10
-rw-r--r--src/type_check.mli2
11 files changed, 56 insertions, 28 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2ccfee04..25b34402 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -921,7 +921,7 @@ let typschm_of_string order str =
let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
typschm
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (string_of_id id), false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (fun _ -> string_of_id id), false))
let val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index fada02a2..ea0662a3 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -331,7 +331,6 @@ let function_header () =
then (first_function := false; string "let rec")
else string "and"
-
let funcls_id = function
| [] -> failwith "Ocaml: empty function"
| FCL_aux (FCL_Funcl (id, pat, exp),_) :: _ -> id
@@ -455,8 +454,6 @@ let ocaml_string_of_abbrev ctx id typq typ =
separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals]
^//^ ocaml_string_typ typ arg
-
-
let ocaml_typedef ctx (TD_aux (td_aux, _)) =
match td_aux with
| TD_record (id, _, typq, fields, _) ->
@@ -483,7 +480,7 @@ let get_externs (Defs defs) =
let extern_id (VS_aux (vs_aux, _)) =
match vs_aux with
| VS_val_spec (typschm, id, None, _) -> []
- | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id ext)]
+ | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id (ext "ocaml"))]
in
let rec extern_ids = function
| DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index cfd749ba..fba0b1ec 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -423,7 +423,7 @@ type_def_aux = (* Type definition body *)
type
val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id * string option * bool
+ VS_val_spec of typschm * id * (string -> string) option * bool
type
diff --git a/src/parser.mly b/src/parser.mly
index 8c055b33..b204801f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1057,21 +1057,21 @@ val_spec:
| Val Cast typ id
{ vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, None, true)) }
| Val Extern typquant typ id
- { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (string_of_id $5), false)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> string_of_id $5), false)) }
| Val Extern typ id
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (string_of_id $4), false)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (fun _ -> string_of_id $4), false)) }
| Val Extern typquant typ id Eq String
- { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some $7, false)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> $7), false)) }
| Val Extern typ id Eq String
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some $6, false)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some (fun _ -> $6), false)) }
| Val Cast Extern typquant typ id
- { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (string_of_id $6), true)) }
+ { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (fun _ -> string_of_id $6), true)) }
| Val Cast Extern typ id
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (string_of_id $5), true)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (fun _ -> string_of_id $5), true)) }
| Val Cast Extern typquant typ id Eq String
- { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some $8, true)) }
+ { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (fun _ -> $8), true)) }
| Val Cast Extern typ id Eq String
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some $7, true)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some (fun _ -> $7), true)) }
kinded_id:
| tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 78724c4d..32b2a2b1 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -48,6 +48,18 @@ open Parse_ast
let loc n m = Range (n, m)
+let default_opt x = function
+ | None -> x
+ | Some y -> y
+
+let assoc_opt key assocs =
+ try Some (List.assoc key assocs) with
+ | Not_found -> None
+
+let string_of_id = function
+ | Id_aux (Id str, _) -> str
+ | Id_aux (DeIid str, _) -> str
+
let mk_id i n m = Id_aux (i, loc n m)
let mk_kid str n m = Kid_aux (Var str, loc n m)
@@ -1033,19 +1045,29 @@ let_def:
| Let_ letbind
{ $2 }
+externs:
+ | id Colon String
+ { [(string_of_id $1, $3)] }
+ | id Colon String Comma externs
+ { (string_of_id $1, $3) :: $5 }
+
val_spec_def:
| Val id Colon typschm
{ mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
| Val Cast id Colon typschm
{ mk_vs (VS_val_spec ($5, $3, None, true)) $startpos $endpos }
| Val id Eq String Colon typschm
- { mk_vs (VS_val_spec ($6, $2, Some $4, false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($6, $2, Some (fun _ -> $4), false)) $startpos $endpos }
| Val Cast id Eq String Colon typschm
- { mk_vs (VS_val_spec ($7, $3, Some $5, true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($7, $3, Some (fun _ -> $5), true)) $startpos $endpos }
| Val String Colon typschm
- { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), Some $2, false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), Some (fun _ -> $2), false)) $startpos $endpos }
| Val Cast String Colon typschm
- { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), Some $3, true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), Some (fun _ -> $3), true)) $startpos $endpos }
+ | Val id Eq Lcurly externs Rcurly Colon typschm
+ { mk_vs (VS_val_spec ($8, $2, Some (fun backend -> default_opt (string_of_id $2) (assoc_opt backend $5)), false)) $startpos $endpos }
+ | Val Cast id Eq Lcurly externs Rcurly Colon typschm
+ { mk_vs (VS_val_spec ($9, $3, Some (fun backend -> default_opt (string_of_id $3) (assoc_opt backend $6)), true)) $startpos $endpos }
register_def:
| Register id Colon typ
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b9ef1aec..0bb73aa5 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -739,7 +739,7 @@ let doc_exp_lem, doc_let_lem =
| _ ->
let call = match annot with
| Some (env, _, _) when Env.is_extern f env ->
- string (Env.get_extern f env)
+ string (Env.get_extern f env "lem")
| _ -> doc_id_lem f in
let argspp = match args with
| [arg] -> expV true arg
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index fa387ad4..8031ba3e 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -533,7 +533,8 @@ let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
let print_spec ppf v =
match v with
| VS_val_spec(ts,id,ext_opt,is_cast) ->
- fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) ext_opt pp_bool_lem is_cast
+ (* FIXME: None *)
+ fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast
| _ -> failwith "Invalid valspec"
in
fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a870f454..710c9dac 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -411,7 +411,8 @@ let doc_spec (VS_aux(v,_)) = match v with
| VS_val_spec(ts,id,ext_opt,is_cast) ->
let cast_pp = if is_cast then [string "cast"] else [] in
let extern_kwd_pp, id_pp = match ext_opt with
- | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string ext))
+ (* This sail syntax only supports a single extern name, so just use the ocaml version *)
+ | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext "ocaml")))
| None -> [], doc_id id
in
separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index efcfc8b9..edea1016 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -329,7 +329,14 @@ let doc_typdef (TD_aux(td,_)) = match td with
let doc_spec (VS_aux(v,_)) =
let doc_extern = function
- | Some s -> equals ^^ space ^^ utf8string ("\"" ^ String.escaped s ^ "\"") ^^ space
+ | Some s ->
+ let ext_for backend = utf8string ("\"" ^ String.escaped (s backend) ^ "\"") in
+ let extern =
+ if s "ocaml" = s "lem"
+ then ext_for "ocaml"
+ else separate space [lbrace; string "ocaml:"; ext_for "ocaml"; string "lem:"; ext_for "lem"; rbrace]
+ in
+ equals ^^ space ^^ extern ^^ space
| None -> empty
in
match v with
diff --git a/src/type_check.ml b/src/type_check.ml
index aede9c67..3dd251ca 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -375,8 +375,8 @@ module Env : sig
val add_overloads : id -> id list -> t -> t
val get_overloads : id -> t -> id list
val is_extern : id -> t -> bool
- val add_extern : id -> string -> t -> t
- val get_extern : id -> t -> string
+ val add_extern : id -> (string -> string) -> t -> t
+ val get_extern : id -> t -> string -> string
val get_default_order : t -> order
val set_default_order_inc : t -> t
val set_default_order_dec : t -> t
@@ -410,7 +410,7 @@ end = struct
enums : IdSet.t Bindings.t;
records : (typquant * (typ * id) list) Bindings.t;
accessors : (typquant * typ) Bindings.t;
- externs : string Bindings.t;
+ externs : (string -> string) Bindings.t;
casts : id list;
allow_casts : bool;
constraints : n_constraint list;
@@ -934,13 +934,13 @@ let initial_env =
(* Internal functions for Monomorphise.AtomToItself *)
- |> Env.add_extern (mk_id "size_itself_int") "size_itself_int"
+ |> Env.add_extern (mk_id "size_itself_int") (fun _ -> "size_itself_int")
|> Env.add_val_spec (mk_id "size_itself_int")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
Parse_ast.Unknown)],Parse_ast.Unknown),
function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
(atom_typ (nvar (mk_kid "n"))) no_effect)
- |> Env.add_extern (mk_id "make_the_value") "make_the_value"
+ |> Env.add_extern (mk_id "make_the_value") (fun _ -> "make_the_value")
|> Env.add_val_spec (mk_id "make_the_value")
(TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
Parse_ast.Unknown)],Parse_ast.Unknown),
diff --git a/src/type_check.mli b/src/type_check.mli
index f3e5e861..81cfd7fb 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -119,7 +119,7 @@ module Env : sig
val is_extern : id -> t -> bool
- val get_extern : id -> t -> string
+ val get_extern : id -> t -> string -> string
(* Lookup id searchs for a specified id in the environment, and
returns it's type and what kind of identifier it is, using the
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 02:59:38 +0000