resolution.ml

(** OCaml source code of https://github.com/Naereen/Tiny-Prolog-in-OCaml
    (C) 2018 Lilian Besson
    MIT License, https://lbesson.mit-license.org/
*)

open Lib;;

let rec subst x t trm =
  match trm with
  | Var p -> if p=x then t else trm
  | Term (f, l) -> Term (f, map (subst x t) l)
;;

let rec app_subst l trm =
  match l with
  | [] -> trm
  | (x, t)::q -> (app_subst q (subst x t trm))
;;

let subst_on_couple x t = function (p, trm) -> (p, subst x t trm);;

let rec apply_subst_on_subst s1 s2 =
  match s1 with
  | [] -> s2
  | (x, t)::q -> (apply_subst_on_subst q (map (subst_on_couple x t) s2))
;;

let vars_subst = map fst;;

let rec compose l1 l2 = (filter (vars_subst l2) l1) @ (apply_subst_on_subst l1 l2);;

let rec occurence x = function
  | Var y -> x=y
  | Term (f, l) -> occurence_list x l
and occurence_list x = function
  | [] -> false
  | t::q -> (occurence x t) || (occurence_list x q)
;;

let rec unification t1 t2 =
  match (t1, t2) with
  | (Var x), (Var y) ->
    if x=y then true, []
    else true, [x, Var y]
  | (Var x), t ->
    if (occurence x t) then false, []
    else true, [x, t]
  | t, (Var x) ->
    if (occurence x t) then false, []
    else true, [x, t]
  | (Term (f1, l1)), (Term (f2, l2)) ->
    if f1=f2 then unification_list l1 l2
    else false, []
and unification_list l1 l2 =
  match (l1, l2) with
  | [], [] -> true, []
  | [], _  -> false, []
  | _ , [] -> false, []
  | t1::q1, t2::q2 ->
    let (b1, s1) = unification t1 t2 in
    if b1 then
      let (b2, s2) = (unification_list
                     (map (app_subst s1) q1)
                     (map (app_subst s1) q2)) in
      if b2 then true, (compose s2 s1)
      else false, []
    else false, []
;;

let rec search_clauses num prog trm =
  match prog with
    [] -> []
  | cl::q ->
    let fresh_cl = fresh num cl in
    let (b, s) = unification trm fresh_cl.pos in
    if b then (s, fresh_cl)::(search_clauses num q trm)
    else (search_clauses num q trm)
;;

let rec prove_goals_rec ?(maxoutput=10) ?(interactive=true) but num prog s = function
  | [] ->
    display_subst (List.filter (fun (v, _) -> occurence_list v but) s);
    if interactive then begin
      if not (yesOrNo "continue ?") then
        failwith "end"
    end;
    if maxoutput = 0 then failwith "end";
  | trm::q ->
    let ssButs = search_clauses num prog trm in
    begin
      do_list
        (fun (s2, cl) ->
           (prove_goals_rec ~maxoutput:(maxoutput-1) ~interactive:interactive but (num+1) prog
              (compose s2 s)
              (map (app_subst s2) (cl.neg @ q))))
        ssButs
    end
;;

let prove_goals ?(maxoutput=10) ?(interactive=true) prog trm_list =
  try
    prove_goals_rec ~maxoutput:maxoutput ~interactive:interactive trm_list 0 prog [] trm_list
  with
    Failure "end" -> ()