(* λProlog interpreter based on "A Semi-Functional Implementation of a
 * Higher-Order Logic Programming Language", translated into OCaml.
 *)

open Printf

type term =
  | Bvar of string              (* Bound Variables *)
  | Evar of varbind * int * term list * (term option) ref
  (* Logic Variables, Stamped, Depends on *)
  | Uvar of varbind * int                (* Parameters, Stamped *)
  | Const of string                      (* Constants *)
  | Appl of term * term                  (* Applications *)
  | Abst of varbind * term               (* Abstractions *)
and varbind = Varbind of string * term   (* Variable binders *)

let ttype = Const "type"
let make_quant qname ((Varbind (_, a) as vb, t) : varbind * term) = 
  Appl(Appl(Const(qname), a), Abst (vb, t))
let make_pi = make_quant "pi"
let make_arrow (a1,a2) = make_pi(Varbind("#",a1),a2)
 
type gform =                    (* Goal formula *)
  | Gtrue                       (* Truth *)
  | Gand of gform * gform       (* Conjunction *)
  | Gor of gform * gform        (* Disjunction *)
  | Gatom of term               (* Atomic G formula *)
  | Gexists of varbind * gform  (* Existential *)
  | Gimplies of dform * gform   (* Embedded Implication *)
  | Gall of varbind * gform     (* Embedded Implication *)
  | Guard of gform * gform * gform (* "If-Then-Else" *)
  | Gflex of term               (* Flexible Head *)
and dform =                     (* Program formula *)
  | Dtrue                       (* Truth *)
  | Dand of dform * dform       (* Conjunction *)
  | Dimplies of gform * dform   (* Implication *)
  | Datom of term               (* Atomic D formula *)
  | Dall of varbind * dform     (* Universal *)
  | Dflex of term               (* Flexible Head *)

type dpair = Dpair of term * term
type dset = dpair list

type head = string

let rec head term =
  match term with
  | Const cname -> cname
  | Appl (t1, t2) -> head t1
  | _ -> raise (Failure "head of term is not a constant") 

type clause = Clause of head * varbind list * term * gform

(* Counter to create unique variables *)
let varcount = ref 0

let new_evar xofA uvars =
  varcount := !varcount + 1;
  Evar(xofA, !varcount, uvars, ref None) 

let new_evar_sb vbds uvars =
  List.map (fun vbd -> (vbd, new_evar vbd uvars)) vbds

let new_uvar xofA =
  varcount := !varcount + 1;
  Uvar(xofA, !varcount) 

type trail = ConsTrail of term * (trail ref) | NilTrail

let (unwind_trail, trail, instantiate_evar) =
  let global_trail = ref (ref NilTrail) in
  let rec unwind_trail (shorter : trail ref) (longer : trail ref) =
    if shorter == longer
    then global_trail := shorter
    else match !longer with
         | (ConsTrail (Evar (_, _, _, vslot), rest)) -> begin
             vslot := None;
             unwind_trail shorter rest;
           end
         | _ -> raise (Failure "argument is not an Evar") in
  let trail func =
    let old_trail = !global_trail in begin
        func ();
        unwind_trail old_trail (!global_trail);
        ()
      end in
  let instantiate_evar s t =
    match s with 
    | ((Evar (_, _, _, vslot)) as s) -> begin
      vslot := Some t;
      global_trail := ref (ConsTrail (s, !global_trail));
      end
    | _ -> raise (Failure "is not an Evar") in
  (unwind_trail, trail, instantiate_evar)

let gand_opt g1 g2 =
  match g1, g2 with
  | Gtrue, _ -> g2
  | _, Gtrue -> g1
  | _, _ -> Gand (g1, g2)

let shadow vname1 vname2 = vname1 = vname2

let shadow_sb ((Varbind(x,_)) as xofA) sb =
  ((xofA,Bvar(x))::sb)

let suffix_count = ref 0
let new_varname vname = begin
    suffix_count := !suffix_count + 1;
    sprintf "%s^%d" vname !suffix_count
  end
  
let rename_sb ((Varbind(x,a)) as xofA) sb =
  let x' = new_varname x
  in (Varbind(x', a),(xofA,Bvar(x')) :: sb)

exception Loose_Bvar of term

let lookup_vbind x sb =
  let rec lk names =
    match names with
    | ((Varbind(y, _),t)::rest) ->
       if x = y then t else lk rest
    | [] -> raise (Loose_Bvar (Bvar(x)))
  in lk sb

