Move some files to the Charon project

1 files changed, 1 insertions, 189 deletions

diff --git a/compiler/LlbcAst.ml b/compiler/LlbcAst.ml
index 1b08f1ea..f4d26e18 100644
--- a/compiler/LlbcAst.ml
+++ b/compiler/LlbcAst.ml
@@ -1,46 +1,6 @@
-open Names
 open Types
 open Values
-open Expressions
-open Identifiers
-module FunDeclId = IdGen ()
-module GlobalDeclId = IdGen ()
-open Meta
-
-(** A variable, as used in a function definition *)
-type var = {
-  index : VarId.id;  (** Unique variable identifier *)
-  name : string option;
-  var_ty : ety;
-      (** The variable type - erased type, because variables are not used
-       ** in function signatures: they are only used to declare the list of
-       ** variables manipulated by a function body *)
-}
-[@@deriving show]
-
-type assumed_fun_id =
-  | Replace  (** [core::mem::replace] *)
-  | BoxNew
-  | BoxDeref  (** [core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref] *)
-  | BoxDerefMut
-      (** [core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut] *)
-  | BoxFree
-  | VecNew
-  | VecPush
-  | VecInsert
-  | VecLen
-  | VecIndex  (** [core::ops::index::Index::index<alloc::vec::Vec<T>, usize>] *)
-  | VecIndexMut
-      (** [core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>] *)
-[@@deriving show, ord]
-
-type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
-[@@deriving show, ord]
-
-type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
-[@@deriving show]
-
-type assertion = { cond : operand; expected : bool } [@@deriving show]
+include Charon.LlbcAst
 
 type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 [@@deriving show]
@@ -48,17 +8,6 @@ type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
 [@@deriving show]
 
-(** A function signature, as used when declaring functions *)
-type fun_sig = {
-  region_params : region_var list;
-  num_early_bound_regions : int;
-  regions_hierarchy : region_var_groups;
-  type_params : type_var list;
-  inputs : sty list;
-  output : sty;
-}
-[@@deriving show]
-
 (** A function signature, after instantiation *)
 type inst_fun_sig = {
   regions_hierarchy : abs_region_groups;
@@ -66,140 +15,3 @@ type inst_fun_sig = {
   output : rty;
 }
 [@@deriving show]
-
-type call = {
-  func : fun_id;
-  region_args : erased_region list;
-  type_args : ety list;
-  args : operand list;
-  dest : place;
-}
-[@@deriving show]
-
-(** Ancestor for [typed_value] iter visitor *)
-class ['self] iter_statement_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.iter
-
-    method visit_global_assignment : 'env -> global_assignment -> unit =
-      fun _ _ -> ()
-
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
-    method visit_place : 'env -> place -> unit = fun _ _ -> ()
-    method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
-    method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
-    method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
-    method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
-    method visit_call : 'env -> call -> unit = fun _ _ -> ()
-    method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-    method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
-  end
-
-(** Ancestor for [typed_value] map visitor *)
-class ['self] map_statement_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.map
-
-    method visit_global_assignment
-        : 'env -> global_assignment -> global_assignment =
-      fun _ x -> x
-
-    method visit_meta : 'env -> meta -> meta = fun _ x -> x
-    method visit_place : 'env -> place -> place = fun _ x -> x
-    method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
-    method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
-    method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
-    method visit_operand : 'env -> operand -> operand = fun _ x -> x
-    method visit_call : 'env -> call -> call = fun _ x -> x
-
-    method visit_integer_type : 'env -> integer_type -> integer_type =
-      fun _ x -> x
-
-    method visit_scalar_value : 'env -> scalar_value -> scalar_value =
-      fun _ x -> x
-  end
-
-type statement = {
-  meta : meta;  (** The statement meta-data *)
-  content : raw_statement;  (** The statement itself *)
-}
-
-and raw_statement =
-  | Assign of place * rvalue
-  | AssignGlobal of global_assignment
-  | FakeRead of place
-  | SetDiscriminant of place * VariantId.id
-  | Drop of place
-  | Assert of assertion
-  | Call of call
-  | Panic
-  | Return
-  | Break of int
-      (** Break to (outer) loop. The [int] identifies the loop to break to:
-          * 0: break to the first outer loop (the current loop)
-          * 1: break to the second outer loop
-          * ...
-          *)
-  | Continue of int
-      (** Continue to (outer) loop. The loop identifier works
-          the same way as for {!Break} *)
-  | Nop
-  | Sequence of statement * statement
-  | Switch of operand * switch_targets
-  | Loop of statement
-
-and switch_targets =
-  | If of statement * statement  (** Gives the "if" and "else" blocks *)
-  | SwitchInt of integer_type * (scalar_value list * statement) list * statement
-      (** The targets for a switch over an integer are:
-          - the list [(matched values, statement to execute)]
-            We need a list for the matched values in case we do something like this:
-            [switch n { 0 | 1 => ..., _ => ... }]
-          - the "otherwise" statement
-          Also note that we precise the type of the integer (uint32, int64, etc.)
-          which we switch on. *)
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_statement";
-        variety = "iter";
-        ancestors = [ "iter_statement_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_statement";
-        variety = "map";
-        ancestors = [ "map_statement_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
-
-type fun_body = {
-  meta : meta;
-  arg_count : int;
-  locals : var list;
-  body : statement;
-}
-[@@deriving show]
-
-type fun_decl = {
-  def_id : FunDeclId.id;
-  meta : meta;
-  name : fun_name;
-  signature : fun_sig;
-  body : fun_body option;
-  is_global_decl_body : bool;
-}
-[@@deriving show]
-
-type global_decl = {
-  def_id : GlobalDeclId.id;
-  meta : meta;
-  body_id : FunDeclId.id;
-  name : global_name;
-  ty : ety;
-}
-[@@deriving show]