summaryrefslogtreecommitdiff
path: root/contrib/jprover/jterm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/jprover/jterm.ml')
-rw-r--r--contrib/jprover/jterm.ml872
1 files changed, 0 insertions, 872 deletions
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 19:27:46 +0000