summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/ExtractToFstar.ml111
-rw-r--r--src/PureToExtract.ml117
-rw-r--r--src/main.ml1
3 files changed, 210 insertions, 19 deletions
diff --git a/src/ExtractToFstar.ml b/src/ExtractToFstar.ml
new file mode 100644
index 00000000..ef7d756a
--- /dev/null
+++ b/src/ExtractToFstar.ml
@@ -0,0 +1,111 @@
+(** Extract to F* *)
+
+open Errors
+open Pure
+open TranslateCore
+open PureToExtract
+module F = Format
+
+(** Iter "between".
+
+ Iterate over a list, but call a function between every two elements
+ (but not before the first element, and not after the last).
+ *)
+let list_iterb (between : unit -> unit) (f : 'a -> unit) (ls : 'a list) : unit =
+ let rec iter ls =
+ match ls with
+ | [] -> ()
+ | [ x ] -> f x
+ | x :: y :: ls ->
+ f x;
+ between ();
+ iter (y :: ls)
+ in
+ iter ls
+
+(** [inside] constrols whether we should add parentheses or not around type
+ application (if `true` we add parentheses).
+ *)
+let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+ (ty : ty) : unit =
+ match ty with
+ | Adt (type_id, tys) -> (
+ match type_id with
+ | Tuple ->
+ F.pp_print_string fmt "(";
+ list_iterb (F.pp_print_space fmt) (extract_ty ctx fmt true) tys;
+ F.pp_print_string fmt ")"
+ | AdtId _ | Assumed _ ->
+ if inside then F.pp_print_string fmt "(";
+ F.pp_print_string fmt (ctx_find_type type_id ctx);
+ if tys <> [] then F.pp_print_space fmt ();
+ list_iterb (F.pp_print_space fmt) (extract_ty ctx fmt true) tys;
+ if inside then F.pp_print_string fmt ")")
+ | TypeVar vid -> F.pp_print_string fmt (ctx_find_type_var vid ctx)
+ | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
+ | Char -> F.pp_print_string fmt ctx.fmt.char_name
+ | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+ | Str -> F.pp_print_string fmt ctx.fmt.str_name
+ | Array _ | Slice _ -> raise Unimplemented
+
+let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
+ (type_name : string) (type_params : string list) (fields : field list) :
+ unit =
+ (* We want to generate a definition which looks like this:
+ * ```
+ * type s = { x : int; y : bool; }
+ * ```
+ *
+ * Or if there isn't enough space on one line:
+ * ```
+ * type s = {
+ * x : int;
+ * y : bool;
+ * }
+ * ```
+ * Note that we already printed: `type s =`
+ *)
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "{";
+ (* The body itself *)
+ F.pp_open_hvbox fmt 0;
+ F.pp_open_hvbox fmt ctx.indent_incr;
+ F.pp_print_space fmt ();
+ (* Print the fields *)
+ let print_field (f : field) : unit =
+ let field_name = ctx.fmt.field_name type_name f.field_name in
+ F.pp_open_box fmt ctx.indent_incr;
+ F.pp_print_string fmt field_name;
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ extract_ty ctx fmt false f.field_ty;
+ F.pp_close_box fmt ()
+ in
+ List.iter print_field fields;
+ (* Close *)
+ F.pp_close_box fmt ();
+ F.pp_print_string fmt "}";
+ F.pp_close_box fmt ()
+
+let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
+ (type_name : string) (type_params : string list) (variants : variant list) :
+ unit =
+ raise Unimplemented
+
+let rec extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
+ (def : type_def) : unit =
+ let name = ctx_find_local_type def.def_id ctx in
+ let ctx, type_params = ctx_add_type_params def.type_params ctx in
+ (* > "type TYPE_NAME =" *)
+ F.pp_print_string fmt "type";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt name;
+ match def.kind with
+ | Struct fields ->
+ extract_type_def_struct_body ctx fmt name type_params fields
+ | Enum variants ->
+ extract_type_def_enum_body ctx fmt name type_params variants
+
+(*let rec extract_field (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+ (ty : ty) : unit =*)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index d5fd4432..7bafad08 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -13,18 +13,6 @@ module RegionVarId = T.RegionVarId
(** The local logger *)
let log = L.pure_to_extract_log
-type extraction_ctx = {
- type_context : C.type_context;
- fun_context : C.fun_context;
-}
-(** Extraction context.
-
- Note that the extraction context contains information coming from the
- CFIM AST (not only the pure AST). This is useful for naming, for instance:
- we use the region information to generate the names of the backward
- functions, etc.
- *)
-
type region_group_info = {
id : RegionGroupId.id;
(** The id of the region group.
@@ -47,6 +35,16 @@ type name_formatter = {
char_name : string;
int_name : integer_type -> string;
str_name : string;
+ field_name : string -> string -> string;
+ (** Inputs:
+ - type name
+ - field name
+ *)
+ variant_name : string -> string -> string;
+ (** Inputs:
+ - type name
+ - variant name
+ *)
type_name : name -> string; (** Provided a basename, compute a type name. *)
fun_name : A.fun_id -> name -> int -> region_group_info option -> string;
(** Inputs:
@@ -70,6 +68,14 @@ type name_formatter = {
if necessary to prevent name clashes: the burden of name clashes checks
is thus on the caller's side.
*)
+ type_var_basename : StringSet.t -> string;
+ (** Generates a type variable basename. *)
+ append_index : string -> int -> string;
+ (** Appends an index to a name - we use this to generate unique
+ names: when doing so, the role of the formatter is just to concatenate
+ indices to names, the responsability of finding a proper index is
+ delegated to helper functions.
+ *)
}
(** A name formatter's role is to come up with name suggestions.
For instance, provided some information about a function (its basename,
@@ -124,7 +130,7 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
the name for a backward function, we try to use the names of the regions
to
*)
-let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter)
+let compute_fun_def_name (ctx : trans_ctx) (fmt : name_formatter)
(fun_id : A.fun_id) (rg_id : RegionGroupId.id option) : string =
(* Lookup the function CFIM signature (we need the region information) *)
let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
@@ -150,6 +156,7 @@ let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter)
type id =
| FunId of A.fun_id * RegionGroupId.id option
| TypeId of type_id
+ | TypeVarId of TypeVarId.id
| VarId of VarId.id
| UnknownId
(** Used for stored various strings like keywords, definitions which
@@ -195,6 +202,7 @@ let names_map_add (id : id) (name : string) (nm : names_map) : names_map =
let names_set = StringSet.add name nm.names_set in
{ id_to_name; name_to_id; names_set }
+(* TODO: remove those functions? We use the ones of extraction_ctx *)
let names_map_find (id : id) (nm : names_map) : string =
IdMap.find id nm.id_to_name
@@ -213,17 +221,88 @@ let names_map_find_type (id : type_id) (nm : names_map) : string =
let names_map_find_local_type (id : TypeDefId.id) (nm : names_map) : string =
names_map_find_type (AdtId id) nm
-(** Make a basename unique (by adding an index).
+let names_map_find_var (id : VarId.id) (nm : names_map) : string =
+ names_map_find (VarId id) nm
+
+let names_map_find_type_var (id : TypeVarId.id) (nm : names_map) : string =
+ names_map_find (TypeVarId id) nm
+
+(** Make a (variable) basename unique (by adding an index).
We do this in an inefficient manner (by testing all indices starting from
0) but it shouldn't be a bottleneck.
- [add_index]: concatenates a given index to the variable's basename.
+ [append]: appends an index to a string
*)
-let var_basename_to_unique (names_set : StringSet.t) (add_index : int -> string)
- : string =
+let basename_to_unique (names_set : StringSet.t)
+ (append : string -> int -> string) (basename : string) : string =
let rec gen (i : int) : string =
- let s = add_index i in
+ let s = append basename i in
if StringSet.mem s names_set then gen (i + 1) else s
in
- gen 0
+ if StringSet.mem basename names_set then gen 0 else basename
+
+type extraction_ctx = {
+ trans_ctx : trans_ctx;
+ names_map : names_map;
+ fmt : name_formatter;
+ indent_incr : int;
+ (** The indent increment we insert whenever we need to indent more *)
+}
+(** Extraction context.
+
+ Note that the extraction context contains information coming from the
+ CFIM AST (not only the pure AST). This is useful for naming, for instance:
+ we use the region information to generate the names of the backward
+ functions, etc.
+ *)
+
+let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
+ let names_map = names_map_add id name ctx.names_map in
+ { ctx with names_map }
+
+let ctx_find (id : id) (ctx : extraction_ctx) : string =
+ IdMap.find id ctx.names_map.id_to_name
+
+let ctx_find_function (id : A.fun_id) (rg : RegionGroupId.id option)
+ (ctx : extraction_ctx) : string =
+ ctx_find (FunId (id, rg)) ctx
+
+let ctx_find_local_function (id : FunDefId.id) (rg : RegionGroupId.id option)
+ (ctx : extraction_ctx) : string =
+ ctx_find_function (A.Local id) rg ctx
+
+let ctx_find_type (id : type_id) (ctx : extraction_ctx) : string =
+ assert (id <> Tuple);
+ ctx_find (TypeId id) ctx
+
+let ctx_find_local_type (id : TypeDefId.id) (ctx : extraction_ctx) : string =
+ ctx_find_type (AdtId id) ctx
+
+let ctx_find_var (id : VarId.id) (ctx : extraction_ctx) : string =
+ ctx_find (VarId id) ctx
+
+let ctx_find_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string =
+ ctx_find (TypeVarId id) ctx
+
+(** Generate a unique type variable name and add to the context *)
+let ctx_add_type_var (basename : string) (id : TypeVarId.id)
+ (ctx : extraction_ctx) : extraction_ctx * string =
+ let name =
+ basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
+ in
+ let ctx = ctx_add (TypeVarId id) name ctx in
+ (ctx, name)
+
+(** See [ctx_add_type_var] *)
+let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
+ (ctx : extraction_ctx) : extraction_ctx * string list =
+ List.fold_left_map
+ (fun ctx (name, id) -> ctx_add_type_var name id ctx)
+ ctx vars
+
+let ctx_add_type_params (vars : type_var list) (ctx : extraction_ctx) :
+ extraction_ctx * string list =
+ List.fold_left_map
+ (fun ctx (var : type_var) -> ctx_add_type_var var.name var.index ctx)
+ ctx vars
diff --git a/src/main.ml b/src/main.ml
index baa76b77..1e402f54 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -8,6 +8,7 @@ module EL = Easy_logging.Logging
module TA = TypesAnalysis
open PureToExtract
open ExtractAst
+open ExtractToFstar
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.