diff options
author | Son Ho | 2022-05-01 16:03:40 +0200 |
---|---|---|
committer | Son Ho | 2022-05-01 16:03:40 +0200 |
commit | 3b25cdd34516b1b89f265624003c518922727edc (patch) | |
tree | 0d767f626475541c8b6b1da7d6b92ddb715f1fb0 | |
parent | 5c2ddca25137de0062fc37239f261a6a8187d885 (diff) |
Perform more renamings
-rw-r--r-- | src/ExtractToFStar.ml | 2 | ||||
-rw-r--r-- | src/PrintPure.ml | 8 | ||||
-rw-r--r-- | src/Pure.ml | 14 | ||||
-rw-r--r-- | src/SymbolicToPure.ml | 6 |
4 files changed, 14 insertions, 16 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index e00a4e53..0bcf66bd 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -986,7 +986,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (** 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) + (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` *) diff --git a/src/PrintPure.ml b/src/PrintPure.ml index b29f6e70..2da653bb 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -201,12 +201,12 @@ let var_to_string (fmt : type_formatter) (v : var) : string = let varname = var_to_varname v in "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")" -let rec projection_to_string (fmt : ast_formatter) (inside : string) - (p : projection) : string = +let rec mprojection_to_string (fmt : ast_formatter) (inside : string) + (p : mprojection) : string = match p with | [] -> inside | pe :: p' -> ( - let s = projection_to_string fmt inside p' in + let s = mprojection_to_string fmt inside p' in match pe.pkind with | E.ProjOption variant_id -> assert (variant_id = T.option_some_id); @@ -232,7 +232,7 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = * regular places use indices for the pure variables: we want to make * this explicit, otherwise it is confusing. *) let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in - projection_to_string fmt name p.projection + mprojection_to_string fmt name p.projection let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id) (variant_id : VariantId.id option) : string = diff --git a/src/Pure.ml b/src/Pure.ml index 3798c555..9cf7a077 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -152,15 +152,15 @@ type var = { * Also: tuples... * Rmk: projections are actually only used as meta-data. * *) -type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id } +type mprojection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id } [@@deriving show] -type projection = projection_elem list [@@deriving show] +type mprojection = mprojection_elem list [@@deriving show] type mplace = { var_id : V.VarId.id; name : string option; - projection : projection; + projection : mprojection; } [@@deriving show] (** "Meta" place. @@ -360,17 +360,15 @@ type adt_cons_id = { adt_id : type_id; variant_id : variant_id option } [@@deriving show] (** An identifier for an ADT constructor *) -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 +type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] +(** Projection - 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 | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) - | Proj of proj_kind (** Field projector *) + | Proj of projection (** Field projector *) [@@deriving show] type qualif = { id : qualif_id; type_args : ty list } [@@deriving show] diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 64b3929f..14a844a1 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -808,13 +808,13 @@ let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : texpression list = log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs)); List.filter_map (typed_avalue_to_consumed ctx) abs.avalues -let translate_mprojection_elem (pe : E.projection_elem) : projection_elem option - = +let translate_mprojection_elem (pe : E.projection_elem) : + mprojection_elem option = match pe with | Deref | DerefBox -> None | Field (pkind, field_id) -> Some { pkind; field_id } -let translate_mprojection (p : E.projection) : projection = +let translate_mprojection (p : E.projection) : mprojection = List.filter_map translate_mprojection_elem p (** Translate a "meta"-place *) |