Update some assumed type names/variants

2 files changed, 41 insertions, 34 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c8c16c08..a4319482 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -173,12 +173,7 @@ let extract_adt_g_value
          *)
         let cons =
           match variant_id with
-          | Some vid -> (
-              (* In the case of Lean, we might have to add the type name as a prefix *)
-              match (!backend, adt_id) with
-              | Lean, TAssumed _ ->
-                  ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
-              | _ -> ctx_get_variant adt_id vid ctx)
+          | Some vid -> ctx_get_variant adt_id vid ctx
           | None -> ctx_get_struct adt_id ctx
         in
         let use_parentheses = inside && field_values <> [] in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index dffe1ea3..b7fa7788 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -960,31 +960,40 @@ let keywords () =
   List.concat [ named_unops; named_binops; misc ]
 
 let assumed_adts () : (assumed_ty * string) list =
-  match !backend with
-  | Lean ->
-      [
-        (TState, "State");
-        (TResult, "Result");
-        (TError, "Error");
-        (TFuel, "Nat");
-        (TArray, "Array");
-        (TSlice, "Slice");
-        (TStr, "Str");
-        (TRawPtr Mut, "MutRawPtr");
-        (TRawPtr Const, "ConstRawPtr");
-      ]
-  | Coq | FStar | HOL4 ->
-      [
-        (TState, "state");
-        (TResult, "result");
-        (TError, "error");
-        (TFuel, if !backend = HOL4 then "num" else "nat");
-        (TArray, "array");
-        (TSlice, "slice");
-        (TStr, "str");
-        (TRawPtr Mut, "mut_raw_ptr");
-        (TRawPtr Const, "const_raw_ptr");
-      ]
+  let state =
+    if !use_state then
+      match !backend with
+      | Lean -> [ (TState, "State") ]
+      | Coq | FStar | HOL4 -> [ (TState, "state") ]
+    else []
+  in
+  (* We voluntarily omit the type [Error]: it is never directly
+     referenced in the generated translation, and easily collides
+     with user-defined types *)
+  let adts =
+    match !backend with
+    | Lean ->
+        [
+          (TResult, "Result");
+          (TFuel, "Nat");
+          (TArray, "Array");
+          (TSlice, "Slice");
+          (TStr, "Str");
+          (TRawPtr Mut, "MutRawPtr");
+          (TRawPtr Const, "ConstRawPtr");
+        ]
+    | Coq | FStar | HOL4 ->
+        [
+          (TResult, "result");
+          (TFuel, if !backend = HOL4 then "num" else "nat");
+          (TArray, "array");
+          (TSlice, "slice");
+          (TStr, "str");
+          (TRawPtr Mut, "mut_raw_ptr");
+          (TRawPtr Const, "const_raw_ptr");
+        ]
+  in
+  state @ adts
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
@@ -1015,9 +1024,12 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Lean ->
       [
-        (TResult, result_return_id, "ret");
-        (TResult, result_fail_id, "fail");
-        (TError, error_failure_id, "panic");
+        (TResult, result_return_id, "Result.ret");
+        (TResult, result_fail_id, "Result.fail");
+        (* For panic: we omit the prefix "Error." because the type is always
+           clear from the context. Also, "Error" is often used by user-defined
+           types (when we omit the crate as a prefix). *)
+        (TError, error_failure_id, ".panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]