/[mojave]/metaprl/refiner/reflib/jall.ml
ViewVC logotype

Diff of /metaprl/refiner/reflib/jall.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2918 by steph, Wed Feb 2 18:19:32 2000 UTC revision 2919 by steph, Mon Mar 13 22:17:11 2000 UTC
# Line 43  Line 43 
43    
44  type atom  = {aname : string;  type atom  = {aname : string;
45                aaddress : int list;                aaddress : int list;
46                aprefix : string array;                aprefix : string list;
47                apredicate :  operator;                apredicate :  operator;
48                apol : polarity;                apol : polarity;
49                ast : stype;                ast : stype;
# Line 61  Line 61 
61    
62    
63    
64    (* definition: rules, inferences for LJ, LJmc, and LK *)
65    
66    type rule = Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl |
67                Allr | Alll| Exr | Exl | Fail
68    
69    (* Assume only constants for instantiations, not adapted to terms yet *)
70    
71    
72    
73    type inf = rule * term  * term
74    
75    
76    
77    
# Line 76  Line 87 
87  module AtomSet = Set.Make(OrderedAtom);;  module AtomSet = Set.Make(OrderedAtom);;
88    
89    
 (*****************************************************************)  
90    
91    module OrderedString =
92     struct
93      type t = string
94      let compare a1 a2 = if a1 = a2 then 0 else
95                           if a1 < a2 then -1 else 1
96     end;;
97    
98    
99  (************* printing function *************************************)  module StringSet = Set.Make(OrderedString);;
100    
101    
102    
103    (*****************************************************************)
104    
 (************ printing T-string unifiers ****************************)  
105    
106    
107  let rec list_to_string s =  (************* printing function *************************************)
  match s with  
   [] -> ""  
  |f::r ->  
   f^"."^(list_to_string r)  
108    
109    
 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  
110    
111    
112  let print_tunify sigma =  (************ printing T-string unifiers ****************************)
  let (n,subst) = sigma in  
  begin  
   print_endline ("MaxVar = "^(string_of_int (n-1)));  
   print_endline " ";  
   print_endline "Substitution:";  
   print_subst subst;  
   print_endline " "  
  end  
113    
114    (* se unification module *)
115    
116    
117    
# Line 180  Line 174 
174     Format.force_newline ();     Format.force_newline ();
175     Format.print_break (tab+1) (tab+1);     Format.print_break (tab+1) (tab+1);
176     Format.print_string "prefix=";     Format.print_string "prefix=";
177     print_prefix (Array.to_list z);     print_prefix z;
178     Format.print_string "; predicate=<abstr>; ";     Format.print_string "; predicate=<abstr>; ";
179     Format.print_break (tab+1) (tab+1);     Format.print_break (tab+1) (tab+1);
180     Format.print_break (tab+1) (tab+1);     Format.print_break (tab+1) (tab+1);
# Line 351  Line 345 
345   end;;   end;;
346    
347    
348  let rec print_ordering ordering =  
349   match ordering with  
350    
351    let rec print_set_list set_list =
352     match set_list with
353      [] -> ""
354     |f::r ->
355       (f.aname)^" "^(print_set_list r)
356    
357    let print_set  set =
358     let set_list = AtomSet.elements set in
359      if set_list = [] then "empty"
360      else
361       print_set_list set_list
362    
363    
364    
365    
366    
367    
368    let rec print_stringlist slist =
369      match slist with
370        [] ->
371         Format.print_string ""
372       |f::r ->
373         begin
374          Format.print_string (f^".");
375          print_stringlist r
376         end
377    
378    
379    let rec print_list_sets list_of_sets =
380     match list_of_sets with
381      [] -> Format.print_string ""
382     |(pos,fset)::r ->
383      begin
384        Format.print_string (pos^": ");   (* first element = node which successors depend on *)
385        print_stringlist (StringSet.elements fset);
386        Format.force_newline ();
387        print_list_sets r
388      end
389    
390    
391    let print_ordering list_of_sets =
392      begin
393       Format.open_box 0;
394       print_list_sets list_of_sets;
395       Format.print_flush ()
396      end
397    
398    
399    
400    
401    let rec print_pairlist pairlist =
402     match pairlist with
403    [] -> Format.print_string ""    [] -> Format.print_string ""
404   |(a,b)::rest ->   |(a,b)::rest ->
405     begin     begin
406      Format.print_break 1 1;      Format.print_break 1 1;
407      Format.print_string ("("^a^","^b^")");      Format.print_string ("("^a^","^b^")");
408      print_ordering rest      print_pairlist rest
409     end     end
410    
 let print_pos_n  pos_n =  
   Format.print_int pos_n  
411    
412    
413    
414    let print_pos_n  pos_n =
415      Format.print_int pos_n
416    
417    
418  let print_formula_info ftree ordering pos_n =  let print_formula_info ftree ordering pos_n =
419  begin  begin
# Line 377  Line 425 
425   Format.force_newline ();   Format.force_newline ();
426   Format.print_string "number of positions: ";   Format.print_string "number of positions: ";
427   print_pos_n pos_n;   print_pos_n pos_n;
428     Format.force_newline ();
429   print_endline "";   print_endline "";
430   print_endline "";   print_endline "";
431   Format.print_flush ()   Format.print_flush ()
# Line 387  Line 436 
436    
437    
438    
439  (************ T-STRING UNIFICATION *********************************)  (************** PROOF RECONSTRUCTION without redundancy deletion ******************************)
440    
441    
442    
443  let is_const name  =  (* proof tree for pretty print only *)
   (String.get name 0) = 'c'  
444    
445    
446  let is_var name  =  type 'inf ptree = PEmpty |
447    (String.get name 0) = 'v'                    PNodeAx of 'inf |
448                      PNodeA of 'inf * 'inf ptree |
449                      PNodeB of 'inf * 'inf ptree * 'inf ptree;;
450    
451    
452    
 let r_1 s ft rt =  
   (s = []) & (ft = []) & (rt = [])  
453    
454    
455    (* build the proof tree from a list of inference rules *)
456    
457    let rec unclosed subtree =  
458        match subtree with
459           PEmpty -> true
460         | PNodeAx(y) -> false
461         | PNodeA(y,left) -> (unclosed left)
462         | PNodeB(y,left,right) -> (or) (unclosed left) (unclosed right);;
463      
464    
465    
466  let r_2 s ft rt =  let rec extend prooftree element =  
467    (s = []) & (ft = []) & (List.length rt >= 1)     match prooftree with
468         PEmpty ->
469           let (rule,formula,term) = element in
470             if rule = Ax then  
471              PNodeAx(element)
472             else
473               if List.mem rule [Andr; Orl; Impl] then
474                  PNodeB(element,PEmpty,PEmpty)
475               else
476                  PNodeA(element,PEmpty)
477       | PNodeAx(y) ->
478            PEmpty           (* that's only for  exhaustive pattern matching *)
479       | PNodeA(y, left) ->
480            PNodeA(y, (extend left element))
481       | PNodeB(y, left, right) ->
482            if (unclosed left) then
483              PNodeB(y, (extend left element), right)
484            else
485              PNodeB(y, left, (extend right element));;
486    
487    
488    let rec bptree prooftree nodelist nax=
489       match nodelist with
490        [] -> prooftree,nax
491       |  (rule,formula,term)::rest ->
492          let newax =  
493           if rule = Ax then
494             1
495           else
496             0
497          in
498            bptree (extend prooftree (rule,formula,term)) rest (nax+newax);;
499    
500    
501    let bproof nodelist =
502         bptree PEmpty nodelist 0
503    
504    
505    
 let r_3 s ft rt =  
   if ft=[] then  
     if (List.length s >= 1) &  (List.length rt >= 1) then  
      let x = List.hd s  
      and y = List.hd rt in  
        x=y  
     else  
      false  
   else  
    false  
506    
507    
508    let ruletable r =  
509      match r with
510       Fail -> "Fail"  
511     | Ax ->     "Ax"
512     | Negl ->  "Negl"
513     | Negr ->  "Negr"
514     | Andl ->  "Andl"
515     | Andr ->  "Andr"
516     | Orl ->   "Orl"
517     | Orr ->   "Orr"
518     | Orr1 ->   "Orr1"
519     | Orr2 ->   "Orr2"
520     | Impl ->   "Impl"
521     | Impr ->   "Impr"
522     | Exl ->   "Exl"
523     | Exr ->   "Exr"
524     | Alll ->   "Alll"
525     | Allr ->   "Allr";;
526    
527    
 let r_4 s ft rt =  
   if ft=[] then  
     if (List.length s >= 1) &  (List.length rt >= 1) then  
      let c = List.hd s  
      and v = List.hd rt in  
        (is_const c) & (is_var v)  
     else  
      false  
   else  
    false  
528    
529    let pp_rule (r,formula,term) tab =
530      let rep = ruletable r in  
531       if List.mem rep ["Alll";"Allr";"Exl";"Exr"] then
532            begin
533              Format.open_box 0;
534              Format.force_newline ();
535              Format.print_break tab 0;
536              Format.print_string (rep^" ");
537              Format.print_break tab 0;
538              Format.force_newline ();
539              Format.print_break tab 0;
540              print_term stdout formula;
541              print_term stdout term;
542        (*      Format.force_newline (); *)
543              Format.print_flush ()
544            end
545          else
546            begin
547              Format.open_box 0;
548              Format.print_break tab 0;
549              Format.print_string (rep^" ");
550              Format.print_flush ();
551              Format.open_box 0;
552    (*        Format.print_break tab 0; *)
553              Format.force_newline ();
554    (*        Format.print_break tab 0; *)
555              print_term stdout formula;
556              Format.force_newline ()
557            end
558    
559    
560    let last addr =
561     if addr = ""
562      then ""
563     else
564      String.make 1 (String.get addr (String.length addr-1));;
565    
566    
567   let r_5 s ft rt =  let rest addr =
568    if rt=[] then   if addr = ""
569      if (List.length s >= 1) then    then ""
570       let v = List.hd s in   else
571         (is_var v)    String.sub addr 0 ((String.length addr) - 1);;
     else  
      false  
   else  
    false  
572    
573    
574    
575    let rec get_r_chain addr =  
576     if addr = "" then
577      0
578     else  
579      let l = last addr in
580       if l = "l" then
581        0
582       else (* l = "r" *)
583       let rs = rest addr in
584         1 + (get_r_chain rs);;
585    
586    
587    
 let r_6 s ft rt =  
   if ft=[] then  
     if (List.length s >= 1) &  (List.length rt >= 1) then  
      let v = List.hd s  
      and c1 = List.hd rt in  
        (is_var v) & (is_const c1)  
     else  
      false  
   else  
    false  
588    
589    let rec tpp seqtree tab addr =  
590     match seqtree with
591     | PEmpty -> raise (Failure "Invalid argument")
592     | PNodeAx(rule) ->
593        let (r,p,pa) = rule in  
594         begin
595          pp_rule (r,p,pa) tab;
596    (*      Format.force_newline (); *)
597    (*      let mult = get_r_chain addr in  *)
598    (*        Format.print_break 100 (tab - (3 * mult)) *)
599         end
600     | PNodeA(rule,left) ->
601       let (r,p,pa) = rule in  
602            begin
603             pp_rule (r,p,pa) tab;
604             tpp left tab addr  
605            end
606     | PNodeB(rule,left,right) ->
607       let (r,p,pa) = rule in  
608           let newtab = tab + 3 in
609            begin
610             pp_rule (r,p,pa) tab;
611    (*       Format.force_newline (); *)
612    (*       Format.print_break 100 newtab; *)
613             (tpp left newtab (addr^"l"));
614             (tpp right newtab (addr^"r"))
615            end;;
616    
617    
618    
619  let r_7 s ft rt =  let tt seqtree =
620      if (List.length s >= 1) &  (List.length rt >= 2) then   begin
621       let v = List.hd s    Format.open_box 0;
622       and c1 = List.hd rt    tpp seqtree 0 "";
623       and c2 = (List.hd (List.tl rt)) in    Format.force_newline ();
624         (is_var v) & (is_const c1) & (is_const c2)    Format.close_box ();
625      else    Format.print_newline ()
626       false   end;;
627    
628    
629    
630    
631    
632    
 let r_8 s ft rt =  
   if ft=[] then  
     if (List.length s >= 2) &  (List.length rt >= 1) then  
      let v = List.hd s  
      and v1 = List.hd rt in  
        (is_var v) & (is_var v1) & (v <> v1)  
     else  
      false  
   else  
    false  
633    
634    
635    
636    
637    
 let r_9 s ft rt =  
     if (List.length s >= 2) & (List.length ft >= 1) & (List.length rt >= 1) then  
      let v = (List.hd s)  
      and v1 = (List.hd rt) in  
        (is_var v) & (is_var v1) & (v <> v1)  
     else  
       false  
638    
639    
640    
641  let r_10 s ft rt =  
642      if (List.length s >= 1) &  (List.length rt >= 1) then  let rec init_unsolved treelist =
643       let v = List.hd s   match treelist with  
644       and x = List.hd rt in    [] -> []
645         (is_var v) & (v <> x) &   |f::r ->
646          (((List.tl s) =[]) or (is_const x) or ((List.tl rt) <> []))     match f with
647      else       Empty -> []
648       false      |NodeAt(pos) ->
649          (pos.name)::(init_unsolved r)
650        |NodeA(pos,suctrees) ->
651          let new_treelist = (Array.to_list suctrees) @ r in
652           (pos.name)::(init_unsolved new_treelist)
653    
654    
655    (* only the unsolved positions will be represented --> skip additional root position *)
656    
657    let build_unsolved ftree =
658     match ftree with
659       Empty ->  
660        raise (Failure "Invalid Argument")
661      |NodeAt(_) ->
662        raise (Failure "Invalid Argument")
663      |NodeA(pos,suctrees) ->
664        ((pos.name),init_unsolved (Array.to_list suctrees))
665    
666    
667    
668    
669    let rec collect_variables tree_list =
670     match tree_list with  
671      [] -> []
672     |f::r ->
673       match f with
674         Empty -> []
675        |NodeAt(pos) ->
676          if pos.st = Gamma_0 then
677            pos.name::collect_variables r
678          else
679            collect_variables r
680        |NodeA(pos,suctrees) ->
681          let new_tree_list = (Array.to_list suctrees) @ r in
682           if pos.st = Gamma_0 then
683             pos.name::collect_variables new_tree_list
684           else
685             collect_variables new_tree_list
686    
687    
688    
689    let rec extend_sigmaQ sigmaQ vlist =
690     match vlist with
691      [] -> []
692     |f::r ->
693      let vf = mk_var_term f in
694       if List.exists (fun x -> (fst x = vf)) sigmaQ then
695         extend_sigmaQ sigmaQ r
696       else
697    (* first and second component are var terms in meta-prl *)
698         [(vf,vf)] @ (extend_sigmaQ sigmaQ r)
699    
700    
701    
702    let build_sigmaQ sigmaQ ftree =
703      let vlist = collect_variables [ftree] in
704        sigmaQ @ (extend_sigmaQ sigmaQ vlist)
705    
706    
707    
708    
709    
710    (* subformula relation subrel is assumed to be represented in pairs
711       (a,b) *)
712    
713    
714  let rec com_subst slist (ov,ovlist) =  
715   match slist with  
716    [] -> raise (Failure "Invalid argument")  let rec delete e list =     (* e must not necessarily occur in list *)
717     match list with
718        [] -> []               (* e must not necessarily occur in list *)
719      | first::rest ->
720        if e = first then
721          rest
722        else
723          first::(delete e rest);;
724    
725        
726    let rec key_delete fname pos_list =   (* in key_delete, f is a pos name (key) but sucs is a list of positions *)
727      match pos_list with
728       [] -> []               (* the position with name f  must not necessarily occur in pos_list *)
729    |f::r ->    |f::r ->
730     if f = ov then     if fname = f.name then
731      (ovlist @ r)       r
732     else     else
733      f::(com_subst r (ov,ovlist))      f::(key_delete fname r)
734    
735    
736  let rec combine subst (ov,oslist)  =  
737   match subst with  
738    [] -> []  let rec get_roots treelist =
739     match treelist with
740       [] -> []
741   |f::r ->   |f::r ->
742    let (v,slist) = f in       match f with
743     if (List.mem ov slist) & (not (List.mem v oslist)) then       Empty -> (get_roots r)    (* Empty is posible below alpha-nodes after purity *)
744      (v,(com_subst slist (ov,oslist)))::(combine r (ov,oslist))     | NodeAt(pos) -> pos::(get_roots r)
745     else     | NodeA(pos,trees) ->  pos::(get_roots r);;
     f::(combine r (ov,oslist))  
746    
747    
748    
749  let compose sigma one_subst =  (* the composition could be optimized for *)  let rec comp_ps padd ftree =
750                                 (* practical reasons *)   match ftree with
751    let (n,subst)=sigma    Empty -> raise (Failure "invalid argument")
752    and (ov,oslist) = one_subst in   |NodeAt(pos) ->
753     let com = combine subst (ov,oslist)      []
754      in   |NodeA(pos,strees) ->
755  (*    begin      match padd with
756       print_endline "!!!!!!!!!test print!!!!!!!!!!";       [] -> get_roots (Array.to_list strees)
757       print_subst [one_subst];      |f::r ->
758       print_subst subst;         if r = [] then
759       print_endline "!!!!!!!!! END test print!!!!!!!!!!";           pos::(comp_ps r (Array.get strees (f-1)))
760  *)         else
761       if List.mem one_subst subst then           comp_ps r (Array.get strees (f-1))
762         (n,com)  
763    
764    
765    (* computes a list: first element predecessor, next elements successoes of p *)
766    
767    let tpredsucc p ftree =        
768     let padd = p.address in
769      comp_ps padd ftree
770    
771    
772    
773    
774    
775    
776    (* set an element in an array, without side effects *)
777    
778    let myset array int element =
779     let length = Array.length array in
780      let firstpart = Array.sub array 0 (int) in
781       let secondpart = Array.sub array (int+1) (length-(int+1)) in
782        (Array.append firstpart (Array.append [|element|] secondpart));;
783    
784    
785    
786    
787    let rec compute_open treelist slist =
788     match treelist with
789       [] -> []
790      |first::rest ->
791       let elements =
792         match first with
793             Empty -> []  
794           | NodeAt(pos) ->
795             if (List.mem (pos.name) slist) then
796              [pos]
797             else
798              []
799           | NodeA(pos,suctrees) ->
800             if (List.mem (pos.name) slist) then
801               [pos]
802             else
803               compute_open (Array.to_list suctrees) slist
804      in
805       elements @ (compute_open rest slist);;
806    
807    
808    
809    let rec select_connection pname connections slist =
810     match connections with
811       [] -> ("none","none")
812      |f::r ->
813       let partner =
814        if (fst f) = pname then
815          (snd f)
816        else
817         if (snd f) = pname then
818          (fst f)
819       else       else
820  (* ov may multiply as variable in subst with DIFFERENT values *)        "none"
821  (* in order to avoid explicit atom instances!!! *)     in
822        (n,(com @ [one_subst]))     if ((partner = "none") or (List.mem partner slist)) then
823  (*   end *)      select_connection pname r slist
824       else
825        f;;
826    
827    
828    
829    
830    let rec replace_element element element_set redord =
831      match redord with
832       [] -> raise (Failure "Invalid argument")   (* element occurs in redord *)
833      |(f,fset)::r ->
834        if f = element then
835         (f,element_set)::r
836        else
837         (f,fset)::(replace_element element element_set r)
838        
839    
840    
841    let rec collect_succ_sets sucs redord =
842      match redord with
843       [] -> StringSet.empty
844      |(f,fset)::r ->
845       let new_sucs = key_delete f sucs in
846        if (List.length sucs) = (List.length new_sucs) then   (* position with name f did not occur in sucs -- no deletion *)
847         (collect_succ_sets sucs r)
848        else
849          StringSet.union (StringSet.add f fset) (collect_succ_sets new_sucs r)
850    
851    
852    let replace_ordering psucc_name sucs redord =
853      let new_psucc_set = collect_succ_sets sucs redord in
854       replace_element psucc_name new_psucc_set redord
855    
856    
857    
858    let rec update pname redord =  
859      match redord with
860       [] -> []
861      |(f,fset)::r ->
862       if pname=f then
863         r
864       else
865         (f,fset)::(update pname r)
866        
867    
868    
869    (*  rule construction *)
870    
871    let rec selectQ spos_var csigmaQ =
872     match csigmaQ  with
873      [] ->
874       raise (Failure "Invalid argument")
875     |(var,term)::r ->
876       if spos_var=var then
877         term
878       else
879         selectQ  spos_var r
880        
881    
882    
883    let apply_sigmaQ term sigmaQ =    (* this has to be done *)
884       term
885    
 let rec compute_all fs ft rt sigma =  
886    
887  let apply_r1 fs ft rt sigma =  
888   begin  let build_rule pos spos csigmaQ orr_flag calculus =  
889  (*  print_endline "r1 -- SUCEED WITH AN UNIFIER!!!";    match pos.op,pos.pol with
890    print_tunify sigma;      Null,_ -> raise (Failure "Invalid argument")
891      | At,O ->
892         let inst_atom = apply_sigmaQ pos.label csigmaQ in
893            Ax,(inst_atom),(mk_string_term (make_opname []) "dummy") (* to give back a term *)
894      | At,I ->
895          let inst_atom = apply_sigmaQ pos.label csigmaQ in
896            Ax,(inst_atom),(mk_string_term (make_opname []) "dummy")
897      | And,O -> Andr,(pos.label),(mk_string_term (make_opname []) "dummy")
898      | And,I -> Andl,(pos.label),(mk_string_term (make_opname []) "dummy")
899      | Or,O ->
900         if calculus = "LJ" then
901          let or_rule =
902           if orr_flag = 1 then
903            Orr1
904           else
905            Orr2
906          in
907           or_rule,(pos.label),(mk_string_term (make_opname [])"dummy")
908         else  
909           Orr,(pos.label),(mk_string_term (make_opname [])"dummy")
910      | Or,I -> Orl,(pos.label),(mk_string_term (make_opname [])"dummy")
911      | Neg,O -> Negr,(pos.label),(mk_string_term (make_opname [])"dummy")
912      | Neg,I -> Negl,(pos.label),(mk_string_term (make_opname [])"dummy")
913      | Imp,O -> Impr,(pos.label),(mk_string_term (make_opname [])"dummy")
914      | Imp,I -> Impl,(pos.label),(mk_string_term (make_opname [])"dummy")
915      | All,I -> Alll,(pos.label),(selectQ (mk_var_term (spos.name)) csigmaQ)
916      | Ex,O -> Exr,(pos.label), (selectQ  (mk_var_term (spos.name)) csigmaQ)
917      | All,O -> Allr,(pos.label),(mk_string_term (make_opname []) (spos.name)) (* must be a proper term *)
918      | Ex,I -> Exl,(pos.label),(mk_string_term (make_opname []) (spos.name)) (* must be a proper term *)
919    
920    
921    
922    (* %%%%%%%%%%%%%%%%%%%% Split begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
923    
924    
925    let rec nonemptys treearray j n =
926     if j = n then
927      0
928     else
929      let count =
930       if (Array.get treearray j) <> Empty then
931        1
932       else
933        0
934      in
935      count + (nonemptys treearray (j+1) n);;
936    
937    
938    
939    let rec collect_pure ftreelist (flist,slist) =  
940    
941     let rec collect_itpure ftree (flist,slist) =
942      match ftree with
943         Empty ->  (* assumed that not all brother trees are Empty *)
944          []
945       | NodeAt(pos) -> (* that may NOT longer be an inner node *)
946          if ((List.mem (pos.name) flist) or (List.mem (pos.name) slist)) then
947           []
948          else
949           [pos]
950       | NodeA(pos,treearray) ->
951           collect_pure (Array.to_list treearray) (flist,slist)
952    in
953     match ftreelist with
954      [] -> []
955     |f::r ->
956       (collect_itpure f (flist,slist)) @ (collect_pure r (flist,slist))
957    
958    
959    
960    
961    
962    
963    
964    let rec update_list testlist list =
965     match testlist with
966       [] -> list
967      |f::r ->
968        let newlist = delete f list in    (* f may not occur in list; then newlist=list *)
969         update_list r newlist
970    
971    
972    
973    
974    
975    
976    let rec update_pairlist p pairlist =
977     match pairlist with
978       [] -> []
979      |f::r ->
980        if ((fst f) = p) or ((snd f) = p) then
981          update_pairlist p r
982        else
983          f::(update_pairlist p r)
984    
985    
986    
987    let rec update_connections slist connections =
988      match slist with
989        [] -> connections
990       |f::r ->
991        let connew = update_pairlist f connections in
992         update_connections r connew
993      
994    
995    
996    
997    
998    let rec update_redord delset redord =   (* delset is the set of positions to be deleted *)
999     match redord with
1000      [] -> []
1001      |(f,fset)::r ->
1002        if (StringSet.mem f delset) then
1003         update_redord delset r   (* delete all key elements f from redord which are in delset *)
1004        else
1005         let new_fset  = StringSet.diff fset delset in  (* no successor of f from delset should remain in fset *)
1006          (f,new_fset)::(update_redord delset r)
1007        
1008    
1009    
1010    
1011    
1012    
1013    let rec get_position_names treelist =
1014     match treelist with
1015       [] -> []
1016      |deltree::rests ->
1017       match deltree with
1018        Empty -> get_position_names rests
1019      | NodeAt(pos) ->
1020         (pos.name)::get_position_names rests
1021      | NodeA(pos,strees) ->
1022         (pos.name)::(get_position_names ((Array.to_list strees) @ rests))
1023    
1024    
1025    
1026    
1027    let rec slist_to_set slist =
1028     match slist with
1029      [] ->
1030       StringSet.empty
1031     |f::r ->
1032       StringSet.add f (slist_to_set r)
1033    
1034    
1035    
1036    
1037    let rec print_purelist pr =
1038     match pr with
1039      [] ->
1040       begin
1041        print_string ".";
1042        print_endline " ";
1043       end
1044     |f::r ->  
1045       print_string ((f.name)^", ");
1046       print_purelist r;;
1047    
1048    
1049    
1050    
1051    let update_relations deltree redord connections unsolved_list =
1052      let pure_names = get_position_names [deltree] in
1053       begin
1054    (*        print_ftree deltree;
1055            Format.open_box 0;
1056            print_endline " ";
1057            print_stringlist pure_names;
1058            Format.force_newline ();
1059            Format.print_flush ();
1060  *)  *)
1061     [sigma]       let rednew = update_redord (slist_to_set pure_names) redord
1062   end       and connew = update_connections pure_names connections
1063         and unsolnew = update_list pure_names unsolved_list in
1064          (rednew,connew,unsolnew)
1065        end
1066      
1067    
 in  
 let apply_r2 fs ft rt sigma =  
 (*  print_endline "r2"; *)  
   compute_all rt fs ft sigma  
1068    
 in  
 let apply_r3 fs ft rt sigma =  
 (*  print_endline "r3";  *)  
   compute_all (List.tl fs) ft (List.tl rt) sigma  
1069    
 in  
 let apply_r4 fs ft rt sigma =  
 (*  print_endline "r4"; *)  
   compute_all rt ft fs sigma  
1070    
 in  
 let apply_r5 fs ft rt sigma =  
 (*  print_endline "r5"; *)  
  let v = (List.hd fs) in  
    let sigma_new = (compose sigma (v,ft)) in  
      compute_all (List.tl fs) rt rt sigma_new  
1071    
1072  in  let rec reduce_tree addr actual_node ftree beta_flag =
1073  let apply_r6 fs ft rt sigma =   match addr with
1074  (*  print_endline "r6"; *)    [] -> (ftree,Empty,actual_node,beta_flag)
1075   let v = (List.hd fs) in   |a::radd ->
1076    let sigma_new = (compose sigma (v,[])) in    match ftree with
1077      compute_all (List.tl fs) ft rt sigma_new      Empty ->
1078          print_endline "Empty purity tree";
1079          raise (Failure "Invalid argument")
1080       |NodeAt(_) ->
1081          print_endline "Atom purity tree";
1082           raise (Failure "Invalid argument")
1083       |NodeA(pos,strees) ->  
1084    (*       print_endline pos.name; *)
1085        (* the associated node occurs above f (or the empty address) and hence, is neither atom nor empty tree *)
1086      
1087         let nexttree = (Array.get strees (a-1)) in
1088           if (nonemptys strees 0 (Array.length strees)) < 2  then
1089             begin
1090    (*        print_endline "strees 1 or non-empties < 2"; *)
1091              let (ft,dt,an,bf) =  reduce_tree radd actual_node nexttree beta_flag in
1092               let nstrees = myset strees (a-1) ft in
1093    (*            print_endline ("way back "^pos.name); *)
1094                 (NodeA(pos,nstrees),dt,an,bf)
1095             end
1096           else  (* nonemptys >= 2 *)
1097              begin
1098    (*             print_endline "nonempties  >= 2 "; *)
1099               let (new_act,new_bf) =  
1100                if pos.pt = Beta then
1101                  (actual_node,true)
1102                else
1103                  ((pos.name),false)
1104                in
1105                let (ft,dt,an,bf) = reduce_tree radd new_act nexttree new_bf in  
1106                  if an = pos.name then
1107                    let nstrees = myset strees (a-1) Empty in
1108    (*                 print_endline ("way back assocnode "^pos.name); *)
1109                     (NodeA(pos,nstrees),nexttree,an,bf)
1110                  else  (* has been replaced / will be replaced below / above pos *)
1111                    let nstrees = myset strees (a-1) ft in
1112    (*                 print_endline ("way back "^pos.name); *)
1113                       (NodeA(pos,nstrees),dt,an,bf)
1114              end;;
1115    
1116    
1117    
1118    
 in  
 let apply_r7 fs ft rt sigma =  
 (*  print_endline "r7"; *)  
  let v = (List.hd fs)  
  and c1 = (List.hd rt)  
  and c2t =(List.tl rt) in  
   let sigma_new = (compose sigma (v,(ft @ [c1]))) in  
     compute_all (List.tl fs) [] c2t sigma_new  
1119    
 in  
 let apply_r8 fs ft rt sigma =  
 (*  print_endline "r8"; *)  
   compute_all rt [(List.hd fs)] (List.tl fs) sigma  
1120    
1121    
 in  
 let apply_r9 fs ft rt sigma =  
 (*  print_endline "r9"; *)  
  let v = (List.hd fs)  
  and (max,subst) = sigma in  
   let v_new = ("vnew"^(string_of_int max)) in  
     let sigma_new = (compose ((max+1),subst) (v,(ft @ [v_new]))) in  
       compute_all rt [v_new] (List.tl fs) sigma_new  
1122    
 in  
 let apply_r10 fs ft rt sigma =  
 (*  print_endline "r10"; *)  
  let x = List.hd rt in  
  compute_all fs (ft @ [x]) (List.tl rt) sigma  
1123    
1124    let rec purity ftree redord connections unsolved_list =
1125    
1126    let rec purity_reduction pr ftree redord connections unsolved_list =
1127           begin
1128    (*      Format.open_box 0;
1129            print_endline " ";
1130            print_purelist pr;
1131            Format.force_newline ();
1132            Format.print_flush ();
1133    *)
1134     match pr with
1135      [] -> (ftree,redord,connections,unsolved_list)
1136     |f::r ->
1137    (*   print_endline ("pure position "^(f.name)); *)
1138        let (ftnew,deltree,assocn,beta_flag) = reduce_tree f.address "" ftree false
1139        in
1140    (*     print_endline ("assoc node "^assocn); *)
1141         if assocn = "" then  
1142           (Empty,[],[],[])  (* should not occur in the final version *)
1143         else
1144           let (rednew,connew,unsolnew) = update_relations deltree redord connections unsolved_list in
1145           begin
1146    (*      Format.open_box 0;
1147            print_endline " ";
1148            print_pairlist connew;
1149            Format.force_newline ();      
1150            Format.print_flush ();
1151    *)
1152            if beta_flag = true then
1153             begin
1154    (*          print_endline "beta_flag true"; *)
1155             purity ftnew rednew connew unsolnew  
1156      (* new pure positions may occur; old ones may not longer exist *)
1157             end
1158            else
1159             purity_reduction r ftnew rednew connew unsolnew (* let's finish the old pure positions *)
1160           end
1161         end
1162      
1163  in  in
1164    if r_1 fs ft rt then    let flist,slist = List.split connections in
1165     let sigma_1_list = apply_r1 fs ft rt sigma in      let pr = collect_pure [ftree] (flist,slist) in
1166      sigma_1_list         purity_reduction pr ftree redord connections unsolved_list
1167    else  
1168    if r_2 fs ft rt then  
1169     let sigma_1_list = apply_r2 fs ft rt sigma in  
1170      sigma_1_list  let rec betasplit addr ftree redord connections unsolved_list =
1171    else     match ftree with
1172    if r_3 fs ft rt then       Empty  ->
1173     let sigma_1_list = apply_r3 fs ft rt sigma in  (*       print_endline "bsplit Empty tree";*)
1174      sigma_1_list         raise (Failure "Invalid argument")
1175    else      |NodeAt(_) ->
1176    if r_4 fs ft rt then  (*       print_endline "bsplit Atom tree";*)
1177     let sigma_1_list = apply_r4 fs ft rt sigma in         raise (Failure "Invalid argument")   (* the beta-node should actually occur! *)
1178      sigma_1_list      |NodeA(pos,strees) ->
1179    else       match addr with
1180    if r_5 fs ft rt then        [] ->    (* we are at the beta node under consideration *)
1181     let sigma_1_list = apply_r5 fs ft rt sigma in           let st1tree = (Array.get strees 0)
1182      sigma_1_list         and st2tree = (Array.get strees 1) in
1183    else          let (zw1red,zw1conn,zw1uslist) = update_relations st2tree redord connections unsolved_list
1184    if r_6 fs ft rt then          and (zw2red,zw2conn,zw2uslist) = update_relations st1tree redord connections unsolved_list in
1185     let sigma_1_list = apply_r6 fs ft rt sigma            ((NodeA(pos,[|st1tree;Empty|])),zw1red,zw1conn,zw1uslist),
1186     and sigma_2_list = apply_r10 fs ft rt sigma   in (* r10 always applicable *)            ((NodeA(pos,[|Empty;st2tree|])),zw2red,zw2conn,zw2uslist)
1187                                                      (*if r6 was *)       |f::rest ->
1188        if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *)          let nexttree  = Array.get strees (f-1) in
1189         let sigma_3_list = apply_r7 fs ft rt sigma in           let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) =
1190           (sigma_1_list @ sigma_2_list @ sigma_3_list)              betasplit rest nexttree redord connections unsolved_list in
1191        else  (*          let scopytrees = Array.copy strees in  *)
1192           (sigma_1_list @ sigma_2_list)               let zw1trees = myset strees (f-1) zw1ft
1193    else               and zw2trees = myset strees (f-1) zw2ft in
1194    if r_7 fs ft rt then  (* not r6 and r7 possible if z <> [] *)                 (NodeA(pos,zw1trees),zw1red,zw1conn,zw1uslist),(NodeA(pos,zw2trees),zw2red,zw2conn,zw2uslist)
1195     let sigma_1_list = apply_r7 fs ft rt sigma            
1196     and sigma_2_list = apply_r10 fs ft rt sigma in (* r10 always applicable *)  
1197                                                    (* if r7 was *)  
1198        (sigma_1_list @ sigma_2_list)  
1199    else  let split addr ftree redord connections unsolved_list =  
1200    if r_8 fs ft rt then      let  (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) =
1201      let sigma_1_list = apply_r8 fs ft rt sigma in       betasplit addr ftree redord connections unsolved_list in
1202        if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *)  (*   print_endline "betasp_out"; *)
1203         let sigma_2_list = apply_r10 fs ft rt sigma in    let ft1,red1,conn1,uslist1 =  purity zw1ft zw1red zw1conn zw1uslist in
1204           (sigma_1_list @ sigma_2_list)  (*   print_endline "purity_one_out"; *)
1205        else    let ft2,red2,conn2,uslist2 =  purity zw2ft zw2red zw2conn zw2uslist in
1206          sigma_1_list  (*        print_endline "purity_two_out"; *)
1207    else          (ft1,red1,conn1,uslist1),(ft2,red2,conn2,uslist2);;
1208    if r_9 fs ft rt then    
     let sigma_1_list = apply_r9 fs ft rt sigma in  
       if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *)  
        let sigma_2_list = apply_r10 fs ft rt sigma in  
          (sigma_1_list @ sigma_2_list)  
       else  
          sigma_1_list  
   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') *)  
     let sigma_1_list = apply_r10 fs ft rt sigma in  
       sigma_1_list  
   else  (* NO rule applicable *)  
    begin  
 (*    print_endline "FAIL BRANCH!!!"; *)  
       []   (* global failure unifier *)  
     end  
1209        
1210    (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Splitting end %%%%%%%%%%%%%%%%  *)
1211    
1212    
1213    
1214    
1215  let rec apply_subst subst us ns =  (* for wait labels we collect all solved atoms with pol=0 *)
1216   match us with  
1217     [] -> []  let rec collect_solved_O_At ftreelist slist =
1218      match ftreelist with
1219       [] ->
1220        []
1221    |f::r ->    |f::r ->
1222     if (is_var f) & (f<>ns) & (List.mem_assoc f subst) then (* don't apply atom instances!! *)      match f with
1223       (List.assoc f subst) @ (apply_subst subst r ns)       Empty ->    (* may become possible after purity *)
1224     else         collect_solved_O_At r slist
1225       f::(apply_subst subst r ns)     |NodeAt(pos) ->
1226         if ((List.mem (pos.name) slist) or (pos.pol = I)) then  (* recall slist is the unsolved list *)
1227           collect_solved_O_At r slist
1228         else
1229        (* here, we have pos solved and pos.pol = O) *)
1230           pos::(collect_solved_O_At r slist)
1231     | NodeA(pos,treearray) ->
1232        collect_solved_O_At ((Array.to_list treearray) @ r) slist
1233    
1234    
1235  let apply_univ sigma us ns=  
1236  (*  print_endline "apply old sigma"; *)  
1237   let (n,subst) = sigma in  let rec red_ord_block pname redord =
1238    if subst  = [] then   match redord with
1239     us    [] -> false
1240     |(f,fset)::r ->
1241      if ((f = pname) or (not (StringSet.mem pname fset))) then
1242       red_ord_block pname r
1243      else  
1244       true   (* then, we have (StringSet.mem pname fset) *)
1245    
1246    
1247    
1248    
1249    
1250    
1251    
1252    
1253    let rec check_wait_succ_LJ faddress ftree =
1254     match ftree with
1255      Empty -> raise (Failure "invalid argument")
1256     | NodeAt(pos) -> raise (Failure "invalid argument") (* we have an gamma_0 position or an or-formula *)
1257     | NodeA(pos,strees) ->
1258        match faddress with
1259         [] ->
1260           if pos.op = Or then
1261             match (strees.(0),strees.(1)) with
1262               (Empty,Empty) -> raise (Failure "Invalid argument: redundancies occur")
1263             |(Empty,_) -> (false,2)   (* determines the Orr2 rule *)
1264             |(_,Empty) -> (false,1)   (* determines the Orr1 ruke *)
1265             |(_,_)  -> (true,0)    (* wait-label is set *)
1266           else
1267            (false,0)
1268        |f::r ->
1269          if r = [] then
1270           if (pos.pt = Gamma) & ((nonemptys strees 0 (Array.length strees)) > 1)  then
1271            (true,0)             (* we are at a gamma position (exr) with one than one successor -- wait label in LJ*)
1272           else    
1273             check_wait_succ_LJ r (Array.get strees (f-1))
1274          else
1275             check_wait_succ_LJ r (Array.get strees (f-1))
1276    
1277    
1278    
1279    
1280    
1281    
1282    let blocked f po redord ftree connections slist logic calculus =
1283    (* print_endline ("Blocking check "^(f.name)); *)
1284     if (red_ord_block (f.name) redord) then
1285        begin
1286    (*     print_endline "wait-1 check positive"; *)
1287         true,0
1288        end
1289    else    else
1290     apply_subst subst us ns     if logic = "C" then
1291          false,0  (* ready, in C only redord counts *)
1292       else
1293        let pa_O = collect_solved_O_At [ftree] slist      (* solved atoms in ftree *)
1294        and po_test = (delete f po) in
1295         if calculus = "LJmc" then (* we provide dynamic wait labels for both sequent calculi *)
1296    (*       print_endline "wait-2 check"; *)
1297            if (f.st = Psi_0)  &  (f.pt <> PNull) &
1298               ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) then
1299              begin
1300    (*          print_endline "wait-2 positive"; *)
1301                true,0 (* wait_2 label *)
1302              end
1303            else
1304              begin
1305    (*          print_endline "wait-2 negative"; *)
1306                false,0
1307              end
1308          else  (* calculus is supposed to be LJ *)
1309           if calculus = "LJ" then
1310            if  ((f.st = Phi_0)  & ((f.op=Neg) or (f.op=Imp)) &
1311                 ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test))
1312                )
1313             (* this would cause an impl or negl rule with an non-empty succedent *)
1314                then
1315                 if (f.op=Neg) then
1316                   true,0
1317                 else  (* (f.op=Imp) *)
1318                  (* In case of an impl rule on A => B, the wait_label must NOT be set
1319                     iff all succedent formulae depend exclusively on B. For this, we
1320                     perform a split operation and determine, if in the A-subgoal
1321                     all succedent formulae are pure, i.e.~have been deleted from treds.
1322                     Otherwise, in case of A-dependent succedent formulae, the
1323                     wait_label must be set.
1324                   *)
1325                  let slist_fake = delete f.name slist in
1326                  let  ((zw1ft,zw1red,zw1conn,zw1uslist),_) =
1327                   betasplit (f.address) ftree redord connections slist_fake in  
1328                    let ft1,_,_,uslist1 =  purity zw1ft zw1red zw1conn zw1uslist in
1329    (*                   print_endline "wait label purity_one_out"; *)
1330                     let ft1_root = (List.hd (List.tl (tpredsucc f ft1))) in
1331    (*                 print_endline ("wait-root "^(ft1_root.name)); *)
1332                     let po_fake = compute_open [ft1] uslist1 in
1333                     let po_fake_test = delete ft1_root po_fake
1334                     and pa_O_fake = collect_solved_O_At [ft1] uslist1 in
1335    (*                  print_purelist (po_fake_test @ pa_O_fake); *)
1336                      if ((pa_O_fake <> []) or (List.exists (fun x -> x.pol = O) po_fake_test)) then
1337                       true,0  
1338                      else
1339                       false,0  
1340             else
1341              if ((f.pol=O) & ((f.st=Gamma_0) or (f.op=Or))) then
1342               let (bool,orr_flag) = check_wait_succ_LJ f.address ftree in
1343                 (bool,orr_flag)    
1344            (* here is determined if orr1 or orr2 will be performed, provided bool=false) *)
1345            (* orr_flag can be 1 or 2 *)
1346              else
1347               false,0
1348           else
1349            raise (Failure "Invalid argument: calculus should be LJmc or LJ")
1350    
1351    
1352    let rec select_pos search_po po redord ftree connections slist logic calculus =
1353     match search_po with
1354       [] ->
1355        failwith "deadlock"
1356      |f::r ->  (* there exist an open position *)
1357        let (bool,orr_flag) = (blocked f po redord ftree connections slist logic calculus) in
1358        if (bool = true) then
1359         select_pos r po redord  ftree connections slist logic calculus
1360        else
1361         (f,orr_flag)
1362    
1363    
1364    
1365    
1366    (* total corresponds to tot in the thesis,
1367       tot simulates the while-loop, solve is the rest *)
1368    
1369    
1370    let rec total  ftree redord connections csigmaQ slist logic calculus =
1371    
1372    let rec tot  ftree redord connections po slist =
1373    
1374    let rec solve  ftree redord connections p po slist (pred,succs) orr_flag =  
1375       let newslist = delete (p.name) slist in
1376         let rback =
1377           if p.st = Gamma_0 then
1378            begin
1379    (*       print_endline "that's the gamma rule";  *)
1380             [(build_rule pred p csigmaQ orr_flag calculus)]
1381            end
1382             else
1383              []
1384           in    
1385    (*        print_endline "gamma check finish";  *)
1386            let pnew =  
1387             if p.pt <> Beta then
1388               succs @ (delete  p po)
1389             else
1390              po
1391            in
1392             match p.pt with
1393               Gamma ->
1394                rback @ (tot  ftree redord connections pnew newslist)
1395             | Psi   ->
1396                if p.op = At then
1397                 let succ = List.hd succs in
1398                   rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag)  (* solve atoms immediately *)
1399                else
1400                 rback @ (tot  ftree redord connections pnew newslist)
1401             | Phi   ->
1402                if p.op = At then
1403                 let succ = List.hd succs in
1404                   rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag)  (* solve atoms immediately *)
1405                else
1406                 rback @ (tot  ftree redord connections pnew newslist)
1407             | PNull ->
1408                 let c = select_connection (p.name) connections slist in
1409                   if c = ("none","none") then
1410                     rback @ (tot  ftree redord connections pnew newslist)
1411                   else
1412                    rback @ [(build_rule p p csigmaQ orr_flag calculus)] (* one possibility of recursion end *)
1413             | Alpha ->
1414                 rback @ ((build_rule p p csigmaQ orr_flag calculus)::(tot  ftree redord connections pnew newslist))
1415             | Delta ->
1416                let sp = List.hd succs in
1417                  rback @ ((build_rule p sp csigmaQ orr_flag calculus)::(tot ftree redord connections pnew newslist))
1418             | Beta  ->  
1419    (*             print_endline "split_in"; *)
1420                let (ft1,red1,conn1,uslist1),(ft2,red2,conn2,uslist2) =
1421                    split (p.address) ftree redord connections newslist in  
1422    (*           print_endline "split_out"; *)
1423                 let p1 = total  ft1 red1 conn1 csigmaQ uslist1 logic calculus in
1424    (*           print_endline "compute p1 out";          *)
1425                  let p2 = total  ft2 red2 conn2 csigmaQ uslist2 logic calculus in
1426    (*           print_endline "compute p2 out";          *)
1427                     rback @ [(build_rule p p csigmaQ orr_flag calculus)] @ p1 @ p2  (* second possibility of recursion end *)
1428    in      
1429     (try
1430      let (p,orr_flag) = select_pos po po redord ftree connections slist logic calculus
1431       in
1432    (*    print_endline ((p.name)^" "^(string_of_int orr_flag)); *)
1433         let predsuccs = tpredsucc p ftree in
1434          let pred = List.hd predsuccs
1435          and succs = List.tl predsuccs in
1436           let redpo = update (p.name) redord in   (* deletes the entry (p,psuccset) from the redord *)
1437           let rednew =
1438             if (p.pt = Delta) then                 (* keep the tree ordering for the successor position only *)
1439              let psucc = List.hd succs in
1440               let ppsuccs = tpredsucc psucc ftree in  
1441                 let pre = List.hd ppsuccs
1442                 and sucs = List.tl ppsuccs in
1443                  replace_ordering (psucc.name) sucs redord (* union the succsets of psucc *)
1444             else
1445              redpo
1446         in
1447    (*      print_endline "update ok"; *)
1448         solve ftree rednew connections p po slist (pred,succs) orr_flag
1449       with
1450        Failure("deadlock") ->
1451          failwith "not_reconstructible"  (* this possibility should of course be eliminated *)
1452      )
1453    
1454    in
1455    let po  = compute_open [ftree] slist in
1456      tot ftree redord connections po slist;;
1457    
1458    
1459    
1460    
1461    
1462    let reconstruct ftree redord sigmaQ connections logic calculus =  
1463      let complete_sigmaQ = build_sigmaQ sigmaQ ftree in
1464       let  (newroot_name,unsolved_list) =  build_unsolved ftree in
1465        let redord2 = (update newroot_name redord) in   (* otherwise we would have a deadlock *)
1466          let (init_tree,init_redord,init_connections,init_unsolved_list) =
1467             purity ftree redord2 connections unsolved_list in
1468              total init_tree init_redord init_connections complete_sigmaQ
1469                    init_unsolved_list logic calculus
1470      
1471    
 let tunify us ut ns nt sigma =    
  let s = (apply_univ sigma us ns)  
  and t = (apply_univ sigma ut nt) in  
 (* print_endline "go compute"; *)  
   compute_all s [] t sigma  
