Make more updates to Charon-ML

AeneasVerif · Nov 16, 2023 · 1c2d2da · 1c2d2da
1 parent ea97c19
commit 1c2d2da
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 15 deletions.
diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml
@@ -166,7 +166,7 @@ type trait_impl = {
 }
 [@@deriving show]
 
-type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
+type 'id g_declaration_group = NonRecGroup of 'id | RecGroup of 'id list
 [@@deriving show]
 
 type type_declaration_group = TypeDeclId.id g_declaration_group

diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
@@ -1165,10 +1165,10 @@ let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
     (match js with
     | `Assoc [ ("NonRec", id) ] ->
         let* id = id_of_json id in
-        Ok (NonRec id)
+        Ok (NonRecGroup id)
     | `Assoc [ ("Rec", ids) ] ->
         let* ids = list_of_json id_of_json ids in
-        Ok (Rec ids)
+        Ok (RecGroup ids)
     | _ -> Error "")
 
 let type_declaration_group_of_json (js : json) :
@@ -1186,24 +1186,24 @@ let global_declaration_group_of_json (js : json) :
   combine_error_msgs js __FUNCTION__
     (let* decl = g_declaration_group_of_json GlobalDeclId.id_of_json js in
      match decl with
-     | NonRec id -> Ok id
-     | Rec _ -> Error "got mutually dependent globals")
+     | NonRecGroup id -> Ok id
+     | RecGroup _ -> Error "got mutually dependent globals")
 
 let trait_declaration_group_of_json (js : json) :
     (TraitDeclId.id, string) result =
   combine_error_msgs js __FUNCTION__
     (let* decl = g_declaration_group_of_json TraitDeclId.id_of_json js in
      match decl with
-     | NonRec id -> Ok id
-     | Rec _ -> Error "got mutually dependent trait decls")
+     | NonRecGroup id -> Ok id
+     | RecGroup _ -> Error "got mutually dependent trait decls")
 
 let trait_implementation_group_of_json (js : json) :
     (TraitImplId.id, string) result =
   combine_error_msgs js __FUNCTION__
     (let* decl = g_declaration_group_of_json TraitImplId.id_of_json js in
      match decl with
-     | NonRec id -> Ok id
-     | Rec _ -> Error "got mutually dependent trait impls")
+     | NonRecGroup id -> Ok id
+     | RecGroup _ -> Error "got mutually dependent trait impls")
 
 let declaration_group_of_json (js : json) : (declaration_group, string) result =
   combine_error_msgs js __FUNCTION__

diff --git a/charon-ml/src/GAstUtils.ml b/charon-ml/src/GAstUtils.ml
@@ -80,8 +80,9 @@ let split_declarations_to_group_maps (decls : declaration_group list) :
     let add_group (map : M.key g_declaration_group M.t)
         (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
       match group with
-      | NonRec id -> M.add id group map
-      | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
+      | NonRecGroup id -> M.add id group map
+      | RecGroup ids ->
+          List.fold_left (fun map id -> M.add id group map) map ids
 
     let create_map (groups : M.key g_declaration_group list) :
         M.key g_declaration_group M.t =

diff --git a/charon-ml/src/LlbcAstUtils.ml b/charon-ml/src/LlbcAstUtils.ml
@@ -71,8 +71,9 @@ let compute_fun_decl_groups_map (c : crate) : FunDeclId.Set.t FunDeclId.Map.t =
     (List.flatten
        (List.filter_map
           (function
-            | FunGroup (NonRec id) -> Some [ (id, FunDeclId.Set.singleton id) ]
-            | FunGroup (Rec ids) ->
+            | FunGroup (NonRecGroup id) ->
+                Some [ (id, FunDeclId.Set.singleton id) ]
+            | FunGroup (RecGroup ids) ->
                 let idset = FunDeclId.Set.of_list ids in
                 Some (List.map (fun id -> (id, idset)) ids)
             | TypeGroup _ | GlobalGroup _ | TraitDeclGroup _ | TraitImplGroup _

diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml
@@ -4,7 +4,6 @@ open Types
 open Expressions
 open LlbcAst
 open PrintUtils
-open PrintPrimitiveValues
 open PrintTypes
 
 let var_id_to_pretty_string (id : var_id) : string = "v@" ^ VarId.to_string id

diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml
@@ -1,8 +1,8 @@
 (** Pretty-printing for types *)
 
+include PrintPrimitiveValues
 open Types
 open TypesUtils
-open PrintPrimitiveValues
 open GAst
 open PrintUtils
 

diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml
@@ -17,6 +17,9 @@ module RegionSet = Collections.MakeSet (RegionOrderedType)
 let to_name (ls : string list) : name =
   List.map (fun s -> PeIdent (s, Disambiguator.zero)) ls
 
+let as_ident (e : path_elem) : string =
+  match e with PeIdent (s, _) -> s | _ -> raise (Failure "Unexpected")
+
 let type_decl_is_opaque (d : type_decl) : bool =
   match d.kind with Struct _ | Enum _ -> false | Opaque -> true