summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-24 17:22:33 +0100
committerSon Ho2023-11-24 17:22:33 +0100
commitfeb10e653131716698205f0b77b9623cdd1712b0 (patch)
tree174d6c220d352981604d6ca6e61aef4d2489f6d2
parent5b9f8de676829817d2b776166fda66bfb5128d6c (diff)
Update some assumed type names/variants
-rw-r--r--compiler/Extract.ml7
-rw-r--r--compiler/ExtractBase.ml68
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 *)
]