1472    
1473    
1474    
1475  let stringunify ext_atom try_one sigma logic =  
1476    
1477    
1478    
1479    
1480    
1481    
1482    
1483    
1484    
1485    
1486    
1487    (************ T-STRING UNIFICATION *********************************)
1488    
1489    
1490    
1491    let stringunify ext_atom try_one eqlist logic =
1492   if logic = "C" then   if logic = "C" then
1493    [sigma]    ((0,[]),[])
1494   else   else
1495    let us  = (Array.to_list ext_atom.aprefix)    let us  = ext_atom.aprefix
1496    and ut  = (Array.to_list try_one.aprefix)    and ut  = try_one.aprefix
1497    and ns = ext_atom.aname    and ns = ext_atom.aname
1498    and nt = try_one.aname in    and nt = try_one.aname in
1499    tunify us ut ns nt sigma    Jtunify.do_stringunify us ut ns nt eqlist
1500    
1501    
1502    
# Line 799  Line 1557 
1557    
1558    
1559    
 let rec copy_and_rename_tree last_tree replace_n predecessor ordering pos_n mult subst_list =  
1560    
1561   let rec rename_subtrees tree_list nposition s_ordering s_pos_n nsubst_list =    
1562    
1563    
1564    
1565    
1566    
1567    let rec append_orderings list_of_lists =
1568      match list_of_lists with
1569       [] ->  
1570         []
1571      |f::r ->
1572       f @ (append_orderings r)
1573    
1574    
1575    let rec union_orderings first_orderings =
1576      match first_orderings with
1577        [] ->
1578         StringSet.empty
1579       |(pos,fset)::r ->
1580         StringSet.union (StringSet.add pos fset) (union_orderings r)
1581    
1582    
1583    let rec select_orderings add_orderings =
1584     match add_orderings with
1585       [] -> []
1586      |f::r ->
1587       (List.hd f)::select_orderings r
1588      
1589    
1590    let combine_ordering_list add_orderings pos_name =
1591      let first_orderings = select_orderings add_orderings in
1592       let pos_succs = union_orderings first_orderings in
1593        let rest_orderings  = append_orderings add_orderings in
1594         (pos_name,pos_succs)::rest_orderings
1595        
1596    
1597    
1598    
1599    
1600    
1601    
1602    let rec copy_and_rename_tree last_tree replace_n pos_n mult subst_list =
1603    
1604     let rec rename_subtrees tree_list nposition s_pos_n nsubst_list =  
1605      match tree_list with      match tree_list with
1606       [] -> ([||],s_ordering,s_pos_n)       [] -> ([||],[],s_pos_n)
1607      | f::r ->      | f::r ->
1608       let (f_subtree,f_ordering,f_pos_n) =       let (f_subtree,f_ordering,f_pos_n) =
1609         copy_and_rename_tree f replace_n nposition s_ordering s_pos_n  mult nsubst_list in         copy_and_rename_tree f replace_n s_pos_n  mult nsubst_list in
1610        let (r_subtrees,r_ordering,r_pos_n) = rename_subtrees r nposition f_ordering f_pos_n nsubst_list in        let (r_subtrees,r_ordering_list,r_pos_n) = rename_subtrees r nposition f_pos_n nsubst_list in
1611          ((Array.append [|f_subtree|] r_subtrees),r_ordering,r_pos_n)          ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n)
1612    
1613   in   in
1614   match last_tree with     match last_tree with  
1615    Empty -> raise (Failure "Invalid argument")    Empty -> raise (Failure "Invalid argument")
1616    |NodeAt(position) ->   (* can never be a Gamma_0 position -> no replacements *)    |NodeAt(position) ->   (* can never be a Gamma_0 position -> no replacements *)
1617        let (nposition,npos_n,_) = update_position position (pos_n+1) replace_n subst_list mult in        let (nposition,npos_n,_) = update_position position (pos_n+1) replace_n subst_list mult in
1618          ((NodeAt(nposition)),((predecessor.name,nposition.name)::ordering),npos_n)          ((NodeAt(nposition)),[(nposition.name,StringSet.empty)],npos_n)
1619    |NodeA(position, suctrees) ->    |NodeA(position, suctrees) ->
1620        let (nposition,npos_n,nsubst_list) = update_position position (pos_n+1) replace_n subst_list mult in        let (nposition,npos_n,nsubst_list) = update_position position (pos_n+1) replace_n subst_list mult in
1621          let (new_suctrees, new_ordering, new_pos_n) =          let (new_suctrees, new_ordering_list, new_pos_n) =
1622            rename_subtrees (Array.to_list suctrees) nposition ordering npos_n nsubst_list in            rename_subtrees (Array.to_list suctrees) nposition npos_n nsubst_list in
1623             ((NodeA(nposition,new_suctrees)),((predecessor.name,nposition.name)::new_ordering),new_pos_n)             let new_ordering = combine_ordering_list new_ordering_list (nposition.name) in
1624               ((NodeA(nposition,new_suctrees)),new_ordering,new_pos_n)
1625        
1626    
1627    
1628    
1629    
1630    (* we construct for each pos a list orderings representing and correspondning to the array of succtrees *)
1631    
1632    
1633  let rec add_multiplicity ftree ordering pos_n  mult =  let rec add_multiplicity ftree pos_n  mult logic =
1634    
1635    let rec parse_subtrees tree_list s_ordering s_pos_n =      let rec parse_subtrees tree_list s_pos_n =  
1636      match tree_list with      match tree_list with
1637       [] -> ([||],s_ordering,s_pos_n)       [] -> ([||],[],s_pos_n)
1638      |f::r ->      |f::r ->
1639       let (f_subtree,f_ordering,f_pos_n) = add_multiplicity f s_ordering s_pos_n  mult in       let (f_subtree,f_ordering,f_pos_n) = add_multiplicity f s_pos_n  mult logic in
1640        let (r_subtrees,r_ordering,r_pos_n) = parse_subtrees r f_ordering f_pos_n in        let (r_subtrees,r_ordering_list,r_pos_n) = parse_subtrees r f_pos_n in
1641          ((Array.append [|f_subtree|] r_subtrees),r_ordering,r_pos_n)          ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n)
1642            
1643    in    in
1644    match ftree with      match ftree with  
1645     Empty -> raise (Failure "Invalid argument")     Empty -> raise (Failure "Invalid argument")
1646     |NodeAt(_) -> (ftree, ordering, pos_n)     |NodeAt(pos) -> (ftree,[(pos.name,StringSet.empty)],pos_n)
1647     |NodeA(pos,suctrees) ->     |NodeA(pos,suctrees) ->
1648      let (new_suctrees, new_ordering, new_pos_n) = parse_subtrees (Array.to_list suctrees) ordering pos_n in      let (new_suctrees, new_ordering_list, new_pos_n) = parse_subtrees (Array.to_list suctrees) pos_n in
1649          if (((pos.pt = Phi) & (pos.op <> At))  (* no explicit atom-instances *)          if (((pos.pt = Phi) & (((pos.op <> At) & (logic="J")) or ((pos.op = All) & (logic = "C"))))
1650              (* no explicit atom-instances *)
1651          or ((pos.pt = Gamma) & (pos.st <> Phi_0))) then   (* universal quantifiers are copied *)          or ((pos.pt = Gamma) & (pos.st <> Phi_0))) then   (* universal quantifiers are copied *)
1652                                                                  (* at their Phi positions *)                                                                  (* at their Phi positions *)
1653           let replace_n = (List.length pos.address)  (* points to the following argument in the array_of_address *)           let replace_n = (List.length pos.address)  (* points to the following argument in the array_of_address *)
1654           and last = (Array.length new_suctrees) - 1 in           and last = (Array.length new_suctrees) - 1 in (* array first element has index 0 *)
1655            let last_tree = new_suctrees.(last) in            let last_tree = new_suctrees.(last) in
1656             let (new_tree,final_ordering,final_pos_n) =             let (add_tree,add_ordering,final_pos_n) =
1657               copy_and_rename_tree last_tree replace_n  pos new_ordering new_pos_n mult [] in              copy_and_rename_tree last_tree replace_n new_pos_n mult [] in
1658              let final_suctrees = Array.append new_suctrees [|new_tree|] in               let final_suctrees = Array.append new_suctrees [|add_tree|]
1659               ((NodeA(pos,final_suctrees)),final_ordering,final_pos_n)               and add_orderings = List.append new_ordering_list [add_ordering] in
1660                  let final_ordering = combine_ordering_list add_orderings (pos.name) in
1661                   ((NodeA(pos,final_suctrees)),final_ordering,final_pos_n)
1662          else                else      
1663           ((NodeA(pos,new_suctrees)),new_ordering,new_pos_n)           let final_ordering = combine_ordering_list new_ordering_list (pos.name) in
1664               ((NodeA(pos,new_suctrees)),final_ordering,new_pos_n)
1665    
1666    
1667    
# Line 932  Line 1739 
1739     check_ext_list ext_list fail_set atom_sets     check_ext_list ext_list fail_set atom_sets
1740                
1741    
1742  let rec ext_partners con path ext_atom atom_sets =  
1743    let rec ext_partners con path ext_atom (reduction_partners,extension_partners) atom_sets =
1744   match con with   match con with
1745    [] -> AtomSet.empty    [] ->
1746       (reduction_partners,extension_partners)
1747   |f::r ->   |f::r ->
1748     let (a,b) = f in     let (a,b) = f in
1749      if List.mem ext_atom [a;b] then      if List.mem ext_atom [a;b] then
1750       let ext_partner =         let ext_partner =  
1751         if ext_atom = a then b else a         if ext_atom = a then b else a
1752       in       in
1753        if (AtomSet.mem ext_partner path) or        let (new_red_partners,new_ext_partners) =
1754           (check_alpha_relation ext_partner path atom_sets) then  (* force reduction steps first *)
1755           AtomSet.add ext_partner (ext_partners r path ext_atom atom_sets)         if (AtomSet.mem ext_partner path) then
1756        else           ((AtomSet.add ext_partner reduction_partners),extension_partners)
1757          ext_partners r path ext_atom atom_sets         else
1758      else          if (check_alpha_relation ext_partner path atom_sets) then
1759        ext_partners r path ext_atom atom_sets           (reduction_partners,(AtomSet.add ext_partner extension_partners))
1760            else
1761             (reduction_partners,extension_partners)
1762          in  
1763            ext_partners r path ext_atom (new_red_partners,new_ext_partners) atom_sets
1764        else
1765            ext_partners r path ext_atom (reduction_partners,extension_partners) atom_sets
1766            
1767            
1768    
 let rec print_set_list set_list =  
  match set_list with  
   [] -> ""  
  |f::r ->  
    (f.aname)^" "^(print_set_list r)  