let apply_sb sb s =
  let rec asb term =
    match term with
    | Bvar(vname) -> lookup_vbind vname sb
    | Appl(s1, s2) -> Appl (asb s1, asb s2)
    | t -> t
  in asb s

let (gapply_sb, dapply_sb) =
  let rec gsb sb = function
    | Gtrue -> Gtrue
    | Gand(g1,g2) -> Gand(gsb sb g1, gsb sb g2)
    | Gor(g1,g2) -> Gor(gsb sb g1, gsb sb g2)
    | Gatom(s) -> Gatom(apply_sb sb s)
    | Gexists(y,g) -> Gexists(y, gsb (shadow_sb y sb) g)
    | Gimplies (d, g) -> Gimplies(dsb sb d, gsb sb g)
    | Gall (y, g) -> Gall(y, gsb (shadow_sb y sb) g)
    | Guard (g1, g2, g3) -> Guard (gsb sb g1, gsb sb g2, gsb sb g3)
    | Gflex(m) -> Gflex(apply_sb sb m)
  and dsb sb = function
    | Dtrue -> Dtrue
    | Dand(d1,d2) -> Dand(dsb sb d1, dsb sb d2)
    | Dimplies(g,d) -> Dimplies(gsb sb g, dsb sb d)
    | Datom(s) -> Datom(apply_sb sb s)
    | Dall(y,d) -> Dall(y, dsb (shadow_sb y sb) d)
    | Dflex(m) -> Dflex(apply_sb sb m)
  in (gsb, dsb)

exception Fail of string

let rec head_reduce_term term =
  match term with
  | Appl (m, n) ->
     let rec hrt t =
       match t with
       | Abst(xofA, m0) -> apply_sb [(xofA,n)] m0
       | Evar(_, _, _, { contents = Some m0}) -> hrt m0
       | _ -> Appl (head_reduce_term m, n)
     in hrt m
  | Evar(_, _, _, { contents = Some m0}) -> head_reduce_term m0
  | _ -> raise (Fail "head_reduce_term")

