diff options
Diffstat (limited to 'contrib/jprover/jtunify.ml')
| -rw-r--r-- | contrib/jprover/jtunify.ml | 507 |
1 files changed, 0 insertions, 507 deletions
diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml deleted file mode 100644 index 91aa6b4b..00000000 --- a/contrib/jprover/jtunify.ml +++ /dev/null @@ -1,507 +0,0 @@ -(* - * Unification procedures for JProver. See jall.mli for more - * information on JProver. - * - * ---------------------------------------------------------------- - * - * This file is part of MetaPRL, a modular, higher order - * logical framework that provides a logical programming - * environment for OCaml and other languages. - * - * See the file doc/index.html for information on Nuprl, - * OCaml, and more information about this system. - * - * Copyright (C) 2000 Stephan Schmitt - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program; if not, write to the Free Software - * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. - * - * Author: Stephan Schmitt <schmitts@spmail.slu.edu> - * Modified by: Aleksey Nogin <nogin@cs.cornell.edu> - *) - -exception Not_unifiable -exception Failed - -let jprover_bug = Invalid_argument "Jprover bug (Jtunify module)" - -(* ************ T-STRING UNIFICATION *********************************) - - -(* ******* printing ********** *) - -let rec list_to_string s = - match s with - [] -> "" - | f::r -> - f^"."^(list_to_string r) - -let rec print_eqlist eqlist = - match eqlist with - [] -> - print_endline "" - | (atnames,f)::r -> - let (s,t) = f in - let ls = list_to_string s - and lt = list_to_string t in - begin - print_endline ("Atom names: "^(list_to_string atnames)); - print_endline (ls^" = "^lt); - print_eqlist r - end - -let print_equations eqlist = - begin - Format.open_box 0; - Format.force_newline (); - print_endline "Equations:"; - print_eqlist eqlist; - Format.force_newline (); - end - -let rec print_subst sigma = - match sigma with - [] -> - print_endline "" - | f::r -> - let (v,s) = f in - let ls = list_to_string s in - begin - print_endline (v^" = "^ls); - print_subst r - end - -let print_tunify sigma = - let (n,subst) = sigma in - begin - print_endline " "; - print_endline ("MaxVar = "^(string_of_int (n-1))); - print_endline " "; - print_endline "Substitution:"; - print_subst subst; - print_endline " " - end - - (*****************************************************) - -let is_const name = - (String.get name 0) = 'c' - -let is_var name = - (String.get name 0) = 'v' - -let r_1 s ft rt = - (s = []) && (ft = []) && (rt = []) - -let r_2 s ft rt = - (s = []) && (ft = []) && (List.length rt >= 1) - -let r_3 s ft rt = - ft=[] && (List.length s >= 1) && (List.length rt >= 1) && (List.hd s = List.hd rt) - -let r_4 s ft rt = - ft=[] - && (List.length s >= 1) - && (List.length rt >= 1) - && is_const (List.hd s) - && is_var (List.hd rt) - -let r_5 s ft rt = - rt=[] - && (List.length s >= 1) - && is_var (List.hd s) - -let r_6 s ft rt = - ft=[] - && (List.length s >= 1) - && (List.length rt >= 1) - && is_var (List.hd s) - && is_const (List.hd rt) - -let r_7 s ft rt = - List.length s >= 1 - && (List.length rt >= 2) - && is_var (List.hd s) - && is_const (List.hd rt) - && is_const (List.hd (List.tl rt)) - -let r_8 s ft rt = - ft=[] - && List.length s >= 2 - && List.length rt >= 1 - && let v = List.hd s - and v1 = List.hd rt in - (is_var v) & (is_var v1) & (v <> v1) - -let r_9 s ft rt = - (List.length s >= 2) && (List.length ft >= 1) && (List.length rt >= 1) - && let v = (List.hd s) - and v1 = (List.hd rt) in - (is_var v) & (is_var v1) & (v <> v1) - -let r_10 s ft rt = - (List.length s >= 1) && (List.length rt >= 1) - && let v = List.hd s - and x = List.hd rt in - (is_var v) && (v <> x) - && (((List.tl s) =[]) or (is_const x) or ((List.tl rt) <> [])) - -let rec com_subst slist ((ov,ovlist) as one_subst) = - match slist with - [] -> raise jprover_bug - | f::r -> - if f = ov then - (ovlist @ r) - else - f::(com_subst r one_subst) - -let rec combine subst ((ov,oslist) as one_subst) = - match subst with - [] -> [] - | ((v, slist) as f) :: r -> - let rest_combine = (combine r one_subst) in - if (List.mem ov slist) then (* subst assumed to be idemponent *) - let com_element = com_subst slist one_subst in - ((v,com_element)::rest_combine) - else - (f::rest_combine) - -let compose ((n,subst) as _sigma) ((ov,oslist) as one_subst) = - let com = combine subst one_subst in -(* begin - print_endline "!!!!!!!!!test print!!!!!!!!!!"; - print_subst [one_subst]; - print_subst subst; - print_endline "!!!!!!!!! END test print!!!!!!!!!!"; -*) - if List.mem one_subst subst then - (n,com) - else -(* ov may multiply as variable in subst with DIFFERENT values *) -(* in order to avoid explicit atom instances!!! *) - (n,(com @ [one_subst])) -(* end *) - -let rec apply_element fs ft (v,slist) = - match (fs,ft) with - ([],[]) -> - ([],[]) - | ([],(ft_first::ft_rest)) -> - let new_ft_first = - if ft_first = v then - slist - else - [ft_first] - in - let (emptylist,new_ft_rest) = apply_element [] ft_rest (v,slist) in - (emptylist,(new_ft_first @ new_ft_rest)) - | ((fs_first::fs_rest),[]) -> - let new_fs_first = - if fs_first = v then - slist - else - [fs_first] - in - let (new_fs_rest,emptylist) = apply_element fs_rest [] (v,slist) in - ((new_fs_first @ new_fs_rest),emptylist) - | ((fs_first::fs_rest),(ft_first::ft_rest)) -> - let new_fs_first = - if fs_first = v then - slist - else - [fs_first] - and new_ft_first = - if ft_first = v then - slist - else - [ft_first] - in - let (new_fs_rest,new_ft_rest) = apply_element fs_rest ft_rest (v,slist) in - ((new_fs_first @ new_fs_rest),(new_ft_first @ new_ft_rest)) - -let rec shorten us ut = - match (us,ut) with - ([],_) | (_,[]) -> (us,ut) (*raise jprover_bug*) - | ((fs::rs),(ft::rt)) -> - if fs = ft then - shorten rs rt - else - (us,ut) - -let rec apply_subst_list eq_rest (v,slist) = - match eq_rest with - [] -> - (true,[]) - | (atomnames,(fs,ft))::r -> - let (n_fs,n_ft) = apply_element fs ft (v,slist) in - let (new_fs,new_ft) = shorten n_fs n_ft in (* delete equal first elements *) - match (new_fs,new_ft) with - [],[] -> - let (bool,new_eq_rest) = apply_subst_list r (v,slist) in - (bool,((atomnames,([],[]))::new_eq_rest)) - | [],(fft::rft) -> - if (is_const fft) then - (false,[]) - else - let (bool,new_eq_rest) = apply_subst_list r (v,slist) in - (bool,((atomnames,([],new_ft))::new_eq_rest)) - | (ffs::rfs),[] -> - if (is_const ffs) then - (false,[]) - else - let (bool,new_eq_rest) = apply_subst_list r (v,slist) in - (bool,((atomnames,(new_fs,[]))::new_eq_rest)) - | (ffs::rfs),(fft::rft) -> - if (is_const ffs) & (is_const fft) then - (false,[]) - (* different first constants cause local fail *) - else - (* at least one of firsts is a variable *) - let (bool,new_eq_rest) = apply_subst_list r (v,slist) in - (bool,((atomnames,(new_fs,new_ft))::new_eq_rest)) - -let apply_subst eq_rest (v,slist) atomnames = - if (List.mem v atomnames) then (* don't apply subst to atom variables !! *) - (true,eq_rest) - else - apply_subst_list eq_rest (v,slist) - - -(* let all_variable_check eqlist = false needs some discussion with Jens! -- NOT done *) - -(* - let rec all_variable_check eqlist = - match eqlist with - [] -> true - | ((_,(fs,ft))::rest_eq) -> - if (fs <> []) & (ft <> []) then - let fs_first = List.hd fs - and ft_first = List.hd ft - in - if (is_const fs_first) or (is_const ft_first) then - false - else - all_variable_check rest_eq - else - false -*) - -let rec tunify_list eqlist init_sigma = - let rec tunify atomnames fs ft rt rest_eq sigma = - let apply_r1 fs ft rt rest_eq sigma = - (* print_endline "r1"; *) - tunify_list rest_eq sigma - - in - let apply_r2 fs ft rt rest_eq sigma = - (* print_endline "r2"; *) - tunify atomnames rt fs ft rest_eq sigma - - in - let apply_r3 fs ft rt rest_eq sigma = - (* print_endline "r3"; *) - let rfs = (List.tl fs) - and rft = (List.tl rt) in - tunify atomnames rfs ft rft rest_eq sigma - - in - let apply_r4 fs ft rt rest_eq sigma = - (* print_endline "r4"; *) - tunify atomnames rt ft fs rest_eq sigma - - in - let apply_r5 fs ft rt rest_eq sigma = - (* print_endline "r5"; *) - let v = (List.hd fs) in - let new_sigma = compose sigma (v,ft) in - let (bool,new_rest_eq) = apply_subst rest_eq (v,ft) atomnames in - if (bool=false) then - raise Not_unifiable - else - tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma - - in - let apply_r6 fs ft rt rest_eq sigma = - (* print_endline "r6"; *) - let v = (List.hd fs) in - let new_sigma = (compose sigma (v,[])) in - let (bool,new_rest_eq) = apply_subst rest_eq (v,[]) atomnames in - if (bool=false) then - raise Not_unifiable - else - tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma - - in - let apply_r7 fs ft rt rest_eq sigma = - (* print_endline "r7"; *) - let v = (List.hd fs) - and c1 = (List.hd rt) - and c2t =(List.tl rt) in - let new_sigma = (compose sigma (v,(ft @ [c1]))) in - let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [c1])) atomnames in - if bool=false then - raise Not_unifiable - else - tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma - in - let apply_r8 fs ft rt rest_eq sigma = - (* print_endline "r8"; *) - tunify atomnames rt [(List.hd fs)] (List.tl fs) rest_eq sigma - - in - let apply_r9 fs ft rt rest_eq sigma = - (* print_endline "r9"; *) - let v = (List.hd fs) - and (max,subst) = sigma in - let v_new = ("vnew"^(string_of_int max)) in - let new_sigma = (compose ((max+1),subst) (v,(ft @ [v_new]))) in - let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [v_new])) atomnames in - if (bool=false) then - raise Not_unifiable - else - tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma - - in - let apply_r10 fs ft rt rest_eq sigma = - (* print_endline "r10"; *) - let x = List.hd rt in - tunify atomnames fs (ft @ [x]) (List.tl rt) rest_eq sigma - - in - if r_1 fs ft rt then - apply_r1 fs ft rt rest_eq sigma - else if r_2 fs ft rt then - apply_r2 fs ft rt rest_eq sigma - else if r_3 fs ft rt then - apply_r3 fs ft rt rest_eq sigma - else if r_4 fs ft rt then - apply_r4 fs ft rt rest_eq sigma - else if r_5 fs ft rt then - apply_r5 fs ft rt rest_eq sigma - else if r_6 fs ft rt then - (try - apply_r6 fs ft rt rest_eq sigma - with Not_unifiable -> - if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *) - (try - apply_r7 fs ft rt rest_eq sigma - with Not_unifiable -> - apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r6 was *) - ) - else - (* r10 could be represented only once if we would try it before r7.*) - (* but looking at the transformation rules, r10 should be tried at last in any case *) - apply_r10 fs ft rt rest_eq sigma (* r10 always applicable r6 was *) - ) - else if r_7 fs ft rt then (* not r6 and r7 possible if z <> [] *) - (try - apply_r7 fs ft rt rest_eq sigma - with Not_unifiable -> - apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r7 was *) - ) - else if r_8 fs ft rt then - (try - apply_r8 fs ft rt rest_eq sigma - with Not_unifiable -> - if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *) - apply_r10 fs ft rt rest_eq sigma - else - raise Not_unifiable (* simply back propagation *) - ) - else if r_9 fs ft rt then - (try - apply_r9 fs ft rt rest_eq sigma - with Not_unifiable -> - if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *) - apply_r10 fs ft rt rest_eq sigma - else - raise Not_unifiable (* simply back propagation *) - ) - else if r_10 fs ft rt then (* not ri, i<10, and r10 possible if for instance *) - (* (s=[] and x=v1) or (z<>[] and xt=C1V1t') *) - apply_r10 fs ft rt rest_eq sigma - else (* NO rule applicable *) - raise Not_unifiable - in - match eqlist with - [] -> - init_sigma - | f::rest_eq -> - let (atomnames,(fs,ft)) = f in - tunify atomnames fs [] ft rest_eq init_sigma - -let rec test_apply_eq atomnames eqs eqt subst = - match subst with - [] -> (eqs,eqt) - | (f,flist)::r -> - let (first_appl_eqs,first_appl_eqt) = - if List.mem f atomnames then - (eqs,eqt) - else - (apply_element eqs eqt (f,flist)) - in - test_apply_eq atomnames first_appl_eqs first_appl_eqt r - -let rec test_apply_eqsubst eqlist subst = - match eqlist with - [] -> [] - | f::r -> - let (atomnames,(eqs,eqt)) = f in - let applied_element = test_apply_eq atomnames eqs eqt subst in - (atomnames,applied_element)::(test_apply_eqsubst r subst) - -let ttest us ut ns nt eqlist orderingQ atom_rel = - let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 *) - (* to eliminate common beginning *) - let new_element = ([ns;nt],(short_us,short_ut)) in - let full_eqlist = - if List.mem new_element eqlist then - eqlist - else - new_element::eqlist - in - let sigma = tunify_list full_eqlist (1,[]) in - let (n,subst) = sigma in - let test_apply = test_apply_eqsubst full_eqlist subst in - begin - print_endline ""; - print_endline "Final equations:"; - print_equations full_eqlist; - print_endline ""; - print_endline "Final substitution:"; - print_tunify sigma; - print_endline ""; - print_endline "Applied equations:"; - print_equations test_apply - end - -let do_stringunify us ut ns nt equations = - let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 to eliminate common beginning *) - let new_element = ([ns;nt],(short_us,short_ut)) in - let full_eqlist = - if List.mem new_element equations then - equations - else - new_element::equations - in -(* print_equations full_eqlist; *) - (try - let new_sigma = tunify_list full_eqlist (1,[]) in - (new_sigma,(1,full_eqlist)) - with Not_unifiable -> - raise Failed (* new connection please *) - ) - - -(* type of one unifier: int * (string * string) list *) |