1769    
1770  let print_set  set =    
1771   let set_list = AtomSet.elements set in  
1772    if set_list = [] then "empty"  let rec transitive_closure addset const ordering =  
1773    else    match ordering with
1774     print_set_list set_list      [] ->
1775         []
1776      |(pos,fset)::r ->
1777       if (pos = const) or (StringSet.mem const fset) then
1778        (pos,(StringSet.union fset addset)) :: (transitive_closure addset const r)
1779       else
1780        (pos,fset)::(transitive_closure addset const r)
1781    
1782    
1783    let rec search_set var ordering =
1784     match ordering with
1785      [] ->
1786       raise (Failure "Invalid argument")
1787     |(pos,fset)::r ->
1788       if pos = var then
1789         StringSet.add pos fset
1790       else
1791         search_set var r
1792    
1793    
1794    let add_sets var const ordering =
1795     let addset =  search_set var ordering  in
1796      transitive_closure addset const ordering
1797    
1798    
1799    
1800  let rec add_arrows (v,vlist) ordering =  let rec add_arrows (v,vlist) ordering =
1801   match vlist with   match vlist with
1802    [] -> []    [] -> ordering
1803   |f::r ->   |f::r ->
1804     if ((String.get f 0)='c') & (not (List.mem (f,v) ordering)) then     if ((String.get f 0)='c') then  
1805       (f,v)::(add_arrows (v,r) ordering)       let new_ordering = add_sets v f ordering in
1806           add_arrows (v,r) new_ordering
1807     else     else
1808       add_arrows (v,r) ordering       add_arrows (v,r) ordering
1809      
1810      
1811    
1812    
1813  let rec check_subst subst ordering atom_rel =  let rec check_subst subst ordering atom_rel =
1814   match subst with   match subst with
1815    [] -> ordering    [] -> ordering
# Line 984  Line 1818 
1818        or (List.exists (fun (x,_,_) -> (x.aname = v)) atom_rel) then   (* no reduction ordering at atoms *)        or (List.exists (fun (x,_,_) -> (x.aname = v)) atom_rel) then   (* no reduction ordering at atoms *)
1819      (check_subst r ordering atom_rel)        (check_subst r ordering atom_rel)  
1820     else     else
1821      (add_arrows (v,vlist) ordering) @ (check_subst r ordering atom_rel)      let next_ordering = add_arrows (v,vlist) ordering in
1822          check_subst r next_ordering atom_rel
1823            
1824    
1825    
1826  let add_subst tau ordering atom_rel =  let add_subst sigma ordering atom_rel =
1827   let (n,subst) = tau in   let (n,subst) = sigma in
1828     check_subst subst ordering atom_rel     check_subst subst ordering atom_rel
1829    
1830    
1831    
1832  let path_checker atom_rel atom_sets ordering logic =    let path_checker atom_rel atom_sets init_ordering logic =  
1833    
1834    let con = connections atom_rel [] in    let con = connections atom_rel [] in
1835  (*   print_endline "";  (*   print_endline "";
1836     print_endline ("number of connections: "^(string_of_int (List.length con)));     print_endline ("number of connections: "^(string_of_int (List.length con)));
1837  *)  *)
1838    
1839    
1840  (* sigma global in provable ?? *)     let rec provable path closed (ordering,reduction_ordering) eqlist sigma =
    let rec provable path closed sigma ordering =  