let rew_and (r1 : 'a -> 'a) (r2 : 'a -> 'a) (x : 'a) : 'a = r2 (r1 x)
let rew_or (r1 : 'a -> 'a) (r2 : 'a -> 'a) (x : 'a) : 'a = try r1 x with Fail _ -> r2 x
let rew_id (x : 'a) : 'a = x
let rew_try r = rew_or r rew_id
let rec rew_repeat (r : 'a -> 'a) (x : 'a) : 'a =
  rew_try (rew_and r (rew_repeat r)) x

let rew_dpair rew =
  rew_or
    (fun (Dpair(m,n)) -> Dpair(rew m, n))
    (fun (Dpair(m,n)) -> Dpair(m, rew n))

let rew_first (rew : 'a -> 'a) (ls : 'a list) : 'a list =
  match ls with
  | h::t -> (rew h) :: t
  | [] -> raise (Fail "rew_first")

let rew_rest (list_rew : 'a list -> 'a list) (ls : 'a list) : 'a list =
  match ls with
  | h::t -> h :: (list_rew t)
  | [] -> []

let head_reduce_dpair = rew_dpair head_reduce_term

let rec abst_reduce_dpair pair =
  match pair with
  | Dpair(Evar(_,_,_,{contents = Some m0}), n) ->
     abst_reduce_dpair (Dpair (m0, n))
  | Dpair(m, Evar(_,_,_,{contents = Some n0})) ->
     abst_reduce_dpair (Dpair (m, n0))
  | Dpair(Abst (xofA, m0), Abst (yofA, n0)) ->
     let a = new_uvar xofA
     in Dpair (apply_sb [(xofA, a)] m0, apply_sb [(yofA, a)] n0)
  | Dpair(Abst (xofA, m0), n) ->
     let a = new_uvar xofA
     in Dpair (apply_sb [(xofA, a)] m0, Appl (n, a))
  | Dpair(m, Abst (yofA, n0)) ->
     let a = new_uvar yofA
     in Dpair (Appl (m, a), apply_sb [(yofA, a)] n0)
  | _ -> raise (Fail "abst_reduce_dpair")

exception Nonunifiable

let free_in (Varbind(x,_) as xofA) m =
  let rec fin term =
    match term with
    | Bvar(y) -> x = y
    | Appl(m1,m2) -> fin m1 || fin m2
    | Abst(yofB,m) ->
       if shadow yofB xofA then false else fin m
    | _ -> false  (* Evar , Uvar , Const *)
  in fin m

let rec is_rigid term =
  match term with
  | Const _ -> true
  | Uvar _ -> true
  | Evar (_, _, _, {contents = Some m0}) -> is_rigid m0
  | Evar (_, _, _, {contents = None}) -> false
  | Appl (m, _) -> is_rigid m
  | _ -> raise (Failure "is not in applicative head normal form")

let rec rigid_rigid pair dset =
  match pair with
  | Dpair (Evar (_, _, _, { contents = Some m0}), n) ->
     rigid_rigid (Dpair (m0, n)) dset
  | Dpair (m, Evar (_, _, _, { contents = Some n0})) ->
     rigid_rigid (Dpair (m, n0)) dset
  | Dpair (Appl (m1, n1), Appl (m2, n2)) ->
     rigid_rigid (Dpair (m1, m2)) (Dpair (n1, n2) :: dset)
  | Dpair (Const n1, Const n2) ->
     if n1 = n2 then dset else raise Nonunifiable
  | Dpair (Uvar (_, s1), Uvar (_, s2)) ->
     if s1 = s2 then dset else raise Nonunifiable
  | Dpair (m, n) ->
     if is_rigid m && is_rigid n
     then raise Nonunifiable
     else raise (Fail "rigid_rigid")

let rigid_rigid_rew list =
  match list with
  | (dp :: rest) -> rigid_rigid dp rest
  | [] -> raise (Fail "rigid_rigid_rew")

let rec rigid_head term =
  match term with
  | Const _ -> true
  | (Uvar _) -> true
  | (Evar(_,_,_,{contents = Some m0})) -> rigid_head m0
  | (Appl(m,_)) -> rigid_head m
  | _ -> false

let rec free_in_rhs xofA sb =
  List.exists (fun (_, m) -> free_in xofA m) sb

and renaming_varbind_sb sb (Varbind(x, a)) =
  Varbind(x, renaming_apply_sb sb a)

and rename_vbds gamma =
  let rec rvbds ls sb =
    match ls with
    | xofA::gamma ->
       let xofA' = renaming_varbind_sb sb xofA in
       let (xofA'', new_sb) =
         if free_in_rhs xofA' sb
         then rename_sb xofA' sb
         else xofA', shadow_sb xofA' sb
       in xofA'' :: rvbds gamma new_sb
    | [] -> []
  in rvbds gamma []

and renaming_apply_sb sb m =
  let rec rasb (term : term) =
    match term with
    | Bvar x -> begin
        try lookup_vbind x sb
        with Loose_Bvar _ -> term
      end
    | Appl (m1, m2) -> Appl(rasb m1, rasb m2)
    | Abst (xofA, m) ->
       let xofA' = renaming_varbind_sb sb xofA in
       let (xofA'',new_sb) = if free_in_rhs xofA' sb
                             then rename_sb xofA' sb
                             else (xofA',shadow_sb xofA' sb)
       in Abst(xofA'', renaming_apply_sb new_sb m) 

    | _ -> term
  in rasb m

let rec head_beta_normalize m =
  match m with
  | (Bvar _) -> m
  | (Evar(_,_,_,{contents = None})) -> m
  | (Evar(_,_,_,{contents = (Some m0)})) ->
       head_beta_normalize m0
  | (Uvar _) -> m
  | (Const _) -> m
  | (Appl(m1,m2)) ->
      let normal_m1 = head_beta_normalize m1 in
      (match normal_m1 with
       | (Abst(vbd,body)) ->
	  head_beta_normalize (renaming_apply_sb [(vbd, m2)] body)
       (* Invariant of apply_sb would be violated in preceding line,
	  thus calling rename_apply_sb! *)
       | _ -> Appl(normal_m1,m2))
  | (Abst _) -> m

let rec term_to_gform m = ttg_norm (head_beta_normalize m)
and term_to_dform m = ttd_norm (head_beta_normalize m)

and ttg_norm term =
  match term with
  | (Const("true")) -> Gtrue
  | (Appl(Appl(Const(","),m),n)) -> Gand(term_to_gform m,term_to_gform n)
  | (Appl(Appl(Const(";"),m),n)) -> Gor(term_to_gform m,term_to_gform n)
  | (Appl(Appl(Const("=>"),m),n)) -> Gimplies(term_to_dform m,term_to_gform n)
  | (Appl(Appl(Const("exists"),a),m)) ->
     let (xofA, m) = ttg_abst(head_beta_normalize m) 
     in Gexists (xofA, m)
  | (Appl(Appl(Const("forall"),a),m)) ->
     let (xofA, m) = ttg_abst(head_beta_normalize m)
     in Gexists (xofA, m)
  | (Appl(Appl(Appl(Const("guard"),m),n1),n2)) ->
       Guard (term_to_gform m, term_to_gform n1, term_to_gform n2)
  | m -> if rigid_head m then Gatom(m) else Gflex(m)

and ttd_norm term =
  match term with
  | (Const("true")) -> Dtrue
  | (Appl(Appl(Const(","),m),n)) -> Dand(term_to_dform m,term_to_dform n)
  | (Appl(Appl(Const("=>"),m),n)) -> Dimplies(term_to_gform m,term_to_dform n)
  | (Appl(Appl(Const("forall"),a),m)) ->
     let (xofA, m) = ttd_abst(head_beta_normalize m)
     in Dall (xofA, m)
  | (Appl(Appl(Appl(Const("guard"),m),n1),n2)) ->
       raise (Failure "Guard as program")
  | (Appl(Appl(Const(";"),m),n)) ->
       raise (Failure "Disjunctive program")
  | (Appl(Appl(Const("exists"),a),m)) ->
       raise (Failure "Existential program")
  | m -> if rigid_head m then Datom(m) else Dflex(m)

and ttg_abst term =
  match term with
  | (Abst(xofA,m)) -> (xofA,term_to_gform m)
  | _ -> raise (Failure "Argument to quantifier is not an abstraction")

and ttd_abst term =
  match term with
  | Abst(xofA,m) -> (xofA,term_to_dform m)
  | _ -> raise (Failure "Argument to quantifier is not an abstraction")


let rec clausify (prog : dform) (body : gform) vars rest =
  match prog with
  | Dtrue -> rest
  | Dand (d1, d2) ->
     clausify d1 body vars (clausify d2 body vars rest)
  | Dall (x, d) ->
     if List.exists (fun y -> shadow x y) vars
     then let (new_x, sb) = rename_sb x []
          in clausify (dapply_sb sb d) body (new_x :: vars) rest
     else clausify d body (x :: vars) rest
  | Dimplies (g, d) ->
     clausify d (gand_opt body g) vars rest
  | Datom (t) ->
     Clause(head t, vars, t, body) :: rest
  | Dflex(m) ->
     (match term_to_dform m with
      | Dflex(m') -> raise (Failure "Atom with predicate variable as program")
      | d -> clausify d body vars rest)

let same_evar s t =
  match s with
  | Evar(_, s0, _, { contents = Some v0 }) ->
     (let rec se t =
        match t with
        | Evar(_, s1, _, { contents = None }) -> s0 == s1
        | Evar(_, _, _, { contents = Some v1 }) -> se v1
        | _ -> false
      in se t)
  | _ -> raise (Failure "argument is not an Evar")

let init_seg uvars1 uvars2 =
  List.length uvars1 <= List.length uvars2

let rec find_flex_rigid pairs =
  match pairs with
  | (Dpair(m,n) as dp :: rest) ->
     if is_rigid n then Some dp
     else if is_rigid m then Some (Dpair(n,m))
     else find_flex_rigid rest
  | [] -> None

let simplifier_rew : dset -> dset =
  rew_or
    (rew_or
       (rew_first head_reduce_dpair)
       (rew_first abst_reduce_dpair))
    rigid_rigid_rew

(* formerly SIMPL *)
let rec simplifier (ds : dset) : dset =
  rew_and (rew_repeat simplifier_rew) (rew_rest simplifier) ds

let rec flex_term_head term =
  match term with
  | Appl(m,_) -> flex_term_head m
  | Evar(_,_,_,{ contents = (Some m0) }) -> flex_term_head m0
  | Evar(_) as m -> m
  | _ -> raise (Failure "Not rigid term")

let head_norm_term = rew_repeat head_reduce_term

let rec dest_quant qname t =
  match t with
  | (Appl (m1, m2)) ->
     let rec check_quant_rator_rator term =
       match term with
       | Const (cname) -> qname = cname
       | Evar (_,_,_,{ contents = Some m110}) ->
          check_quant_rator_rator m110
       | _ -> false in
     let rec dest_quant_rator term =
       match term with
       | Appl(m11, m12) ->
          if check_quant_rator_rator m11
          then let rec dest_quant_rand term0 =
                 match term0 with
                 | Abst (xofA, m) -> Some (xofA, m)
                 | Evar (_,_,_,{ contents = Some m20}) ->
                    dest_quant_rand m20
                 | n -> Some (Varbind("@", m12), Appl(n, Bvar("@")))
               in dest_quant_rand m2
          else None
       | Evar (_,_,_,{ contents = Some m10}) ->
          dest_quant_rator m10
       | _ -> None
     in dest_quant_rator m1
  | Evar (_,_,_,{ contents = Some m0}) ->
     dest_quant qname m0
  | _ -> None

let dest_pi = dest_quant "pi"

let pi_vbds b =
  let rec rev_pi_vbds b rev_gamma =
    let b' = head_norm_term b
    in match dest_pi b' with
       | Some (xofA, b0) -> rev_pi_vbds b0 (xofA :: rev_gamma)
       | None -> List.rev rev_gamma, b'
  in rev_pi_vbds b []

let rec add_pis ls m =
  match ls with
  | xofA :: gamma -> make_pi (xofA, add_pis gamma m)
  | [] -> m

let rec add_absts ls m = 
  match ls with
  | xofA :: gamma -> Abst(xofA, add_absts gamma m)
  | [] -> m

let rec rigid_term_head m =
  match m with
  | Const _ -> m
  | Uvar _ -> m
  | Appl(m,_) -> rigid_term_head m
  | Evar(_,_,_,{ contents = Some m0}) ->
     rigid_term_head m0
  | _ -> raise (Failure "is not rigid")

type hosig = (string * term) list

exception Sig_not_found of string
let sig_lookup hosig cname =
  match List.assq_opt cname hosig with
  | Some t -> t
  | None -> raise (Sig_not_found cname)

let basic_list : hosig = [
    ("type", ttype)
  ; ("pi", make_pi (Varbind("A", ttype),
                     make_arrow (make_arrow (Bvar("A"), ttype), ttype)))
  ;
    ("o", ttype)
  ; ("=", make_pi (Varbind("A", ttype),
	            make_arrow (Bvar("A"), make_arrow (Bvar("A"), Const("o")))))
  ; ("true", Const("o"))
  ; (",", make_arrow(Const("o"), make_arrow(Const("o"), Const("o"))))
  ; (";", make_arrow(Const("o"), make_arrow(Const("o"), Const("o"))))
  ; ("=>", make_arrow(Const("o"), make_arrow(Const("o"), Const("o"))))
  ; ("exists", make_pi (Varbind("A", ttype),
                         make_arrow (make_arrow (Bvar("A"), Const("o")), Const("o"))))
  ; ("forall", make_pi (Varbind("A", ttype),
                         make_arrow (make_arrow (Bvar("A"), Const("o")), Const("o"))))
  ; ("guard", make_arrow(Const("o"), make_arrow(Const("o"), make_arrow(Const("o"), Const("o")))))

  ; ("int", ttype)
  ; ("0", Const("int"))
  ; ("1", Const("int"))
  ; ("2", Const("int"))

  ; ("bool", ttype)
  ; ("true", Const("bool"))
  ; ("false", Const("bool"))

  ; ("list", make_arrow(ttype, ttype))
  ; ("nil", make_pi (Varbind("s", ttype), Appl(Const("list"), Bvar("s"))))
  ; ("cons", make_pi (Varbind("s", ttype),
		       make_arrow (Bvar("s"),
			           make_arrow (Appl(Const("list"), Bvar("s")),
				               Appl(Const("list"), Bvar("s"))))))

  ; ("prop", ttype)
  ; ("proof", make_arrow(Const("prop"), ttype))
  ]

let current_sig = ref basic_list
let const_type cname = sig_lookup (!current_sig) cname

(* formerly MATCH *)
let matcher (Dpair(flex,rigid)) ds sc =
  match flex_term_head flex with
  | Evar(Varbind(fname, ftype),_,ok_uvars,_) as f ->
     let (fgamma, ftype') = pi_vbds ftype in
     let gamma_w = rename_vbds fgamma in
     let new_raised_evar b =
       let rec add_args sofar ls =
         match ls with
         | Varbind(wi,_) :: gamma_i ->
            add_args (Appl(sofar, Bvar(wi))) gamma_i
         | [] -> sofar
       in add_args (new_evar (Varbind(fname, add_pis gamma_w b))
		      ok_uvars)
	    gamma_w in
     let try_subst_term m a = begin
         instantiate_evar f m;
	 sc (Dpair(ftype, a) :: ds)
       end in
     let rec add_match_rands n b =
        let b' = head_norm_term b
	in match dest_pi b' with
           | Some (Varbind(yj,bj) as yj_of_Bj, b'') ->
	      let fj_w1_wn = new_raised_evar bj
	      in add_match_rands (Appl(n,fj_w1_wn))
		   (renaming_apply_sb ([(yj_of_Bj, fj_w1_wn)]) b'')
	   | None -> (n,b') in
     let try_head head c =
       let (head_F1_Fm,c') = add_match_rands head c
       in try_subst_term (add_absts gamma_w head_F1_Fm)
	    (add_pis gamma_w c') in
     let imitate () =
       match rigid_term_head rigid with
       | Uvar(Varbind(_,c),stamp1) as a ->
          (if List.exists (fun term -> match term with
                                       | Uvar(_,stamp2) -> stamp1 = stamp2
                                       | _ -> raise (Failure "Not a Uver"))
		ok_uvars
	   then try_head a c
	   else ())
       | Const(cname) as const -> try_head const (const_type cname)
       | _ -> raise (Failure "Not a rigid head") in

     let rec project_from ls =
       match ls with
       | [Varbind(wi,ai)] ->
          try_head (Bvar(wi)) ai
       | Varbind(wi,ai) :: gamma -> begin
           trail (fun () -> try_head (Bvar(wi)) ai);
	   project_from gamma
         end
       | [] -> ()
     in begin
         trail imitate;
         project_from gamma_w
       end
  | _ -> raise (Failure "Not an evar")

let rec unify_dset (ds : dset) (sc : dset -> unit) =
  try 
    let ds' = (simplifier : dset -> dset) ds
    in match (find_flex_rigid ds') with
       | Some dp -> matcher dp ds' (fun match_ds -> unify_dset match_ds sc)
       | None -> sc ds'
  with Nonunifiable -> ()
let unify (m : term) (n : term) (dset : dset) (sc : dset -> unit)
  = unify_dset (Dpair(m,n) :: dset) sc

let rec solve
          (gform : gform)
          (clauses : clause list)
          (uvars : term list)
          (con : dset)
          (sc : dset -> unit) =
  match gform with
  | Gtrue -> sc con
  | Gand(g1,g2) ->
     solve g1 clauses uvars con (fun newcon -> solve g2 clauses uvars newcon sc)
  | Gor(g1,g2) -> 
     trail (fun () -> solve g1 clauses uvars con sc);
     solve g2 clauses uvars con sc;
  | Gatom(t) ->
     match_atom t clauses uvars con sc
  | Gexists(x,g) ->
     solve (gapply_sb (new_evar_sb [x] uvars) g) clauses uvars con sc
  | Gimplies (d,g) ->
     solve g (clausify d (Gtrue) [] clauses) uvars con sc
  | Gall (x,g) ->
     let uvar = new_uvar x in
     solve (gapply_sb ([(x,uvar)]) g) clauses (uvar :: uvars) con sc
  | Guard (g1, g2, g3) -> begin
     let exception Guard_success of dset in
     try
       trail (fun () -> solve g1 clauses uvars con (fun newcon -> raise (Guard_success newcon)));
       solve g3 clauses uvars con sc
     with Guard_success newcon -> solve g2 clauses uvars newcon sc
    end
  | Gflex(m) ->
     match term_to_gform m with
     | Gflex(_) -> raise (Failure "Atom with predicate variable as goal")
     | g -> solve g clauses uvars con sc

and match_atom t clauses uvars (con : dset) (sc : dset -> unit) =
  let t_head = head t in
  let rec rec_match cs =
    match cs with
    | (Clause (s_head,vars,s,gbody) :: rest) ->
       if s_head = t_head
       then let nesb = new_evar_sb vars uvars
            in begin
                trail (fun () ->
                    unify (apply_sb nesb s) t con
                      (fun (newcon : dset) ->
                        solve (gapply_sb nesb gbody) clauses uvars newcon sc));
                rec_match rest
              end
       else rec_match rest
    | [] -> ()
  in rec_match clauses

let one_solve goal prog =
  try
    solve goal prog [] [] (fun con ->
        print_endline "yes";
        raise Exit);
    print_endline "no" 
  with Exit -> ()
     | Failure err -> eprintf "Subtype: %s" err