From fc21cf96f80ccb7e6455c057987bb0ff4597c0bb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 13 Nov 2022 23:00:38 +0100 Subject: Make good progress on the Coq backend --- compiler/ExtractToBackend.ml | 1639 ------------------------------------------ 1 file changed, 1639 deletions(-) delete mode 100644 compiler/ExtractToBackend.ml (limited to 'compiler/ExtractToBackend.ml') diff --git a/compiler/ExtractToBackend.ml b/compiler/ExtractToBackend.ml deleted file mode 100644 index fc04ce90..00000000 --- a/compiler/ExtractToBackend.ml +++ /dev/null @@ -1,1639 +0,0 @@ -(** Extract to F* *) - -open Utils -open Pure -open PureUtils -open TranslateCore -open PureToExtract -open StringUtils -module F = Format - -(** A qualifier for a type definition. - - Controls whether we should use [type ...] or [and ...] (for mutually - recursive datatypes). - *) -type type_decl_qualif = - | Type (** [type t = ...] *) - | And (** [type t0 = ... and t1 = ...] *) - | AssumeType (** [assume type t] *) - | TypeVal (** In an fsti: [val t : Type0] *) - -(** A qualifier for function definitions. - - Controls whether we should use [let ...], [let rec ...] or [and ...], - or only generate a declaration with [val] or [assume val] - *) -type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal - -let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string = - match qualif with - | Let -> "let" - | LetRec -> "let rec" - | And -> "and" - | Val -> "val" - | AssumeVal -> "assume val" - -(** Small helper to compute the name of an int type *) -let fstar_int_name (int_ty : integer_type) = - match int_ty with - | Isize -> "isize" - | I8 -> "i8" - | I16 -> "i16" - | I32 -> "i32" - | I64 -> "i64" - | I128 -> "i128" - | Usize -> "usize" - | U8 -> "u8" - | U16 -> "u16" - | U32 -> "u32" - | U64 -> "u64" - | U128 -> "u128" - -(** Small helper to compute the name of a unary operation *) -let fstar_unop_name (unop : unop) : string = - match unop with - | Not -> "not" - | Neg int_ty -> fstar_int_name int_ty ^ "_neg" - | Cast _ -> raise (Failure "Unsupported") - -(** Small helper to compute the name of a binary operation (note that many - binary operations like "less than" are extracted to primitive operations, - like [<]. - *) -let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string = - let binop = - match binop with - | Div -> "div" - | Rem -> "rem" - | Add -> "add" - | Sub -> "sub" - | Mul -> "mul" - | _ -> raise (Failure "Unreachable") - in - fstar_int_name int_ty ^ "_" ^ binop - -(** A list of keywords/identifiers used in F* and with which we want to check - collision. *) -let fstar_keywords = - let named_unops = - fstar_unop_name Not - :: List.map (fun it -> fstar_unop_name (Neg it)) T.all_signed_int_types - in - let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in - let named_binops = - List.concat - (List.map - (fun bn -> - List.map (fun it -> fstar_named_binop_name bn it) T.all_int_types) - named_binops) - in - let misc = - [ - "let"; - "rec"; - "in"; - "fn"; - "val"; - "int"; - "nat"; - "list"; - "FStar"; - "FStar.Mul"; - "type"; - "match"; - "with"; - "assert"; - "assert_norm"; - "assume"; - "Type0"; - "Type"; - "unit"; - "not"; - "scalar_cast"; - ] - in - List.concat [ named_unops; named_binops; misc ] - -let fstar_assumed_adts : (assumed_ty * string) list = - [ (State, "state"); (Result, "result"); (Option, "option"); (Vec, "vec") ] - -let fstar_assumed_structs : (assumed_ty * string) list = [] - -let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list = - [ - (Result, result_return_id, "Return"); - (Result, result_fail_id, "Fail"); - (Option, option_some_id, "Some"); - (Option, option_none_id, "None"); - ] - -let fstar_assumed_llbc_functions : - (A.assumed_fun_id * T.RegionGroupId.id option * string) list = - let rg0 = Some T.RegionGroupId.zero in - [ - (Replace, None, "mem_replace_fwd"); - (Replace, rg0, "mem_replace_back"); - (VecNew, None, "vec_new"); - (VecPush, None, "vec_push_fwd") (* Shouldn't be used *); - (VecPush, rg0, "vec_push_back"); - (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *); - (VecInsert, rg0, "vec_insert_back"); - (VecLen, None, "vec_len"); - (VecIndex, None, "vec_index_fwd"); - (VecIndex, rg0, "vec_index_back") (* shouldn't be used *); - (VecIndexMut, None, "vec_index_mut_fwd"); - (VecIndexMut, rg0, "vec_index_mut_back"); - ] - -let fstar_assumed_pure_functions : (pure_assumed_fun_id * string) list = - [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ] - -let fstar_names_map_init : names_map_init = - { - keywords = fstar_keywords; - assumed_adts = fstar_assumed_adts; - assumed_structs = fstar_assumed_structs; - assumed_variants = fstar_assumed_variants; - assumed_llbc_functions = fstar_assumed_llbc_functions; - assumed_pure_functions = fstar_assumed_pure_functions; - } - -let fstar_extract_unop (extract_expr : bool -> texpression -> unit) - (fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit - = - match unop with - | Not | Neg _ -> - let unop = fstar_unop_name unop in - if inside then F.pp_print_string fmt "("; - F.pp_print_string fmt unop; - F.pp_print_space fmt (); - extract_expr true arg; - if inside then F.pp_print_string fmt ")" - | Cast (src, tgt) -> - (* The source type is an implicit parameter *) - if inside then F.pp_print_string fmt "("; - F.pp_print_string fmt "scalar_cast"; - F.pp_print_space fmt (); - F.pp_print_string fmt - (StringUtils.capitalize_first_letter - (PrintPure.integer_type_to_string src)); - F.pp_print_space fmt (); - F.pp_print_string fmt - (StringUtils.capitalize_first_letter - (PrintPure.integer_type_to_string tgt)); - F.pp_print_space fmt (); - extract_expr true arg; - if inside then F.pp_print_string fmt ")" - -let fstar_extract_binop (extract_expr : bool -> texpression -> unit) - (fmt : F.formatter) (inside : bool) (binop : E.binop) - (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit = - if inside then F.pp_print_string fmt "("; - (* Some binary operations have a special treatment *) - (match binop with - | Eq | Lt | Le | Ne | Ge | Gt -> - let binop = - match binop with - | Eq -> "=" - | Lt -> "<" - | Le -> "<=" - | Ne -> "<>" - | Ge -> ">=" - | Gt -> ">" - | _ -> raise (Failure "Unreachable") - in - extract_expr false arg0; - F.pp_print_space fmt (); - F.pp_print_string fmt binop; - F.pp_print_space fmt (); - extract_expr false arg1 - | Div | Rem | Add | Sub | Mul -> - let binop = fstar_named_binop_name binop int_ty in - F.pp_print_string fmt binop; - F.pp_print_space fmt (); - extract_expr false arg0; - F.pp_print_space fmt (); - extract_expr false arg1 - | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented); - if inside then F.pp_print_string fmt ")" - -(** - [ctx]: we use the context to lookup type definitions, to retrieve type names. - This is used to compute variable names, when they have no basenames: in this - case we use the first letter of the type name. - - [variant_concatenate_type_name]: if true, add the type name as a prefix - to the variant names. - Ex.: - In Rust: - {[ - enum List = { - Cons(u32, Box),x - Nil, - } - ]} - - F*, if option activated: - {[ - type list = - | ListCons : u32 -> list -> list - | ListNil : list - ]} - - F*, if option not activated: - {[ - type list = - | Cons : u32 -> list -> list - | Nil : list - ]} - - Rk.: this should be true by default, because in Rust all the variant names - are actively uniquely identifier by the type name [List::Cons(...)], while - in other languages it is not necessarily the case, and thus clashes can mess - up type checking. Note that some languages actually forbids the name clashes - (it is the case of F* ). - *) -let mk_formatter (ctx : trans_ctx) (crate_name : string) - (variant_concatenate_type_name : bool) : formatter = - let int_name = fstar_int_name in - - (* Prepare a name. - * The first id elem is always the crate: if it is the local crate, - * we remove it. - * We also remove all the disambiguators, then convert everything to strings. - * **Rmk:** because we remove the disambiguators, there may be name collisions - * (which is ok, because we check for name collisions and fail if there is any). - *) - let get_name (name : name) : string list = - (* Rmk.: initially we only filtered the disambiguators equal to 0 *) - let name = Names.filter_disambiguators name in - match name with - | Ident crate :: name -> - let name = if crate = crate_name then name else Ident crate :: name in - let name = - List.map - (function - | Names.Ident s -> s - | Disambiguator d -> Names.Disambiguator.to_string d) - name - in - name - | _ -> - raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) - in - let get_type_name = get_name in - let type_name_to_camel_case name = - let name = get_type_name name in - let name = List.map to_camel_case name in - String.concat "" name - in - let type_name_to_snake_case name = - let name = get_type_name name in - let name = List.map to_snake_case name in - String.concat "_" name - in - let type_name name = type_name_to_snake_case name ^ "_t" in - let field_name (def_name : name) (field_id : FieldId.id) - (field_name : string option) : string = - let def_name = type_name_to_snake_case def_name ^ "_" in - match field_name with - | Some field_name -> def_name ^ field_name - | None -> def_name ^ FieldId.to_string field_id - in - let variant_name (def_name : name) (variant : string) : string = - let variant = to_camel_case variant in - if variant_concatenate_type_name then - type_name_to_camel_case def_name ^ variant - else variant - in - let struct_constructor (basename : name) : string = - let tname = type_name basename in - "Mk" ^ tname - in - let get_fun_name = get_name in - let fun_name_to_snake_case (fname : fun_name) : string = - let fname = get_fun_name fname in - (* Converting to snake case should be a no-op, but it doesn't cost much *) - let fname = List.map to_snake_case fname in - (* Concatenate the elements *) - String.concat "_" fname - in - let global_name (name : global_name) : string = - (* Converting to snake case also lowercases the letters (in Rust, global - * names are written in capital letters). *) - let parts = List.map to_snake_case (get_name name) in - String.concat "_" parts - in - let fun_name (fname : fun_name) (num_rgs : int) - (rg : region_group_info option) (filter_info : bool * int) : string = - let fname = fun_name_to_snake_case fname in - (* Compute the suffix *) - let suffix = default_fun_suffix num_rgs rg filter_info in - (* Concatenate *) - fname ^ suffix - in - - let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string - = - let fname = fun_name_to_snake_case fname in - (* Compute the suffix *) - let suffix = "_decreases" in - (* Concatenate *) - fname ^ suffix - in - - let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) - : string = - (* If there is a basename, we use it *) - match basename with - | Some basename -> - (* This should be a no-op *) - to_snake_case basename - | None -> ( - (* No basename: we use the first letter of the type *) - match ty with - | Adt (type_id, tys) -> ( - match type_id with - | Tuple -> - (* The "pair" case is frequent enough to have its special treatment *) - if List.length tys = 2 then "p" else "t" - | Assumed Result -> "r" - | Assumed Option -> "opt" - | Assumed Vec -> "v" - | Assumed State -> "st" - | AdtId adt_id -> - let def = - TypeDeclId.Map.find adt_id ctx.type_context.type_decls - in - (* We do the following: - * - compute the type name, and retrieve the last ident - * - convert this to snake case - * - take the first letter of every "letter group" - * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm" - *) - (* Thename shouldn't be empty, and its last element should - * be an ident *) - let cl = List.nth def.name (List.length def.name - 1) in - let cl = to_snake_case (Names.as_ident cl) in - let cl = String.split_on_char '_' cl in - let cl = List.filter (fun s -> String.length s > 0) cl in - assert (List.length cl > 0); - let cl = List.map (fun s -> s.[0]) cl in - StringUtils.string_of_chars cl) - | TypeVar _ -> "x" (* lacking imagination here... *) - | Bool -> "b" - | Char -> "c" - | Integer _ -> "i" - | Str -> "s" - | Arrow _ -> "f" - | Array _ | Slice _ -> raise Unimplemented) - in - let type_var_basename (_varset : StringSet.t) (basename : string) : string = - (* This is *not* a no-op: type variables in Rust often start with - * a capital letter *) - to_snake_case basename - in - let append_index (basename : string) (i : int) : string = - basename ^ string_of_int i - in - - let extract_primitive_value (fmt : F.formatter) (_inside : bool) - (cv : primitive_value) : unit = - match cv with - | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value) - | Bool b -> - let b = if b then "true" else "false" in - F.pp_print_string fmt b - | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'") - | String s -> - (* We need to replace all the line breaks *) - let s = - StringUtils.map - (fun c -> if c = '\n' then "\n" else String.make 1 c) - s - in - F.pp_print_string fmt ("\"" ^ s ^ "\"") - in - { - bool_name = "bool"; - char_name = "char"; - int_name; - str_name = "string"; - field_name; - variant_name; - struct_constructor; - type_name; - global_name; - fun_name; - decreases_clause_name; - var_basename; - type_var_basename; - append_index; - extract_primitive_value; - extract_unop = fstar_extract_unop; - extract_binop = fstar_extract_binop; - } - -(** [inside] constrols whether we should add parentheses or not around type - applications (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 -> - (* This is a bit annoying, but in F* [()] is not the unit type: - * we have to write [unit]... *) - if tys = [] then F.pp_print_string fmt "unit" - else ( - F.pp_print_string fmt "("; - Collections.List.iter_link - (fun () -> - F.pp_print_space fmt (); - F.pp_print_string fmt "&"; - F.pp_print_space fmt ()) - (extract_ty ctx fmt true) tys; - F.pp_print_string fmt ")") - | AdtId _ | Assumed _ -> - let print_paren = inside && tys <> [] in - if print_paren then F.pp_print_string fmt "("; - F.pp_print_string fmt (ctx_get_type type_id ctx); - if tys <> [] then F.pp_print_space fmt (); - Collections.List.iter_link (F.pp_print_space fmt) - (extract_ty ctx fmt true) tys; - if print_paren then F.pp_print_string fmt ")") - | TypeVar vid -> F.pp_print_string fmt (ctx_get_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 - | Arrow (arg_ty, ret_ty) -> - if inside then F.pp_print_string fmt "("; - extract_ty ctx fmt false arg_ty; - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - F.pp_print_space fmt (); - extract_ty ctx fmt false ret_ty; - if inside then F.pp_print_string fmt ")" - | Array _ | Slice _ -> raise Unimplemented - -(** Compute the names for all the top-level identifiers used in a type - definition (type name, variant names, field names, etc. but not type - parameters). - - We need to do this preemptively, beforce extracting any definition, - because of recursive definitions. - *) -let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : - extraction_ctx = - (* Compute and register the type def name *) - let ctx = ctx_add_type_decl def ctx in - (* Compute and register: - * - the variant names, if this is an enumeration - * - the field names, if this is a structure - *) - let ctx = - match def.kind with - | Struct fields -> - (* Add the fields *) - let ctx = - fst - (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) - in - (* Add the constructor name *) - fst (ctx_add_struct def ctx) - | Enum variants -> - fst - (ctx_add_variants def - (VariantId.mapi (fun id v -> (id, v)) variants) - ctx) - | Opaque -> - (* Nothing to do *) - ctx - in - (* Return *) - ctx - -let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) - (def : type_decl) (fields : field list) : unit = - (* We want to generate a definition which looks like this: - {[ - type t = { x : int; y : bool; } - ]} - - If there isn't enough space on one line: - {[ - type t = - { - x : int; y : bool; - } - ]} - - And if there is even less space: - {[ - type t = - { - x : int; - y : bool; - } - ]} - - Also, in case there are no fields, we need to define the type as [unit] - ([type t = {}] doesn't work in F* ). - *) - (* Note that we already printed: [type t =] *) - if fields = [] then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "unit") - else ( - F.pp_print_space fmt (); - F.pp_print_string fmt "{"; - F.pp_print_break fmt 1 ctx.indent_incr; - (* The body itself *) - F.pp_open_hvbox fmt 0; - (* Print the fields *) - let print_field (field_id : FieldId.id) (f : field) : unit = - let field_name = ctx_get_field (AdtId def.def_id) field_id ctx 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_print_string fmt ";"; - F.pp_close_box fmt () - in - let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in - Collections.List.iter_link (F.pp_print_space fmt) - (fun (fid, f) -> print_field fid f) - fields; - (* Close *) - F.pp_close_box fmt (); - F.pp_print_space fmt (); - F.pp_print_string fmt "}") - -let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) - (def : type_decl) (def_name : string) (type_params : string list) - (variants : variant list) : unit = - (* We want to generate a definition which looks like this: - {[ - type list a = | Cons : a -> list a -> list a | Nil : list a - ]} - - If there isn't enough space on one line: - {[ - type s = - | Cons : a -> list a -> list a - | Nil : list a - ]} - - And if we need to write the type of a variant on several lines: - {[ - type s = - | Cons : - a -> - list a -> - list a - | Nil : list a - ]} - - Finally, it is possible to give names to the variant fields in Rust. - In this situation, we generate a definition like this: - {[ - type s = - | Cons : hd:a -> tl:list a -> list a - | Nil : list a - ]} - - Note that we already printed: [type s =] - *) - (* Print the variants *) - let print_variant (variant_id : VariantId.id) (variant : variant) : unit = - let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in - F.pp_print_space fmt (); - F.pp_open_hvbox fmt ctx.indent_incr; - (* variant box *) - (* [| Cons :] - * Note that we really don't want any break above so we print everything - * at once. *) - F.pp_print_string fmt ("| " ^ variant_name ^ " :"); - F.pp_print_space fmt (); - let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) : - extraction_ctx = - (* Open the field box *) - F.pp_open_box fmt ctx.indent_incr; - (* Print the field names - * [ x :] - * Note that when printing fields, we register the field names as - * *variables*: they don't need to be unique at the top level. *) - let ctx = - match f.field_name with - | None -> ctx - | Some field_name -> - let var_id = VarId.of_int (FieldId.to_int fid) in - let field_name = - ctx.fmt.var_basename ctx.names_map.names_set (Some field_name) - f.field_ty - in - let ctx, field_name = ctx_add_var field_name var_id ctx in - F.pp_print_string fmt (field_name ^ " :"); - F.pp_print_space fmt (); - ctx - in - (* Print the field type *) - extract_ty ctx fmt false f.field_ty; - (* Print the arrow [->]*) - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - (* Close the field box *) - F.pp_close_box fmt (); - F.pp_print_space fmt (); - (* Return *) - ctx - in - (* Print the fields *) - let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in - let _ = - List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields - in - (* Print the final type *) - F.pp_open_hovbox fmt 0; - F.pp_print_string fmt def_name; - List.iter - (fun type_param -> - F.pp_print_space fmt (); - F.pp_print_string fmt type_param) - type_params; - F.pp_close_box fmt (); - (* Close the variant box *) - F.pp_close_box fmt () - in - (* Print the variants *) - let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in - List.iter (fun (vid, v) -> print_variant vid v) variants - -(** Extract a type declaration. - - Note that all the names used for extraction should already have been - registered. - *) -let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : type_decl_qualif) (def : type_decl) : unit = - (* Retrieve the definition name *) - let def_name = ctx_get_local_type def.def_id ctx in - (* Add the type params - note that we need those bindings only for the - * body translation (they are not top-level) *) - let ctx_body, type_params = ctx_add_type_params def.type_params ctx in - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Print a comment to link the extracted type to its original rust definition *) - F.pp_print_string fmt ("(** [" ^ Print.name_to_string def.name ^ "] *)"); - F.pp_print_space fmt (); - (* Open a box for the definition, so that whenever possible it gets printed on - * one line *) - F.pp_open_hvbox fmt 0; - (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* > "type TYPE_NAME" *) - let extract_body, qualif = - match qualif with - | Type -> (true, "type") - | And -> (true, "and") - | AssumeType -> (false, "assume type") - | TypeVal -> (false, "val") - in - F.pp_print_string fmt (qualif ^ " " ^ def_name); - (* Print the type parameters *) - if def.type_params <> [] then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx_body in - F.pp_print_string fmt pname; - F.pp_print_space fmt ()) - def.type_params; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type0)"); - (* Print the "=" if we extract the body*) - if extract_body then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "=") - else ( - (* Otherwise print ": Type0" *) - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type0"); - (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *) - F.pp_close_box fmt (); - (if extract_body then - match def.kind with - | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields - | Enum variants -> - extract_type_decl_enum_body ctx_body fmt def def_name type_params - variants - | Opaque -> raise (Failure "Unreachable")); - (* Close the box for the definition *) - F.pp_close_box fmt (); - (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 - -(** Extract the state type declaration. *) -let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) - (qualif : type_decl_qualif) : unit = - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Print a comment *) - F.pp_print_string fmt "(** The state type used in the state-error monad *)"; - F.pp_print_space fmt (); - (* Open a box for the definition, so that whenever possible it gets printed on - * one line *) - F.pp_open_hvbox fmt 0; - (* Retrieve the name *) - let state_name = ctx_get_assumed_type State ctx in - (* The qualif should be [AssumeType] or [TypeVal] *) - (match qualif with - | Type | And -> raise (Failure "Unexpected") - | AssumeType -> - F.pp_print_string fmt "assume"; - F.pp_print_space fmt (); - F.pp_print_string fmt "type"; - F.pp_print_space fmt (); - F.pp_print_string fmt state_name; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type0" - | TypeVal -> - F.pp_print_string fmt "val"; - F.pp_print_space fmt (); - F.pp_print_string fmt state_name; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type0"); - (* Close the box for the definition *) - F.pp_close_box fmt (); - (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 - -(** Compute the names for all the pure functions generated from a rust function - (forward function and backward functions). - *) -let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) - (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx - = - let fwd, back_ls = def in - (* Register the decrease clause, if necessary *) - let ctx = - if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx - in - (* Register the forward function name *) - let ctx = ctx_add_fun_decl (keep_fwd, def) fwd ctx in - (* Register the backward functions' names *) - let ctx = - List.fold_left - (fun ctx back -> ctx_add_fun_decl (keep_fwd, def) back ctx) - ctx back_ls - in - (* Return *) - ctx - -(** Simply add the global name to the context. *) -let extract_global_decl_register_names (ctx : extraction_ctx) - (def : A.global_decl) : extraction_ctx = - ctx_add_global_decl_and_body def ctx - -(** The following function factorizes the extraction of ADT values. - - Note that patterns can introduce new variables: we thus return an extraction - context updated with new bindings. - - TODO: we don't need something very generic anymore - *) -let extract_adt_g_value - (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx) - (fmt : F.formatter) (ctx : extraction_ctx) (inside : bool) - (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : - extraction_ctx = - match ty with - | Adt (Tuple, _) -> - (* Tuple *) - F.pp_print_string fmt "("; - let ctx = - Collections.List.fold_left_link - (fun () -> - F.pp_print_string fmt ","; - F.pp_print_space fmt ()) - (fun ctx v -> extract_value ctx false v) - ctx field_values - in - F.pp_print_string fmt ")"; - ctx - | Adt (adt_id, _) -> - (* "Regular" ADT *) - (* We print something of the form: [Cons field0 ... fieldn]. - * We could update the code to print something of the form: - * [{ field0=...; ...; fieldn=...; }] in case of structures. - *) - let cons = - match variant_id with - | Some vid -> ctx_get_variant adt_id vid ctx - | None -> ctx_get_struct adt_id ctx - in - if inside && field_values <> [] then F.pp_print_string fmt "("; - F.pp_print_string fmt cons; - let ctx = - Collections.List.fold_left - (fun ctx v -> - F.pp_print_space fmt (); - extract_value ctx true v) - ctx field_values - in - if inside && field_values <> [] then F.pp_print_string fmt ")"; - ctx - | _ -> raise (Failure "Inconsistent typed value") - -(* Extract globals in the same way as variables *) -let extract_global (ctx : extraction_ctx) (fmt : F.formatter) - (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global id ctx) - -(** [inside]: see {!extract_ty}. - - As a pattern can introduce new variables, we return an extraction context - updated with new bindings. - *) -let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (v : typed_pattern) : extraction_ctx = - match v.value with - | PatConstant cv -> - ctx.fmt.extract_primitive_value fmt inside cv; - ctx - | PatVar (v, _) -> - let vname = - ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty - in - let ctx, vname = ctx_add_var vname v.id ctx in - F.pp_print_string fmt vname; - ctx - | PatDummy -> - F.pp_print_string fmt "_"; - ctx - | PatAdt av -> - let extract_value ctx inside v = extract_typed_pattern ctx fmt inside v in - extract_adt_g_value extract_value fmt ctx inside av.variant_id - av.field_values v.ty - -(** [inside]: controls the introduction of parentheses. See [extract_ty] - - TODO: replace the formatting boolean [inside] with something more general? - Also, it seems we don't really use it... - Cases to consider: - - right-expression in a let: [let x = re in _] (never parentheses?) - - next expression in a let: [let x = _ in next_e] (never parentheses?) - - application argument: [f (exp)] - - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _] - *) -let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (e : texpression) : unit = - match e.e with - | Var var_id -> - let var_name = ctx_get_var var_id ctx in - F.pp_print_string fmt var_name - | Const cv -> ctx.fmt.extract_primitive_value fmt inside cv - | App _ -> - let app, args = destruct_apps e in - extract_App ctx fmt inside app args - | Abs _ -> - let xl, e = destruct_abs_list e in - extract_Abs ctx fmt inside xl e - | Qualif _ -> - (* We use the app case *) - extract_App ctx fmt inside e [] - | Let (monadic, lv, re, next_e) -> - extract_Let ctx fmt inside monadic lv re next_e - | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body - | Meta (_, e) -> extract_texpression ctx fmt inside e - -(* Extract an application *or* a top-level qualif (function extraction has - * to handle top-level qualifiers, so it seemed more natural to merge the - * two cases) *) -and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (app : texpression) (args : texpression list) : unit = - (* We don't do the same thing if the app is a top-level identifier (function, - * ADT constructor...) or a "regular" expression *) - match app.e with - | Qualif qualif -> ( - (* Top-level qualifier *) - match qualif.id with - | FunOrOp fun_id -> - extract_function_call ctx fmt inside fun_id qualif.type_args args - | Global global_id -> extract_global ctx fmt global_id - | AdtCons adt_cons_id -> - extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args - | Proj proj -> - extract_field_projector ctx fmt inside app proj qualif.type_args args) - | _ -> - (* "Regular" expression *) - (* Open parentheses *) - if inside then F.pp_print_string fmt "("; - (* Open a box for the application *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the app expression *) - let app_inside = (inside && args = []) || args <> [] in - extract_texpression ctx fmt app_inside app; - (* Print the arguments *) - List.iter - (fun ve -> - F.pp_print_space fmt (); - extract_texpression ctx fmt true ve) - args; - (* Close the box for the application *) - F.pp_close_box fmt (); - (* Close parentheses *) - if inside then F.pp_print_string fmt ")" - -(** Subcase of the app case: function call *) -and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (fid : fun_or_op_id) (type_args : ty list) - (args : texpression list) : unit = - match (fid, args) with - | Unop unop, [ arg ] -> - (* A unop can have *at most* one argument (the result can't be a function!). - * Note that the way we generate the translation, we shouldn't get the - * case where we have no argument (all functions are fully instantiated, - * and no AST transformation introduces partial calls). *) - ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg - | Binop (binop, int_ty), [ arg0; arg1 ] -> - (* Number of arguments: similar to unop *) - ctx.fmt.extract_binop - (extract_texpression ctx fmt) - fmt inside binop int_ty arg0 arg1 - | Fun fun_id, _ -> - if inside then F.pp_print_string fmt "("; - (* Open a box for the function call *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the function name *) - let fun_name = ctx_get_function fun_id ctx in - F.pp_print_string fmt fun_name; - (* Print the type parameters *) - List.iter - (fun ty -> - F.pp_print_space fmt (); - extract_ty ctx fmt true ty) - type_args; - (* Print the arguments *) - List.iter - (fun ve -> - F.pp_print_space fmt (); - extract_texpression ctx fmt true ve) - args; - (* Close the box for the function call *) - F.pp_close_box fmt (); - (* Return *) - if inside then F.pp_print_string fmt ")" - | (Unop _ | Binop _), _ -> - raise - (Failure - ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid - ^ ",\nNumber of arguments: " - ^ string_of_int (List.length args) - ^ ",\nArguments: " - ^ String.concat " " (List.map show_texpression args))) - -(** Subcase of the app case: ADT constructor *) -and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) : - unit = - match adt_cons.adt_id with - | Tuple -> - (* Tuple *) - (* For now, we only support fully applied tuple constructors *) - assert (List.length type_args = List.length args); - F.pp_print_string fmt "("; - Collections.List.iter_link - (fun () -> - F.pp_print_string fmt ","; - F.pp_print_space fmt ()) - (fun v -> extract_texpression ctx fmt false v) - args; - F.pp_print_string fmt ")" - | _ -> - (* "Regular" ADT *) - (* We print something of the form: [Cons field0 ... fieldn]. - * We could update the code to print something of the form: - * [{ field0=...; ...; fieldn=...; }] in case of fully - * applied structure constructors. - *) - let cons = - match adt_cons.variant_id with - | Some vid -> ctx_get_variant adt_cons.adt_id vid ctx - | None -> ctx_get_struct adt_cons.adt_id ctx - in - let use_parentheses = inside && args <> [] in - if use_parentheses then F.pp_print_string fmt "("; - F.pp_print_string fmt cons; - Collections.List.iter - (fun v -> - F.pp_print_space fmt (); - extract_texpression ctx fmt true v) - args; - if use_parentheses then F.pp_print_string fmt ")" - -(** Subcase of the app case: ADT field projector. *) -and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (original_app : texpression) (proj : projection) - (_proj_type_params : ty list) (args : texpression list) : unit = - (* We isolate the first argument (if there is), in order to pretty print the - * projection ([x.field] instead of [MkAdt?.field x] *) - match args with - | [ arg ] -> - (* Exactly one argument: pretty-print *) - let field_name = ctx_get_field proj.adt_id proj.field_id ctx in - (* Open a box *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Extract the expression *) - extract_texpression ctx fmt true arg; - (* We allow to break where the "." appears *) - F.pp_print_break fmt 0 0; - F.pp_print_string fmt "."; - F.pp_print_string fmt field_name; - (* Close the box *) - F.pp_close_box fmt () - | arg :: args -> - (* Call extract_App again, but in such a way that the first argument is - * isolated *) - extract_App ctx fmt inside (mk_app original_app arg) args - | [] -> - (* No argument: shouldn't happen *) - raise (Failure "Unreachable") - -and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (xl : typed_pattern list) (e : texpression) : unit = - (* Open a box for the abs expression *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Open parentheses *) - if inside then F.pp_print_string fmt "("; - (* Print the lambda - note that there should always be at least one variable *) - assert (xl <> []); - F.pp_print_string fmt "fun"; - let ctx = - List.fold_left - (fun ctx x -> - F.pp_print_space fmt (); - extract_typed_pattern ctx fmt true x) - ctx xl - in - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - F.pp_print_space fmt (); - (* Print the body *) - extract_texpression ctx fmt false e; - (* Close parentheses *) - if inside then F.pp_print_string fmt ")"; - (* Close the box for the abs expression *) - F.pp_close_box fmt () - -and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (monadic : bool) (lv : typed_pattern) (re : texpression) - (next_e : texpression) : unit = - (* Open a box for the whole expression *) - F.pp_open_hvbox fmt 0; - (* Open parentheses *) - if inside then F.pp_print_string fmt "("; - (* Open a box for the let-binding *) - F.pp_open_hovbox fmt ctx.indent_incr; - let ctx = - if monadic then ( - (* Note that in F*, the left value of a monadic let-binding can only be - * a variable *) - let ctx = extract_typed_pattern ctx fmt true lv in - F.pp_print_space fmt (); - F.pp_print_string fmt "<--"; - F.pp_print_space fmt (); - extract_texpression ctx fmt false re; - F.pp_print_string fmt ";"; - ctx) - else ( - F.pp_print_string fmt "let"; - F.pp_print_space fmt (); - let ctx = extract_typed_pattern ctx fmt true lv in - F.pp_print_space fmt (); - F.pp_print_string fmt "="; - F.pp_print_space fmt (); - extract_texpression ctx fmt false re; - F.pp_print_space fmt (); - F.pp_print_string fmt "in"; - ctx) - in - (* Close the box for the let-binding *) - F.pp_close_box fmt (); - (* Print the next expression *) - F.pp_print_space fmt (); - extract_texpression ctx fmt false next_e; - (* Close parentheses *) - if inside then F.pp_print_string fmt ")"; - (* Close the box for the whole expression *) - F.pp_close_box fmt () - -and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (scrut : texpression) (body : switch_body) : unit = - (* Open a box for the whole expression *) - F.pp_open_hvbox fmt 0; - (* Open parentheses *) - if inside then F.pp_print_string fmt "("; - (* Extract the switch *) - (match body with - | If (e_then, e_else) -> - (* Open a box for the [if] *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "if"; - F.pp_print_space fmt (); - let scrut_inside = PureUtils.let_group_requires_parentheses scrut in - extract_texpression ctx fmt scrut_inside scrut; - (* Close the box for the [if] *) - F.pp_close_box fmt (); - (* Extract the branches *) - let extract_branch (is_then : bool) (e_branch : texpression) : unit = - F.pp_print_space fmt (); - (* Open a box for the then/else+branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - let then_or_else = if is_then then "then" else "else" in - F.pp_print_string fmt then_or_else; - F.pp_print_space fmt (); - (* Open a box for the branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the [begin] if necessary *) - let parenth = PureUtils.let_group_requires_parentheses e_branch in - if parenth then ( - F.pp_print_string fmt "begin"; - F.pp_print_space fmt ()); - (* Print the branch expression *) - extract_texpression ctx fmt false e_branch; - (* Close the [begin ... end ] *) - if parenth then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "end"); - (* Close the box for the branch *) - F.pp_close_box fmt (); - (* Close the box for the then/else+branch *) - F.pp_close_box fmt () - in - - extract_branch true e_then; - extract_branch false e_else - | Match branches -> - (* Open a box for the [match ... with] *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the [match ... with] *) - F.pp_print_string fmt "begin match"; - F.pp_print_space fmt (); - let scrut_inside = PureUtils.let_group_requires_parentheses scrut in - extract_texpression ctx fmt scrut_inside scrut; - F.pp_print_space fmt (); - F.pp_print_string fmt "with"; - (* Close the box for the [match ... with] *) - F.pp_close_box fmt (); - - (* Extract the branches *) - let extract_branch (br : match_branch) : unit = - F.pp_print_space fmt (); - (* Open a box for the pattern+branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "|"; - (* Print the pattern *) - F.pp_print_space fmt (); - let ctx = extract_typed_pattern ctx fmt false br.pat in - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - F.pp_print_space fmt (); - (* Open a box for the branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the branch itself *) - extract_texpression ctx fmt false br.branch; - (* Close the box for the branch *) - F.pp_close_box fmt (); - (* Close the box for the pattern+branch *) - F.pp_close_box fmt () - in - - List.iter extract_branch branches; - - (* End the match *) - F.pp_print_space fmt (); - F.pp_print_string fmt "end"); - (* Close parentheses *) - if inside then F.pp_print_string fmt ")"; - (* Close the box for the whole expression *) - F.pp_close_box fmt () - -(** A small utility to print the parameters of a function signature. - - We return two contexts: - - the context augmented with bindings for the type parameters - - the previous context augmented with bindings for the input values - *) -let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_decl) : extraction_ctx * extraction_ctx = - (* Add the type parameters - note that we need those bindings only for the - * body translation (they are not top-level) *) - let ctx, _ = ctx_add_type_params def.signature.type_params ctx in - (* Print the parameters - rk.: we should have filtered the functions - * with no input parameters *) - (* The type parameters *) - if def.signature.type_params <> [] then ( - (* Open a box for the type parameters *) - F.pp_open_hovbox fmt 0; - F.pp_print_string fmt "("; - List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx in - F.pp_print_string fmt pname; - F.pp_print_space fmt ()) - def.signature.type_params; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type0)"; - (* Close the box for the type parameters *) - F.pp_close_box fmt (); - F.pp_print_space fmt ()); - (* The input parameters - note that doing this adds bindings to the context *) - let ctx_body = - match def.body with - | None -> ctx - | Some body -> - List.fold_left - (fun ctx (lv : typed_pattern) -> - (* Open a box for the input parameter *) - F.pp_open_hovbox fmt 0; - F.pp_print_string fmt "("; - let ctx = extract_typed_pattern ctx fmt false lv in - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - extract_ty ctx fmt false lv.ty; - F.pp_print_string fmt ")"; - (* Close the box for the input parameters *) - F.pp_close_box fmt (); - F.pp_print_space fmt (); - ctx) - ctx body.inputs_lvs - in - (ctx, ctx_body) - -(** A small utility to print the types of the input parameters in the form: - [u32 -> list u32 -> ...] - (we don't print the return type of the function) - - This is used for opaque function declarations, in particular. - *) -let extract_fun_input_parameters_types (ctx : extraction_ctx) - (fmt : F.formatter) (def : fun_decl) : unit = - let extract_param (ty : ty) : unit = - let inside = false in - extract_ty ctx fmt inside ty; - F.pp_print_space fmt (); - F.pp_print_string fmt "->"; - F.pp_print_space fmt () - in - List.iter extract_param def.signature.inputs - -(** Extract a decrease clause function template body. - - In order to help the user, we can generate a template for the functions - required by the decreases clauses. We simply generate definitions of - the following form in a separate file: - {[ - let f_decrease (t : Type0) (x : t) : nat = admit() - ]} - - Where the translated functions for [f] look like this: - {[ - let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ... - ]} - *) -let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_decl) : unit = - (* Retrieve the function name *) - let def_name = ctx_get_decreases_clause def.def_id ctx in - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Print a comment to link the extracted type to its original rust definition *) - F.pp_print_string fmt - ("(** [" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause *)"); - F.pp_print_space fmt (); - (* Open a box for the definition, so that whenever possible it gets printed on - * one line *) - F.pp_open_hvbox fmt 0; - (* Add the [unfold] keyword *) - F.pp_print_string fmt "unfold"; - F.pp_print_space fmt (); - (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) - F.pp_open_hvbox fmt ctx.indent_incr; - (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* > "let FUN_NAME" *) - F.pp_print_string fmt ("let " ^ def_name); - F.pp_print_space fmt (); - (* Extract the parameters *) - let _, _ = extract_fun_parameters ctx fmt def in - F.pp_print_string fmt ":"; - (* Print the signature *) - F.pp_print_space fmt (); - F.pp_print_string fmt "nat"; - (* Print the "=" *) - F.pp_print_space fmt (); - F.pp_print_string fmt "="; - (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) - F.pp_close_box fmt (); - F.pp_print_space fmt (); - (* Print the "admit ()" *) - F.pp_print_string fmt "admit ()"; - (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) - F.pp_close_box fmt (); - (* Close the box for the whole definition *) - F.pp_close_box fmt (); - (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 - -(** Extract a function declaration. - - Note that all the names used for extraction should already have been - registered. - - We take the definition of the forward translation as parameter (which is - equal to the definition to extract, if we extract a forward function) because - it is useful for the decrease clause. - *) -let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) : - unit = - assert (not def.is_global_decl_body); - (* Retrieve the function name *) - let def_name = ctx_get_local_function def.def_id def.back_id ctx in - (* (* Add the type parameters - note that we need those bindings only for the - * body translation (they are not top-level) *) - let ctx, _ = ctx_add_type_params def.signature.type_params ctx in *) - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Print a comment to link the extracted type to its original rust definition *) - F.pp_print_string fmt - ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)"); - F.pp_print_space fmt (); - (* Open a box for the definition, so that whenever possible it gets printed on - * one line *) - F.pp_open_hvbox fmt ctx.indent_incr; - (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* > "let FUN_NAME" *) - let is_opaque = Option.is_none def.body in - let qualif = fun_decl_qualif_keyword qualif in - F.pp_print_string fmt (qualif ^ " " ^ def_name); - F.pp_print_space fmt (); - (* Open a box for "(PARAMS) : EFFECT =" *) - F.pp_open_hvbox fmt 0; - (* Open a box for "(PARAMS)" *) - F.pp_open_hovbox fmt 0; - let ctx, ctx_body = extract_fun_parameters ctx fmt def in - (* Close the box for "(PARAMS)" *) - F.pp_close_box fmt (); - (* Print the return type - note that we have to be careful when - * printing the input values for the decrease clause, because - * it introduces bindings in the context... We thus "forget" - * the bindings we introduced above. - * TODO: figure out a cleaner way *) - let _ = - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - (* Open a box for the EFFECT *) - F.pp_open_hvbox fmt 0; - (* Open a box for the return type *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the return type *) - (* For opaque definitions, as we don't have named parameters under the hand, - * we don't print parameters in the form [(x : a) (y : b) ...] above, - * but wait until here to print the types: [a -> b -> ...]. *) - if is_opaque then extract_fun_input_parameters_types ctx fmt def; - (* [Tot] *) - if has_decreases_clause then ( - F.pp_print_string fmt "Tot"; - F.pp_print_space fmt ()); - extract_ty ctx fmt has_decreases_clause def.signature.output; - (* Close the box for the return type *) - F.pp_close_box fmt (); - (* Print the decrease clause - rk.: a function with a decreases clause - * is necessarily a transparent function *) - if has_decreases_clause then ( - F.pp_print_space fmt (); - (* Open a box for the decrease clause *) - F.pp_open_hovbox fmt 0; - (* *) - F.pp_print_string fmt "(decreases"; - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - (* The name of the decrease clause *) - let decr_name = ctx_get_decreases_clause def.def_id ctx in - F.pp_print_string fmt decr_name; - (* Print the type parameters *) - List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx in - F.pp_print_space fmt (); - F.pp_print_string fmt pname) - def.signature.type_params; - (* Print the input values: we have to be careful here to print - * only the input values which are in common with the *forward* - * function (the additional input values "given back" to the - * backward functions have no influence on termination: we thus - * share the decrease clauses between the forward and the backward - * functions - we also ignore the additional state received by the - * backward function, if there is one). - *) - let inputs_lvs = - let all_inputs = (Option.get def.body).inputs_lvs in - let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in - Collections.List.prefix num_fwd_inputs all_inputs - in - let _ = - List.fold_left - (fun ctx (lv : typed_pattern) -> - F.pp_print_space fmt (); - let ctx = extract_typed_pattern ctx fmt false lv in - ctx) - ctx inputs_lvs - in - F.pp_print_string fmt "))"; - (* Close the box for the decrease clause *) - F.pp_close_box fmt ()); - (* Close the box for the EFFECT *) - F.pp_close_box fmt () - in - (* Print the "=" *) - if not is_opaque then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "="); - (* Close the box for "(PARAMS) : EFFECT =" *) - F.pp_close_box fmt (); - (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) - F.pp_close_box fmt (); - if not is_opaque then ( - F.pp_print_space fmt (); - (* Open a box for the body *) - F.pp_open_hvbox fmt 0; - (* Extract the body *) - let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in - (* Close the box for the body *) - F.pp_close_box fmt ()); - (* Close the box for the definition *) - F.pp_close_box fmt (); - (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 - -(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) -let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (name : string) (ty : ty) - (extract_body : (F.formatter -> unit) Option.t) : unit = - let is_opaque = Option.is_none extract_body in - - (* Open the definition box (depth=0) *) - F.pp_open_hvbox fmt ctx.indent_incr; - - (* Open "QUALIF NAME : TYPE =" box (depth=1) *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print "QUALIF NAME " *) - F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name); - F.pp_print_space fmt (); - - (* Open ": TYPE =" box (depth=2) *) - F.pp_open_hvbox fmt 0; - (* Print ": " *) - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - - (* Open "TYPE" box (depth=3) *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print "TYPE" *) - extract_ty ctx fmt false ty; - (* Close "TYPE" box (depth=3) *) - F.pp_close_box fmt (); - - if not is_opaque then ( - (* Print " =" *) - F.pp_print_space fmt (); - F.pp_print_string fmt "="); - (* Close ": TYPE =" box (depth=2) *) - F.pp_close_box fmt (); - (* Close "QUALIF NAME : TYPE =" box (depth=1) *) - F.pp_close_box fmt (); - - if not is_opaque then ( - F.pp_print_space fmt (); - (* Open "BODY" box (depth=1) *) - F.pp_open_hvbox fmt 0; - (* Print "BODY" *) - (Option.get extract_body) fmt; - (* Close "BODY" box (depth=1) *) - F.pp_close_box fmt ()); - (* Close the definition box (depth=0) *) - F.pp_close_box fmt () - -(** Extract a global declaration. - We generate the body which computes the global value separately from the value declaration itself. - - For example in Rust, - [static X: u32 = 3;] - - will be translated to: - [let x_body : result u32 = Return 3] - [let x_c : u32 = eval_global x_body] - *) -let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = - assert body.is_global_decl_body; - assert (Option.is_none body.back_id); - assert (List.length body.signature.inputs = 0); - assert (List.length body.signature.doutputs = 1); - assert (List.length body.signature.type_params = 0); - - (* Add a break then the name of the corresponding LLBC declaration *) - F.pp_print_break fmt 0 0; - F.pp_print_string fmt - ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); - F.pp_print_space fmt (); - - let decl_name = ctx_get_global global.def_id ctx in - let body_name = - ctx_get_function (FromLlbc (Regular global.body_id, None)) ctx - in - - let decl_ty, body_ty = - let ty = body.signature.output in - if body.signature.info.effect_info.can_fail then (unwrap_result_ty ty, ty) - else (ty, mk_result_ty ty) - in - match body.body with - | None -> - let qualif = if interface then Val else AssumeVal in - extract_global_decl_body ctx fmt qualif decl_name decl_ty None - | Some body -> - extract_global_decl_body ctx fmt Let body_name body_ty - (Some (fun fmt -> extract_texpression ctx fmt false body.body)); - F.pp_print_break fmt 0 0; - extract_global_decl_body ctx fmt Let decl_name decl_ty - (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name))); - F.pp_print_break fmt 0 0 - -(** Extract a unit test, if the function is a unit function (takes no - parameters, returns unit). - - A unit test simply checks that the function normalizes to [Return ()]: - {[ - let _ = assert_norm (FUNCTION () = Return ()) - ]} - *) -let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_decl) : unit = - (* We only insert unit tests for forward functions *) - assert (def.back_id = None); - (* Check if this is a unit function *) - let sg = def.signature in - if - sg.type_params = [] - && (sg.inputs = [ mk_unit_ty ] || sg.inputs = []) - && sg.output = mk_result_ty mk_unit_ty - then ( - (* Add a break before *) - F.pp_print_break fmt 0 0; - (* Print a comment *) - F.pp_print_string fmt - ("(** Unit test for [" ^ Print.fun_name_to_string def.basename ^ "] *)"); - F.pp_print_space fmt (); - (* Open a box for the test *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the test *) - F.pp_print_string fmt "let _ ="; - F.pp_print_space fmt (); - F.pp_print_string fmt "assert_norm"; - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - let fun_name = ctx_get_local_function def.def_id def.back_id ctx in - F.pp_print_string fmt fun_name; - if sg.inputs <> [] then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "()"); - F.pp_print_space fmt (); - F.pp_print_string fmt "="; - F.pp_print_space fmt (); - let success = ctx_get_variant (Assumed Result) result_return_id ctx in - F.pp_print_string fmt (success ^ " ())"); - (* Close the box for the test *) - F.pp_close_box fmt (); - (* Add a break after *) - F.pp_print_break fmt 0 0) - else (* Do nothing *) - () -- cgit v1.2.3