diff options
author | Son Ho | 2023-12-07 12:07:39 +0100 |
---|---|---|
committer | Son Ho | 2023-12-07 12:07:39 +0100 |
commit | 0209fee47a11b371d258fe02b8cc59b325de21d6 (patch) | |
tree | 9e23c2618c7138a02be28310eb8deaac2b4b3c5c /compiler/ExtractBase.ml | |
parent | eb05c2e3b63377c323c33c1296495baa9357596a (diff) |
Use a better syntax when extracting tuple types (structures with unnamed fields)
Diffstat (limited to '')
-rw-r--r-- | compiler/ExtractBase.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 43658b6e..93204515 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -109,7 +109,7 @@ let decl_is_first_from_group (kind : decl_kind) : bool = let decl_is_not_last_from_group (kind : decl_kind) : bool = not (decl_is_last_from_group kind) -type type_decl_kind = Enum | Struct [@@deriving show] +type type_decl_kind = Enum | Struct | Tuple [@@deriving show] (** We use identifiers to look for name clashes *) type id = @@ -1194,12 +1194,13 @@ let type_decl_kind_to_qualif (kind : decl_kind) | Declared -> Some "val") | Coq -> ( match (kind, type_kind) with + | SingleNonRec, Some Tuple -> Some "Definition" | SingleNonRec, Some Enum -> Some "Inductive" | SingleNonRec, Some Struct -> Some "Record" | (SingleRec | MutRecFirst), Some _ -> Some "Inductive" | (MutRecInner | MutRecLast), Some _ -> (* Coq doesn't support groups of mutually recursive definitions which mix - * records and inducties: we convert everything to records if this happens + * records and inductives: we convert everything to records if this happens *) Some "with" | (Assumed | Declared), None -> Some "Axiom" @@ -1214,12 +1215,12 @@ let type_decl_kind_to_qualif (kind : decl_kind) ^ ")"))) | Lean -> ( match kind with - | SingleNonRec -> - if type_kind = Some Struct then Some "structure" else Some "inductive" - | SingleRec -> Some "inductive" - | MutRecFirst -> Some "inductive" - | MutRecInner -> Some "inductive" - | MutRecLast -> Some "inductive" + | SingleNonRec -> ( + match type_kind with + | Some Tuple -> Some "def" + | Some Struct -> Some "structure" + | _ -> Some "inductive") + | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> Some "inductive" | Assumed -> Some "axiom" | Declared -> Some "axiom") | HOL4 -> None |