diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | compiler/Extract.ml | 37 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 75 | ||||
| -rw-r--r-- | compiler/Pure.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 3 |
5 files changed, 68 insertions, 58 deletions
@@ -91,7 +91,7 @@ tests: trans-no_nested_borrows trans-paper \ transp-polonius_list transp-betree_main \ test-transp-betree_main \ trans-loops \ - trans-array # TODO: generalize to all backends + trans-array trans-traits # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -131,6 +131,14 @@ tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += +trans-traits: OPTIONS += -no-state +trans-traits: SUBDIR := traits +tfstar-traits: OPTIONS += -decreases-clauses -template-clauses +tcoq-traits: OPTIONS += -use-fuel +tlean-traits: SUBDIR := +tlean-traits: OPTIONS += +thol4-traits: OPTIONS += + # TODO: activate the arrays for all the backends thol4-array: echo "Ignoring the array test for HOL4" diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 574602c7..a73bf0fd 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1808,7 +1808,6 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) (trait_decl : trait_decl) (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) : extraction_ctx = - let generics = trait_decl.generics in (* Compute the clause names *) let clause_names = match builtin_info with @@ -1822,11 +1821,11 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) else ctx.fmt.trait_decl_name trait_decl ^ name in (c.clause_id, name)) - generics.trait_clauses + trait_decl.parent_clauses | Some info -> List.map (fun (c, name) -> (c.clause_id, name)) - (List.combine generics.trait_clauses info.parent_clauses) + (List.combine trait_decl.parent_clauses info.parent_clauses) in (* Register the names *) List.fold_left @@ -2113,12 +2112,15 @@ let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter) extract_trait_item ctx fmt item_name assign ty (** Small helper - TODO: move *) -let generic_params_drop_prefix (g1 : generic_params) (g2 : generic_params) : - generic_params = +let generic_params_drop_prefix ~(drop_trait_clauses : bool) + (g1 : generic_params) (g2 : generic_params) : generic_params = let open Collections.List in let types = drop (length g1.types) g2.types in let const_generics = drop (length g1.const_generics) g2.const_generics in - let trait_clauses = drop (length g1.trait_clauses) g2.trait_clauses in + let trait_clauses = + if drop_trait_clauses then drop (length g1.trait_clauses) g2.trait_clauses + else g2.trait_clauses + in { types; const_generics; trait_clauses } (** Small helper. @@ -2139,7 +2141,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) (* We need to add the generics specific to the method, by removing those which actually apply to the trait decl *) let generics = - generic_params_drop_prefix decl.generics f.signature.generics + let drop_trait_clauses = false in + generic_params_drop_prefix ~drop_trait_clauses decl.generics + f.signature.generics in let ctx, type_params, cg_params, trait_clauses = ctx_add_generic_params generics ctx @@ -2189,8 +2193,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt decl_name; (* Print the generics *) - (* We ignore the trait clauses, which we extract as *fields* *) - let generics = { decl.generics with trait_clauses = [] } in + let generics = decl.generics in (* Add the type and const generic params - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, type_params, cg_params, trait_clauses = @@ -2199,17 +2202,6 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params cg_params trait_clauses; - (* Add the parent clauses as local clauses, so that we can refer to them *) - let ctx = - List.fold_left - (fun ctx clause -> - let item_name = - ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx - in - ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx) - ctx decl.generics.trait_clauses - in - F.pp_print_space fmt (); (match !backend with | Lean -> F.pp_print_string fmt "where" @@ -2233,7 +2225,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause in extract_trait_decl_item ctx fmt item_name ty) - decl.generics.trait_clauses; + decl.parent_clauses; (* The constants *) List.iter @@ -2330,7 +2322,8 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) are specific to the method, and call it will all the generics (trait impl + method generics) *) let f_generics = - generic_params_drop_prefix + let drop_trait_clauses = true in + generic_params_drop_prefix ~drop_trait_clauses { impl.generics with types = impl_types } f_generics in diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 688ed352..56290ab4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1239,42 +1239,45 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" - | TraitType (trait_ref, generics, type_name) -> + | TraitType (trait_ref, generics, type_name) -> ( if !parameterize_trait_types then raise (Failure "Unimplemented") - else if trait_ref.trait_id <> Self then ( - (* HOL4 doesn't have 1st class types *) - assert (!backend <> HOL4); - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; - extract_trait_ref ctx fmt no_params_tys false trait_ref; - extract_generic_args ctx fmt no_params_tys generics; - let name = - ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name - ctx - in - if use_brackets then F.pp_print_string fmt ")"; - F.pp_print_string fmt ("." ^ name)) else - (* There are two situations: - - we are extracting a declared item (typically a function signature) - for a trait declaration. We directly refer to the item (we extract - trait declarations as structures, so we can refer to their fields) - - we are extracting a provided method for a trait declaration. We - refer to the item in the self trait clause (see {!SelfTraitClauseId}). - - Remark: we can't get there for trait *implementations* because then the - types should have been normalized. - *) - let trait_decl_id = Option.get ctx.trait_decl_id in - let item_name = ctx_get_trait_type trait_decl_id type_name ctx in - assert (generics = empty_generic_args); - if ctx.is_provided_method then - (* Provided method: use the trait self clause *) - let self_clause = ctx_get_trait_self_clause ctx in - F.pp_print_string fmt (self_clause ^ "." ^ item_name) - else - (* Declaration: directly refer to the item *) - F.pp_print_string fmt item_name + (* There may be a special treatment depending on the instance id *) + match trait_ref.trait_id with + | Self -> + (* There are two situations: + - we are extracting a declared item (typically a function signature) + for a trait declaration. We directly refer to the item (we extract + trait declarations as structures, so we can refer to their fields) + - we are extracting a provided method for a trait declaration. We + refer to the item in the self trait clause (see {!SelfTraitClauseId}). + + Remark: we can't get there for trait *implementations* because then the + types should have been normalized. + *) + let trait_decl_id = Option.get ctx.trait_decl_id in + let item_name = ctx_get_trait_type trait_decl_id type_name ctx in + assert (generics = empty_generic_args); + if ctx.is_provided_method then + (* Provided method: use the trait self clause *) + let self_clause = ctx_get_trait_self_clause ctx in + F.pp_print_string fmt (self_clause ^ "." ^ item_name) + else + (* Declaration: directly refer to the item *) + F.pp_print_string fmt item_name + | _ -> + (* HOL4 doesn't have 1st class types *) + assert (!backend <> HOL4); + let use_brackets = generics <> empty_generic_args in + if use_brackets then F.pp_print_string fmt "("; + extract_trait_ref ctx fmt no_params_tys false trait_ref; + extract_generic_args ctx fmt no_params_tys generics; + let name = + ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id + type_name ctx + in + if use_brackets then F.pp_print_string fmt ")"; + F.pp_print_string fmt ("." ^ name)) and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_ref) : unit = @@ -1342,7 +1345,9 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter) | Self -> (* This has specific treatment depending on the item we're extracting (associated type, etc.). We should have caught this elsewhere. *) - raise (Failure "Unexpected") + if !Config.extract_fail_hard then + raise (Failure "Unexpected occurrence of `Self`") + else F.pp_print_string fmt "ERROR(\"Unexpected Self\")" | TraitImpl id -> let name = ctx_get_trait_impl id ctx in F.pp_print_string fmt name diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 70653e57..c33a745c 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1013,6 +1013,7 @@ type trait_decl = { name : name; generics : generic_params; preds : predicates; + parent_clauses : trait_clause list; consts : (trait_item_name * (ty * global_decl_id option)) list; types : (trait_item_name * (trait_clause list * ty option)) list; required_methods : (trait_item_name * fun_decl_id) list; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index c629a96f..46aa3b83 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3096,6 +3096,7 @@ let translate_trait_decl (type_infos : TA.type_infos) name; generics; preds; + parent_clauses; consts; types; required_methods; @@ -3105,6 +3106,7 @@ let translate_trait_decl (type_infos : TA.type_infos) in let generics = translate_generic_params generics in let preds = translate_predicates preds in + let parent_clauses = List.map translate_trait_clause parent_clauses in let consts = List.map (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) @@ -3123,6 +3125,7 @@ let translate_trait_decl (type_infos : TA.type_infos) name; generics; preds; + parent_clauses; consts; types; required_methods; |