summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml8
-rw-r--r--src/ocaml_backend.ml9
-rw-r--r--src/parse_ast.ml5
-rw-r--r--src/parser.mly24
-rw-r--r--src/parser2.mly16
-rw-r--r--src/pretty_print_lem.ml9
-rw-r--r--src/pretty_print_sail.ml6
-rw-r--r--src/pretty_print_sail2.ml9
-rw-r--r--src/type_check.ml32
-rw-r--r--src/type_check.mli2
-rw-r--r--src/util.ml5
-rw-r--r--src/util.mli4
12 files changed, 74 insertions, 55 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 25b34402..df715e17 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 (fun _ -> 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, (fun _ -> Some (string_of_id id)), false))
let val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
@@ -983,20 +983,20 @@ let generate_undefineds vs_ids (Defs defs) =
let undefined_td = function
| TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
- [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None, false));
+ [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
(mk_pat (P_lit (mk_lit L_unit)))
(mk_exp (E_app (mk_id "internal_pick",
[mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
| TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
pat
(mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
| TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
pat
(mk_exp (E_app (mk_id "internal_pick",
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index ea0662a3..28bf624d 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -477,10 +477,10 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
| _ -> failwith "Unsupported typedef"
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 "ocaml"))]
+ let extern_id (VS_aux (VS_val_spec (typschm, id, ext, _), _)) =
+ match ext "ocaml" with
+ | None -> []
+ | Some ext -> [(id, mk_id ext)]
in
let rec extern_ids = function
| DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
@@ -574,4 +574,3 @@ let ocaml_compile spec defs =
let _ = Unix.system ("ocamlbuild -pkg zarith -pkg uint " ^ spec ^ ".cmo") in
();
Unix.chdir cwd
-
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index fba0b1ec..fb6c75e1 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 -> string) option * bool
+ VS_val_spec of typschm * id * (string -> string option) * bool
type
@@ -514,6 +514,3 @@ and lexp =
type
defs = (* Definition sequence *)
Defs of (def) list
-
-
-
diff --git a/src/parser.mly b/src/parser.mly
index b204801f..edfc0783 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1049,29 +1049,29 @@ fun_def:
val_spec:
| Val typquant typ id
- { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4, None, false)) }
+ { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4, (fun _ -> None), false)) }
| Val typ id
- { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3, None, false)) }
+ { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3, (fun _ -> None), false)) }
| Val Cast typquant typ id
- { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, None, true)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> None), true)) }
| Val Cast typ id
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, None, true)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, (fun _ -> None), true)) }
| Val Extern typquant typ id
- { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> string_of_id $5), false)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> Some (string_of_id $5)), false)) }
| Val Extern typ id
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (fun _ -> string_of_id $4), false)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, (fun _ -> Some (string_of_id $4)), false)) }
| Val Extern typquant typ id Eq String
- { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> $7), false)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> Some $7), false)) }
| Val Extern typ id Eq String
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some (fun _ -> $6), false)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, (fun _ -> Some $6), false)) }
| Val Cast Extern typquant typ id
- { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (fun _ -> string_of_id $6), true)) }
+ { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, (fun _ -> Some (string_of_id $6)), true)) }
| Val Cast Extern typ id
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (fun _ -> string_of_id $5), true)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, (fun _ -> Some (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 (fun _ -> $8), true)) }
+ { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, (fun _ -> Some $8), true)) }
| Val Cast Extern typ id Eq String
- { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some (fun _ -> $7), true)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, (fun _ -> Some $7), true)) }
kinded_id:
| tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 32b2a2b1..ee8cdfb8 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -1053,21 +1053,21 @@ externs:
val_spec_def:
| Val id Colon typschm
- { mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos }
| Val Cast id Colon typschm
- { mk_vs (VS_val_spec ($5, $3, None, true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos }
| Val id Eq String Colon typschm
- { mk_vs (VS_val_spec ($6, $2, Some (fun _ -> $4), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos }
| Val Cast id Eq String Colon typschm
- { mk_vs (VS_val_spec ($7, $3, Some (fun _ -> $5), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos }
| Val String Colon typschm
- { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), Some (fun _ -> $2), false)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos }
| Val Cast String Colon typschm
- { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), Some (fun _ -> $3), true)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $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 }
+ { mk_vs (VS_val_spec ($8, $2, (fun backend -> (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 }
+ { mk_vs (VS_val_spec ($9, $3, (fun backend -> (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 0bb73aa5..c32212a6 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -738,7 +738,7 @@ let doc_exp_lem, doc_let_lem =
if aexp_needed then parens (align epp) else epp
| _ ->
let call = match annot with
- | Some (env, _, _) when Env.is_extern f env ->
+ | Some (env, _, _) when Env.is_extern f env "lem" ->
string (Env.get_extern f env "lem")
| _ -> doc_id_lem f in
let argspp = match args with
@@ -1649,7 +1649,7 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
(clauses ^/^ string "end")
| FCL_aux (FCL_Funcl(id,_,exp),_) :: _
- when not (Env.is_extern id (env_of exp)) ->
+ when not (Env.is_extern id (env_of exp) "lem") ->
string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem sequential mwords fd)
| _ -> empty
@@ -1689,11 +1689,12 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
match valspec with
- | VS_val_spec (typschm,id,None,_) ->
+ | VS_val_spec (typschm,id,ext,_) when ext "lem" = None ->
(* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
if contains_t_pp_var mwords typ then empty else *)
separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem sequential mwords true typschm] ^/^ hardline
- | VS_val_spec (_,_,Some _,_) -> empty
+ (* | VS_val_spec (_,_,Some _,_) -> empty *)
+ | _ -> empty
let rec doc_def_lem sequential mwords def =
(* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 710c9dac..c53d30b4 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -410,9 +410,9 @@ let doc_default (DT_aux(df,_)) = match df with
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
- (* 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")))
+ (* This sail syntax only supports a single extern name, so just use the ocaml version *)
+ let extern_kwd_pp, id_pp = match ext_opt "ocaml" with
+ | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext)))
| 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 edea1016..ce64d1b4 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -328,7 +328,12 @@ let doc_typdef (TD_aux(td,_)) = match td with
| _ -> string "TYPEDEF"
let doc_spec (VS_aux(v,_)) =
- let doc_extern = function
+ let doc_extern ext =
+ let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
+ utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in
+ let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in
+ if docs = [] then empty else braces (separate (comma ^^ space) docs)
+ (* function
| Some s ->
let ext_for backend = utf8string ("\"" ^ String.escaped (s backend) ^ "\"") in
let extern =
@@ -337,7 +342,7 @@ let doc_spec (VS_aux(v,_)) =
else separate space [lbrace; string "ocaml:"; ext_for "ocaml"; string "lem:"; ext_for "lem"; rbrace]
in
equals ^^ space ^^ extern ^^ space
- | None -> empty
+ | None -> empty *)
in
match v with
| VS_val_spec(ts,id,ext,is_cast) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index ff4a748b..f380b54b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -374,8 +374,8 @@ module Env : sig
val get_num_def : id -> t -> nexp
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 -> string) -> t -> t
+ val is_extern : id -> t -> string -> bool
+ val add_extern : id -> (string -> string option) -> t -> t
val get_extern : id -> t -> string -> string
val get_default_order : t -> order
val set_default_order_inc : 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 -> string) Bindings.t;
+ externs : (string -> string option) Bindings.t;
casts : id list;
allow_casts : bool;
constraints : n_constraint list;
@@ -674,14 +674,20 @@ end = struct
typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]");
{ env with overloads = Bindings.add id ids env.overloads }
- let is_extern id env =
- Bindings.mem id env.externs
+ let is_extern id env backend =
+ try not (Bindings.find id env.externs backend = None) with
+ | Not_found -> false
+ (* Bindings.mem id env.externs *)
let add_extern id ext env =
{ env with externs = Bindings.add id ext env.externs }
- let get_extern id env =
- try Bindings.find id env.externs with
+ let get_extern id env backend =
+ try
+ match Bindings.find id env.externs backend with
+ | Some ext -> ext
+ | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
+ with
| Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
let get_casts env = env.casts
@@ -934,13 +940,13 @@ let initial_env =
(* Internal functions for Monomorphise.AtomToItself *)
- |> Env.add_extern (mk_id "size_itself_int") (fun _ -> "size_itself_int")
+ |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "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") (fun _ -> "make_the_value")
+ |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "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),
@@ -3238,7 +3244,7 @@ let infer_funtyp l env tannotopt funcls =
end
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error l "Cannot infer function type for unannotated function"
-let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, None, false), (Parse_ast.Unknown, None)))
+let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, (fun _ -> None), false), (Parse_ast.Unknown, None)))
let check_tannotopt env typq ret_typ = function
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
@@ -3290,9 +3296,11 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
let check_val_spec env (VS_aux (vs, (l, _))) =
let (id, quants, typ, env) = match vs with
| VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) ->
- let env = match ext_opt with
+ let env =
+ (* match ext_opt with
| None -> env
- | Some ext -> Env.add_extern id ext env
+ | Some ext -> *)
+ Env.add_extern id ext_opt env
in
let env = if is_cast then Env.add_cast id env else env in
(id, quants, typ, env)
diff --git a/src/type_check.mli b/src/type_check.mli
index 81cfd7fb..52afeab7 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -117,7 +117,7 @@ module Env : sig
val get_num_def : id -> t -> nexp
- val is_extern : id -> t -> bool
+ val is_extern : id -> t -> string -> bool
val get_extern : id -> t -> string -> string
diff --git a/src/util.ml b/src/util.ml
index 335fd36f..59ba7026 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -216,6 +216,11 @@ let rec option_binop f x y = match x, y with
| Some x, Some y -> Some (f x y)
| _ -> None
+let rec option_these = function
+ | Some x :: xs -> x :: option_these xs
+ | None :: xs -> option_these xs
+ | [] -> []
+
let changed2 f g x h y =
match (g x, h y) with
| (None,None) -> None
diff --git a/src/util.mli b/src/util.mli
index 11588de2..a7818f93 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -90,6 +90,10 @@ val option_binop : ('a -> 'a -> 'a) -> 'a option -> 'a option -> 'a option
whereas [option_get_exn exn (Some x)] returns [x]. *)
val option_get_exn : exn -> 'a option -> 'a
+(** [option_these xs] extracts the elements of the list [xs]
+ wrapped in [Some]. *)
+val option_these : 'a option list -> 'a list
+
(** [changed2 f g x h y] applies [g] to [x] and [h] to [y].
If both function applications return [None], then [None] is
returned. Otherwise [f] is applied to the results. For this
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:52:20 +0000