[Toss-devel-svn] SF.net SVN: toss:[1746] trunk/Toss

[<luk...@us...>]

Revision: 1746
          http://toss.svn.sourceforge.net/toss/?rev=1746&view=rev
Author:   lukstafi
Date:     2012-07-17 11:31:00 +0000 (Tue, 17 Jul 2012)
Log Message:
-----------
Topological sorting. Term parsing moved to iterated substitutions.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Term/Makefile
    trunk/Toss/Term/ParseArc.ml
    trunk/Toss/Term/ParseArc.mli
    trunk/Toss/Term/ParseArcTest.ml
    trunk/Toss/Term/Term.ml
    trunk/Toss/Term/Term.mli

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Formula/Aux.ml	2012-07-17 11:31:00 UTC (rev 1746)
@@ -484,20 +484,30 @@
 type 'a topol_sort_ops = {
   rem_edge : 'a -> 'a -> unit;          (* [rem_edge a b] removes a->b. *)
   iter_outgoing : ('a -> unit) -> 'a -> unit;
-  no_outgoing : 'a -> bool
+  no_incoming : 'a -> bool;
+  node_to_string : 'a -> string;
 }
 
 let topol_sort ops l =
-  let top = ref (List.filter (fun e -> ops.no_outgoing e) l) in
+  let top = ref (List.filter (fun e -> ops.no_incoming e) l) in
+  (*Printf.printf "topol_sort: top=%s\n%!"
+    (String.concat ", " (List.map (fun n -> ops.node_to_string n) !top));*)
   let res = ref [] in
   while !top <> [] do
     let n = List.hd !top in
     top := List.tl !top; res := n:: !res;
     ops.iter_outgoing (fun m ->
-      ops.rem_edge n m; if ops.no_outgoing m then res := m:: !res) n;
+      ops.rem_edge n m; if ops.no_incoming m then top := m:: !top) n;
   done;
-  if List.for_all ops.no_outgoing l then List.rev !res
-  else raise Not_found
+  (* FIXME *)
+  if List.for_all ops.no_incoming l then List.rev !res
+  else (*
+    Printf.printf "topol_sort: cycle\n%!";
+    List.iter (fun n -> ops.iter_outgoing (fun m ->
+      Printf.printf "%s->%s; " (ops.node_to_string n) (ops.node_to_string m)
+    ) n) l;
+    Printf.printf "\n%!";*)
+    raise Not_found
 
 let all_subsets ?max_size set =
   let size = match max_size with Some i -> i | None -> List.length set in

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Formula/Aux.mli	2012-07-17 11:31:00 UTC (rev 1746)
@@ -219,7 +219,8 @@
 type 'a topol_sort_ops = {
   rem_edge : 'a -> 'a -> unit;          (** [rem_edge a b] removes [a->b]. *)
   iter_outgoing : ('a -> unit) -> 'a -> unit;
-  no_outgoing : 'a -> bool
+  no_incoming : 'a -> bool;
+  node_to_string : 'a -> string;
 }
 
 (** Topogical sort of [l] where [cmp a b = true] means that there is

Modified: trunk/Toss/Term/Makefile
===================================================================
--- trunk/Toss/Term/Makefile	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/Makefile	2012-07-17 11:31:00 UTC (rev 1746)
@@ -1,6 +1,6 @@
 all: allparsed
 
-MKPARSED = ../TRSTest.native -v -l "../Term/lib"
+MKPARSED = OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ../TRSTest.native -v -l "../Term/lib"
 
 coreparsed:
 	make -C .. ./Term/TRSTest.native

Modified: trunk/Toss/Term/ParseArc.ml
===================================================================
--- trunk/Toss/Term/ParseArc.ml	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/ParseArc.ml	2012-07-17 11:31:00 UTC (rev 1746)
@@ -11,8 +11,8 @@
    [term] does not have [substitution] applied. *)
 type parser_elem = 
   | Token of string
-  | PTerm of term * substs * int   (* From [parsed_elems], [cstrn]
-                                      and [endpos] of {!parser_arc}. *)
+  | PTerm of term * isubsts * int      (* From [parsed_elems], [cstrn]
+                                          and [endpos] of {!parser_arc}. *)
 
 (* Print a parser elem. *)
 let elem_str = function 
@@ -33,7 +33,7 @@
   spos : int;                      (* Start position of the arc. *)
   endpos : int;                    (* The current end position of the
                                       arc. FIXME: unnecessary? *)
-  cstrn : substs;                       (* Constraint for the arc. *)
+  cstrn : isubsts;                      (* Constraint for the arc. *)
 }
 
 (* --- Extending and closing arcs --- *)
@@ -71,35 +71,27 @@
       (* For now (first-order mgu) we assume single type. *)
       let pty = type_of t in
       try
-        (* Purely an optimization step. *)
-        precheck_eq ty pty;
-        (*let ty = Term.apply_sb arc.cstrn ty in
-        let pty = Term.apply_sb t_cstrn pty in
-        precheck_eq ty pty;*)
         (* Combine the constraints so far, and extend them to cover
            the new parsed element. *)
