diff options
author | Son Ho | 2023-11-09 16:22:09 +0100 |
---|---|---|
committer | Son Ho | 2023-11-09 16:22:09 +0100 |
commit | 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 (patch) | |
tree | 33a01390332163a14d6d7d5da1ab3d295fccf3a6 /compiler/ExtractBase.ml | |
parent | 9157959cc421c481cf584ada69f51d58da82e8f9 (diff) |
Make the traits work for Coq
Diffstat (limited to '')
-rw-r--r-- | compiler/ExtractBase.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 55b1bca3..31b1a447 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -246,6 +246,7 @@ type formatter = { *) trait_decl_name : trait_decl -> string; trait_impl_name : trait_decl -> trait_impl -> string; + trait_decl_constructor : trait_decl -> string; trait_parent_clause_name : trait_decl -> trait_clause -> string; trait_const_name : trait_decl -> string -> string; trait_type_name : trait_decl -> string -> string; @@ -388,6 +389,7 @@ type id = | TraitDeclId of TraitDeclId.id | TraitImplId of TraitImplId.id | LocalTraitClauseId of TraitClauseId.id + | TraitDeclConstructorId of TraitDeclId.id | TraitMethodId of TraitDeclId.id * string * T.RegionGroupId.id option (** Something peculiar with trait methods: because we have to take into account forward/backward functions, we may need to generate fields @@ -801,6 +803,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | TraitImplId id -> "trait_impl_id: " ^ TraitImplId.to_string id | LocalTraitClauseId id -> "local_trait_clause_id: " ^ TraitClauseId.to_string id + | TraitDeclConstructorId id -> + "trait_decl_constructor: " ^ trait_decl_id_to_string id | TraitParentClauseId (id, clause_id) -> "trait_parent_clause_id: " ^ trait_decl_id_to_string id ^ ", clause_id: " ^ TraitClauseId.to_string clause_id @@ -959,6 +963,10 @@ let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string = let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = ctx_get_type (Assumed id) ctx +let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) : + string = + ctx_get (TraitDeclConstructorId id) ctx + let ctx_get_trait_self_clause (ctx : extraction_ctx) : string = ctx_get TraitSelfClauseId ctx |