From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 contrib/jprover/jterm.ml | 872 -----------------------------------------------
 1 file changed, 872 deletions(-)
 delete mode 100644 contrib/jprover/jterm.ml

(limited to 'contrib/jprover/jterm.ml')

diff --git a/contrib/jprover/jterm.ml b/contrib/jprover/jterm.ml
deleted file mode 100644
index 7fc923a5..00000000
--- a/contrib/jprover/jterm.ml
+++ /dev/null
@@ -1,872 +0,0 @@
-open Printf
-open Opname
-open List
-
-(* Definitions of [jterm]: *)
-type  param = param'
-   and operator = operator'
-   and term = term'
-   and bound_term = bound_term'
-   and param' =
-    | Number of int
-    | String of string
-    | Token of string
-    | Var of string
-    | ParamList of param list
-   and operator' = { op_name : opname; op_params : param list }
-   and term' = { term_op : operator; term_terms : bound_term list }
-   and bound_term' = { bvars : string list; bterm : term }
-;;
-
-(* Debugging tools: *)
-(*i*)
-let mbreak s = Format.print_flush (); print_string ("-break at: "^s);
-               Format.print_flush (); let _ = input_char stdin in ()
-(*i*)
-
-type error_msg =
-    | TermMatchError of term * string
-    | StringError of string
-
-exception RefineError of string * error_msg
-
-let ref_raise = function
- |  RefineError(s,e) -> raise (RefineError(s,e))
- |  _ -> raise (RefineError ("Jterm", StringError "unexpected error"))
-
-(* Printing utilities: *)
-
-let fprint_str ostream s =
-    let _ = fprintf ostream "%s." s in ostream
-
-let fprint_str_list ostream sl =
-    ignore (List.fold_left fprint_str ostream sl);
-    Format.print_flush ()
-
-let fprint_opname ostream = function
-    { opname_token= tk; opname_name = sl } ->
-        fprint_str_list ostream sl
-
-let rec fprint_param ostream = function
-    | Number n -> fprintf ostream " %d " n
-    | String s -> fprint_str_list ostream [s]
-    | Token t -> fprint_str_list ostream [t]
-    | Var v -> fprint_str_list ostream [v]
-    | ParamList ps -> fprint_param_list ostream ps
-and fprint_param_list ostream = function
-    | [] -> ()
-    | param::r -> fprint_param ostream param;
-                  fprint_param_list ostream r
-;;
-
-let print_strs = fprint_str_list stdout
-
-
-(* Interface to [Jall.ml]: *)
-(* It is extracted from Meta-Prl's standard implementation. *)
-(*c begin of the extraction *)
-
-type term_subst = (string * term) list
-let mk_term op bterms = { term_op = op; term_terms = bterms }
-let make_term x = x (* external [make_term : term' -> term] = "%identity" *)
-let dest_term x = x (* external [dest_term : term -> term'] = "%identity" *)
-let mk_op name params =
-   { op_name = name; op_params = params }
-
-let make_op x = x (* external [make_op : operator' -> operator] = "%identity" *)
-let dest_op x = x (* external [dest_op : operator -> operator'] = "%identity" *)
-let mk_bterm bvars term = { bvars = bvars; bterm = term }
-let make_bterm x = x (* external [make_bterm : bound_term' -> bound_term] = "%identity" *)
-let dest_bterm x = x (* external [dest_bterm : bound_term -> bound_term'] = "%identity" *)
-let make_param x = x (* external [make_param : param' -> param] = "%identity" *)
-let dest_param x = x (* external [dest_param : param -> param'] = "%identity" *)
-
-(*
- * Operator names.
- *)
-let opname_of_term = function
-   { term_op = { op_name = name } } ->
-      name
-
-(*
- * Get the subterms.
- * None of the subterms should be bound.
- *)
-let subterms_of_term t =
-   List.map (fun { bterm = t } -> t) t.term_terms
-
-let subterm_count { term_terms = terms } =
-   List.length terms
-
-let subterm_arities { term_terms = terms } =
-   List.map (fun { bvars = vars } -> List.length vars) terms
-
-(*
- * Manifest terms are injected into the "perv" module.
- *)
-let xperv = make_opname ["Perv"]
-let sequent_opname = mk_opname "sequent" xperv
-
-(*
- * Variables.
- *)
-
-let var_opname = make_opname ["var"]
-
-(*
- * See if a term is a variable.
- *)
-let is_var_term = function
- | { term_op = { op_name = opname; op_params = [Var v] };
-     term_terms = []
-   } when Opname.eq opname var_opname -> true
- | _ ->
-      false
-
-(*
- * Destructor for a variable.
- *)
-let dest_var = function
- | { term_op = { op_name = opname; op_params = [Var v] };
-     term_terms = []
-   } when Opname.eq opname var_opname -> v
- | t ->
-       ref_raise(RefineError ("dest_var", TermMatchError (t, "not a variable")))
-(*
- * Make a variable.
- *)
-let mk_var_term v =
-   { term_op = { op_name = var_opname; op_params = [Var v] };
-     term_terms = []
-   }
-
-(*
- * Simple terms
- *)
-(*
- * "Simple" terms have no parameters and no binding variables.
- *)
-let is_simple_term_opname name = function
- | { term_op = { op_name = name'; op_params = [] };
-     term_terms = bterms
-   } when Opname.eq name' name ->
-      let rec aux = function
-       | { bvars = []; bterm = _ }::t -> aux t
-       | _::t -> false
-       | [] -> true
-      in
-         aux bterms
- | _ -> false
-
-let mk_any_term op terms =
-   let aux t =
-      { bvars = []; bterm = t }
-   in
-      { term_op = op; term_terms = List.map aux terms }
-
-let mk_simple_term name terms =
-   mk_any_term { op_name = name; op_params = [] } terms
-
-let dest_simple_term = function
- | ({ term_op = { op_name = name; op_params = [] };
-      term_terms = bterms
-    } : term) as t ->
-      let aux = function
-       | { bvars = []; bterm = t } ->
-            t
-       | _ ->
-            ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "binding vars exist")))
-      in
-         name, List.map aux bterms
- | t ->
-      ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "params exist")))
-
-let dest_simple_term_opname name = function
- | ({ term_op = { op_name = name'; op_params = [] };
-      term_terms = bterms
-    } : term) as t ->
-      if Opname.eq name name' then
-         let aux = function
-          | { bvars = []; bterm = t } -> t
-          | _ -> ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "binding vars exist")))
-         in
-            List.map aux bterms
-      else
-         ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "opname mismatch")))
- | t ->
-      ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "params exist")))
-
-(*
- * Bound terms.
- *)
-let mk_simple_bterm bterm =
-   { bvars = []; bterm = bterm }
-
-let dest_simple_bterm = function
- | { bvars = []; bterm = bterm } ->
-      bterm
- | _ ->
-      ref_raise(RefineError ("dest_simple_bterm", StringError ("bterm is not simple")))
-
-(* Copy from [term_op_std.ml]: *)
-(*i modified for Jprover, as a patch... i*)
-let mk_string_term opname s =
-   { term_op = { op_name = opname; op_params = [String s] }; term_terms = [] }
-
-(*i let mk_string_term opname s =
-  let new_opname={opname_token=opname.opname_token; opname_name=(List.tl opname.opname_name)@[s]} in
-    { term_op = { op_name = new_opname; op_params = [String (List.hd opname.opname_name)] }; term_terms = [] }
-i*)
-
-(* Copy from [term_subst_std.ml]: *)
-
-let rec free_vars_term gvars bvars = function
-    | { term_op = { op_name = opname; op_params = [Var v] }; term_terms = bterms } when Opname.eq opname var_opname ->
-         (* This is a variable *)
-         let gvars' =
-            if List.mem v bvars or List.mem v gvars then
-               gvars
-            else
-               v::gvars
-         in
-            free_vars_bterms gvars' bvars bterms
-    | { term_terms = bterms } ->
-         free_vars_bterms gvars bvars bterms
-   and free_vars_bterms gvars bvars = function
-    | { bvars = vars; bterm = term}::l ->
-         let bvars' = vars @ bvars in
-         let gvars' = free_vars_term gvars bvars' term in
-            free_vars_bterms gvars' bvars l
-    | [] ->
-         gvars
-
-let free_vars_list = free_vars_term [] []
-
-
-(* Termop: *)
-
-let is_no_subterms_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = []
-   } ->
-      Opname.eq opname' opname
- | _ ->
-      false
-
-(*
- * Terms with one subterm.
- *)
-let is_dep0_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = [] }]
-   } -> Opname.eq opname' opname
- | _ -> false
-
-let mk_dep0_term opname t =
-   { term_op = { op_name = opname; op_params = [] };
-     term_terms = [{ bvars = []; bterm = t }]
-   }
-
-let dest_dep0_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = []; bterm = t }]
-   } when Opname.eq opname' opname -> t
- | t -> ref_raise(RefineError ("dest_dep0_term", TermMatchError (t, "not a dep0 term")))
-
-(*
- * Terms with two subterms.
- *)
-let is_dep0_dep0_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = [] }; { bvars = [] }]
-   } -> Opname.eq opname' opname
- | _ -> false
-
-let mk_dep0_dep0_term opname = fun
-   t1 t2 ->
-      { term_op = { op_name = opname; op_params = [] };
-        term_terms = [{ bvars = []; bterm = t1 };
-                      { bvars = []; bterm = t2 }]
-      }
-
-let dest_dep0_dep0_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = []; bterm = t1 };
-                   { bvars = []; bterm = t2 }]
-   } when Opname.eq opname' opname -> t1, t2
- | t -> ref_raise(RefineError ("dest_dep0_dep0_term", TermMatchError (t, "bad arity")))
-
-(*
- * Bound term.
- *)
-
-let is_dep0_dep1_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = [] }; { bvars = [_] }]
-   } when Opname.eq opname' opname -> true
- | _ -> false
-
-let is_dep0_dep1_any_term = function
- | { term_op = { op_params = [] };
-     term_terms = [{ bvars = [] }; { bvars = [_] }]
-   } -> true
- | _ -> false
-
-let mk_dep0_dep1_term opname = fun
-   v t1 t2 -> { term_op = { op_name = opname; op_params = [] };
-                term_terms = [{ bvars = []; bterm = t1 };
-                              { bvars = [v]; bterm = t2 }]
-              }
-
-let dest_dep0_dep1_term opname = function
- | { term_op = { op_name = opname'; op_params = [] };
-     term_terms = [{ bvars = []; bterm = t1 };
-                   { bvars = [v]; bterm = t2 }]
-   } when Opname.eq opname' opname -> v, t1, t2
- | t -> ref_raise(RefineError ("dest_dep0_dep1_term", TermMatchError (t, "bad arity")))
-
-let rec smap f = function
- | [] -> []
- | (hd::tl) as l ->
-      let hd' = f hd in
-      let tl' = smap f tl in
-      if (hd==hd')&&(tl==tl') then l else hd'::tl'
-
-let rec try_check_assoc v v' = function
- | [] -> raise Not_found
- | (v1,v2)::tl ->
-      begin match v=v1, v'=v2 with
-       | true, true -> true
-       | false, false -> try_check_assoc v v' tl
-       | _ -> false
-      end
-
-let rec zip_list l l1 l2 = match (l1,l2) with
- | (h1::t1), (h2::t2) ->
-      zip_list ((h1,h2)::l) t1 t2
- | [], [] ->
-      l
- | _ -> raise (Failure "Term.zip_list")
-
-let rec assoc_in_range eq y = function
- | (_, y')::tl ->
-      (eq y y') || (assoc_in_range eq y tl)
- | [] ->
-      false
-
-let rec check_assoc v v' = function
- | [] -> v=v'
- | (v1,v2)::tl ->
-      begin match v=v1, v'=v2 with
-       | true, true -> true
-       | false, false -> check_assoc v v' tl
-       | _ -> false
-      end
-
-let rec zip a b = match (a,b) with
- | (h1::t1), (h2::t2) ->
-      (h1, h2) :: zip t1 t2
- | [], [] ->
-      []
- |
-   _ -> raise (Failure "Term.zip")
-
-let rec for_all2 f l1 l2 =
-   match (l1,l2) with
-    | h1::t1, h2::t2 -> for_all2 f t1 t2 & f h1 h2
-    | [], [] -> true
-    | _ -> false
-
-let newname v i =
-   v ^ "_" ^ (string_of_int i)
-
-let rec new_var v avoid i =
-   let v' = newname v i in
-   if avoid v'
-      then new_var v avoid (succ i)
-      else v'
-
-let vnewname v avoid = new_var v avoid 1
-
-let rev_mem a b = List.mem b a
-
-let rec find_index_aux v i = function
- | h::t ->
-      if h = v then
-         i
-      else
-         find_index_aux v (i + 1) t
- | [] ->
-      raise Not_found
-
-let find_index v l = find_index_aux v 0 l
-
-let rec remove_elements l1 l2 =
-   match l1, l2 with
-    | flag::ft, h::t ->
-         if flag then
-            remove_elements ft t
-         else
-            h :: remove_elements ft t
-    | _, l ->
-         l
-
-let rec subtract l1 l2 =
-   match l1 with
-    | h::t ->
-         if List.mem h l2 then
-            subtract t l2
-         else
-            h :: subtract t l2
-    | [] ->
-         []
-
-let rec fv_mem fv v =
-      match fv with
-       | [] -> false
-       | h::t ->
-            List.mem v h || fv_mem t v
-
-let rec new_vars fv = function
-    | [] -> []
-    | v::t ->
-         (* Rename the first one, then add it to free vars *)
-         let v' = vnewname v (fv_mem fv) in
-            v'::(new_vars ([v']::fv) t)
-
-let rec fsubtract l = function
-    | [] -> l
-    | h::t ->
-         fsubtract (subtract l h) t
-
-let add_renames_fv r l =
-    let rec aux = function
-    | [] -> l
-    | v::t -> [v]::(aux t)
-   in
-      aux r
-
-let add_renames_terms r l =
-   let rec aux = function
-    | [] -> l
-    | v::t -> (mk_var_term v)::(aux t)
-   in
-      aux r
-
-(*
- * First order simultaneous substitution.
- *)
-let rec subst_term terms fv vars = function
- | { term_op = { op_name = opname; op_params = [Var(v)] }; term_terms = [] } as t
-   when Opname.eq opname var_opname->
-      (* Var case *)
-      begin
-         try List.nth terms (find_index v vars) with
-            Not_found ->
-               t
-      end
- | { term_op = op; term_terms = bterms } ->
-      (* Other term *)
-      { term_op = op; term_terms = subst_bterms terms fv vars bterms }
-
-and subst_bterms terms fv vars bterms =
-   (* When subst through bterms, catch binding occurrences *)
-   let rec subst_bterm = function
-    | { bvars = []; bterm = term } ->
-         (* Optimize the common case *)
-         { bvars = []; bterm = subst_term terms fv vars term }
-
-    | { bvars = bvars; bterm = term } ->
-         (* First subtract bound instances *)
-         let flags = List.map (function v -> List.mem v bvars) vars in
-         let vars' = remove_elements flags vars in
-         let fv' = remove_elements flags fv in
-         let terms' = remove_elements flags terms in
-
-         (* If any of the binding variables are free, rename them *)
-         let renames = subtract bvars (fsubtract bvars fv') in
-            if renames <> [] then
-               let fv'' = (free_vars_list term)::fv' in
-               let renames' = new_vars fv'' renames in
-                  { bvars = subst_bvars renames' renames bvars;
-                    bterm = subst_term
-                            (add_renames_terms renames' terms')
-                            (add_renames_fv renames' fv')
-                            (renames @ vars')
-                            term
-                  }
-            else
-               { bvars = bvars;
-                 bterm = subst_term terms' fv' vars' term
-               }
-   in
-      List.map subst_bterm bterms
-
-and subst_bvars renames' renames bvars =
-   let subst_bvar v =
-      try List.nth renames' (find_index v renames) with
-         Not_found -> v
-   in
-      List.map subst_bvar bvars
-
-let subst term vars terms =
-      subst_term terms (List.map free_vars_list terms) vars term
-
-(*i bug!!! in the [term_std] module
-      let subst1 t var term =
-      let fv = free_vars_list term in
-      if List.mem var fv then
-         subst_term [term] [fv] [var] t
-      else
-         t
-The following is the correct implementation
-i*)
-
-let subst1 t var term =
-if List.mem var (free_vars_list t) then
-   subst_term [term] [free_vars_list term] [var] t
-else
-   t
-
-let apply_subst t s =
-   let vs,ts = List.split s in
-   subst t vs ts
-
-let rec equal_params p1 p2 =
-   match p1, p2 with
-    | Number n1, Number n2 ->
-         n1 = n2
-    | ParamList pl1, ParamList pl2 ->
-         List.for_all2 equal_params pl1 pl2
-    | _ ->
-         p1 = p2
-
-let rec equal_term vars t t' =
-   match t, t' with
-    | { term_op = { op_name = opname1; op_params = [Var v] };
-        term_terms = []
-      },
-      { term_op = { op_name = opname2; op_params = [Var v'] };
-        term_terms = []
-      } when Opname.eq opname1 var_opname & Opname.eq opname2 var_opname ->
-         check_assoc v v' vars
-    | { term_op = { op_name = name1; op_params = params1 }; term_terms = bterms1 },
-      { term_op = { op_name = name2; op_params = params2 }; term_terms = bterms2 } ->
-         (Opname.eq name1 name2)
-         & (for_all2 equal_params params1 params2)
-         & (equal_bterms vars bterms1 bterms2)
-and equal_bterms vars bterms1 bterms2 =
-   let equal_bterm = fun
-      { bvars = bvars1; bterm = term1 }
-      { bvars = bvars2; bterm = term2 } ->
-         equal_term (zip_list vars bvars1 bvars2) term1 term2
-   in
-      for_all2 equal_bterm bterms1 bterms2
-
-
-let alpha_equal t1 t2 =
-   try equal_term [] t1 t2 with Failure _ -> false
-
-let var_subst t t' v =
-   let { term_op = { op_name = opname } } = t' in
-   let vt = mk_var_term v in
-   let rec subst_term = function
-      { term_op = { op_name = opname'; op_params = params };
-        term_terms = bterms
-      } as t ->
-         (* Check if this is the same *)
-         if Opname.eq opname' opname & alpha_equal t t' then
-            vt
-         else
-            { term_op = { op_name = opname'; op_params = params };
-              term_terms = List.map subst_bterm bterms
-            }
-
-   and subst_bterm { bvars = vars; bterm = term } =
-      if List.mem v vars then
-         let av = vars @ (free_vars_list term) in
-         let v' = vnewname v (fun v -> List.mem v av) in
-         let rename var = if var = v then v' else var in
-         let term = subst1 term v (mk_var_term v') in
-            { bvars =  smap rename vars; bterm = subst_term term }
-      else
-         { bvars = vars; bterm = subst_term term }
-   in
-      subst_term t
-
-let xnil_opname = mk_opname "nil" xperv
-let xnil_term = mk_simple_term xnil_opname []
-let is_xnil_term = is_no_subterms_term xnil_opname
-
-(*c End of the extraction from Meta-Prl *)
-
-(* Huang's modification: *)
-let all_opname = make_opname ["quantifier";"all"]
-let is_all_term = is_dep0_dep1_term all_opname
-let dest_all = dest_dep0_dep1_term all_opname
-let mk_all_term = mk_dep0_dep1_term all_opname
-
-let exists_opname = make_opname ["quantifier";"exst"]
-let is_exists_term = is_dep0_dep1_term exists_opname
-let dest_exists = dest_dep0_dep1_term exists_opname
-let mk_exists_term = mk_dep0_dep1_term exists_opname
-
-let or_opname = make_opname ["connective";"or"]
-let is_or_term = is_dep0_dep0_term or_opname
-let dest_or = dest_dep0_dep0_term or_opname
-let mk_or_term = mk_dep0_dep0_term or_opname
-
-let and_opname = make_opname ["connective";"and"]
-let is_and_term = is_dep0_dep0_term and_opname
-let dest_and = dest_dep0_dep0_term and_opname
-let mk_and_term = mk_dep0_dep0_term and_opname
-
-let cor_opname = make_opname ["connective";"cor"]
-let is_cor_term = is_dep0_dep0_term cor_opname
-let dest_cor = dest_dep0_dep0_term cor_opname
-let mk_cor_term = mk_dep0_dep0_term cor_opname
-
-let cand_opname = make_opname ["connective";"cand"]
-let is_cand_term = is_dep0_dep0_term cand_opname
-let dest_cand = dest_dep0_dep0_term cand_opname
-let mk_cand_term = mk_dep0_dep0_term cand_opname
-
-let implies_opname = make_opname ["connective";"=>"]
-let is_implies_term = is_dep0_dep0_term implies_opname
-let dest_implies = dest_dep0_dep0_term implies_opname
-let mk_implies_term = mk_dep0_dep0_term implies_opname
-
-let iff_opname = make_opname ["connective";"iff"]
-let is_iff_term = is_dep0_dep0_term iff_opname
-let dest_iff = dest_dep0_dep0_term iff_opname
-let mk_iff_term = mk_dep0_dep0_term iff_opname
-
-let not_opname = make_opname ["connective";"not"]
-let is_not_term = is_dep0_term not_opname
-let dest_not = dest_dep0_term not_opname
-let mk_not_term = mk_dep0_term not_opname
-
-let var_ = mk_var_term
-let fun_opname = make_opname ["function"]
-let fun_ f ts = mk_any_term {op_name = fun_opname; op_params = [String f] } ts
-
-let is_fun_term = function
- | { term_op = { op_name = opname; op_params = [String f] }}
-   when Opname.eq opname fun_opname -> true
- | _ ->
-      false
-
-let dest_fun = function
- | { term_op = { op_name = opname; op_params = [String f] }; term_terms = ts}
-   when Opname.eq opname fun_opname -> (f, List.map (fun { bterm = t } -> t) ts)
- | t ->
-   ref_raise(RefineError ("dest_fun", TermMatchError (t, "not a function symbol")))
-
-let const_ c = fun_ c []
-let is_const_term = function
- | { term_op = { op_name = opname; op_params = [String f] }; term_terms = [] }
-   when Opname.eq opname fun_opname -> true
- | _ ->
-      false
-
-let dest_const t =
-  let (n, ts) = dest_fun t in n
-
-let pred_opname = make_opname ["predicate"]
-let pred_ p ts = mk_any_term {op_name = pred_opname; op_params = [String p] } ts
-
-let not_ = mk_not_term
-let and_ = mk_and_term
-let or_ = mk_or_term
-let imp_ = mk_implies_term
-let cand_ = mk_cand_term
-let cor_ = mk_cor_term
-let iff_ = mk_iff_term
-let nil_term = {term_op={op_name=nil_opname; op_params=[]}; term_terms=[] }
-let forall v t = mk_all_term v nil_term t
-let exists v t= mk_exists_term v nil_term t
-let rec wbin op = function
-  |  [] ->  raise (Failure "Term.wbin")
-  |  [t] -> t
-  |  t::r -> op t (wbin op r)
-
-let wand_ = wbin and_
-let wor_ = wbin or_
-let wimp_ = wbin imp_
-
-(*i let true_opname = make_opname ["bool";"true"]
-let is_true_term = is_no_subterms_term true_opname
-let true_ = mk_simple_term true_opname []
-let false_ = not_ true_
-
-let is_false_term t =
-  if is_not_term t then
-  let t1 = dest_not t in
-    is_true_term t1
-  else
-    false
-i*)
-
-let dummy_false_ = mk_simple_term (make_opname ["bool";"false"]) []
-let dummy_true_ = mk_simple_term (make_opname ["bool";"true"]) []
-let false_ = and_ (dummy_false_) (not_ dummy_false_)
-let true_ = not_ (and_ (dummy_true_) (not_ dummy_true_))
-
-let is_false_term t =
-  if (alpha_equal t false_) then true
-  else false
-
-let is_true_term t =
-  if (alpha_equal t true_) then true
-  else false
-
-(* Print a term [t] via the [ostream]: *)
-let rec fprint_term ostream t prec =
-  let l_print op_prec =
-      if (prec > op_prec) then fprintf ostream "(" in
-  let r_print op_prec =
-      if (prec > op_prec) then fprintf ostream ")" in
-  if is_false_term t then                       (* false *)
-      fprint_str_list ostream ["False"]
-  else if is_true_term t then                   (* true *)
-      fprint_str_list ostream ["True"]
-  else if is_all_term t then                    (* for all *)
-      let v, t1, t2 = dest_all t in
-          fprint_str_list ostream ["A."^v];
-          fprint_term ostream t2 4
-  else if is_exists_term t then                 (* exists *)
-      let v, t1, t2 = dest_exists t in
-          fprint_str_list ostream ["E."^v];
-          fprint_term ostream t2 4              (* implication *)
-  else if is_implies_term t then
-      let t1, t2 = dest_implies t in
-          l_print 0;
-          fprint_term ostream t1 1;
-          fprint_str_list ostream ["=>"];
-          fprint_term ostream t2 0;
-          r_print 0
-  else if is_and_term t then                    (* logical and *)
-      let t1, t2 = dest_and t in
-          l_print 3;
-          fprint_term ostream t1 3;
-          fprint_str_list ostream ["&"];
-          fprint_term ostream t2 3;
-          r_print 3
-  else if is_or_term t then                     (* logical or *)
-      let t1, t2 = dest_or t in
-          l_print 2;
-          fprint_term ostream t1 2;
-          fprint_str_list ostream ["|"];
-          fprint_term ostream t2 2;
-          r_print 2
-  else if is_not_term t then                    (* logical not *)
-      let t2 = dest_not t in
-          fprint_str_list ostream ["~"];
-          fprint_term ostream t2 4              (* nil term *)
-  else if is_xnil_term t then
-          fprint_str_list ostream ["NIL"]
-  else match t with                             (* other cases *)
-    { term_op = { op_name = opname; op_params = opparm }; term_terms = bterms} ->
-        if (Opname.eq opname pred_opname) || (Opname.eq opname fun_opname) then
-        begin
-           fprint_param_list ostream opparm;
-           if bterms != [] then
-           begin
-              fprintf ostream "(";
-              fprint_bterm_list ostream prec bterms;
-              fprintf ostream ")";
-           end
-        end else
-        begin
-           fprintf ostream "[";
-(*           fprint_opname ostream opname;
-           fprintf ostream ": "; *)
-           fprint_param_list ostream opparm;
-           if bterms != [] then
-           begin
-              fprintf ostream "(";
-              fprint_bterm_list ostream prec bterms;
-              fprintf ostream ")";
-           end;
-           fprintf ostream "]"
-        end
-and fprint_bterm_list ostream prec = function
-   |  [] -> ()
-   | {bvars=bv; bterm=bt}::r ->
-        fprint_str_list ostream bv;
-        fprint_term ostream bt prec;
-        if (r<>[]) then fprint_str_list ostream [","];
-        fprint_bterm_list ostream prec r
-;;
-
-
-let print_term ostream t =
-    Format.print_flush ();
-    fprint_term ostream t 0;
-    Format.print_flush ()
-
-let print_error_msg = function
-    | RefineError(s,e) -> print_string ("(module "^s^") ");
-      begin
-      match e with
-       | TermMatchError(t,s) -> print_term stdout t; print_string (s^"\n")
-       | StringError s -> print_string (s^"\n")
-      end
-    | ue -> print_string "Unexpected error for Jp.\n";
-           raise ue
-
-
-(* Naive implementation for [jterm] substitution, unification, etc.: *)
-let substitute subst term =
-    apply_subst term subst
-
-(* A naive unification algorithm: *)
-let compsubst subst1 subst2 =
-  (List.map (fun (v, t) -> (v, substitute subst1 t)) subst2) @ subst1
-;;
-
-let rec extract_terms = function
-    | [] -> []
-    | h::r -> let {bvars=_; bterm=bt}=h in bt::extract_terms r
-
-(* Occurs check: *)
-let occurs v t =
-  let rec occur_rec t =
-    if is_var_term t then v=dest_var t
-    else let { term_op = _ ; term_terms = bterms} = t in
-         let sons = extract_terms bterms in
-            List.exists occur_rec sons
-  in
-  occur_rec t
-
-(* The naive unification algorithm: *)
-let rec unify2 (term1,term2) =
-  if is_var_term term1 then
-    if equal_term [] term1 term2 then []
-    else let v1 = dest_var term1 in
-            if occurs v1 term2 then raise (RefineError ("unify1", StringError ("1")))
-            else [v1,term2]
-  else if is_var_term term2 then
-    let v2 = dest_var term2 in
-       if occurs v2 term1 then raise (RefineError ("unify2", StringError ("2")))
-       else [v2,term1]
-  else
-      let { term_op = { op_name = opname1; op_params = params1 };
-            term_terms = bterms1
-          } = term1
-      in
-      let { term_op = { op_name = opname2; op_params = params2 };
-            term_terms = bterms2
-          } = term2
-      in
-         if Opname.eq opname1 opname2 & params1 = params2 then
-            let sons1 = extract_terms bterms1
-            and sons2 = extract_terms bterms2 in
-            List.fold_left2
-               (fun s t1 t2 -> compsubst
-                               (unify2 (substitute s t1, substitute s t2)) s)
-               [] sons1 sons2
-         else raise (RefineError ("unify3", StringError ("3")))
-
-let unify term1 term2 = unify2 (term1, term2)
-let unify_mm term1 term2 _ = unify2 (term1, term2)
-- 
cgit v1.2.3