-        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
+        (*if !debug then Printf.printf
           "extend_arc: sd_n=%s; #parsed=%d\nty=%s; pty=%s\nt=%s\nt_cstrn=%s\narc.cstrn=%s\n%!"
           arc.sd_n (List.length arc.parsed_elems)
-          (type_to_string ty) (type_to_string pty)
-          (Coding.term_to_string t) (substs_str t_cstrn) (substs_str arc.cstrn)
-          ;*)
-        let cstrn' = combine_mgu_sbs t_cstrn arc.cstrn in
-        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
-          "S(ty)=%s; S(pty)=%s\ncstrn'=%s\n%!"
-          (type_to_string (apply_sbs cstrn' ty))
-          (type_to_string (apply_sbs cstrn' pty))
-          (substs_str cstrn');*)
+          (term_str ty) (term_str pty)
+          (term_str t)
+          (isubsts_str t_cstrn) (isubsts_str arc.cstrn);*)
+        let cstrn' = aux_mgu_i_cont global_decls t_cstrn arc.cstrn in
+        (*if !debug then Printf.printf
+          "cstrn'=%s\n%!" (isubsts_str cstrn');*)
         let cstrn =
-          mgu cstrn' [apply_sbs cstrn' pty, apply_sbs cstrn' ty] in
-        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
+          aux_mgu_i global_decls cstrn' pty ty in
+        (*if !debug then Printf.printf
           "cstrn=%s\n%!"
-          (substs_str cstrn);*)
+          (isubsts_str cstrn);*)
         Some
           {arc with rem_elems; parsed_elems = elem::arc.parsed_elems;
             endpos = t_endpos; cstrn}
       with UNIFY ->
-        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
+        (*if !debug then Printf.printf
           "NO UNIFY\n%!";*)
         None
 
@@ -158,7 +150,7 @@
     rem_elems = elems;
     parsed_elems = [];
     endpos = spos;
-    cstrn = empty_sbs;
+    cstrn = empty_isbs;
   }
 
 (* TODO: clean-up the description.
@@ -284,11 +276,12 @@
 (* --- Final parsing --- *)
 let parse_with_sdefs sdefs str =
   (*Printf.printf "\nparse_with_sdefs: str=%s\n%!" str;
-  if str = "if is digit string from c_a :: [] then added ending cl_a else false"
-  then debug := true;*)
+  if str = "Let map f_1 {} | {} to x :: xs with first argument v_a be 
+    (f_1 v_a | x) :: map f_1 {} | {} to xs with first argument v_a"
+  then (debug := true; Term.debug := true);*)
   let type_of_pe = function Token _ -> None
     | PTerm (te, cstrn, _) ->
-      let result = apply_sbs cstrn te in
-      Some result in
+      try Some (apply_isbs cstrn te)
+      with UNIFY -> None in
   let elems = parse sdefs (split_input_string str) in
   Aux.map_some type_of_pe elems

Modified: trunk/Toss/Term/ParseArc.mli
===================================================================
--- trunk/Toss/Term/ParseArc.mli	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/ParseArc.mli	2012-07-17 11:31:00 UTC (rev 1746)
@@ -9,8 +9,8 @@
     have [substitution] applied. *)
 type parser_elem = 
   | Token of string
-  | PTerm of term * substs * int   (** From [parsed_elems], [cstrn]
-                                       and [endpos] of {!parser_arc}. *)
+  | PTerm of term * isubsts * int     (** From [parsed_elems], [cstrn]
+                                          and [endpos] of {!parser_arc}. *)
 
 (** Print a parser elem. *)
 val elem_str : parser_elem -> string
@@ -29,7 +29,7 @@
                                        rev. order (all will be arguments). *)
   spos : int;                      (** Start position of the arc. *)
   endpos : int;                    (** The current end position of the arc. *)
-  cstrn : substs;                  (** Constraint for the arc. *)
+  cstrn : isubsts;                 (** Constraint for the arc. *)
 }
 
 

Modified: trunk/Toss/Term/ParseArcTest.ml
===================================================================
--- trunk/Toss/Term/ParseArcTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/ParseArcTest.ml	2012-07-17 11:31:00 UTC (rev 1746)
@@ -37,12 +37,30 @@
       let cons_closed = fst (Aux.find_some close_arc cons_arc) in
       elem_eq "Te @L[@V [Vx @: @? a @: 0 ]]" cons_closed;
 
+    (* With iterated substitutions, occurs/cyclicity check is only performed
+       when the substitution is applied, which only happens when
+       parser element is converted to standard term in [parse_with_sdefs].
+
       let cons_bad_arc = extend_arc_list var_closed cons_part2_arc in
       let cons_bad_closed = Aux.map_some close_arc cons_bad_arc in
-      assert_equal ~printer:(fun x -> "empty list test") [] cons_bad_closed;
+      assert_equal ~printer:(fun l ->
+        "["^String.concat"; "(List.map (fun (e,_)->elem_str e) l)^"]")
+       [not empty] cons_bad_closed;
+
+       Instead, we check non-polymorphic case: *)
+
+      let cst_arc = extend_arc_list (Token "true") arcs in
+      let cst_closed = fst (Aux.find_some close_arc cst_arc) in
+      let cons_part1_arc = extend_arc_list cst_closed arcs in
+      let cons_part2_arc = extend_arc_list (Token ",") cons_part1_arc in
+      let cons_bad_arc = extend_arc_list cst_closed cons_part2_arc in
+      let cons_bad_closed = Aux.map_some close_arc cons_bad_arc in
+      assert_equal ~printer:(fun l ->
+        "["^String.concat"; "(List.map (fun (e,_)->elem_str e) l)^"]")
+        [] cons_bad_closed;
     );
 
