diff options
-rw-r--r-- | pretyping/evarconv.mli | 36 |
1 files changed, 26 insertions, 10 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9d0c79143..655dc1c1a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -15,8 +15,12 @@ open Reductionops open Evd open Locus +(** Unification for type inference. } *) + exception UnableToUnify of evar_map * Pretype_errors.unification_error +(** {6 Main unification algorithm for type inference. } *) + (** returns exception NotUnifiable with best known evar_map if not unifiable *) val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map @@ -26,25 +30,37 @@ val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_ma val e_conv : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool -(**/**) -(* For debugging *) -val evar_conv_x : transparent_state -> - env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result -val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state -> - env -> evar_map -> - conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> - Evarsolve.unification_result -(**/**) +(** {6 Unification heuristics. } *) + +(** Try heuristics to solve pending unification problems and to solve + evars with candidates *) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map +(** Check if a canonical structure is applicable *) + val check_conv_record : constr * types stack -> constr * types stack -> constr * constr list * (constr list * constr list) * (constr list * types list) * (constr stack * types stack) * constr * (int * constr) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +(** Try to solve problems of the form ?x[args] = c by second-order + matching, using typing to select occurrences *) val second_order_matching : transparent_state -> env -> evar_map -> existential -> occurrences option list -> constr -> evar_map * bool + +(** Declare function to enforce evars resolution by using typing constraints *) + +val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit + +(**/**) +(* For debugging *) +val evar_conv_x : transparent_state -> + env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result +val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state -> + env -> evar_map -> + conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> + Evarsolve.unification_result +(**/**) |