(** Exemple repris de plzoo/miniprolog *)

(** Syntaxe
    ========
    On souhaite unifier des *termes*, définis comme suit. On introduit des alias
    de types pour distinguer des variables et des constantes. *)

type variable = string

type constant = string

type term =
  | Var of variable (** les variables sont des termes écrits en majuscules, par exemple X *)
  | Const of constant (** les constantes sont des termes écrits en minuscules, par exemple, x *)
  | Compound of constant * term list (** un terme composé est par exemple f(X, y) *)

(** Substitutions
    =============
    On va utiliser des environnements pour dénoter les substitutions voulues.
    Chaque variable à substituer sera associée dans l'environnement au terme qui la
    remplacera.  *)
type env = (string * term) list

(** La fonction suivante permet de regarder le terme associé à une variable dans
    un environnement. Il est possible qu'une variable n'ai pas encore été
    associée à un terme, auquel cas on retourne None (ce que fait directement
    `List.assoc_opt`)  *)

let lookup (env : env) (x : string) : term option =
  List.assoc_opt x env

let rec subst (env : env) (term : term) : term = match term with
  | Var x -> begin match lookup env x with
      | None ->
        (* Il n'y a pas de substitution pour X, on n'a donc rien d'autre à faire *)
        Var x
      | Some term' ->
        (* On a trouvé une substitution pour X. Il faut continuer la
           substitution dans le terme qui en résulte. C'est par exemple le cas
           lorsqu'on souhaite remplacer X par f(Y) et Y par z : X devient f(Y), et
           il faut continuer la substitution dans f(Y). *)
        subst env term'
    end
  | Const _ ->
    (* Les constantes ne sont pas à substituer *)
    term
  | Compound (f, args) ->
    (* L'opérateur d'un terme composé est une constante, il n'y a donc rien à faire sur f.
       Par contre, il faut substituer dans les arguments *)
    Compound (f, List.map (subst env) args)

(** Occur-check
    ============
    On va avoir besoin de vérifier la présence d'une variable dans un terme. *)
let rec occurs (x : variable) (t : term) = match t with
  | Var y -> x = y
  | Const _ -> false
  | Compound (_, args) -> List.exists (occurs x) args

(** Unification
    =========== *)

(** Dans le cas où on n'arrive pas à unifier deux termes, on lèvera l'exception suivante *)
exception NoUnify

(* TODO: montrer des exemples, ou en faire à la main dans les slides avant d'arriver ici *)

(** Le but de l'unification est de calculer un environnement de substitution. Si on unifie `t1` avec `t2`, cela nous donne un environnement `env`. En appliquant une substitution avec cet environnement à `t1`, cela doit nous donner `t2.

    L'unification va garder une liste de substitutions trouvées. Chaque fois
    qu'on unifie une variable avec autre chose, on ajoute cela à notre environnement
    de substitutions.*)

let rec unify (env : env) (t1 : term) (t2 : term) =
  match subst env t1, subst env t2 with
  | t1, t2 when t1 = t2 ->
    (* On a deux termes qui unifient avec notre environnement courant, on a donc fini *)
    env
  | (Var x, t) | (t, Var x) ->
    if occurs x t then
      (* Ceci est l'occurs-check *)
      raise NoUnify
    else
      (* On a trouvé une nouvelle substitution: x doit être t *)
      (x, t) :: env
  | Const _, _ ->
    (* On essaye d'unifier une constante avec autre chose. (Ce ne peut pas être
       avec la même constante, car sinon on aurait été dans le premier cas. Il est
       donc impossible d'unifier ces deux termes. *)
    raise NoUnify
  | Compound (f1, args1), Compound (f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
    (* On ne peut unifier des termes composés que si les opérateurs
       correspondent et qu'ils ont le même nombre d'arguments. Si c'est le cas,
       alors on unifie les arguments ensemble, ce que fait `unify_lists`. *)
    unify_lists env args1 args2
  | _ ->
    (* Sinon, on ne peut pas unifier *)
    raise NoUnify

and unify_lists (env : env) (l1 : term list) (l2 : term list) : env =
  List.fold_left2 unify env l1 l2