-  "parse" >::
+  "parse_with_sdefs" >::
     (fun () ->
       let type_decls_list = [
 	(list_cons_name, Term (Term.fun_type_name, [||],
@@ -57,16 +75,16 @@
       let sdefs_basic = [list_cons_sd; list_nil_sd;
 			 boolean_true_sd; boolean_false_sd; var_x_a_sd] in
       let sdefs = List.map (fun sd -> (name_of_sd sd, sd)) sdefs_basic in
-      let parse_test res l = 
-	let ls = String.concat ", " (List.map elem_str (parse sdefs l)) in
+      let parse_test res s = 
+	let ls = String.concat ", "
+          (List.map term_str (parse_with_sdefs sdefs s)) in
 	assert_equal ~printer:(fun x -> x) res ls in
-      parse_test "Te @V [Vx @: @? a @: 0 ]" ["x"];
-      parse_test "Te @L[@V [Vx @: @? a @: 0 ]]" 
-	["x"; ","; "["; "]"];
-      parse_test "" ["x"; ","; "x"];
+      parse_test "Vx[0:?a]" "x";
+      parse_test "F\\?_\\cm_\\?[:T\\?_list(?a._.7)](Vx[0:?a._.7], F\\ls_\\rs[:T\\?_list(?a._.7)])" "x , [ ]";
+      parse_test "" "x , x";
       parse_test
-        ("Te @L[@V [Vx @: @? a @: 0 ], @V [Vx @: @? a @: 0 ]]")
-        ["x"; ","; "x"; ","; "["; "]"];
+        "F\\?_\\cm_\\?[:T\\?_list(?a._.40)](Vx[0:?a._.40], F\\?_\\cm_\\?[:T\\?_list(?a._.40)](Vx[0:?a._.40], F\\ls_\\rs[:T\\?_list(?a._.40)]))"
+        "x , x , [ ]";
     );
 
 

Modified: trunk/Toss/Term/Term.ml
===================================================================
--- trunk/Toss/Term/Term.ml	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/Term.ml	2012-07-17 11:31:00 UTC (rev 1746)
@@ -243,6 +243,25 @@
    which is a distinctive kind of toplevel types. *)
 let fun_type_name = "fffuuunnntyppe"
 
+(* Concise readable form. *)
+let rec term_str term =
+  let term_array_str ta =
+    String.concat ", " (to_list (map term_str ta)) in
+  match term with
+    | TVar n -> "?"^n
+    | SVar (v, d, t, [||]) ->
+      v ^ "[" ^ string_of_int d ^ ":" ^ term_str t ^ "]"
+    | SVar (v, d, t, a) ->
+      v ^ "[" ^ string_of_int d ^ ":" ^ term_str t ^ "](" ^
+        term_array_str a ^ ")"
+    | Term (n, [||], [||]) -> n
+    | Term (n, [||], a) ->
+      n ^ "(" ^ term_array_str a ^ ")"
+    | Term (n, t, [||]) ->
+      n ^ "[:" ^ term_array_str t ^ "]"
+    | Term (n, t, a) ->
+      n ^ "[:" ^ term_array_str t ^ "](" ^ term_array_str a ^ ")"
+
 (* Suffix variables to rename them. *)
 let rec suffix i = function
   | Term (n, t, a) -> Term (n, map (fun t -> suffix i t) t,
@@ -307,10 +326,12 @@
 type optimize = {
   mutable no_glb_type_of_var : bool;
   mutable no_isa_match_type_of_var : bool;
+  mutable no_mgu_type_of_var : bool;
 }
 let optimize = {
   no_glb_type_of_var = false;
   no_isa_match_type_of_var = false;
+  no_mgu_type_of_var = false;
 }
   
 
@@ -780,7 +801,26 @@
 type iterated_subst = (string * term) list
 type iter_s_subst = iterated_subst
 type iter_t_subst = iterated_subst
+type isubsts = iter_s_subst * iter_t_subst
 
+let empty_t_isb = empty_sb
+let empty_s_isb = empty_sb
+let empty_isbs = empty_s_isb, empty_t_isb
+
+let subst_str subst = String.concat ", "
+  (List.map (fun (s, t) -> s ^ " <- " ^ (term_str t)) subst)
+
+let s_subst_str = subst_str
+let t_subst_str = subst_str
+
+let substs_str (s_sb, t_sb) =
+  (* "S:"^ *)s_subst_str s_sb ^ (if s_sb <> [] && t_sb <> [] then "; " else "")
+  ^ (* "T:"^ *)t_subst_str t_sb
+
+let isubsts_str = substs_str
+
+let debug = ref false
+
 let rec merge_isbs op acc = function
   | [], isb | isb, [] ->                (* with optimization *)
     (match acc with
@@ -790,8 +830,11 @@
       | [p3; p2; p1] -> p1::p2::p3::isb
       | _ -> List.rev (List.rev_append isb acc))
   | ((v1, t1 as p1)::isb1' as isb1), ((v2, t2 as p2)::isb2' as isb2) ->
-    if v1 < v2 then merge_isbs op (p1::acc) (isb1', isb2)
-    else if v1 = v2 then merge_isbs op ((v1, op t1 t2)::acc) (isb1', isb2')
+    let vcmp = String.compare v1 v2 in
+    if vcmp < 0 (* v1 < v2 *)
+    then merge_isbs op (p1::acc) (isb1', isb2)
+    else if vcmp = 0 (* v1 = v2 *)
+    then merge_isbs op ((v1, op t1 t2)::acc) (isb1', isb2')
     else merge_isbs op (p2::acc) (isb1, isb2')
 
 (** [subst_t_pos p subt t] places [subt] at supertype position [p] in [t]. *)
@@ -839,23 +882,47 @@
 let rec glb decls t1 t2 =
   match t1, t2 with
     | _ when t1 == t2 -> ([], []), t1
+    | SVar (v1, _, ty1, [||]), SVar (v2, _, ty2, [||]) ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], []), t1
+      else
+        let v, var, ty, te =
+          if vcmp < 0 then v1, t1, ty1, t2 else v2, t2, ty2, t1 in
+        if optimize.no_glb_type_of_var
+        then ([v, te], []), var
+        else aux_glb decls ([v, te], []) ty te
+
+    | TVar v1, TVar v2 ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], []), t1
+      else
+        let v, var, te = if vcmp < 0 then v1, t1, t2 else v2, t2, t1 in
+        ([], [v, te]), var
+
     | (SVar (v, _, ty, [||]) as var, te | te, (SVar (v, _, ty, [||]) as var)) ->
       if optimize.no_glb_type_of_var
       then ([v, te], []), var
       else aux_glb decls ([v, te], []) ty te
 
     | (SVar (v, d, ty, ste1), (Term (c, sty, ste2) as te)
-          | (Term (c, sty, ste2) as te), SVar (v, d, ty, ste1)) ->
+          | (Term (c, sty, ste2) as te), SVar (v, d, ty, ste1))
+        when Array.length ste1 = Array.length ste2 ->
       let isbs, glste =
         Aux.array_fold_map2 (aux_glb decls) ([v,te],[]) ste1 ste2 in
       (* TODO: ignoring the var type *)
       isbs, SVar (v, d, ty, glste)
+    | (SVar _, Term _ | Term _, SVar _) (* when arity mismatch *) ->
+      raise UNIFY
 
-    | (SVar (v, d, ty, ste1), (SVar (_, _, ty2, ste2) as te)) ->
+    | (SVar (v, d, ty, ste1), (SVar (_, _, ty2, ste2) as te))
+        when Array.length ste1 = Array.length ste2 ->
+      (* TODO: ignoring v1 = v2, v1 > v2 *)
       let isbs, glste =
         Aux.array_fold_map2 (aux_glb decls) ([v,te],[]) ste1 ste2 in
       (* TODO: ignoring the var type *)
       isbs, SVar (v, d, ty, glste)
+    | SVar _, SVar _ (* when arity mismatch *) ->
+      raise UNIFY
 
     | (TVar v as var, te | te, (TVar v as var)) ->
       ([], [v, te]), var
@@ -876,11 +943,15 @@
           let isbs, glte = glb decls t1 (get_t_pos p t2) in
           isbs, subst_t_pos p glte t2
         | GLB_equal ->
-          let isbs, glsty =
-            Aux.array_fold_map2 (aux_glb decls) ([], []) sty1 sty2 in
-          let isbs, glste =
-            Aux.array_fold_map2 (aux_glb decls) isbs ste1 ste2 in
-          isbs, Term (c1, glsty, glste)
+          if Array.length sty1 = Array.length sty2 &&
+             Array.length ste1 = Array.length ste2
+          then
+            let isbs, glsty =
+              Aux.array_fold_map2 (aux_glb decls) ([], []) sty1 sty2 in
+            let isbs, glste =
+              Aux.array_fold_map2 (aux_glb decls) isbs ste1 ste2 in
+            isbs, Term (c1, glsty, glste)
+          else raise UNIFY              (* arity mismatch *)
         | GLB_disjoint -> raise UNIFY
 
 (** Least Upper Bound Unification w.r.t. the ISA relation. Returns
@@ -891,6 +962,23 @@
 and lub decls t1 t2 =
   match t1, t2 with
     | _ when t1 == t2 -> ([], []), t1
+    | SVar (v1, _, ty1, [||]), SVar (v2, _, ty2, [||]) ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], []), t1
+      else
+        let v, var, ty, te =
+          if vcmp < 0 then v1, t1, ty1, t2 else v2, t2, ty2, t1 in
+        if optimize.no_glb_type_of_var
+        then ([v, te], []), var
+        else aux_glb decls ([v, te], []) ty te
+
+    | TVar v1, TVar v2 ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], []), t1
+      else
+        let v, var, te = if vcmp < 0 then v1, t1, t2 else v2, t2, t1 in
+        ([], [v, te]), var
+
     | (SVar (v, _, ty, [||]) as var, te | te, (SVar (v, _, ty, [||]) as var)) ->
       if optimize.no_glb_type_of_var
       then ([v, te], []), var
