Make.WithItemsmodule I : sig ... endval associated_items_per_roles :
Ast.attrs ->
AST.item Prelude.list AssocRole.Map.tval associated_item : AssocRole.t -> Ast.attrs -> AST.item Prelude.optionval associated_fn :
AssocRole.t ->
Ast.attrs ->
(AST.generics * AST.param Prelude.list * AST.expr) Prelude.optionval associated_expr :
?keep_last_args:Prelude.int ->
AssocRole.t ->
Ast.attrs ->
AST.expr Prelude.optionval associated_items : AssocRole.t -> Ast.attrs -> AST.item Prelude.listval associated_fns :
AssocRole.t ->
Ast.attrs ->
(AST.generics * AST.param Prelude.list * AST.expr) Prelude.listval associated_exprs :
?keep_last_args:Prelude.int ->
AssocRole.t ->
Ast.attrs ->
AST.expr Prelude.listval expect_fn : AST.item -> AST.generics * AST.param Prelude.list * AST.exprval expect_expr :
?keep_last_args:Prelude.int ->
(AST.generics * AST.param Prelude.list * AST.expr) ->
AST.exprval associated_refinement_in_type :
Ast.span ->
Prelude.string Prelude.list ->
Ast.attrs ->
AST.expr Prelude.optionFor type, there is a special treatment. The name of fields are global identifiers, and thus are subject to rewriting by Concrete_ident at the moment of printing. In contrast, in the refinement `fn` item generated by the proc-macros, the arguments are local identifiers, and thus are rewrited in a different manner.
Thus, associated_refinement_in_type takes a list of free_variables: those are already formatted strings as printed by the backend. Then, we rewrite identities in the refinement formula to match exactly this print policy, using *final* local identifiers (see `Local_ident.make_final`).
include sig ... endval find_unique_attr :
Ast.attrs ->
f:(Types.ha_payload -> 'a Prelude.option) ->
'a0 Prelude.optionval status : Ast.attrs -> Types.ha_item_statusval late_skip : Ast.attrs -> Prelude.boolval is_erased : Ast.attrs -> Prelude.boolval uid : Ast.attrs -> UId.t Prelude.optionval lemma : Ast.attrs -> Prelude.boolval raw_associated_item : Ast.attrs -> (AssocRole.t * UId.t) Prelude.list