1841        
1842       let rec check_unifiers ext_atom try_one sigmalist =       let rec check_connections (reduction_partners,extension_partners) ext_atom =
1843        match sigmalist with        let try_one =
1844         [] -> failwith "fail1"         if reduction_partners = AtomSet.empty then
1845        |tau::rest ->          if extension_partners = AtomSet.empty then
1846               failwith "fail2"
1847            else
1848              AtomSet.choose extension_partners
1849           else
1850           (* force reduction steps always first!! *)
1851             AtomSet.choose reduction_partners
1852          in
1853    (*         print_endline ("connection partner "^(try_one.aname)); *)
1854    (*       print_endline ("partner path "^(print_set path));
1855    *)
1856          (try          (try
1857          let new_ordering = add_subst tau ordering atom_rel in           let (new_sigma,new_eqlist) =  stringunify ext_atom try_one eqlist logic in
1858           let new_closed = AtomSet.add ext_atom closed in              let new_ordering = add_subst new_sigma ordering atom_rel in
1859             let (subst,next_ordering,subproof) =  (*           print_endline ("make reduction ordering "^((string_of_int (List.length new_ordering)))); *)
1860               let new_closed = AtomSet.add ext_atom closed in  
1861                let (next_ordering,next_eqlist,next_sigma,subproof) =
1862               if AtomSet.mem try_one path then               if AtomSet.mem try_one path then
1863                let (tau_1,nordering,p0) =                   provable path new_closed (ordering,new_ordering) new_eqlist new_sigma
1864                   provable path new_closed tau new_ordering in                       (* always use old tree ordering for recursion *)
                   (tau_1,nordering,p0)  
1865               else               else
1866                let new_path = AtomSet.add ext_atom path                let new_path = AtomSet.add ext_atom path
1867                and extension = AtomSet.add try_one AtomSet.empty in                and extension = AtomSet.add try_one AtomSet.empty in
1868                 let (tau_1,nordering,p1) =                 let (nordering,neqlist,nsigma,p1) =
1869                   provable new_path extension tau new_ordering in                   provable new_path extension (ordering,new_ordering) new_eqlist new_sigma in  
1870                   let (tau_2,nnordering,p2) =                   let (nnordering,nneqlist,nnsigma,p2) =
1871                     provable path new_closed tau_1 nordering in                     provable path new_closed (ordering,nordering) neqlist nsigma in
1872                      (tau_2,nnordering, (p1 @ p2))                      (nnordering,nneqlist,nnsigma,(p1 @ p2))
1873        (* first the extension subgoals = depth first; then other subgoals in same clause *)        (* first the extension subgoals = depth first; then other subgoals in same clause *)
1874             in             in
1875              (subst,next_ordering,(((ext_atom.aname),(try_one.aname))::subproof))              (next_ordering,next_eqlist,next_sigma,(((ext_atom.aname),(try_one.aname))::subproof))
          with  
            Failure("fail3next") ->                   (* go to next unifier *)  
             print_endline "fail3next";  
             check_unifiers ext_atom try_one rest  
          | Failure("fail3skip") ->                   (* go to next connection  -> fail1 *)  
             print_endline "fail3skip";          
             check_unifiers ext_atom try_one [])  
      in    
   
      let rec check_connections ext_partners ext_atom  =    
       if ext_partners = AtomSet.empty then failwith "fail2"  
       else  
        let try_one = AtomSet.choose ext_partners in  
         let try_set = AtomSet.add try_one AtomSet.empty in        (* try_set consisting of one atom *)  
          print_endline ("connection partner "^(try_one.aname));  
 (*       print_endline ("partner path "^(print_set path));  
 *)  
         (try  
          let sigmalist = stringunify ext_atom try_one sigma logic in  
            check_unifiers ext_atom try_one sigmalist  
1876           with Failure("fail1") ->           with Failure("fail1") ->
1877  (*          print_endline ("new connection for "^(ext_atom.aname)); *)  (*          print_endline ("new connection for "^(ext_atom.aname)); *)
1878             print_endline ("fail1");  (*            print_endline ("fail1"); *)
1879             check_connections (AtomSet.diff ext_partners try_set) ext_atom)              check_connections ((AtomSet.remove try_one reduction_partners),
1880                                   (AtomSet.remove try_one extension_partners)
1881                                  ) ext_atom
1882            )
1883    
1884       in       in
1885         let rec check_extension  extset =
 (* failflag says if the current subgoals -- including recursion through fail2 -- *)  
 (* had ever any connections in ext_partners. If so, then backtracking over other *)  
 (* tunifiers of the actual entry connection is required: failwith fail3. *)  
 (* Otherwise, we can cut the search  and go directly to a new entry connection: failwith fail1. *)  
      let rec check_extension  extset failflag =  