@@ -898,19 +986,25 @@
       else aux_glb decls ([v, te], []) ty te
 
     | (SVar (v, d, ty, ste1), (Term (c, sty, ste2) as te)
-          | (Term (c, sty, ste2) as te), SVar (v, d, ty, ste1)) ->
+          | (Term (c, sty, ste2) as te), SVar (v, d, ty, ste1))
+        when Array.length ste1 = Array.length ste2 ->
       (* TODO: not sure whether GLB or LUB *)
       let isbs, glste =
         Aux.array_fold_map2 (aux_glb decls) ([v,te],[]) ste1 ste2 in
       (* TODO: ignoring the var type *)
       isbs, SVar (v, d, ty, glste)
+    | (SVar _, Term _ | Term _, SVar _) (* when arity mismatch *) ->
+      raise UNIFY
 
-    | (SVar (v, d, ty, ste1), (SVar (_, _, ty2, ste2) as te)) ->
+    | (SVar (v, d, ty, ste1), (SVar (_, _, ty2, ste2) as te))
+        when Array.length ste1 = Array.length ste2 ->
       (* TODO: not sure whether GLB or LUB *)
       let isbs, glste =
         Aux.array_fold_map2 (aux_glb decls) ([v,te],[]) ste1 ste2 in
       (* TODO: ignoring the var type *)
       isbs, SVar (v, d, ty, glste)
