Module MiniSolver (.ml)

module MiniSolver: sig .. end

This module provides a constraint solver based on unification under a mixed prefix.

include Solver.SolverException

type environment

The solver environment.

type tconstraint = (Constraint.crterm, Constraint.variable) Constraint.type_constraint

The constraint to solve.

type solving_step =

`\|`	`Init of tconstraint`
`\|`	`Solve of tconstraint`
`\|`	`Solved of tconstraint`
`\|`	`UnifyTerms of Constraint.crterm * Constraint.crterm`
`\|`	`UnifyVars of Constraint.variable * Constraint.variable`
`\|`	`Generalize of int * Constraint.variable list`

A solving_step describes a elementary step of the solver.

val solve : ?tracer:(solving_step -> unit) ->
       tconstraint -> environment

solve tracer c solves c by doing in-place modifications resulting in a environment.

val environment_as_list : environment -> (string * Constraint.variable) list

environment_as_list env converts env into a list.

val print_env : ?use_user_def:'a ->
       (Constraint.variable -> string) -> environment -> unit

print_env printer env use the printer of variable in order to display env.