1886        if extset = AtomSet.empty then        if extset = AtomSet.empty then
1887         if failflag = true then           failwith "fail1"             (* go directly to a new entry connection *)
          failwith "fail3next"           (* try other tunifiers of the actual entry connection *)  
        else  
          failwith "fail3skip"             (* go directly to a new entry connection *)  
1888        else        else
1889         let select_one = AtomSet.choose extset in         let select_one = AtomSet.choose extset in
1890          print_endline ("extension literal "^(select_one.aname));  (*        print_endline ("extension literal "^(select_one.aname)); *)
1891  (*        print_endline ("extension path "^(print_set path));*)  (*        print_endline ("extension path "^(print_set path));*)
1892          let ext_partners = ext_partners con path select_one atom_sets in          let (reduction_partners,extension_partners) =
1893           let newflag =            ext_partners con path select_one (AtomSet.empty,AtomSet.empty) atom_sets in
1894            if (failflag = true) or (ext_partners <> AtomSet.empty) then          (try
1895             true             check_connections (reduction_partners,extension_partners) select_one
           else  
            false  
         in  
          (try  
            check_connections ext_partners select_one  
1896            with Failure("fail2") ->            with Failure("fail2") ->
1897  (*         print_endline ("no connections for subgoal "^(select_one.aname)); *)  (*         print_endline ("no connections for subgoal "^(select_one.aname)); *)
1898             print_endline ("fail2");  (*           print_endline ("fail2"); *)
1899             let fail_ext_set = fail_ext_set select_one extset atom_sets in             let fail_ext_set = fail_ext_set select_one extset atom_sets in
1900             check_extension fail_ext_set newflag)             check_extension fail_ext_set
1901            )
1902    
1903       in       in
     