+    | SVar _, SVar _ (* when arity mismatch *) ->
+      raise UNIFY
 
     | (TVar v as var, te | te, (TVar v as var)) ->
       ([], [v, te]), var
@@ -927,11 +1021,15 @@
         | LUB_greater p ->
           lub decls t1 (get_t_pos p t2)
         | LUB_equal ->
-          let isbs, lusty =
-            Aux.array_fold_map2 (aux_lub decls) ([], []) sty1 sty2 in
-          let isbs, luste =
-            Aux.array_fold_map2 (aux_lub decls) isbs ste1 ste2 in
-          isbs, Term (c1, lusty, luste)
+          if Array.length sty1 = Array.length sty2 &&
+             Array.length ste1 = Array.length ste2
+          then
+            let isbs, lusty =
+              Aux.array_fold_map2 (aux_lub decls) ([], []) sty1 sty2 in
+            let isbs, luste =
+              Aux.array_fold_map2 (aux_lub decls) isbs ste1 ste2 in
+            isbs, Term (c1, lusty, luste)
+          else raise UNIFY              (* arity mismatch *)
         | LUB_unconnected -> raise UNIFY
 
 and aux_glb decls isbs t1 t2 =
@@ -980,19 +1078,28 @@
 and isa_match decls pa te =
   match pa, te with
     | _ when pa == te -> [], []
+    | SVar (v1, _, _, _), SVar (v2, _, _, _) when v1 = v2 ->
+      ([], [])
+    | TVar v1, TVar v2 when v1 = v2 ->
+      ([], [])
+
     | SVar (v, _, ty, [||]), te ->
       if optimize.no_isa_match_type_of_var
       then [v, te], []
       else aux_match decls ([v, te], []) ty te
 
-    | SVar (v, _, ty, ste1), (Term (c, sty, ste2) as te) ->
-      (* TODO: ignoring variable type *)
-      (* TODO: ignoring arity mismatch *)
+    | SVar (v, _, ty, ste1), (Term (c, sty, ste2) as te)
+      when Array.length ste1 = Array.length ste2 ->
+      (* TODO: ignoring variable type -- should first try to match
+         the proper level in the other term *)
       Aux.array_fold_left2 (aux_match decls) ([v,te],[]) ste1 ste2
+    | SVar _, Term _ (* when arity mismatch *) -> raise UNIFY
 
-    | SVar (v, _, ty, ste1), (SVar (_, _, ty2, ste2) as te) ->
+    | SVar (v, _, ty, ste1), (SVar (_, _, ty2, ste2) as te)
+      when Array.length ste1 = Array.length ste2 ->
       (* TODO: ignoring variable type *)
       Aux.array_fold_left2 (aux_match decls) ([v,te],[]) ste1 ste2
+    | SVar _, SVar _ (* when arity mismatch *) -> raise UNIFY
 
     | SVar _, TVar _ -> raise UNIFY
 
@@ -1009,10 +1116,13 @@
         | GLB_greater p ->
           isa_match decls pa (get_t_pos p te)
         | GLB_equal ->
-          let isbs =
-            Aux.array_fold_left2 (aux_match decls) ([], []) sty1 sty2 in
-          Aux.array_fold_left2 (aux_match decls) isbs ste1 ste2
-
+          if Array.length sty1 = Array.length sty2 &&
+            Array.length ste1 = Array.length ste2
+          then
+            let isbs =
+              Aux.array_fold_left2 (aux_match decls) ([], []) sty1 sty2 in
+            Aux.array_fold_left2 (aux_match decls) isbs ste1 ste2
+          else raise UNIFY
         | GLB_glb _ | GLB_smaller _ | GLB_disjoint -> raise UNIFY
 
 and aux_match decls isbs pa te =
@@ -1035,41 +1145,73 @@
 and mgu_iter decls t1 t2 =
   match t1, t2 with
     | _ when t1 == t2 -> [], []
+    | SVar (v1, _, ty1, [||]), SVar (v2, _, ty2, [||]) ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], [])
+      else
+        let v, var, ty, te =
+          if vcmp < 0 then v1, t1, ty1, t2 else v2, t2, ty2, t1 in
+        if optimize.no_glb_type_of_var
+        then ([v, te], [])
+        else aux_match decls ([v, te], []) ty te
+
+    | TVar v1, TVar v2 ->
+      let vcmp = String.compare v1 v2 in
+      if vcmp = 0 then ([], [])
+      else
+        let v, var, te = if vcmp < 0 then v1, t1, t2 else v2, t2, t1 in
+        ([], [v, te])
+
     | (SVar (v, _, ty, [||]), te | te, SVar (v, _, ty, [||])) ->
-      aux_match decls ([v, te], []) ty te
+      if optimize.no_mgu_type_of_var
+      then [v, te], []
+      else aux_match decls ([v, te], []) ty te
 
     | (SVar (v, _, ty, ste1), (Term (c, _, ste2) as te)
-          | (Term (c, _, ste2) as te), SVar (v, _, ty, ste1)) ->
-      Aux.array_fold_left2 (aux_mgu decls)
+          | (Term (c, _, ste2) as te), SVar (v, _, ty, ste1))
+        when Array.length ste1 = Array.length ste2 ->
+      Aux.array_fold_left2 (aux_mgu_i decls)
         (aux_match decls ([v, te], []) ty te)
         ste1 ste2
+    | (SVar _, Term _ | Term _, SVar _) -> raise UNIFY
 
