open ParseClause
open Term
open TermUnif

module CM = ListMap.Make(String)
module S = Set.Make(String)

let name = function
  | Const s | Var s | (Fun (s, _)) -> s

let add_clause ((head, body) as cl) cm = CM.push (name head) cl cm

let ren_clause suff (head, body) =
  let rec ren_suffix suff = function
    | Var v -> Var (v ^ suff)
    | Fun (f, tl) -> Fun (f, List.map (ren_suffix suff) tl)
    | t -> t
  in (ren_suffix suff head, List.map (ren_suffix suff) body)

let rec evalrec endgoal d cm tm = function
  | [] -> (print_mapterm endgoal tm; ignore (read_line()))
  | goal :: gtail ->
    let eval_clause clause =
      let (head, body) = ren_clause ("@" ^ (string_of_int d)) clause in
      try evalrec endgoal (d+1) cm (unifmap tm goal head) (body @ gtail)
      with Not_unifiable -> () in        
    try List.iter eval_clause (CM.find (name goal) cm) 
    with Not_found -> ()
      
let cm = List.fold_right add_clause (read_clauses()) CM.empty

let rec loop f = (f (); loop f)

let evalgoal () =
  let goal = read_term()
  in evalrec goal 0 cm emptysubst [goal]
;;

loop evalgoal;;

This document was generated using caml2html