diff options
Diffstat (limited to 'compiler/Pure.ml')
| -rw-r--r-- | compiler/Pure.ml | 292 |
1 files changed, 245 insertions, 47 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index ac4ca081..0ae83007 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1,6 +1,4 @@ open Identifiers -open Names -module PV = PrimitiveValues module T = Types module V = Values module E = Expressions @@ -13,6 +11,10 @@ module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId module FunDeclId = A.FunDeclId module GlobalDeclId = A.GlobalDeclId +module TraitDeclId = T.TraitDeclId +module TraitImplId = T.TraitImplId +module TraitClauseId = T.TraitClauseId +module Disambiguator = T.Disambiguator (** We redefine identifiers for loop: in {!Values}, the identifiers are global (they monotonically increase across functions) while in {!module:Pure} we want @@ -21,8 +23,6 @@ module GlobalDeclId = A.GlobalDeclId module LoopId = IdGen () -type loop_id = LoopId.id [@@deriving show, ord] - (** We give an identifier to every phase of the synthesis (forward, backward for group of regions 0, etc.) *) module SynthPhaseId = @@ -34,9 +34,24 @@ IdGen () module ConstGenericVarId = T.ConstGenericVarId +type llbc_name = T.name [@@deriving show, ord] type integer_type = T.integer_type [@@deriving show, ord] type const_generic_var = T.const_generic_var [@@deriving show, ord] type const_generic = T.const_generic [@@deriving show, ord] +type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord] +type trait_decl_id = T.trait_decl_id [@@deriving show, ord] +type trait_impl_id = T.trait_impl_id [@@deriving show, ord] +type trait_clause_id = T.trait_clause_id [@@deriving show, ord] +type trait_item_name = T.trait_item_name [@@deriving show, ord] +type global_decl_id = T.global_decl_id [@@deriving show, ord] +type fun_decl_id = A.fun_decl_id [@@deriving show, ord] +type loop_id = LoopId.id [@@deriving show, ord] +type region_group_id = T.region_group_id [@@deriving show, ord] +type mutability = Mut | Const [@@deriving show, ord] +type loc = Meta.loc [@@deriving show, ord] +type file_name = Meta.file_name [@@deriving show, ord] +type span = Meta.span [@@deriving show, ord] +type meta = Meta.meta [@@deriving show, ord] (** The assumed types for the pure AST. @@ -53,18 +68,25 @@ type const_generic = T.const_generic [@@deriving show, ord] - [State]: the type of the state, when using state-error monads. Note that this state is opaque to Aeneas (the user can define it, or leave it as assumed) + + TODO: add a prefix "T" *) type assumed_ty = - | State - | Result - | Error - | Fuel - | Vec - | Option - | Array - | Slice - | Str - | Range + | TState + | TResult + | TError + | TFuel + | TArray + | TSlice + | TStr + | TRawPtr of mutability + (** The bool + Raw pointers don't make sense in the pure world, but we don't know + how to translate them yet and we have to handle some functions which + use raw pointers in their signature (for instance some trait declarations + for the slices). For now, we use a dedicated type to "mark" the raw pointers, + and make sure that those functions are actually not used in the translation. + *) [@@deriving show, ord] (* TODO: we should never directly manipulate [Return] and [Fail], but rather @@ -128,7 +150,7 @@ class virtual ['self] mapreduce_type_id_base = fun _ x -> (x, self#zero) end -type type_id = AdtId of type_decl_id | Tuple | Assumed of assumed_ty +type type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty [@@deriving show, ord, @@ -174,8 +196,15 @@ class ['self] iter_ty_base = object (_self : 'self) inherit [_] iter_type_id inherit! [_] T.iter_const_generic - inherit! [_] PV.iter_literal_type method visit_type_var_id : 'env -> type_var_id -> unit = fun _ _ -> () + method visit_trait_decl_id : 'env -> trait_decl_id -> unit = fun _ _ -> () + method visit_trait_impl_id : 'env -> trait_impl_id -> unit = fun _ _ -> () + + method visit_trait_clause_id : 'env -> trait_clause_id -> unit = + fun _ _ -> () + + method visit_trait_item_name : 'env -> trait_item_name -> unit = + fun _ _ -> () end (** Ancestor for map visitor for [ty] *) @@ -183,8 +212,19 @@ class ['self] map_ty_base = object (_self : 'self) inherit [_] map_type_id inherit! [_] T.map_const_generic - inherit! [_] PV.map_literal_type method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x + + method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id = + fun _ x -> x + + method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id = + fun _ x -> x + + method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id = + fun _ x -> x + + method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name = + fun _ x -> x end (** Ancestor for reduce visitor for [ty] *) @@ -192,8 +232,19 @@ class virtual ['self] reduce_ty_base = object (self : 'self) inherit [_] reduce_type_id inherit! [_] T.reduce_const_generic - inherit! [_] PV.reduce_literal_type method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero + + method visit_trait_decl_id : 'env -> trait_decl_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_impl_id : 'env -> trait_impl_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_clause_id : 'env -> trait_clause_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_item_name : 'env -> trait_item_name -> 'a = + fun _ _ -> self#zero end (** Ancestor for mapreduce visitor for [ty] *) @@ -201,26 +252,69 @@ class virtual ['self] mapreduce_ty_base = object (self : 'self) inherit [_] mapreduce_type_id inherit! [_] T.mapreduce_const_generic - inherit! [_] PV.mapreduce_literal_type method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a = fun _ x -> (x, self#zero) + + method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_clause_id + : 'env -> trait_clause_id -> trait_clause_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_item_name + : 'env -> trait_item_name -> trait_item_name * 'a = + fun _ x -> (x, self#zero) end type ty = - | Adt of type_id * ty list * const_generic list - (** {!Adt} encodes ADTs and tuples and assumed types. + | TAdt of type_id * generic_args + (** {!TAdt} encodes ADTs and tuples and assumed types. TODO: what about the ended regions? (ADTs may be parameterized with several region variables. When giving back an ADT value, we may be able to only give back part of the ADT. We need a way to encode such "partial" ADTs. *) - | TypeVar of type_var_id - | Literal of literal_type - | Arrow of ty * ty + | TVar of type_var_id + | TLiteral of literal_type + | TArrow of ty * ty + | TTraitType of trait_ref * generic_args * string + (** The string is for the name of the associated type *) + +and trait_ref = { + trait_id : trait_instance_id; + generics : generic_args; + trait_decl_ref : trait_decl_ref; +} + +and trait_decl_ref = { + trait_decl_id : trait_decl_id; + decl_generics : generic_args; (* The name: annoying field collisions... *) +} + +and generic_args = { + types : ty list; + const_generics : const_generic list; + trait_refs : trait_ref list; +} + +and trait_instance_id = + | Self + | TraitImpl of trait_impl_id + | Clause of trait_clause_id + | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id + | ItemClause of + trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id + | TraitRef of trait_ref + | UnknownTrait of string [@@deriving show, + ord, visitors { name = "iter_ty"; @@ -264,12 +358,51 @@ type type_decl_kind = Struct of field list | Enum of variant list | Opaque type type_var = T.type_var [@@deriving show] +type trait_clause = { + clause_id : trait_clause_id; + trait_id : trait_decl_id; + generics : generic_args; +} +[@@deriving show] + +type generic_params = { + types : type_var list; + const_generics : const_generic_var list; + trait_clauses : trait_clause list; +} +[@@deriving show] + +type trait_type_constraint = { + trait_ref : trait_ref; + generics : generic_args; + type_name : trait_item_name; + ty : ty; +} +[@@deriving show, ord] + +type predicates = { trait_type_constraints : trait_type_constraint list } +[@@deriving show] + type type_decl = { def_id : TypeDeclId.id; - name : name; - type_params : type_var list; - const_generic_params : const_generic_var list; + is_local : bool; + llbc_name : llbc_name; + (** The original name coming from the LLBC declaration *) + name : string; + (** We use the name only for printing purposes (for debugging): + the name used at extraction time will be derived from the + llbc_name. + *) + meta : meta; + generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) kind : type_decl_kind; + preds : predicates; } [@@deriving show] @@ -420,8 +553,15 @@ type pure_assumed_fun_id = | FuelEqZero (** Test if some fuel is equal to 0 - TODO: ugly *) [@@deriving show, ord] +type fun_id_or_trait_method_ref = + | FunId of A.fun_id + | TraitMethod of trait_ref * string * fun_decl_id + (** The fun decl id is not really needed and here for convenience purposes *) +[@@deriving show, ord] + (** A function id for a non-assumed function *) -type regular_fun_id = A.fun_id * LoopId.id option * T.RegionGroupId.id option +type regular_fun_id = + fun_id_or_trait_method_ref * LoopId.id option * T.RegionGroupId.id option [@@deriving show, ord] (** A function identifier *) @@ -457,23 +597,20 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] type qualif_id = | FunOrOp of fun_or_op_id (** A function or an operation *) - | Global of GlobalDeclId.id + | Global of global_decl_id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) + | TraitConst of trait_ref * generic_args * string + (** A trait associated constant *) [@@deriving show] -(** An instantiated qualified. +(** An instantiated qualifier. Note that for now we have a clear separation between types and expressions, - which explains why we have the [type_params] field: a function or ADT + which explains why we have the [generics] field: a function or ADT constructor is always fully instantiated. *) -type qualif = { - id : qualif_id; - type_args : ty list; - const_generic_args : const_generic list; -} -[@@deriving show] +type qualif = { id : qualif_id; generics : generic_args } [@@deriving show] type field_id = FieldId.id [@@deriving show, ord] type var_id = VarId.id [@@deriving show, ord] @@ -536,6 +673,7 @@ class virtual ['self] mapreduce_expression_base = *) type expression = | Var of var_id (** a variable *) + | CVar of const_generic_var_id (** a const generic var *) | Const of literal | App of texpression * texpression (** Application of a function to an argument. @@ -590,7 +728,7 @@ type expression = | Switch of texpression * switch_body | Loop of loop (** See the comments for {!loop} *) | StructUpdate of struct_update (** See the comments for {!struct_update} *) - | Meta of (meta[@opaque]) * texpression (** Meta-information *) + | Meta of (emeta[@opaque]) * texpression (** Meta-information *) and switch_body = If of texpression * texpression | Match of match_branch list and match_branch = { pat : typed_pattern; branch : texpression } @@ -609,6 +747,7 @@ and match_branch = { pat : typed_pattern; branch : texpression } and loop = { fun_end : texpression; loop_id : loop_id; + meta : meta; [@opaque] fuel0 : var_id; fuel : var_id; input_state : var_id option; @@ -664,7 +803,7 @@ and texpression = { e : expression; ty : ty } and mvalue = (texpression[@opaque]) (** Meta-information stored in the AST *) -and meta = +and emeta = | Assignment of mplace * mvalue * mplace option (** Information about an assignment which occured in LLBC. We use this to guide the heuristics which derive pretty names. @@ -787,11 +926,17 @@ type fun_sig_info = { - etc. *) type fun_sig = { - type_params : type_var list; - const_generic_params : const_generic_var list; + generics : generic_params; (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *) + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) + preds : predicates; inputs : ty list; - (** The input types. + (** The types of the inputs. Note that those input types take into account the [fuel] parameter, if the function uses fuel for termination, and the [state] parameter, @@ -861,8 +1006,13 @@ type fun_body = { } [@@deriving show] +type fun_kind = A.fun_kind [@@deriving show] + type fun_decl = { def_id : FunDeclId.id; + is_local : bool; + meta : meta; + kind : fun_kind; num_loops : int; (** The number of loops in the parent forward function (basically the number of loops appearing in the original Rust functions, unless some loops are @@ -871,14 +1021,62 @@ type fun_decl = { loop_id : LoopId.id option; (** [Some] if this definition was generated for a loop *) back_id : T.RegionGroupId.id option; - basename : fun_name; - (** The "base" name of the function. - - The base name is the original name of the Rust function. We add suffixes - (to identify the forward/backward functions) later. + llbc_name : llbc_name; (** The original LLBC name. *) + name : string; + (** We use the name only for printing purposes (for debugging): + the name used at extraction time will be derived from the + llbc_name. *) signature : fun_sig; is_global_decl_body : bool; body : fun_body option; } [@@deriving show] + +type trait_decl = { + def_id : trait_decl_id; + is_local : bool; + llbc_name : llbc_name; + name : string; + meta : meta; + generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) + preds : predicates; + parent_clauses : trait_clause list; + llbc_parent_clauses : Types.trait_clause list; + consts : (trait_item_name * (ty * global_decl_id option)) list; + types : (trait_item_name * (trait_clause list * ty option)) list; + required_methods : (trait_item_name * fun_decl_id) list; + provided_methods : (trait_item_name * fun_decl_id option) list; +} +[@@deriving show] + +type trait_impl = { + def_id : trait_impl_id; + is_local : bool; + llbc_name : llbc_name; + name : string; + meta : meta; + impl_trait : trait_decl_ref; + llbc_impl_trait : Types.trait_decl_ref; + (** Same remark as for {!field:llbc_generics}. *) + generics : generic_params; + llbc_generics : Types.generic_params; + (** We use the LLBC generics to generate "pretty" names, for instance + for the variables we introduce for the trait clauses: we derive + those names from the types, and when doing so it is more meaningful + to derive them from the original LLBC types from before the + simplification of types like boxes and references. *) + preds : predicates; + parent_trait_refs : trait_ref list; + consts : (trait_item_name * (ty * global_decl_id)) list; + types : (trait_item_name * (trait_ref list * ty)) list; + required_methods : (trait_item_name * fun_decl_id) list; + provided_methods : (trait_item_name * fun_decl_id) list; +} +[@@deriving show] |