1904       let extset = extset atom_sets path closed in       let extset = extset atom_sets path closed in
1905        if extset = AtomSet.empty then (sigma,ordering,[])        if extset = AtomSet.empty then
1906            (reduction_ordering,eqlist,sigma,[])
1907        else        else
1908          check_extension extset false          check_extension extset
1909    in        in    
1910     provable AtomSet.empty AtomSet.empty (1,[]) ordering     provable AtomSet.empty AtomSet.empty (init_ordering,[]) [] (1,[])
1911    
1912    
1913    
# Line 1110  Line 1928 
1928    
1929    
1930    
   
1931  let rec make_atom_sets atom_rel =  let rec make_atom_sets atom_rel =
1932   match atom_rel with   match atom_rel with
1933    [] -> []    [] -> []
# Line 1131  Line 1948 
1948       |_,[] -> raise (Failure "Invalid argument")       |_,[] -> raise (Failure "Invalid argument")
1949       | (f1::r1),(f2::r2) ->       | (f1::r1),(f2::r2) ->
1950        if f1 = f2 then        if f1 = f2 then
1951          predecessor r1 r2 (suctrees.(f1-1))          predecessor r1 r2 (suctrees.(f1-1))
1952        else        else
1953          position.pt                position.pt      
1954    
# Line 1173  Line 1990 
1990    
1991  let atom_record position prefix =  let atom_record position prefix =
1992   let aname = (position.name) in   let aname = (position.name) in
1993    let aprefix = (Array.append prefix [|aname|]) in (* atom position is last element in prefix *)    let aprefix = (List.append prefix [aname]) in (* atom position is last element in prefix *)
1994     let (aop,aterms) = (dest_atom (position.label)) in     let (aop,aterms) = (dest_atom (position.label)) in
1995       ({aname=aname; aaddress=(position.address); aprefix=aprefix; apredicate=aop;         ({aname=aname; aaddress=(position.address); aprefix=aprefix; apredicate=aop;  
1996         apol=(position.pol); ast=(position.st); aarguments=aterms})         apol=(position.pol); ast=(position.st); aarguments=aterms})
# Line 1191  Line 2008 
2008      let treelist = Array.to_list suctrees in      let treelist = Array.to_list suctrees in
2009       let prefix_element =       let prefix_element =
2010        if List.mem (position.st) [Psi_0;Phi_0] then        if List.mem (position.st) [Psi_0;Phi_0] then
2011         [|(position.name)|]         [(position.name)]
2012        else        else
2013         [||]         []
2014       in       in
2015        select_atoms_treelist treelist (Array.append prefix prefix_element)        select_atoms_treelist treelist (List.append prefix prefix_element)
2016    
2017   in     in  
2018   match treelist with   match treelist with
# Line 1208  Line 2025 
2025    
2026    
2027  let prepare_prover ftree =    let prepare_prover ftree =  
2028    let alist = select_atoms_treelist [ftree] [||] in    let alist = select_atoms_treelist [ftree] [] in
2029      compute_atomlist_relations alist ftree alist      compute_atomlist_relations alist ftree alist
2030    
2031    
# Line 1261  Line 2078 
2078    
2079    
2080    
2081  let rec build_ftree (variable,old_term) pol stype address pos_n predecessor =  let rec build_ftree (variable,old_term) pol stype address pos_n =
2082   let pos_name = make_position_name stype pos_n in   let pos_name = make_position_name stype pos_n in
2083    let term = check_subst_term (variable,old_term) pos_name stype in    let term = check_subst_term (variable,old_term) pos_name stype in
2084      if JLogic.is_and_term term then      if JLogic.is_and_term term then
# Line 1273  Line 2090 
2090            Alpha,Alpha_1,Alpha_2            Alpha,Alpha_1,Alpha_2
2091         in         in
2092          let position = {name=pos_name; address=address; op=And; pol=pol; pt=ptype; st=stype; label=term} in          let position = {name=pos_name; address=address; op=And; pol=pol; pt=ptype; st=stype; label=term} in
2093           let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) position in           let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in
2094            let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])            let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])
2095                                                                      (posn_left+1) position in                                                                      (posn_left+1) in
2096               let (succ_left,whole_left) = List.hd ordering_left
2097               and (succ_right,whole_right) = List.hd ordering_right in
2098               let pos_succs =
2099                (StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)))
2100               in
2101            (NodeA(position,[|subtree_left;subtree_right|]),            (NodeA(position,[|subtree_left;subtree_right|]),
2102             (predecessor.name,position.name)::(ordering_left@ordering_right),               ((position.name,pos_succs)::(ordering_left @ ordering_right)),
2103             posn_right             posn_right
2104            )            )
2105    else    else
2106     if JLogic.is_or_term term then     if JLogic.is_or_term term then
# Line 1290  Line 2112 
2112          Beta,Beta_1,Beta_2          Beta,Beta_1,Beta_2
2113       in       in
2114        let position = {name=pos_name; address=address; op=Or; pol=pol; pt=ptype; st=stype; label=term} in        let position = {name=pos_name; address=address; op=Or; pol=pol; pt=ptype; st=stype; label=term} in
2115         let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) position in         let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in
2116          let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])          let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])
2117                                                                    (posn_left+1) position in                                                                    (posn_left+1) in
2118               let (succ_left,whole_left) = List.hd ordering_left
2119               and (succ_right,whole_right) = List.hd ordering_right in
2120               let pos_succs =
2121                 StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in
2122            (NodeA(position,[|subtree_left;subtree_right|]),            (NodeA(position,[|subtree_left;subtree_right|]),
2123             (predecessor.name,position.name)::(ordering_left@ordering_right),               ((position.name),pos_succs) :: (ordering_left @ ordering_right),
2124             posn_right             posn_right
2125            )            )
2126     else     else
# Line 1310  Line 2136 
2136        let sposition = {name=pos_name; address=address; op=Imp; pol=pol; pt=ptype_0; st=stype; label=term}        let sposition = {name=pos_name; address=address; op=Imp; pol=pol; pt=ptype_0; st=stype; label=term}
2137        and position = {name=pos2_name; address=address@[1]; op=Imp; pol=pol; pt=ptype; st=stype_0; label=term} in        and position = {name=pos2_name; address=address@[1]; op=Imp; pol=pol; pt=ptype; st=stype_0; label=term} in
2138         let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])         let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])
2139                                                                (pos_n+2) position in                                                                (pos_n+2) in
2140          let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[1;2])          let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[1;2])
2141                                                                    (posn_left+1) position in                                                                    (posn_left+1) in
2142             let (succ_left,whole_left) = List.hd ordering_left
2143             and (succ_right,whole_right) = List.hd ordering_right in
2144              let pos_succs =
2145                StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in
2146               let pos_ordering = (position.name,pos_succs) :: (ordering_left @ ordering_right) in
2147            (NodeA(sposition,[|NodeA(position,[|subtree_left;subtree_right|])|]),            (NodeA(sposition,[|NodeA(position,[|subtree_left;subtree_right|])|]),
2148             [(predecessor.name,sposition.name);(sposition.name,position.name)]@(ordering_left@ordering_right),               ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
2149             posn_right             posn_right
2150            )            )
2151     else     else
# Line 1330  Line 2161 
2161        let sposition = {name=pos_name; address=address; op=Neg; pol=pol; pt=ptype_0; st=stype; label=term}        let sposition = {name=pos_name; address=address; op=Neg; pol=pol; pt=ptype_0; st=stype; label=term}
2162        and position = {name=pos2_name; address=address@[1]; op=Neg; pol=pol; pt=ptype; st=stype_0; label=term} in        and position = {name=pos2_name; address=address@[1]; op=Neg; pol=pol; pt=ptype; st=stype_0; label=term} in
2163         let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])         let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])
2164                                                                   (pos_n+2) position in                                                                   (pos_n+2) in
2165             let (succ_left,whole_left) = List.hd ordering_left in
2166              let pos_succs =
2167                StringSet.add succ_left whole_left in
2168                 let pos_ordering = (position.name,pos_succs) :: ordering_left in
2169            (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]),            (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]),
2170             [(predecessor.name,sposition.name);(sposition.name,position.name)]@(ordering_left),             ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
2171             posn_left             posn_left
2172            )            )
2173    
2174     else     else
2175     if JLogic.is_exists_term term then     if JLogic.is_exists_term term then
2176      let v,s,t = JLogic.dest_exists term in  (* s is type of v and will be supressed here *)      let v,s,t = JLogic.dest_exists term in  (* s is type of v and will be supressed here *)
# Line 1345  Line 2181 
2181          Delta,Delta_0          Delta,Delta_0
2182       in       in
2183        let position = {name=pos_name; address=address; op=Ex; pol=pol; pt=ptype; st=stype; label=term} in        let position = {name=pos_name; address=address; op=Ex; pol=pol; pt=ptype; st=stype; label=term} in
2184          let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1]) (pos_n+1) position in          let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1]) (pos_n+1) in
2185             let (succ_left,whole_left) = List.hd ordering_left in
2186              let pos_succs =
2187                StringSet.add succ_left whole_left in
2188            (NodeA(position,[|subtree_left|]),            (NodeA(position,[|subtree_left|]),
2189             (predecessor.name,position.name)::(ordering_left),             ((position.name,pos_succs) :: ordering_left),
2190             posn_left             posn_left
2191            )            )
2192     else     else
# Line 1364  Line 2203 
2203        let sposition = {name=pos_name; address=address; op=All; pol=pol; pt=ptype_0; st=stype; label=term}        let sposition = {name=pos_name; address=address; op=All; pol=pol; pt=ptype_0; st=stype; label=term}
2204        and position = {name=pos2_name; address=address@[1]; op=All; pol=pol; pt=ptype; st=stype_0; label=term} in        and position = {name=pos2_name; address=address@[1]; op=All; pol=pol; pt=ptype; st=stype_0; label=term} in
2205         let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1;1])         let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1;1])
2206                                                                   (pos_n+2) position in                                                                   (pos_n+2) in
2207             let (succ_left,whole_left) = List.hd ordering_left in
2208              let pos_succs =
2209                StringSet.add succ_left whole_left in
2210                 let pos_ordering = (position.name,pos_succs) :: ordering_left in
2211            (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]),            (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]),
2212             [(predecessor.name,sposition.name);(sposition.name,position.name)]@(ordering_left),             ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
2213             posn_left             posn_left
2214            )            )
2215    
2216     else      (* finally, term is atomic *)     else      (* finally, term is atomic *)
2217      let ptype_0,stype_0 =      let ptype_0,stype_0 =
2218         if pol = O         if pol = O
# Line 1380  Line 2224 
2224       let sposition = {name=pos_name; address=address; op=At; pol=pol; pt=ptype_0; st=stype; label=term}       let sposition = {name=pos_name; address=address; op=At; pol=pol; pt=ptype_0; st=stype; label=term}
2225       and position = {name=pos2_name; address=address@[1]; op=At; pol=pol; pt=PNull; st=stype_0; label=term} in       and position = {name=pos2_name; address=address@[1]; op=At; pol=pol; pt=PNull; st=stype_0; label=term} in
2226       (NodeA(sposition,[|NodeAt(position)|]),       (NodeA(sposition,[|NodeAt(position)|]),
2227        [(predecessor.name,sposition.name);(sposition.name,position.name)],        [(sposition.name,(StringSet.add position.name StringSet.empty));(position.name,StringSet.empty)],
2228        pos_n+1        pos_n+1
2229       )       )
2230    
2231    
       