-    | (SVar (v, _, ty, ste1), (SVar (_, _, ty2, ste2) as te)) ->
-      (* TODO: ignoring variable types *)
-      Aux.array_fold_left2 (aux_mgu decls)
+    | (SVar (v, _, ty, ste1), (SVar (_, _, ty2, ste2) as te))
+        when Array.length ste1 = Array.length ste2 ->
+      (* TODO: ignoring variable types, and v1=v2, v1>v2 *)
+      Aux.array_fold_left2 (aux_mgu_i decls)
         ([v, te], []) ste1 ste2
+    | SVar _, SVar _ -> raise UNIFY
 
     | (TVar v, te | te, TVar v) -> [], [v, te]
 
-    | Term (c1, sty1, ste1), Term (c2, sty2, ste2) when c1 = c2 ->
+    | Term (c1, sty1, ste1), Term (c2, sty2, ste2)
+      when c1 = c2 && Array.length sty1 = Array.length sty2
+              && Array.length ste1 = Array.length ste2 ->
       let isbs =
-        Aux.array_fold_left2 (aux_mgu decls) ([], []) sty1 sty2 in
-      Aux.array_fold_left2 (aux_mgu decls) isbs ste1 ste2
+        Aux.array_fold_left2 (aux_mgu_i decls) ([], []) sty1 sty2 in
+      Aux.array_fold_left2 (aux_mgu_i decls) isbs ste1 ste2
 
-    | Term (c1, _, _), Term (c2, _, _)  (* when c1 <> c2 *) ->
+    | Term (c1, _, _), Term (c2, _, _)(* when c1 <> c2 or arity mismatch *) ->
       raise UNIFY
 
-and aux_mgu decls isbs t1 t2 =
+and aux_mgu_i decls isbs t1 t2 =
   let isbs' = mgu_iter decls t1 t2 in
-  aux_mgu_cont decls isbs isbs'
+  aux_mgu_i_cont decls isbs isbs'
 
-and aux_mgu_cont decls (s_isb, t_isb) (s_isb', t_isb') =
+and aux_mgu_i_cont decls (s_isb, t_isb) (s_isb', t_isb') =
+  (*if !debug then Printf.printf "aux_mgu_i_cont: isbs=%s\nisbs'=%s\n%!"
+    (isubsts_str (s_isb, t_isb))
+    (isubsts_str (s_isb', t_isb'));*)
   let s_isb, more_isbs1 =
     mgu_combine_isbs decls s_isb s_isb' in
   let t_isb, more_isbs2 =
     mgu_combine_isbs decls t_isb t_isb' in
-  List.fold_left (aux_mgu_cont decls)
-    (List.fold_left (aux_mgu_cont decls) (s_isb, t_isb) more_isbs1)
+  (*if !debug then Printf.printf "aux_mgu_i_cont: combined=%s\nmore_isbs=%s\n%!"
+    (isubsts_str (s_isb, t_isb))
+    (String.concat " / "
+       (List.map isubsts_str (more_isbs1 @ more_isbs2)));*)
+  List.fold_left (aux_mgu_i_cont decls)
+    (List.fold_left (aux_mgu_i_cont decls) (s_isb, t_isb) more_isbs1)
     more_isbs2
 
 
@@ -1078,8 +1220,10 @@
   let result = merge_isbs
     (fun t1 t2 -> let isb = mgu_iter decls t1 t2 in
                   if isb <> ([],[]) then more_isbs := isb:: !more_isbs;
-                  (* no change since it's an iterated substitution *)
-                  t1)
+                  (* no change since it's an iterated substitution
+                     t2 not to fall into a loop with cyclic substs --
+                     because isb2 comes from mgu_iter so it's smaller *)
+                  t2)
     [] (isb1, isb2) in
   result, !more_isbs
 
@@ -1125,12 +1269,10 @@
 (* TODO: come up with better function names... *)
 let appl_s_sb sb t =                    (* None = no change *)
   match app_s_sb sb t with None -> t | Some t -> t
-let appl_t_sb sb t =
-  match app_s_sb sb t with None -> t | Some t -> t
 
 let rec app_t_sb sb t =
   let app_tuple a =
-    let a' = Array.map (app_s_sb sb) a in
+    let a' = Array.map (app_t_sb sb) a in
     if Aux.array_for_all (function None -> true | Some _ -> false) a'
     then None
     else
@@ -1139,11 +1281,18 @@
   match t with
     | TVar n ->
       (try Some (List.assoc n sb) with Not_found -> None)
-    | SVar _ -> None
+    | SVar (_,_,(Term (_, [||], [||])   (* TODO: optimization, test *)
+          | Term (_, [|Term (_, [||], [||])|], [||])),[||]) -> None
     | (Term (_, [||], [||])             (* TODO: optimization, test *)
           | Term (_, [|Term (_, [||], [||])|], [||])
           | Term (_, [|Term (_, [||], [||])|],
                   [|Term (_, [||], [||])|])) -> None
+    | SVar (n, d, t, a) ->
+      (match app_t_sb sb t, app_tuple a with
+        | None, None -> None
+        | None, Some a -> Some (SVar (n, d, t, a))
+        | Some t, None -> Some (SVar (n, d, t, a))
+        | Some t, Some a -> Some (SVar (n, d, t, a)))
     | Term (n, t, a) ->
       (match app_tuple t, app_tuple a with
         | None, None -> None
@@ -1151,17 +1300,23 @@
         | Some t, None -> Some (Term (n, t, a))
         | Some t, Some a -> Some (Term (n, t, a)))
 
-type topsort_elem = {
-  e_assoc : string * term;
-  e_outgoing : (string, topsort_elem) Hashtbl.t;
+let appl_t_sb sb t =
+  match app_t_sb sb t with None -> t | Some t -> t
+
+type topsort_node = {
+  n_assoc : string * term;
+  n_outgoing : (string, topsort_node) Hashtbl.t;
+  n_incoming : (string, topsort_node) Hashtbl.t;
 }
 
 let topsort_ops = {
   Aux.rem_edge = (fun n m  ->
-    Hashtbl.remove n.e_outgoing (fst m.e_assoc));
+    Hashtbl.remove m.n_incoming (fst n.n_assoc);
+    Hashtbl.remove n.n_outgoing (fst m.n_assoc));
   iter_outgoing = (fun f n ->
-    Hashtbl.iter (fun _ -> f) n.e_outgoing);
-  no_outgoing = (fun n -> Hashtbl.length n.e_outgoing = 0)
+    Hashtbl.iter (fun _ -> f) n.n_outgoing);
+  no_incoming = (fun n -> Hashtbl.length n.n_incoming = 0);
+  node_to_string = (fun n -> fst n.n_assoc);
 }
 
 (** Apply an iterated substitution -- "unpack" all the variables. We
@@ -1174,34 +1329,54 @@
     to be fixed once explicit sharing gets introduced -- although
     then the need for [apply_isbs] will be smaller. *)
 let apply_isbs (s_isb, t_isb) t =
