From 4cdcf221812d80b978cd92601c3353f4356bd550 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Apr 2022 19:11:19 +0200 Subject: Make more progress propagating the changes --- src/ExtractToFStar.ml | 235 +++++++++++++++++++++++++++++--------------------- src/PrintPure.ml | 3 +- src/Pure.ml | 8 +- src/PureUtils.ml | 15 +--- src/SymbolicToPure.ml | 2 +- 5 files changed, 151 insertions(+), 112 deletions(-) (limited to 'src') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index e9b91c6e..8134144a 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -760,6 +760,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) Note that lvalues 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) @@ -830,57 +832,6 @@ let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter) extract_adt_g_value extract_value fmt ctx inside av.variant_id av.field_values v.ty -let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit - = - let rec extract_projection (pl : projection) : unit = - match pl with - | [] -> - (* No projection element left: print the variable *) - let var_name = ctx_get_var p.var ctx in - F.pp_print_string fmt var_name - | pe :: pl -> - (* Extract the interior of the projection *) - extract_projection pl; - (* Match on the projection element *) - let def_id = - match pe.pkind with - | E.ProjAdt (def_id, None) -> def_id - | E.ProjAdt (_, Some _) | E.ProjOption _ | E.ProjTuple _ -> - (* We can't have field accesses on enumerations (variables for - * the fields are introduced upon the moment we match over the - * enumeration). We also forbid field access on tuples, because - * we don't have the syntax to translate that... We thus - * deconstruct the tuples whenever we need to have access: - * `let (x, y) = p in ...` *) - raise (Failure "Unreachable") - in - let field_name = ctx_get_field (AdtId def_id) pe.field_id ctx in - (* 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 - in - (* We allow to break where "." appears, but we try to prevent that by - * wrapping in a box *) - F.pp_open_hovbox fmt ctx.indent_incr; - extract_projection p.projection; - F.pp_close_box fmt () - -(** [inside]: see [extract_ty] *) -let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (v : typed_rvalue) : extraction_ctx = - match v.value with - | RvConcrete cv -> - ctx.fmt.extract_constant_value fmt inside cv; - ctx - | RvPlace p -> - extract_place ctx fmt p; - ctx - | RvAdt av -> - let extract_value ctx inside v = extract_typed_rvalue 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? @@ -889,16 +840,17 @@ let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter) let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = match e.e with - | Value (rv, _) -> - let _ = extract_typed_rvalue ctx fmt inside rv in - () + | Local var_id -> + let var_name = ctx_get_var var_id ctx in + F.pp_print_string fmt var_name + | Const cv -> ctx.fmt.extract_constant_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 - | Func _ -> + | Qualif _ -> (* We use the app case *) extract_App ctx fmt inside e [] | Let (monadic, lv, re, next_e) -> @@ -908,48 +860,19 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) 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 function identifier or a "regular" expression *) + (* 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 - | Func func -> ( - (* Function identifier *) - match (func.func, args) with - | Unop unop, [ arg ] -> - ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg - | Binop (binop, int_ty), [ arg0; arg1 ] -> - ctx.fmt.extract_binop - (extract_texpression ctx fmt) - fmt inside binop int_ty arg0 arg1 - | Regular (fun_id, rg_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 rg_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) - func.type_params; - (* 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 ")" - | _ -> - raise - (Failure - ("Unreachable:\n" ^ "Function: " ^ show_fun_id func.func - ^ ",\nNumber of arguments: " - ^ string_of_int (List.length args) - ^ ",\nArguments: " - ^ String.concat " " (List.map show_texpression args)))) + | Qualif qualif -> ( + (* Top-level qualifier *) + match qualif.id with + | Func fun_id -> + extract_function_call ctx fmt inside fun_id qualif.type_params args + | AdtCons adt_cons_id -> + extract_adt_cons ctx fmt inside adt_cons_id qualif.type_params args + | Proj proj -> + extract_field_projector ctx fmt inside app proj qualif.type_params + args) | _ -> (* "Regular" expression *) (* Open parentheses *) @@ -970,6 +893,126 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* 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_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 + | Regular (fun_id, rg_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 rg_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 ")" + | _ -> + raise + (Failure + ("Unreachable:\n" ^ "Function: " ^ show_fun_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 false 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 : proj_kind) + (_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; + (* TODO: parentheses: we do something very crude *) + let use_parentheses = not (is_var arg) in + if use_parentheses then F.pp_print_string fmt "("; + (* Extract the expression *) + extract_texpression ctx fmt false 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 parentheses *) + if use_parentheses then F.pp_print_string fmt ")"; + (* 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_lvalue list) (e : texpression) : unit = (* Open a box for the abs expression *) diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 9ba1bba7..3adf4eee 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -507,13 +507,12 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) adt_cons_id.adt_id adt_cons_id.variant_id in ConstStrings.constructor_prefix ^ variant_s - | Proj (ProjField (adt_id, field_id)) -> + | Proj { adt_id; field_id } -> let value_fmt = ast_to_value_formatter fmt in let adt_s = adt_variant_to_string value_fmt adt_id None in let field_s = adt_field_to_string value_fmt adt_id field_id in (* Adopting an F*-like syntax *) ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s - | Proj (ProjTuple field_id) -> "MkTuple?." ^ string_of_int field_id in (* Convert the type instantiation *) let ty_fmt = ast_to_type_formatter fmt in diff --git a/src/Pure.ml b/src/Pure.ml index 2f6ddf0a..243b493e 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -363,8 +363,12 @@ type adt_cons_id = { adt_id : type_id; variant_id : variant_id option } [@@deriving show] (** An identifier for an ADT constructor *) -type proj_kind = ProjField of type_id * FieldId.id | ProjTuple of int -[@@deriving show] +type proj_kind = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] +(** Projection kind - For now we don't support projection of tuple fields + (because not all the backends have syntax for this). + + TODO: rename + *) type qualif_id = | Func of fun_id diff --git a/src/PureUtils.ml b/src/PureUtils.ml index b6676db4..aaae94ca 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -341,7 +341,7 @@ let mk_simpl_tuple_ty (tys : ty list) : ty = (** TODO: rename to "mk_..." *) let unit_ty : ty = Adt (Tuple, []) -(** TODO: rename to "mk_..." *) +(** TODO: rename to "mk_unit_texpression" *) let unit_rvalue : texpression = let id = AdtCons { adt_id = Tuple; variant_id = None } in let qualif = { id; type_params = [] } in @@ -592,24 +592,17 @@ module TypeCheck = struct | Qualif qualif -> ( match qualif.id with | Func _ -> () (* TODO *) - | Proj (ProjField (type_id, field_id)) -> - (* Note we can only project fields of structurs (not enumerations) *) + | Proj { adt_id; field_id } -> + (* Note we can only project fields of structures (not enumerations) *) let variant_id = None in let expected_field_tys = - get_adt_field_types ctx.type_decls type_id variant_id + get_adt_field_types ctx.type_decls adt_id variant_id qualif.type_params in let expected_field_ty = FieldId.nth expected_field_tys field_id in let _adt_ty, field_ty = destruct_arrow e.ty in (* TODO: check the adt_ty *) assert (expected_field_ty = field_ty) - | Proj (ProjTuple field_id) -> ( - let tuple_ty, field_ty = destruct_arrow e.ty in - match tuple_ty with - | Adt (Tuple, tys) -> - let expected_field_ty = List.nth tys field_id in - assert (field_ty = expected_field_ty) - | _ -> raise (Failure "Inconsistently typed projector")) | AdtCons id -> (* TODO: we might also want to check the out type *) let expected_field_tys = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 1150f80c..3a61784c 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1408,7 +1408,7 @@ and translate_expansion (config : config) (p : S.mplace option) in let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression = - let proj_kind = ProjField (adt_id, field_id) in + let proj_kind = { adt_id; field_id } in let qualif = { id = Proj proj_kind; type_params } in let proj_e = Qualif qualif in let proj_ty = mk_arrow scrutinee.ty dest.ty in -- cgit v1.2.3