2232    
2233  let construct_ftree term =  let construct_ftree term =
   print_endline "tree in";  
2234   let new_root = {name="w"; address=[]; op=Null; pol=O; pt=Psi; st=PNull_0; label=term} in   let new_root = {name="w"; address=[]; op=Null; pol=O; pt=Psi; st=PNull_0; label=term} in
2235     let tree,ordering,pos_n = build_ftree ("",term) O Psi_0 [1] 1 new_root in     let tree,ordering,pos_n = build_ftree ("",term) O Psi_0 [1] 1 in
2236       print_endline "tree out";       let (f,fset) = List.hd ordering in
2237        NodeA(new_root,[|tree|]),ordering,pos_n          NodeA(new_root,[|tree|]),(("w",(StringSet.add f fset))::ordering),pos_n
                         
2238    
2239    
2240    
# Line 1404  Line 2245 
2245    
2246  let init_prover ftree =  let init_prover ftree =
2247       let atom_relation = prepare_prover ftree in       let atom_relation = prepare_prover ftree in
2248  (*      print_atom_info atom_relation; *)  (*      print_atom_info atom_relation;  *)
2249          let atom_sets = make_atom_sets atom_relation in          let atom_sets = make_atom_sets atom_relation in
2250           (atom_relation,atom_sets)           (atom_relation,atom_sets)
             