+  (*if !debug then Printf.printf "apply_isbs: initial isbs = %s\n%!"
+    (isubsts_str (s_isb,t_isb));*)
   let s_nodes = List.map
     (fun (v,_ as p) ->
-      v, {e_assoc = p; e_outgoing = Hashtbl.create 2}) s_isb in
+      v, {n_assoc = p; n_outgoing = Hashtbl.create 2;
+          n_incoming = Hashtbl.create 2}) s_isb in
   let t_nodes = List.map
     (fun (v,_ as p) ->
-      v, {e_assoc = p; e_outgoing = Hashtbl.create 2}) t_isb in
-  let s_outgoing (_,{e_assoc=v,t; e_outgoing=vs}) =
+      v, {n_assoc = p; n_outgoing = Hashtbl.create 2;
+          n_incoming = Hashtbl.create 2}) t_isb in
+  (* The incoming edges are the variables in the substituted term. *)
+  let add_edges nodes get_in (_,({n_assoc=v1,t; n_incoming=in_vs} as n1)) =
     List.iter
-      (fun v -> Hashtbl.add vs v (List.assoc v s_nodes))
-      (s_vars_in_term [] t) in
-  let t_outgoing (_,{e_assoc=v,t; e_outgoing=vs}) =
-    List.iter    
-    (fun v -> Hashtbl.add vs v (List.assoc v t_nodes))
-      (t_vars_in_term [] t) in
-  List.iter s_outgoing s_nodes;
-  List.iter t_outgoing t_nodes;
-  let s_isb = List.map (fun n->n.e_assoc)
-    (Aux.topol_sort topsort_ops (List.map snd s_nodes)) in
-  let t_isb = List.map (fun n->n.e_assoc)
-    (Aux.topol_sort topsort_ops (List.map snd t_nodes)) in
+      (fun v2 ->
+        try
+          let n2 = List.assoc v2 nodes in
+          Hashtbl.add n2.n_outgoing v1 n1;
+          Hashtbl.add in_vs v2 n2
+        with Not_found -> ())
+      (get_in t) in
+  List.iter (add_edges s_nodes (s_vars_in_term [])) s_nodes;
+  List.iter (add_edges t_nodes (t_vars_in_term [])) t_nodes;
+  let s_isb =
+    try
+      List.map (fun n->n.n_assoc)
+        (Aux.topol_sort topsort_ops (List.map snd s_nodes))
+    with Not_found ->
+      failwith "apply_isbs: cyclic terms require explicit sharing" in
+  let t_isb =
+    try
+      List.map (fun n->n.n_assoc)
+        (Aux.topol_sort topsort_ops (List.map snd t_nodes))
+    with Not_found -> raise UNIFY in
+  (*if !debug then Printf.printf "apply_isbs: sorted isbs = %s\n%!"
+    (isubsts_str (s_isb,t_isb));*)
   let s_sb = List.fold_left
     (fun sb (v,t) -> (v, appl_s_sb sb t)::sb) [] s_isb in
   let t_sb = List.fold_left
     (fun sb (v,t) -> (v, appl_t_sb sb t)::sb) [] t_isb in
   let s_sb = List.map (fun (v,t) -> v, appl_t_sb t_sb t) s_sb in 
   let t_sb = List.map (fun (v,t) -> v, appl_s_sb s_sb t) t_sb in
+  (*if !debug then Printf.printf "apply_isbs: applied sbs = %s\n%!"
+    (substs_str (s_sb,t_sb));*)
   (* TODO: perhaps someone needs te substitutions *)
-  appl_s_sb s_sb (appl_t_sb t_sb t)
+  let res = appl_s_sb s_sb (appl_t_sb t_sb t) in
+  (*if !debug then Printf.printf "apply_isbs:\nt=%s;\nS(t)=%s\n%!"
+    (term_str t) (term_str res);*)
+  res
 
 
 (* --- Type printing and parsing --- *)
@@ -1288,18 +1463,6 @@
   let (ty, cont) = parse_type (split_to_list s) in
   if cont = [] then ty else failwith "type_of_string: incomplete parse"
 