2251    
2252    
2253  let rec try_multiplicity ftree ordering pos_n mult logic =  let rec try_multiplicity ftree ordering pos_n mult logic =
2254   (try   (try
2255      let (atom_relation,atom_sets) = init_prover ftree in     let (atom_relation,atom_sets) = init_prover ftree in
2256        path_checker atom_relation atom_sets ordering logic        let (red_ordering,eqlist,unifier,ext_proof) =
2257           path_checker atom_relation atom_sets ordering logic in
2258             (ftree,red_ordering,eqlist,unifier,ext_proof)
2259    with    with
2260     fail_multiplicity ->     Failure("fail1") ->
2261      let new_mult = mult+1 in      let new_mult = mult+1 in
2262       begin       begin
2263         print_endline "!!! Multiplicity Fail !!!!";       Format.open_box 0;
2264         print_endline ("Try new multiplicity: "^(string_of_int new_mult));       Format.force_newline ();
2265         let (new_ftree,new_ordering,new_pos_n) = add_multiplicity ftree ordering pos_n new_mult in       Format.print_string "Multiplicity Fail: ";
2266  (*       print_formula_info new_ftree new_ordering new_pos_n;  *)        Format.print_string ("Try new multiplicity "^(string_of_int new_mult));
2267         try_multiplicity new_ftree new_ordering new_pos_n new_mult logic       Format.force_newline ();
2268         Format.print_flush ();
2269    
2270           let (new_ftree,new_ordering,new_pos_n) = add_multiplicity ftree pos_n new_mult logic in
2271            if (new_ftree = ftree) then
2272             failwith "formula_invalid"
2273            else
2274    (*         print_formula_info new_ftree new_ordering new_pos_n;   *)
2275             try_multiplicity new_ftree new_ordering new_pos_n new_mult logic
2276       end       end
2277   )   )
2278    
# Line 1431  Line 2281 
2281    
2282  let prove term logic =  let prove term logic =
2283   let (ftree,ordering,pos_n) = construct_ftree term in (* pos_n = number of positions without new root "w" *)   let (ftree,ordering,pos_n) = construct_ftree term in (* pos_n = number of positions without new root "w" *)
2284  (*   print_formula_info ftree ordering pos_n;  *)  (*   print_formula_info ftree ordering pos_n;   *)
2285      try_multiplicity ftree ordering pos_n 1 logic     (try
2286         try_multiplicity ftree ordering pos_n 1 logic
2287        with
2288         Failure("formula_invalid") ->
2289          (Empty,[],[],(0,[]),[])
2290       )
2291    
2292    
2293    
2294    
2295    
2296    let rec remove_dups list =
2297     match list with
2298      [] -> []
2299     |f::r ->
2300       if List.mem f r then
2301        remove_dups r
2302       else
2303        f::remove_dups r
2304      
2305    
2306    
2307    
2308    
2309    (********** propositional nuprl interface *******************)
2310    
2311    
2312    
2313    let rec make_nuprl_interface rule_list =
2314     match rule_list with
2315       [] -> []
2316      |f::r ->
2317        let (rule,term1,term2) = f in
2318         ((ruletable rule),term1,term2)::(make_nuprl_interface r)
2319    
2320    
2321    let prover term =
2322     let (ftree,red_ordering,eqlist,unifier,ext_proof) = prove term "J" in
2323       if ftree = Empty then
2324        raise (Failure "Formula invalid")
2325       else
2326        let connections = remove_dups ext_proof in
2327         (try
2328           let sequent_proof = reconstruct ftree red_ordering [] connections "J" "LJ" in
2329             make_nuprl_interface sequent_proof  (* transform types *)
2330          with
2331            Failure("not_reconstructible") -> (* this possibility should of course be eliminated *)
2332              raise (Failure "deadlock unsolvable")
2333         )
2334    
2335    
2336    
 (**************** Test multiplicity increase!! ***********************)  
2337    
2338    
 let testt term =  
  let (ftree,ordering,pos_n) = construct_ftree term in (* pos_n = number of positions without new root "w" *)  
 (*   print_formula_info ftree ordering pos_n; *)  
    (ftree,ordering,pos_n)  
2339    
2340    
 let testm  ftree ordering pos_n new_mult =  
     let (new_ftree,new_ordering,new_pos_n) = add_multiplicity ftree ordering pos_n new_mult in  
 (*     print_formula_info new_ftree new_ordering new_pos_n; *)  
       (new_ftree,new_ordering,new_pos_n)  
2341    
 (**************** Test multiplicity increase!! END ***********************)  
2342    
2343    
2344    
2345  let test term logic =  
2346    let (unifier,ordering,ext_proof) = prove term logic in  
2347    
2348    
2349    (************* test with propositional proof reconstruction ************)
2350    
2351    
2352    
2353    let rec count_axioms seq_list =
2354      match seq_list with
2355       [] -> 0
2356      |f::r ->
2357        let (rule,_,_) = f in
2358         if rule = Ax then
2359          1 + count_axioms r
2360         else
2361          count_axioms r
2362    
2363    
2364    
2365    
2366    
2367    
2368    let test term logic calculus =  (* calculus should be LJmc or LJ for J, and LK for C *)
2369      let (ftree,red_ordering,eqlist,unifier,ext_proof) = prove term logic in
2370       if ftree = Empty then
2371        begin
2372         Format.open_box 0;
2373         Format.force_newline ();
2374         Format.force_newline ();
2375         Format.print_string "Formuls is invalid";
2376         Format.force_newline ();
2377         Format.force_newline ();
2378         Format.force_newline ();
2379         Format.print_flush ();
2380        end
2381       else
2382       begin
2383         Format.open_box 0;
2384         Format.force_newline ();
2385         Format.force_newline ();
2386         Format.print_string "Extension proof ready";
2387         Format.force_newline ();
2388         Format.force_newline ();
2389         Format.print_string ("Length of Extension proof: "^((string_of_int (List.length ext_proof)))^
2390                           " Axioms");
2391         Format.force_newline ();
2392         Format.force_newline ();
2393         Format.print_flush ();
2394         Format.open_box 0;
2395         Format.force_newline ();
2396         Format.print_string "Break ... ";
2397         Format.print_flush ();
2398          let _ = input_char stdin in
2399        let connections = remove_dups ext_proof in
2400        (try
2401          let sequent_proof = reconstruct ftree red_ordering [] connections logic calculus in
2402        begin
2403         Format.open_box 0;
2404         Format.force_newline ();
2405         Format.force_newline ();
2406         Format.print_string "Sequent proof ready";
2407         Format.force_newline ();
2408         Format.force_newline ();
2409         Format.print_flush ();
2410           let (ptree,count_ax) = bproof sequent_proof in
2411        begin        begin
2412    (*        print_endline "Extension proof:";
2413          Format.open_box 0;          Format.open_box 0;
2414            print_pairlist connections;       (* print list of type (string * string) list *)
2415            Format.print_flush ();
2416    *)
2417            Format.open_box 0;
2418           Format.print_string ("Length of sequent proof: "^((string_of_int count_ax))^" Axioms");
2419           Format.force_newline ();
2420           Format.force_newline ();
2421           Format.force_newline ();
2422           Format.force_newline ();
2423           Format.print_flush ();
2424            tt ptree;
2425            Format.print_flush ();
2426            print_endline "";
2427            print_endline ""
2428          end
2429         end
2430         with
2431             Failure("not_reconstructible") -> (* this possibility should of course be eliminated *)
2432              print_endline "deadlock unsolvable"
2433           )
2434      end
2435    
2436    
2437    
2438    
2439    
2440    
2441    (*****************************************************************)
2442    
2443    
2444    
2445    
2446    
2447    
2448    
2449    
2450    let test_old term logic =
2451      let (ftree,red_ordering,eqlist,unifier,ext_proof) = prove term logic in
2452       let connections = remove_dups ext_proof in
2453          begin
2454          print_endline "";          print_endline "";
2455          print_endline "";          print_endline "";
2456          print_endline "Extension proof:";          print_endline "Extension proof:";
2457          print_ordering ext_proof;            (* print list of type (string * string) list *)          Format.open_box 0;
2458            print_pairlist ext_proof;       (* print list of type (string * string) list *)
2459            Format.print_flush ();
2460          print_endline "";          print_endline "";
2461          print_endline "";          print_endline "";
2462            print_endline "Connections:";
2463            print_pairlist connections;       (* print list of type (string * string) list *)
2464          Format.print_flush ();          Format.print_flush ();
2465          print_endline "";          print_endline "";
2466          print_endline "";          print_endline "";
2467            print_endline "";
2468            print_endline "";
2469          print_endline ("Length of extension proof: "^((string_of_int (List.length ext_proof))));          print_endline ("Length of extension proof: "^((string_of_int (List.length ext_proof))));
2470            print_endline ("Length of connections: "^((string_of_int (List.length connections))));
2471          print_endline "";          print_endline "";
2472          print_endline "";          print_endline "";
2473          print_tunify unifier;          Format.open_box 0;
2474            Jtunify.print_tunify unifier;
2475            Format.print_flush ();
2476            print_endline "";
2477            print_endline "";
2478            Format.open_box 0;
2479            Jtunify.print_equations eqlist;
2480            Format.print_flush ();
2481          print_endline "";          print_endline "";
2482          print_endline "";          print_endline "";
2483          print_ordering ordering          print_endline ("Length of equations : "^((string_of_int (List.length eqlist))));
2484            print_endline "";
2485            print_endline "";
2486            Format.open_box 0;
2487            print_ordering red_ordering;
2488            Format.print_flush ();
2489            print_endline "";
2490            print_endline "";
2491            print_endline ("Length of reduction ordering: "^((string_of_int (List.length red_ordering))))
2492        end        end
2493    
2494    
2495    
2496    
2497  (* #use "/home/steph/meta-prl/refiner/reflib/jtree.ml" *)  (* #use "/home/steph/meta-prl/refiner/reflib/jtree.ml" *)
2498    
2499    
2500  end (* of struct *)  end (* of struct *)
2501    
2502    
2503    
2504    
2505    
2506    
2507    
2508    
2509    
2510    
2511    
2512    
2513    
2514    
2515    
2516    
2517    

Legend:
Removed from v.2918  
changed lines
  Added in v.2919

  ViewVC Help
Powered by ViewVC 1.1.26