-let subst_str subst = String.concat ", "
-  (List.map (fun (s, tp) ->
-    s ^ " <- " ^ (type_to_string tp)) subst)
-
-let s_subst_str = subst_str
-let t_subst_str = subst_str
-
-let substs_str (s_sb, t_sb) =
-  (* "S:"^ *)s_subst_str s_sb ^ (if s_sb <> [] && t_sb <> [] then "; " else "")
-  ^ (* "T:"^ *)t_subst_str t_sb
-
-
 (* --- Hashtables for Terms --- *)
 
 module HashableTerm =

Modified: trunk/Toss/Term/Term.mli
===================================================================
--- trunk/Toss/Term/Term.mli	2012-07-15 20:43:16 UTC (rev 1745)
+++ trunk/Toss/Term/Term.mli	2012-07-17 11:31:00 UTC (rev 1746)
@@ -12,6 +12,9 @@
 (** The name for function type (type of un-applied function term). *)
 val fun_type_name : string
 
+(** Concise readable form. *)
+val term_str : term -> string
+
 (** Suffix all type variables, useful for renaming. *)
 val suffix : int -> term -> term
 
@@ -76,6 +79,99 @@
 (** Return the supertypes of a term or type of a variable. *)
 val types_of : term -> term array
 
+
+(** {2 ISA relation and iterated substitution based operations.} *)
+
+(** Global optimization settings. *)
+type optimize = {
+  mutable no_glb_type_of_var : bool;
+  mutable no_isa_match_type_of_var : bool;
+  mutable no_mgu_type_of_var : bool;
+}
+val optimize : optimize
+
+(** {i Iterated substitutions} are sets of term equations in solved
+    form, but without disjointness between the domain and variables
+    in the image of substitution. See "Term Rewriting and All That"
+    p. 82. Currently implemented as sorted association lists. *)
+type iter_s_subst
+type iter_t_subst
+type isubsts = iter_s_subst * iter_t_subst
+
+val empty_t_isb : iter_t_subst
+val empty_s_isb : iter_s_subst
+val empty_isbs : isubsts
+
+(** Adding a declaration to a well-formed set of declarations. *)
+type add_to_decls =
+  | Decls_OK                            (** Declaration added. *)
+  | Decls_multi_glb of string * string * string
+  (** The first two symbols already have the third symbol as a greatest
+      lower bound, the proposed declaration would introduce alternative
+      GLB for them. *)
+  | Decls_multi_lub of string * string * string
+  (** The proposed declaration together with the third symbol would
+      have the first two symbols both as least upper bounds. *)
+  | Decls_redundant_s of string * string
+  (** Of proposed direct superclasses one ISA the second one. *)
+  | Decls_var | Decls_repeating
+
+(** Data associated with a well-formed set of declarations; expected
+    to grow monotonically by adding new declarations. *)
+type decls_set
+
+val global_decls : decls_set
+val copy_global_decls : unit -> decls_set
+
+exception EXC_Decls_multi_lub of string * string * string
+
+(** Assuming that the given set of declarations is well-formed, check
+    if it will remain well-formed after adding the given declaration.
+    If so, add it and update the [ISA] order relation. Return whether
+    the declaration was added or the reason it was not added. *)
+val add_to_decls : decls_set -> term -> add_to_decls
+
+(** Greatest Lower Bound Unification w.r.t. the ISA relation. Returns
+    the unsubstituted GLB term and iterated substitutions, or raises
+    [UNIFY]. Shared variables are merged using GLB-unification and
+    type variables are merged using LUB-unification. The returned term
+    contains variables from the substitution.
+
+    Substitutions are never applied during glb-unification. It
+    is important to return this intermediate representation, because
+    parsing is a "distributed glb-unification" as it produces a
+    single term that ISA a declaration. *)
+val glb : decls_set -> term -> term -> isubsts * term
+val aux_glb : decls_set -> isubsts -> term -> term -> isubsts * term
+
+(** Least Upper Bound Unification w.r.t. the ISA relation. Returns
+    the unsubstituted LUB term and iterated substitutions, or raises
+    [UNIFY]. Shared variables are merged using GLB-unification and
+    type variables are merged using LUB-unification. See also {!glb}. *)
+val lub : decls_set -> term -> term -> isubsts * term
+val aux_lub : decls_set -> isubsts -> term -> term -> isubsts * term
+
+val aux_glb_lub_cont : decls_set -> isubsts -> isubsts -> isubsts
+
+(** Returns the ISA-matching or raises [UNIFY]. First term is the
+    pattern. Shared variables are merged using MGU (eq-unification)
+    and type variables are merged using LUB-unification. See also
+    {!glb}. *)
+val isa_match : decls_set -> term -> term -> isubsts
+val aux_match : decls_set -> isubsts -> term -> term -> isubsts
+val aux_match_cont : decls_set -> isubsts -> isubsts -> isubsts
+
+(** Iterated Substitution based variant of the Most General Unifier
+    substitution, throws [UNIFY] if not unifiable. Both shared
+    variables and type variables are merged using MGU
+    (eq-unification). *)
+val mgu_iter : decls_set -> term -> term -> isubsts
+val aux_mgu_i : decls_set -> isubsts -> term -> term -> isubsts
+val aux_mgu_i_cont : decls_set -> isubsts -> isubsts -> isubsts
+
+val debug : bool ref
+val apply_isbs : isubsts -> term -> term
+
 (** {2 Parsing and Printing Types} *)
 
 (** Printing types in the internal format. *)
@@ -93,6 +189,7 @@
 val s_subst_str : s_subst -> string
 val t_subst_str : t_subst -> string
 val substs_str : substs -> string
+val isubsts_str : isubsts -> string
 
 (** {2 Hashtable for Terms} *)
 

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.