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

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

Revision: 1745
          http://toss.svn.sourceforge.net/toss/?rev=1745&view=rev
Author:   lukstafi
Date:     2012-07-15 20:43:16 +0000 (Sun, 15 Jul 2012)
Log Message:
-----------
Hierarchical terms: modified specification. Changed representation of terms. New Speagram step 3: iterated substitution based algorithms: MGU, ISA-matching, greatest lower bound and lowest upper bound unification; untested.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/AuxTest.ml
    trunk/Toss/Term/BuiltinLang.ml
    trunk/Toss/Term/Coding.ml
    trunk/Toss/Term/CodingTest.ml
    trunk/Toss/Term/ParseArc.ml
    trunk/Toss/Term/ParseArc.mli
    trunk/Toss/Term/ParseArcTest.ml
    trunk/Toss/Term/Rewriting.ml
    trunk/Toss/Term/RewritingTest.ml
    trunk/Toss/Term/SyntaxDef.ml
    trunk/Toss/Term/SyntaxDefTest.ml
    trunk/Toss/Term/TRS.ml
    trunk/Toss/Term/TRSTest.ml
    trunk/Toss/Term/Term.ml
    trunk/Toss/Term/Term.mli
    trunk/Toss/Term/TermTest.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Formula/Aux.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -368,6 +368,13 @@
     let new_accu = try f accu a with Not_found -> accu in
     fold_left_try f new_accu l
 
+let array_foldi_left f x a =
+  let r = ref x in
+  for i = 0 to Array.length a - 1 do
+    r := f i !r (Array.unsafe_get a i)
+  done;
+  !r
+
 let rec power ?(timeout = fun () -> false) dom img =
   List.fold_left (fun sbs v ->
     concat_map (fun e -> List.rev (List.rev_map (fun sb -> 
@@ -473,6 +480,25 @@
     | [] -> acc in
   idemp [] (List.sort (fun x y -> - (cmp x y)) l)
 
+(* Operations for imperatively manipulating the graph for {!topol_sort}. *)
+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
+}
+
+let topol_sort ops l =
+  let top = ref (List.filter (fun e -> ops.no_outgoing e) l) in
+  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;
+  done;
+  if List.for_all ops.no_outgoing l then List.rev !res
+  else raise Not_found
+
 let all_subsets ?max_size set =
   let size = match max_size with Some i -> i | None -> List.length set in
   [] :: (unique_sorted (List.map unique_sorted (all_ntuples set size)))
@@ -573,11 +599,33 @@
       if i = len1 then acc else
 	fl2_rec (f acc a1.(i) a2.(i)) (i+1) in
     fl2_rec start 0
-      
 
+let array_fold_map2 f x a1 a2 =
+  let l1 = Array.length a1 and l2 = Array.length a2 in
+  if l1 <> l2 then raise (Invalid_argument "Aux.array_fold_map2");
+  if l1 = 0 then x, [||] else begin
+    let x0, v0 = f x (Array.unsafe_get a1 0) (Array.unsafe_get a2 0) in
+    let rx = ref x0 in
+    let ra = Array.create l1 v0 in
+    for i = 1 to Array.length ra - 1 do
+      let xi, vi = f !rx (Array.unsafe_get a1 i) (Array.unsafe_get a2 i) in
+      rx := xi; Array.unsafe_set ra i vi
+    done;
+    !rx, ra
+  end
+
+
 let array_combine a b =
   array_map2 (fun x y->x,y) a b
 
+let array_exists p a =
+  let res = ref false in
+  let i = ref 0 in
+  while !i < Array.length a && not !res do
+    res := p (Array.unsafe_get a !i);
+    incr i
+  done; !res
+
 let array_existsi p a =
   let res = ref false in
   let i = ref 0 in

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Formula/Aux.mli	2012-07-15 20:43:16 UTC (rev 1745)
@@ -161,6 +161,9 @@
     [Not_found]. *)
 val fold_left_try : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
 
+(** As {!Array.fold_left}, but with the element position passed. *)
+val array_foldi_left : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
+
 (** [power dom img] generates all functions with domain [dom] and
     image [img], as graphs. Tail recursive. *) 
 val power : ?timeout:(unit -> bool) -> 'a list -> 'b list -> ('a * 'b) list list
@@ -212,6 +215,22 @@
     [add_to_maximal cmp l1 l2] computes [maximal cmp (l1 @ l2)]. *)
 val add_to_maximal : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
 
+(** Operations for imperatively manipulating the graph for {!topol_sort}. *)
+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
+}
+
+(** Topogical sort of [l] where [cmp a b = true] means that there is
+    an arrow from [a] to [b]. Elements without incoming edges are first
+    and elements without outgoing edges are last. Returns [None] /
+    raises [Not_found] if a cycle is detected.
+
+    Implementation:
+    http://en.wikipedia.org/wiki/Topological_sort#Algorithms *)
+val topol_sort : 'a topol_sort_ops -> 'a list -> 'a list
+
 (** Return the list of structurally unique elements, in order sorted
     by {!Pervasives.compare}. Not tail-recursive. *)
 val unique_sorted : ?cmp: ('a -> 'a -> int) -> 'a list -> 'a list
@@ -259,10 +278,15 @@
 val array_fold_left2 :
   ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
 
+(** Fold-left and map on two arrays. *)
+val array_fold_map2 :
+  ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
+
 (** Zip two arrays into an array of pairs. Raises [Invalid_argument
     "Aux.array_map2"] if the arrays are of different lengths. *)
 val array_combine : 'a array -> 'b array -> ('a * 'b) array
 
+val array_exists : ('a -> bool) -> 'a array -> bool
 val array_existsi : (int -> 'a -> bool) -> 'a array -> bool
 
 val array_mem : 'a -> 'a array -> bool
@@ -330,7 +354,7 @@
 (** Iterate a function [n] times: [f^n(x)]. *)
 val fold_n : ('a -> 'a) -> 'a -> int -> 'a
 
-(** Returns a string proloning [s] and not appearing in [names]. If
+(** Returns a string prolonging [s] and not appearing in [names]. If
     [truncate] is true, remove numbers from the end of [s]. *)
 val not_conflicting_name : ?truncate:bool -> Strings.t -> string -> string
 

Modified: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Formula/AuxTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -231,6 +231,10 @@
            ["a1";"c2"; "b1"; "a3"; "c7"]);
     );  
 
+  "topol_sort" >::
+    (fun () -> ()
+    );  
+
   "unique, unique_soted, not_unique, take_n" >::
     (fun () ->
       assert_equal ~printer:(String.concat "; ")
@@ -405,6 +409,17 @@
             [|"a";"c";"b"|] [|"e"; "d"|]);
     );  
 
+  "array_fold_map2" >::
+    (fun () ->
+      let printer (v,a) =
+        string_of_int v^", [|"^String.concat "; " (Array.to_list a)^"|]" in
+      let sum acc i j = acc+i*j, string_of_int i^string_of_int j in
+      assert_equal ~printer (5, [|"11";"22";"30"|])
+        (Aux.array_fold_map2 sum 0 [|1;2;3|] [|1;2;0|]);
+      assert_equal ~printer (0, [||])
+        (Aux.array_fold_map2 sum 0 [||] [||]);
+    );  
+
   "partition_choice, partition_map" >::
     (fun () ->
       assert_equal ~printer:(fun (x,y)->

Modified: trunk/Toss/Term/BuiltinLang.ml
===================================================================
--- trunk/Toss/Term/BuiltinLang.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/BuiltinLang.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -29,12 +29,12 @@
 
 let list_sd = SDtype [Tp term_type_tp; Str "list"]
 let list_name = name_of_sd list_sd
-let list_tp t = Term (list_name, toplevel_type, [|t|])
-let list_tp_a = list_tp (Var ("a", 0, top_type_term, [||]))
+let list_tp t = Term (list_name, [||], [|t|])
+let list_tp_a = list_tp (TVar "a")
 
 let list_nil_sd = SDfun ([Str "["; Str "]"], list_tp_a)
 let list_nil_name = name_of_sd list_nil_sd
-let list_cons_sd = SDfun ([Tp (Var ("a",0,top_type_term,[||]));
+let list_cons_sd = SDfun ([Tp (TVar "a");
                            Str ","; Tp list_tp_a],
 			   list_tp_a)
 let list_cons_name = name_of_sd list_cons_sd
@@ -150,8 +150,8 @@
 let input_rewrite_rule_name = name_of_sd input_rewrite_rule_sd
 let input_rewrite_rule_tp = type_of_sd input_rewrite_rule_sd
 
-let let_be_sd = SDfun ([Str "let"; Tp (Var ("a_1",0,top_type_term,[||]));
-                        Str "be"; Tp (Var ("a_1",0,top_type_term,[||]))],
+let let_be_sd = SDfun ([Str "let"; Tp (TVar "a_1");
+                        Str "be"; Tp (TVar "a_1")],
                        input_rewrite_rule_tp)
 let let_be_name = name_of_sd let_be_sd
 
@@ -164,8 +164,8 @@
 
 let let_major_be_sd = 
   SDfun ([Str "let"; Str "major";
-          Tp (Var ("a_1",0,top_type_term,[||])); Str "be";
-          Tp (Var ("a_1",0,top_type_term,[||]))],
+          Tp (TVar "a_1"); Str "be";
+          Tp (TVar "a_1")],
          priority_input_rewrite_rule_tp)
 let let_major_be_name = name_of_sd let_major_be_sd
 
@@ -191,47 +191,47 @@
 
 let exception_cl_sd = SDtype [Tp term_type_tp; Str "exception"]
 let exception_cl_name = name_of_sd exception_cl_sd
-let exception_cl_tp t = Term (exception_cl_name, toplevel_type, [|t|])
+let exception_cl_tp t = Term (exception_cl_name, [||], [|t|])
 
 let exception_sd = 
-  SDfun ([Str "!"; Str "!"; Tp (Var ("a",0,top_type_term,[||]));
+  SDfun ([Str "!"; Str "!"; Tp (TVar "a");
           Str "!";Str "!";],
-          exception_cl_tp (Var ("other_than_a!",0,top_type_term,[||])))
+          exception_cl_tp (TVar "other_than_a!"))
 let exception_name = name_of_sd exception_sd
 
 let exn_ok_sd = 
-  SDfun ([Str "+"; Str "+"; Tp (Var ("a",0,top_type_term,[||]));
+  SDfun ([Str "+"; Str "+"; Tp (TVar "a");
           Str "+";Str "+";],
-          exception_cl_tp (Var ("a",0,top_type_term,[||]))) (* Here it should be a! *)
+          exception_cl_tp (TVar "a")) (* Here it should be a! *)
 let exn_ok_name = name_of_sd exception_sd
 
 
 (* --- Special functions recognized during Normalisation --- *)
 
 let brackets_sd = SDfun ([Str "(";
-                          Tp (Var ("b",0,top_type_term,[||])); Str ")"],
-                         Var ("b",0,top_type_term,[||]))
+                          Tp (TVar "b"); Str ")"],
+                         TVar "b")
 let brackets_name = name_of_sd brackets_sd
 
 
-let verbatim_sd = SDfun ([Str "<"; Str "|"; Tp (Var ("b",0,top_type_term,[||]));
-                          Str "|"; Str ">"], Var ("b",0,top_type_term,[||]))
+let verbatim_sd = SDfun ([Str "<"; Str "|"; Tp (TVar "b");
+                          Str "|"; Str ">"], TVar "b")
 let verbatim_name = name_of_sd verbatim_sd
 
 
 let if_then_else_sd = SDfun ([Str "if"; Tp boolean_tp; Str "then";
-  Tp (Var ("a",0,top_type_term,[||])); Str "else"; 
-  Tp (Var ("a",0,top_type_term,[||]))], Var ("a",0,top_type_term,[||]))
+  Tp (TVar "a"); Str "else"; 
+  Tp (TVar "a")], TVar "a")
 let if_then_else_name = name_of_sd if_then_else_sd
 
-let eq_bool_sd = SDfun ([Tp (Var ("a",0,top_type_term,[||])); Str "=";
-                         Tp (Var ("a",0,top_type_term,[||]))], boolean_tp)
+let eq_bool_sd = SDfun ([Tp (TVar "a"); Str "=";
+                         Tp (TVar "a")], boolean_tp)
 let eq_bool_name = name_of_sd eq_bool_sd
 
 
 (* --- Syntax Definitions for special meta-functions --- *)
 
-let code_as_term_sd = SDfun ([Str "code"; Tp (Var ("a",0,top_type_term,[||]));
+let code_as_term_sd = SDfun ([Str "code"; Tp (TVar "a");
   Str "as"; Str "term"], term_tp)
 let code_as_term_name = name_of_sd code_as_term_sd
 
@@ -287,13 +287,13 @@
 let set_command_tp = type_of_sd set_command_sd
 
 let set_prop_sd = SDfun ([Str "set"; Tp (string_tp); Str "of";
-  Tp (Var ("a",0,top_type_term,[||])); Str "to";
-  Tp (Var ("b",0,top_type_term,[||]))], set_command_tp)
+  Tp (TVar "a"); Str "to";
+  Tp (TVar "b")], set_command_tp)
 let set_prop_name = name_of_sd set_prop_sd
 
 
 let preprocess_sd =  SDfun ([Str "#"; Str "#"; Str "#";
-                       Tp (Var ("p",0,top_type_term,[||]))], Var ("p",0,top_type_term,[||]))
+                       Tp (TVar "p")], TVar "p")
 let preprocess_name = name_of_sd preprocess_sd
 
 

Modified: trunk/Toss/Term/Coding.ml
===================================================================
--- trunk/Toss/Term/Coding.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/Coding.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -95,34 +95,32 @@
   | Term (n, _, [||]) when n = boolean_false_name -> false
   | _ -> raise (DECODE "bool")
 
-
+(* FIXME: remainder of the old Speagram distinction between types and terms *)
 let rec code_term_type = function
-  | Var (name, 0, tp, [||]) when tp = top_type_term ->
+  | TVar name ->
     Term (term_type_var_name, [|term_type_tp|], [|code_string name|])
-  | Var _ -> failwith "code_term_type: non-type variable"
-  | Term (name, tp, arr) when name = Term.fun_type_name && tp = toplevel_type->
+  | SVar _ -> failwith "code_term_type: sharing variable"
+  | Term (name, [||], arr) when name = Term.fun_type_name ->
     let l = Array.length arr in
     let (args_types, return_type) = (Array.sub arr 0 (l-1), arr.(l-1)) in
     Term (term_type_fun_name, [|term_type_tp|], [|
       code_list [|list_tp term_type_tp|] code_term_type (to_list args_types);
       code_term_type return_type|])
-  | Term (name, tp, args) when tp = toplevel_type ->
+  | Term (name, [||], args) ->
     Term (term_type_cons_name, [|term_type_tp|], [|
       code_string name;
       code_list [|list_tp term_type_tp|] code_term_type (to_list args)|])
-  | Term (name, _, _) when name = top_type_name -> failwith
-    "code_term_type: coding top term (the type of a type) not supported"
   | Term (name, _, _) -> failwith
-    ("code_term_type: non-type term at symbol " ^ name)
+    ("code_term_type: non-toplevel-type term at symbol " ^ name)
 
 let rec decode_term_type = function
   | Term (s, _, [|coded_name|]) when s = term_type_var_name ->
-    Var (decode_string coded_name, 0, top_type_term, [||])
+    TVar (decode_string coded_name)
   | Term (s, _, [|coded_1; coded_2|]) when s = term_type_fun_name ->
-    Term (Term.fun_type_name, toplevel_type, of_list (
+    Term (Term.fun_type_name, [||], of_list (
       (decode_list decode_term_type coded_1) @ [decode_term_type coded_2]))
   | Term (s, _, [|coded_1; coded_2|]) when s = term_type_cons_name ->
-    Term (decode_string coded_1, toplevel_type,
+    Term (decode_string coded_1, [||],
            of_list (decode_list decode_term_type coded_2))
   | _ -> raise (DECODE "term_type")
 
@@ -132,7 +130,9 @@
 
 
 let rec code_term = function
-  | Var (name, deg, var_type, args) ->
+  | TVar name ->
+    Term (term_type_var_name, [|term_tp|], [|code_string name|])
+  | SVar (name, deg, var_type, args) ->
     Term (term_var_cons_name, [|term_tp|], 
 	  [|code_string name; 
 	    code_term_type var_type;
@@ -146,8 +146,10 @@
 
 
 let rec code_term_incr_vars = function
-  | Var (name, deg, var_type, args) ->
-    Var (name, deg+1, var_type, map code_term_incr_vars args)
+  | TVar name ->
+    Term (term_type_var_name, [|term_tp|], [|code_string name|])
+  | SVar (name, deg, var_type, args) ->
+    SVar (name, deg+1, var_type, map code_term_incr_vars args)
   | Term (name, types, args) ->
     Term (term_term_cons_name, [|term_tp|],
           [|code_string name;
@@ -156,9 +158,12 @@
 
 
 let rec decode_term = function
+  | Term (s, _, [|coded_name|])
+      when s = term_type_var_name  ->
+    TVar (decode_string coded_name)
   | Term (s, _, [|coded_name; coded_type; coded_deg; coded_args|])
       when s = term_var_cons_name  ->
-    Var (decode_string coded_name,
+    SVar (decode_string coded_name,
 	 bits_to_int (decode_list decode_bit coded_deg),
          decode_term_type coded_type,
          of_list (decode_list decode_term coded_args))
@@ -226,9 +231,9 @@
 let code_type_definition (name, arity) =
   let rec var = function
     | 0 -> []
-    | i -> Var ("a_" ^ (string_of_int i), 0, top_type_term, [||]) :: (var (i-1)) in
+    | i -> TVar ("a_" ^ string_of_int i) :: (var (i-1)) in
   Term (type_of_name, [|type_definition_tp|],
-        [|code_term_type (Term (name, toplevel_type, of_list (var arity)))|])
+        [|code_term_type (Term (name, [||], of_list (var arity)))|])
 
 
 let decode_type_definition = function
@@ -296,36 +301,17 @@
 
 (* --- Term matching and substitutions --- *)
 
-(* Including supertypes.
-let rec matches dict = function
-  | (Term (n1, t1, a1), Term (n2, t2, a2))
-      when n1=n2 && (length t1 = length t2) && (length a1 = length a2)->
-    Aux.array_for_all2 (fun u v -> matches dict (u, v)) t1 t2 &&
-    Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
-  | (Var (n1, d1, t1, a1), Var (n2, d2, t2, a2))
-      when n1 = n2 && d1 = d2 && length a1 = length a2 ->
-    matches dict (t1, t2) &&
-      Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
-  | (Var (n1, d1, t1, [||]), te) ->
-    (try
-       let arg = List.assoc n1 (!dict) in 
-       let coded_arg = fn_apply d1 code_term arg in
-       te = coded_arg
-     with Not_found -> 
-       let decoded_te = fn_apply d1 decode_term te in
-       (dict := (n1, decoded_te) :: (!dict); true)
-    )
-  | _ -> false
-*)
+(* FIXME: these functions should are obsoleted by the Term module. *)
+
 (* Ignoring supertypes. *)
 let rec matches dict = function
   | (Term (n1, _, a1), Term (n2, _, a2))
       when n1=n2 && (length a1 = length a2)->
     Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
-  | (Var (n1, d1, _, a1), Var (n2, d2, _, a2))
+  | (SVar (n1, d1, _, a1), SVar (n2, d2, _, a2))
       when n1 = n2 && d1 = d2 && length a1 = length a2 ->
       Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
-  | (Var (n1, d1, t1, [||]), te) ->
+  | (SVar (n1, d1, t1, [||]), te) ->
     (try
        let arg = List.assoc n1 (!dict) in 
        let coded_arg = fn_apply d1 code_term arg in
@@ -339,45 +325,47 @@
 (* Application of term substitutions (only flat functional
    substitutes). Ignoring supertypes. *)
 let rec apply_s substs = function
-  | Var (n, d, _, [||]) as t ->
+  | SVar (n, d, _, [||]) as t ->
     (* FIXME: why we don't apply substitutions recursively, as below? *)
     (try (fn_apply d code_term (List.assoc n substs)) with Not_found -> t)
   | Term (n, tp, a) -> Term (n, tp, map (apply_s substs) a)
-  | Var (n, deg, t, a) ->
+  | TVar _ as ty -> ty
+  | SVar (n, deg, t, a) ->
       try (
         let raw_result =
           match (List.assoc n substs) with
             | Term (name, tps, [||]) ->
               Term (name, tps, map (apply_s substs) a)
-            | Var (name, d, ty, [||]) ->
-              Var (name, d, ty, map (apply_s substs) a)
+            | SVar (name, d, ty, [||]) ->
+              SVar (name, d, ty, map (apply_s substs) a)
             | _ -> failwith "functional substitution of non-flat term" in
         fn_apply deg code_term raw_result
       )
-      with Not_found -> Var (n, deg, t, map (apply_s substs) a)
+      with Not_found -> SVar (n, deg, t, map (apply_s substs) a)
 
 (* Application of term substitutions (only flat functional
    substitutes). Including supertypes. *)
 let rec apply_st substs = function
-  | Var (n, d, t, [||]) ->
+  | SVar (n, d, t, [||]) ->
     (* FIXME: why we don't apply substitutions recursively, as below? *)
     (try (fn_apply d code_term (List.assoc n substs))
-     with Not_found -> Var (n, d, apply_st substs t, [||]))
+     with Not_found -> SVar (n, d, apply_st substs t, [||]))
   | Term (n, tp, a) ->
     Term (n, map (apply_st substs) tp, map (apply_st substs) a)
-  | Var (n, deg, t, a) ->
+  | TVar _ as ty -> ty
+  | SVar (n, deg, t, a) ->
       try (
         let raw_result =
           match (List.assoc n substs) with
             | Term (name, tps, [||]) ->
               Term (name, map (apply_st substs) tps, map (apply_st substs) a)
-            | Var (name, d, ty, [||]) ->
-              Var (name, d, apply_st substs ty, map (apply_st substs) a)
+            | SVar (name, d, ty, [||]) ->
+              SVar (name, d, apply_st substs ty, map (apply_st substs) a)
             | _ -> failwith "functional substitution of non-flat term" in
         fn_apply deg code_term raw_result
       )
       with Not_found ->
-        Var (n, deg, apply_st substs t, map (apply_st substs) a)
+        SVar (n, deg, apply_st substs t, map (apply_st substs) a)
 
 
 (* --- Nice Term display based on Syntax Definitions --- *)
@@ -393,7 +381,8 @@
   | Term (n, _, a) ->
     let args = List.map display_term (Array.to_list a) in
     display_sd (split_sdef_name n) args
-  | Var (n, _, _, a) ->
+  | TVar _ -> failwith "display_term: type variable"
+  | SVar (n, _, _, a) ->
     let args = List.map display_term (Array.to_list a) in
     display_sd (split_sdef_name n) args
 
@@ -407,7 +396,8 @@
   | Term (n, _, a) ->
     let args = List.map display_term_bracketed (Array.to_list a) in
     display_sd_bracketed (split_sdef_name n) args
-  | Var (n, _, _, a) ->
+  | TVar _ -> failwith "display_term: type variable"
+  | SVar (n, _, _, a) ->
     let args = List.map display_term_bracketed (Array.to_list a) in
     display_sd_bracketed (split_sdef_name n) args
 
@@ -415,9 +405,9 @@
 (* --- Display terms and types as XML --- *)
 
 let rec display_type_xml = function
-  | Var (n, 0, top_type_term, [||]) ->
+  | TVar n ->
     "<type_var>" ^ (make_xml_compatible n) ^ "</type_var>"
-  | Var _ -> failwith "display_type_xml: non-type variable"
+  | SVar _ -> failwith "display_type_xml: sharing variable"
   | Term (n, _, a) ->
     "<type class=\"" ^ (make_xml_compatible n) ^ "\">\n" ^
       (String.concat "\n" (List.map display_type_xml (to_list a))) ^
@@ -434,7 +424,8 @@
     "<term class=\"" ^ (make_xml_compatible n) ^ "\">\n" ^
       (String.concat "\n" (List.map display_term_xml (to_list a))) ^
       "\n</term>"
-  | Var (n, deg, ty, a) ->
+  | TVar _ -> failwith "display_term_xml: type variable"
+  | SVar (n, deg, ty, a) ->
     "<term-variable class=\"" ^ (make_xml_compatible n) ^ 
       "\" deg=\"" ^ (string_of_int deg) ^ "\">" ^
       (String.concat "" (List.map display_term_xml (to_list a))) ^
@@ -464,13 +455,14 @@
     | _ when is_some (decode_term_opt term) -> 
       (match (decode_term_opt term) with None -> ""
 	| Some te -> "@T " ^ (term_to_string te))
-    | Var (v, d, t, [||]) ->
+    | TVar _ as ty -> type_to_string ty
+    | SVar (v, d, t, [||]) ->
       (try
       "@V [" ^ v ^ " @: " ^ (type_to_string t) ^ 
         " @: "^ string_of_int (d) ^ " ]"
        with exn -> Printf.printf "Nontype: %s\n%!"(term_to_string t);
          raise exn)
-    | Var (v, d, t, a) ->
+    | SVar (v, d, t, a) ->
       (try
       "@V [" ^ v ^ " @: " ^ (type_to_string t) ^ 
         " @: "^ string_of_int (d) ^ " ] (" ^
@@ -502,9 +494,10 @@
     (match parse_term_list rest with
       | (l, (Delim "]") :: cont) ->
         let tp = match l with
-          | [] -> top_type_term
-          | Var (_, _, tp, _)::_ -> tp
-          | Term (_, tps, _)::_ -> tps.(0) in
+          | [] -> TVar "a"
+          | SVar (_, _, ty, _)::_ -> ty
+          | TVar _ as ty::_ -> ty
+          | Term (_, tys, _)::_ -> tys.(0) in
         code_list [|list_tp tp|] (fun x -> x) l, cont
       | _ -> failwith "parse_term: list not closed"
     )
@@ -518,7 +511,7 @@
     (match parse_type rest with
       | (ty, (Delim "@:") :: (Text deg) :: (Delim "]") :: cont) ->
 	let (l, c) = parse_bracketed_list cont in
-	(Var (v, int_of_string (deg), ty, of_list l), c)
+	(SVar (v, int_of_string deg, ty, of_list l), c)
       | _ -> failwith "parse_term: var not closed"
     )
   | (Text n) :: Delim "[" :: Delim "@:" :: rest ->
@@ -575,29 +568,29 @@
 (* --- Rules for special built-in functions --- *)
 
 let brackets_rules = 
-  [(Term (brackets_name, [|Var ("b",0,top_type_term,[||])|], [|Var ("x", 0, Var("a",0,top_type_term,[||]),[||])|]),
-    Var ("x", 0, Var ("a",0,top_type_term,[||]), [||]))]
+  [(Term (brackets_name, [|TVar "b"|], [|SVar ("x", 0, TVar "a",[||])|]),
+    SVar ("x", 0, TVar "a", [||]))]
 let verbatim_rules = 
-  [(Term (verbatim_name, [|Var ("b",0,top_type_term,[||])|], [|Var ("x",0,Var ("a",0,top_type_term,[||]),[||])|]),
-    Var ("x", 0, Var ("a",0,top_type_term,[||]), [||]))]
+  [(Term (verbatim_name, [|TVar "b"|], [|SVar ("x",0,TVar "a",[||])|]),
+    SVar ("x", 0, TVar "a", [||]))]
 let if_then_else_rules = [
-  (Term (if_then_else_name, [|Var ("a",0,top_type_term,[||])|],
+  (Term (if_then_else_name, [|TVar "a"|],
          [|code_bool true;
-           Var ("x",0,Var ("a",0,top_type_term,[||]),[||]);
-           Var ("y",0,Var ("a",0,top_type_term,[||]),[||])|]),
-   Var ("x",0,Var ("a",0,top_type_term,[||]),[||]));
-  (Term (if_then_else_name, [|Var ("a",0,top_type_term,[||])|],
+           SVar ("x",0,TVar "a",[||]);
+           SVar ("y",0,TVar "a",[||])|]),
+   SVar ("x",0,TVar "a",[||]));
+  (Term (if_then_else_name, [|TVar "a"|],
          [|code_bool false;
-           Var ("x",0,Var ("a",0,top_type_term,[||]),[||]);
-           Var ("y",0,Var ("a",0,top_type_term,[||]),[||])|]),
-   Var ("y",0,Var ("a",0,top_type_term,[||]),[||]))]
+           SVar ("x",0,TVar "a",[||]);
+           SVar ("y",0,TVar "a",[||])|]),
+   SVar ("y",0,TVar "a",[||]))]
 
-let varx_te = Var ("x", 0, Var ("p",0,top_type_term,[||]), [||])
-let preprocess_rules = [(Term (preprocess_name, [|Var ("q",0,top_type_term,[||])|], [|varx_te|]), varx_te)]
+let varx_te = SVar ("x", 0, TVar "p", [||])
+let preprocess_rules = [(Term (preprocess_name, [|TVar "q"|], [|varx_te|]), varx_te)]
 
 let string_quote_rules = 
-  [(Term (string_quote_name, [|string_tp|], [|Var ("s", 0, string_tp, [||])|]),
-    Var ("s", 0, string_tp, [||]))]
+  [(Term (string_quote_name, [|string_tp|], [|SVar ("s", 0, string_tp, [||])|]),
+    SVar ("s", 0, string_tp, [||]))]
 
 let additional_xslt_rules = 
   [(Term (additional_xslt_name, [|string_tp|], [||]), code_string " ")]

Modified: trunk/Toss/Term/CodingTest.ml
===================================================================
--- trunk/Toss/Term/CodingTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/CodingTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -8,10 +8,10 @@
       let test_code_decode_tt tt =
 	let tt1 = decode_term_type (code_term_type tt) in	
 	assert_equal ~printer:(fun x -> type_to_string x) tt tt1 in
-      let tt1 = Term ("ala", toplevel_type, [||]) in
-      let tt2 = Term ("bolek", toplevel_type, [|tt1; tt1|]) in
-      let tt3 = Term (Term.fun_type_name, toplevel_type, [|tt1; tt2; tt1|]) in
-      let tt4 = Var ("zmienna",0,top_type_term,[||]) in
+      let tt1 = Term ("ala", [||], [||]) in
+      let tt2 = Term ("bolek", [||], [|tt1; tt1|]) in
+      let tt3 = Term (Term.fun_type_name, [||], [|tt1; tt2; tt1|]) in
+      let tt4 = TVar "zmienna" in
       test_code_decode_tt tt1;
       test_code_decode_tt tt2;
       test_code_decode_tt tt3;
@@ -23,11 +23,11 @@
       let test_code_decode_te te =
 	let te1 = decode_term (code_term te) in	
 	assert_equal ~printer:(fun x -> term_to_string x) te te1 in
-      let ty = Term ("text", toplevel_type, [||]) in
+      let ty = Term ("text", [||], [||]) in
       let term1 = Term ("ala", [|ty|], [||]) in
       let term2 = Term ("bolek", [|ty|], [|term1|]) in
       let term3 = Term ("cynik", [|ty|], [|term1; term2|]) in
-      let term4 = Var ("zmienna", 0, Var ("a1",0,top_type_term,[||]), [| |]) in
+      let term4 = SVar ("zmienna", 0, TVar "a1", [| |]) in
       test_code_decode_te term1;
       test_code_decode_te term2;
       test_code_decode_te term3;
@@ -53,10 +53,10 @@
 	let sd1 = decode_syntax_definition (code_syntax_definition sd) in	
 	assert_equal ~printer:(fun x -> "syntax definition test") sd sd1 in
       let se1 = SyntaxDef.Str "napisek" in
-      let se2 = SyntaxDef.Tp (Var ("eee",0,top_type_term,[||])) in
+      let se2 = SyntaxDef.Tp (TVar "eee") in
       let sd1 = SyntaxDef.SDtype [se1; se2] in
-      let sd2 = SyntaxDef.SDfun ([se2; se1; se1], Term ("aaa", toplevel_type, [||])) in
-      let sd3 = SyntaxDef.SDvar ([se2;se2;se1;se1], Term("qza", toplevel_type, [||])) in
+      let sd2 = SyntaxDef.SDfun ([se2; se1; se1], Term ("aaa", [||], [||])) in
+      let sd3 = SyntaxDef.SDvar ([se2;se2;se1;se1], Term("qza", [||], [||])) in
       test_code_decode_sd sd1;
       test_code_decode_sd sd2;
       test_code_decode_sd sd3;

Modified: trunk/Toss/Term/ParseArc.ml
===================================================================
--- trunk/Toss/Term/ParseArc.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/ParseArc.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -11,8 +11,8 @@
    [term] does not have [substitution] applied. *)
 type parser_elem = 
   | Token of string
-  | PTerm of term * substitution * int   (* From [parsed_elems], [cstrn]
-                                           and [endpos] of {!parser_arc}. *)
+  | PTerm of term * substs * int   (* From [parsed_elems], [cstrn]
+                                      and [endpos] of {!parser_arc}. *)
 
 (* Print a parser elem. *)
 let elem_str = function 
@@ -33,11 +33,13 @@
   spos : int;                      (* Start position of the arc. *)
   endpos : int;                    (* The current end position of the
                                       arc. FIXME: unnecessary? *)
-  cstrn : substitution;            (* Constraint for the arc. *)
+  cstrn : substs;                       (* Constraint for the arc. *)
 }
 
 (* --- Extending and closing arcs --- *)
 
+let debug = ref false
+
 (* This function takes a parser element and an arc and extends the arc
    if the next free position in the arc matches the given
    element. Maching means equality for tokens and inference constraint
@@ -76,13 +78,30 @@
         precheck_eq ty pty;*)
         (* Combine the constraints so far, and extend them to cover
            the new parsed element. *)
-        let cstrn = combine_mgu_sb t_cstrn arc.cstrn in
+        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" 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');*)
         let cstrn =
-          mgu cstrn [apply_sb cstrn pty, apply_sb cstrn ty] in
+          mgu cstrn' [apply_sbs cstrn' pty, apply_sbs cstrn' ty] in
+        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
+          "cstrn=%s\n%!"
+          (substs_str cstrn);*)
         Some
           {arc with rem_elems; parsed_elems = elem::arc.parsed_elems;
             endpos = t_endpos; cstrn}
-      with UNIFY -> None
+      with UNIFY ->
+        (*if !debug && arc.sd_n = "Fif_\?_then_\?_else_\?" then Printf.printf
+          "NO UNIFY\n%!";*)
+        None
 
 (* Extends all the arcs in the given list that can be extended
    and removes all other arcs. *)
@@ -105,14 +124,14 @@
   if arc.rem_elems <> [] then None else
     let args = rev_map match_of_tok arc.parsed_elems in
     let res_term = match arc.sd_res with
-      | SD_Term ty when ty = toplevel_type -> 
+      | SD_Term [||] -> 
         Term (BuiltinLang.term_type_cons_name, [|BuiltinLang.term_type_tp|],
 	      [|Coding.code_string arc.sd_n;
                 Coding.code_list
                   [|BuiltinLang.list_tp BuiltinLang.term_type_tp|]
                   (fun x -> x) args|])
       | SD_Term tp -> Term (arc.sd_n, tp, Array.of_list args)
-      | SD_Var tp -> Var (arc.sd_n, 0, tp, Array.of_list args) in
+      | SD_Var tp -> SVar (arc.sd_n, 0, tp, Array.of_list args) in
     (* Note that [arc.cstrn] is not applied to [res_term]. *)
     Some (PTerm (res_term, arc.cstrn, arc.endpos), arc.spos)  
 
@@ -127,7 +146,7 @@
   let elems, sd_res =
     match sdef with
       | SDtype elems -> incr fresh_suffix;
-        freshen elems, SD_Term toplevel_type
+        freshen elems, SD_Term [||]
       | SDfun (elems, ty) -> incr fresh_suffix;
         freshen elems, SD_Term [|suffix !fresh_suffix ty|]
       | SDvar (elems, ty) ->
@@ -139,7 +158,7 @@
     rem_elems = elems;
     parsed_elems = [];
     endpos = spos;
-    cstrn = empty_sb;
+    cstrn = empty_sbs;
   }
 
 (* TODO: clean-up the description.
@@ -264,9 +283,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;*)
   let type_of_pe = function Token _ -> None
     | PTerm (te, cstrn, _) ->
-      let result = apply_sb cstrn te in
+      let result = apply_sbs cstrn te in
       Some result 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-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/ParseArc.mli	2012-07-15 20:43:16 UTC (rev 1745)
@@ -9,8 +9,8 @@
     have [substitution] applied. *)
 type parser_elem = 
   | Token of string
-  | PTerm of term * substitution * int   (** From [parsed_elems], [cstrn]
-                                             and [endpos] of {!parser_arc}. *)
+  | PTerm of term * substs * 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 : substitution;            (** Constraint for the arc. *)
+  cstrn : substs;                  (** Constraint for the arc. *)
 }
 
 

Modified: trunk/Toss/Term/ParseArcTest.ml
===================================================================
--- trunk/Toss/Term/ParseArcTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/ParseArcTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -9,15 +9,15 @@
     (fun () ->
       let elem_eq res e = assert_equal ~printer:(fun x -> x) res (elem_str e) in
       let type_decls_list = [
-	(list_cons_name, Term (Term.fun_type_name, toplevel_type, 
-                            [|Var ("a",0,top_type_term,[||]);
+	(list_cons_name, Term (Term.fun_type_name, [||], 
+                            [|TVar "a";
                               list_tp_a; list_tp_a|]));
 	(list_nil_name, list_tp_a);
 	(boolean_true_name, boolean_tp);
 	(boolean_false_name, boolean_tp)] in
       let tps = Hashtbl.create 7 in
       List.iter (fun (n, t) -> Hashtbl.add tps n t) type_decls_list;
-      let var_x_a_sd = SDvar ([Str "x"], Var ("a",0,top_type_term,[||])) in
+      let var_x_a_sd = SDvar ([Str "x"], TVar "a") in
       let sdefs = [list_cons_sd; list_nil_sd;
 		   boolean_true_sd; boolean_false_sd; var_x_a_sd] in
       let arcs = List.map (fun sd -> create_arc sd (name_of_sd sd) 0) sdefs in
@@ -45,15 +45,15 @@
   "parse" >::
     (fun () ->
       let type_decls_list = [
-	(list_cons_name, Term (Term.fun_type_name, toplevel_type,
-                               [|Var ("a",0,top_type_term,[||]);
+	(list_cons_name, Term (Term.fun_type_name, [||],
+                               [|TVar "a";
                                  list_tp_a; list_tp_a|]));
 	(list_nil_name, list_tp_a);
 	(boolean_true_name, boolean_tp);
 	(boolean_false_name, boolean_tp)] in
       let tps = Hashtbl.create 7 in
       List.iter (fun (n, t) -> Hashtbl.add tps n t) type_decls_list;
-      let var_x_a_sd = SDvar ([Str "x"], Var ("a",0,top_type_term,[||])) in
+      let var_x_a_sd = SDvar ([Str "x"], TVar "a") in
       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

Modified: trunk/Toss/Term/Rewriting.ml
===================================================================
--- trunk/Toss/Term/Rewriting.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/Rewriting.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -14,7 +14,9 @@
 let is_left_linear (lhs, _) =
   let rec vars = function
     | Term (_, _, a) -> List.concat (Array.to_list (Array.map vars a))
-    | Var (v, _, _, a) -> v :: List.concat (Array.to_list (Array.map vars a)) in
+    | TVar _ -> []
+    | SVar (v, _, _, a) ->
+      v :: List.concat (Array.to_list (Array.map vars a)) in
   let vs = List.sort String.compare (vars lhs) in
   let rec has_duplicates = function [] | [_] -> false 
     | x :: y :: _ when x = y -> true | x :: r ->  has_duplicates r in
@@ -40,6 +42,8 @@
 
 exception NO_MATCH
 
+(* TODO: lukstafi proposes to use ISA-matching for rewriting. *)
+
 (* Checking match returning lists to substitute for and detecting clash.
    In documentation this is described as STEP 1. (FIXME: docs)
    We assume that the rewrite rules are correct and therefore have no
@@ -60,9 +64,11 @@
       raise NO_MATCH
     | (Term _, _) -> 
       (true, [])
-    | (Var (n, d, _, [||]), t2) -> 
+    | (SVar (n, d, _, [||]), t2) -> 
       (false, [(n, (d, fn_apply d Coding.decode_term t2))])
-    | (Var (n, _, _, a), _) ->
+    | (TVar _, _ | _, TVar _) ->
+      failwith "type variable inside rr"
+    | (SVar (n, _, _, a), _) ->
       (* Printf.printf "check_clash_match: [2] %s %d\n" n (Array.length a); *)
       failwith "functional var on left side of rr" in
   match (term1, term2) with  (* now term1 = f (args) *)
@@ -99,15 +105,17 @@
       match term, result with
         | Term (_, oldtys, _), Term (n, _, args) ->
           Term (n, oldtys, args)
-        | Var (_, _, oldty, _), Term (n, _, args) ->
+        | SVar (_, _, oldty, _), Term (n, _, args) ->
           Term (n, [|oldty|], args)
-        | Var (_, _, oldty, _), Var (n, d, _, args) ->
-          Var (n, d, oldty, args)
-        | Term (_, [|oldty|], _), Var (n, d, _, args) ->
-          Var (n, d, oldty, args)
+        | SVar (_, _, oldty, _), SVar (n, d, _, args) ->
+          SVar (n, d, oldty, args)
+        | Term (_, [|oldty|], _), SVar (n, d, _, args) ->
+          SVar (n, d, oldty, args)
           (* failwith "apply_check_clash: rewriting non-var with var" *)
-        | Term _, Var (n, d, _, args) ->
-          Var (n, d, term, args)
+        | Term _, SVar (n, d, _, args) ->
+          SVar (n, d, term, args)
+        | TVar _, _ | _, TVar _ ->
+          failwith "rewrite: unexpected type variable"
 
 (* The final rewrite function that takes care of function names in terms. *)
 let rewrite (Rules (rules)) term = 
@@ -122,14 +130,16 @@
 let rec normalise_special_id_one name = function
   | Term (n, _, [|a|]) when n = name -> a
   | Term (n, t, a) -> Term (n, t, Array.map (normalise_special_id_one name) a)
-  | Var (n, d, ty, a) -> 
-    Var (n, d, ty, Array.map (normalise_special_id_one name) a)
+  | TVar _ -> failwith "normalise_special_id_one: unexpected type variable"
+  | SVar (n, d, ty, a) -> 
+    SVar (n, d, ty, Array.map (normalise_special_id_one name) a)
 
 let rec normalise_special_id_all name = function
   | Term (n, _, [|a|]) when n = name -> normalise_special_id_all name a
   | Term (n, t, a) -> Term (n, t, Array.map (normalise_special_id_all name) a)
-  | Var (n, d, ty, a) -> 
-    Var (n, d, ty, Array.map (normalise_special_id_all name) a)
+  | TVar _ -> failwith "normalise_special_id_all: unexpected type variable"
+  | SVar (n, d, ty, a) -> 
+    SVar (n, d, ty, Array.map (normalise_special_id_all name) a)
 
 let normalise_brackets = normalise_special_id_all brackets_name
 let normalise_verbatim = normalise_special_id_one verbatim_name
@@ -141,8 +151,9 @@
     rr_spec normalised
   | Term (n, t, a) ->
     Term (n, t, Array.map (normalise_special rr_spec) a)
-  | Var (n, d, ty, a) ->
-    Var (n, d, ty, Array.map (normalise_special rr_spec) a)
+  | TVar _ -> failwith "normalise_special: unexpected type variable"
+  | SVar (n, d, ty, a) ->
+    SVar (n, d, ty, Array.map (normalise_special rr_spec) a)
 
 let cMEM_USE_INCREASE_FACTOR = 128
 
@@ -190,9 +201,10 @@
   | Term (n, t, a) ->
     let (steps, res) = basic_normalise_arr rr rr_spec m a in
     (steps, Term (n, t, res))
-  | Var (n, d, ty, a) -> 
+  | TVar _ -> failwith "basic_normalise: unexpected type variable"
+  | SVar (n, d, ty, a) -> 
     let (steps, res) = basic_normalise_arr rr rr_spec m a in
-    (steps, Var (n, d, ty, res))
+    (steps, SVar (n, d, ty, res))
 
 
 let normalise mem rules is_special rewrite_special inp_term =

Modified: trunk/Toss/Term/RewritingTest.ml
===================================================================
--- trunk/Toss/Term/RewritingTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/RewritingTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -10,8 +10,8 @@
       let test_rr rl res t =
 	let rs = new_rules_set rl in
 	assert_equal ~printer:(fun x-> x) res (term_to_string (rewrite rs t)) in
-      let var_x_b = Var ("x", 0, boolean_tp, [||]) in
-      let var_y_b = Var ("y", 0, boolean_tp, [||]) in
+      let var_x_b = SVar ("x", 0, boolean_tp, [||]) in
+      let var_y_b = SVar ("y", 0, boolean_tp, [||]) in
       let rr1 =
 	(Term ("Fand",[|boolean_tp|],[|code_bool true;code_bool true|]),code_bool true) in
       let rr2 = (Term ("Fand", [|boolean_tp|], [|var_x_b; var_y_b|]), code_bool false) in
@@ -38,8 +38,8 @@
 	Hashtbl.add rs n (new_rules_set rl);
 	assert_equal ~printer:(fun x-> x) res
           (term_to_string (normalise m rs (fun x -> false) (fun x -> x) t)) in
-      let var_x_b = Var ("x", 0, boolean_tp, [||]) in
-      let var_y_b = Var ("y", 0, boolean_tp, [||]) in
+      let var_x_b = SVar ("x", 0, boolean_tp, [||]) in
+      let var_y_b = SVar ("y", 0, boolean_tp, [||]) in
       let rr1 = 
 	(Term ("Fand",[|boolean_tp|],[|code_bool true;code_bool true|]),code_bool true) in
       let rr2 = (Term ("Fand", [|boolean_tp|], [|var_x_b; var_y_b|]), code_bool false) in

Modified: trunk/Toss/Term/SyntaxDef.ml
===================================================================
--- trunk/Toss/Term/SyntaxDef.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/SyntaxDef.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -76,9 +76,9 @@
     let rec revnumbers i = if i = 0 then [] else i :: (revnumbers (i-1)) in
     let numbers i = List.map string_of_int (List.rev (revnumbers i)) in
     let s = concat_map (function Str _ -> [] | Tp _ -> ["a"]) sel in
-    let arg_of s1 s2 = Var (s1 ^ "_" ^ s2, 0, top_type_term, [||]) in
+    let arg_of s1 s2 = TVar (s1 ^ "_" ^ s2) in
     let args = List.map2 arg_of s (numbers (List.length s)) in
-    Term (name_of_sd sd, toplevel_type, of_list args)
+    Term (name_of_sd sd, [||], of_list args)
   | _ -> failwith "type of sd on non-type definition"
 
 
@@ -89,9 +89,9 @@
   match sd with
     | SDtype _ -> None
     | SDfun (sel, ty)-> Some (if (ts = []) then ty else
-        Term (Term.fun_type_name, toplevel_type, of_list (ts @ [ty])))
+        Term (Term.fun_type_name, [||], of_list (ts @ [ty])))
     | SDvar (sel, ty)-> Some (if (ts = []) then ty else 
-        Term (Term.fun_type_name, toplevel_type, of_list (ts @ [ty])))
+        Term (Term.fun_type_name, [||], of_list (ts @ [ty])))
 
 (* Syntax definition for un-applied syntax definition as function. *)
 let func_sd_of_sd sd =
@@ -243,16 +243,16 @@
     split_sd_name n
   else [Some (n)]
 
+(* FIXME: remainder of the old Speagram distinction between types and terms *)
 let rec display_type = function
-  | tp when tp = top_type_term -> "ttyyppee"         (* FIXME *)
-  | Var (n, 0, tp, [||]) when tp = top_type_term -> "?" ^ n
-  | Var _ -> failwith "display_type on non-type variable"
-  | Term (n, tp, arr) when n = Term.fun_type_name && tp = toplevel_type ->
+  | TVar n -> "?" ^ n
+  | SVar _ -> failwith "display_type on a sharing variable"
+  | Term (n, [||], arr) when n = Term.fun_type_name ->
     let l = Array.length arr in
     let (a, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
     let args = List.map display_type (Array.to_list a) in
     "(" ^ (String.concat ", " args) ^ ") --> " ^ (display_type r)    
-  | Term (n, tp, a) when tp = toplevel_type ->
+  | Term (n, [||], a) ->
     let args = List.map display_type (Array.to_list a) in
     display_sd (split_sdef_name n) args
   | Term _ -> failwith "display_type: non-type term"
@@ -284,7 +284,8 @@
     ) in
   let flat_grammar_name_of_type = function
     | Term (n, _, _) -> "$" ^ String.sub n 1 ((String.length n) - 1)
-    | Var _ -> "$@object" in
+    | SVar _ -> "$@object"
+    | TVar _ -> "$@object" in
   let flat_grammar_name_of_se = function
     | Tp ty -> flat_grammar_name_of_type ty
     | Str s -> if is_all_letters s then s else raise NONLEXICAL in

Modified: trunk/Toss/Term/SyntaxDefTest.ml
===================================================================
--- trunk/Toss/Term/SyntaxDefTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/SyntaxDefTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -5,7 +5,7 @@
 let tests = "SyntaxDef" >::: [
   "name of sd" >::
     (fun () ->
-      let sel1 = [Str "[list]"; Str "of"; Tp (Var ("a",0,top_type_term,[||]))] in
+      let sel1 = [Str "[list]"; Str "of"; Tp (TVar "a")] in
       let n = unique_name_of_sd (SDtype sel1) [name_of_sd (SDtype sel1)] in
       assert_equal ~printer:(fun x -> x) "T\\lslist\\rs_of_\\?_0\\" n;
     );
@@ -20,7 +20,7 @@
 	assert_equal ~printer:(fun x -> x) res_sn sn in
       let sd1 = SDtype [Str "ala_ma_kota"] in
       let sd2 = SDtype [Str "\\atala"; Str "_"; Str "\\?"; Str "m\\_a";
-			Str "\\\\";Str "maa\\"; Tp (Var ("a",0,top_type_term,[||]));
+			Str "\\\\";Str "maa\\"; Tp (TVar "a");
                         Str "kot@"] in
       test_split "Tala\\_ma\\_kota" "Sala_ma_kota" sd1;
       test_split "T\\\\atala_\\__\\\\?_m\\\\\\_a_\\\\\\\\_maa\\\\_\\?_kot\\at"

Modified: trunk/Toss/Term/TRS.ml
===================================================================
--- trunk/Toss/Term/TRS.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/TRS.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -151,7 +151,7 @@
   let elem_of_td (n, ty) = 
     if n.[0] = c then
       match ty with
-	| Term (name, tp, arr) when name = Term.fun_type_name && tp=toplevel_type->
+	| Term (name, [||], arr) when name = Term.fun_type_name->
           let l = Array.length arr in
           let (a, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
           [(n, Array.to_list a, r)]
@@ -175,7 +175,8 @@
 
 let rec has_vars = function
   | Term (_, _, args) -> List.exists has_vars (Array.to_list args)
-  | Var _ -> true
+  | TVar _ -> false                     (* FIXME: rewriting via ISA-matching *)
+  | SVar _ -> true
 
 (* Rewriting special functions given a system. *)
 let rec rewrite_special_funs sys = function
@@ -387,7 +388,8 @@
     | (te, _) -> 
       (* FIXME: at step 4 the "types" will get displayed properly *)
       let ty = match te with
-        | Var (_, _, ty, _) -> ty
+        | SVar (_, _, ty, _) -> ty
+        | TVar _ as ty -> ty
         | Term (_, tys, _) -> tys.(0) in
       if xml_out then
 	"<trs-result>\n" ^

Modified: trunk/Toss/Term/TRSTest.ml
===================================================================
--- trunk/Toss/Term/TRSTest.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/TRSTest.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -53,7 +53,7 @@
     (fun () -> test "simple_algo";);
   (* FIXME: hangs on trashing memory *)
   (*"test entanglement" >::
-    (fun () -> test "entanglement";);*)
+  (fun () -> test "entanglement";);*)
   "test differentiation" >::
     (fun () -> test "differentiation";);
 ]

Modified: trunk/Toss/Term/Term.ml
===================================================================
--- trunk/Toss/Term/Term.ml	2012-07-10 22:44:46 UTC (rev 1744)
+++ trunk/Toss/Term/Term.ml	2012-07-15 20:43:16 UTC (rev 1745)
@@ -5,74 +5,109 @@
 
     Hierarchical terms have the form: [f(s_1, ..., s_m; t_1, ...,
     t_n)] where [f] is a (function/constant/class) symbol, terms [s_1,
-    ..., s_m] are called direct supertypes and terms [t_1, ..., t_n]
-    are called direct subterms of the term, or [X(s)], where [X] is a
-    variable symbol and term [s] is called the type of the variable.
-    When [f(s_1, ..., s_m; t_1, ..., t_n)], resp. [X(s)] is not a
-    subterm or supertype of another term, we call [f], resp. [X] its
-    head symbol. Hierarchical terms are related by [ISA] as formally
+    ..., s_m] are called {i direct supertypes} and terms [t_1, ...,
+    t_n] are called {i direct subterms} of the term; or [X(s)] but not
+    as a direct supertype, where [X] is a sharing variable symbol and
+    term [s] is called the type of the variable, and also its direct
+    supertype (especially when we don't distinguish between variables
+    and other terms); or [?V] (can be a direct supertype), where [?V]
+    is a type variable symbol.  For a term [f(s_1, ..., s_m; t_1, ...,
+    t_n)], resp. [X(s)] or [?V], we call [f], resp. [X] or [?V] its
+    head symbol. We call [X(s)] {i sharing variables} and [?V] {i type
+    variables}, and call them variables when not distinguishing
+    between them. Hierarchical terms are related by [ISA] as formally
     presented below; we drop "hierarchical" when referring to terms
     for convenience.
 
+    A term [s] is a {i supertype} of [t] when it is a direct
+    supertype of [t], or is a direct supertype of a supertype of
+    [t]. A term [t'] is a {i subterm} of [t] when it is a direct
+    subterm of [t], or is a direct subterm of either a subterm or a
+    supertype of [t]. For terms [s] and [t], by [s=t] we denote
+    sytanctic equality of [s] and [t].
+
+    We require certain conditions to hold on well-formed terms,
+    reiterated when we formally introduce well-formedness:
+
+    {ul
+    {- for any two occurrences of a sharing variable [X(s)] and [X(s')],
+    [s=s'],}
+    {- for any two supertypes [s] and [s'] of a term, if they have the
+    same head symbol, they are syntactically equal: [s=s'].}}
+
+    We define a path in a term as a sequence of symbol-number pairs,
+    where the first symbol is the head symbol of a term or its
+    supertype, the first number is the position in the subterm list in
+    that term or supertype, and the remaining of a path selects a
+    subterm in the indicated subterm recursively. Formally, we say
+    that a term [t] has a subterm [t'] at path [p=(f,i),p'], denoted
+    [t|_p=t'], when either [t] or one of its supertypes is equal to
+    [f(...;t_1,...,t_i,...)] and [t_i|_p'=t']; also, [t|_e=t] for
+    empty path [e].
+
     We call the {i upper grounding} of a term [t], [ug(t)], the term
-    [t] with all occurrences of [X(s)] for any variable symbol [X] and
-    term [s] replaced by [s].
+    [t] with all occurrences of [X(s)] for any sharing variable symbol
+    [X] and term [s] replaced by [s]. We call a term {i type-ground}
+    when it does not contain type variables. We call a {i
+    type-substitution} a substitution for type variables.
 
-    We start by defining [t ISA t'] for [t] and [t'] ground terms
-    (i.e. terms without occurrences of variable symbols). 
-    It holds if and only if one of the following holds:
+    We define [ISA] for type-ground terms first. [t ISA t'] holds if
+    and only if one of the following holds:
 
     {ul
-    {- [t' = Type] for the top symbol [Type],}
-    {- [s_i ISA g(s'_1, ..., s'_m'; t'_1, ..., t'_n')] for some i,
-    where [s(t)=f(s_1, ..., s_m; t_1, ..., t_n)] and
-    [r(t')=g(s'_1, ..., s'_m'; t'_1, ..., t'_n')]}
+    {- [s_i ISA t'] for some i, where [t=f(s_1, ..., s_m; t_1, ..., t_n)],}
+    {- [t' = X(s)] and [t ISA s],}
+    {- [t = X(s)], [t' = Y(s')], and [s ISA s'],}
+    {- the following two conditions both hold:
+    {ul
     {- [s_i ISA s'_i] for all [i], [t_i ISA t'_i] for all [i],
-    where [s()t=f(s_1, ..., s_m; t_1, ..., t_n)] and
-    [r(t')=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]}}
+    where [t=f(s_1, ..., s_m; t_1, ..., t_n)] and
+    [t'=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]}
+    {- for any paths [p,p'] in [t'], if they select the same sharing
+    variable, then they are also paths in [t], and [t|_p = t|_p'].}}}}
 
-    Actually we sometimes do not put a special case for the top symbol
-    [Type] into algorithms, and therefore we rely on well-formed sets
-    of declarations that no term except [Type] has no direct
-    supertypes.
+    We consider a sharing variable to be strictly more general than its
+    type. Note that the second part of the last condition only needs
+    to be checked at the root (i.e. only for the originally compared
+    terms, since if it holds, it also holds for subterms and
+    supertypes).
 
-    We define {i ground substitution over variables [V]} by extending
-    into a function over terms in the standard way a finite mapping
-    from all variables in [V] to terms, requiring that [X(s)] is
-    mapped to [t] only when: [t] does not contain variable symbols,
-    and [t ISA ug(s)]. By [FV(t)] we denote the free variables of [t].
+    For arbitrary terms [t] and [t'], [t ISA t'] if and only if for
+    every type-substitution [S] such that [S(t)] is type-ground, there
+    exists a type substitution [R] such that [R(t)] is type-ground
+    and [S(t) ISA R(t)].
 
-    [t ISA t'] if and only if for all ground substitutions [s] over
-    [FV(t)] there is a ground substitution [r] over [FV(t')] such that
-    [s(t) ISA r(t')].
+    Note that we do not ensure neither bottom nor a type-ground top
+    term, but a single type variable is a top term (two terms that
+    both are type variables are ISA-equivalent).
 
     (We present [ISA] as describing generality, "is less (or equally)
     general than". Notice that this relation is often presented as
     describing the amount of information, the reverse quantity, as "has
     more information than".)
 
-    We need two more essential notions.
+    We need two more, also essential notions.
 
     A {i well-formed set of declarations} is defined as a set of terms
     such that all of the following conditions hold:
 
     {ul
     {- no two terms in it have the same head symbol,}
-    {- head symbols of terms in it are not variables,}
-    {- there is at most one glb-unification result for any two (or
-    more) elements from the set,}
-    {- no term except [Type] has no direct supertypes,}
+    {- head symbols of terms in it are not variables (neither sharing
+    nor type variable symbols),}
+    {- when organizing the symbols into a partial order hierarchy
+    according to which supertypes they appear in, there is at most one
+    GLB and at most one LUB for any two symbols,}
     {- every symbol used in any term in the set is a head symbol of
     some element of the set,}
-    {- for any subterm or supertype of a term from the set, its upper
-    grounding ISA the element of the set which has the same head
+    {- for any subterm or supertype of a term from the set that is not
+    a variable, it ISA the element of the set which has the same head
     symbol.}}
 
-    Note that the last three conditions will be enforced by parsing the
+    Note that the last two conditions will be enforced by parsing the
     term to be introduced into the set of declarations, so in the
     current module we only need to check the first three
-    conditions. (The condition "must have direct supertypes" also
-    needs to be ensured in BuiltinLang.)
+    conditions.
 
     A {i well-formed term with respect to a set of declarations} given
     a well-formed set of declarations, is a term [t] such that:
@@ -80,36 +115,79 @@
     {ul
     {- its supertypes and subterms are well-formed (w.r.t. this set of
     declarations),}
-    {- there is a term [d] in the set of declarations such
-    that [t ISA d] and either the head symbol of [t] is a variable or
-    it is the same as the head symbol of [d],}
-    {- for any two occurrences [X(s)] and [X(s')] of variable symbol
-    [X], [s=s'].}}
+    {- either [t] is a type-variable, or there is a term [d] in the
+    set of declarations such that [t ISA d] and either the head symbol
+    of [t] is a sharing variable or it is the same as the head symbol
+    of [d],}
+    {- for any two occurrences of a sharing variable [X(s)] and
+    [X(s')] in [t], [s=s'],}
+    {- for any two supertypes [s] and [s'] of [t], if they have the
+    same head symbol, they are syntactically equal: [s=s'].}}
 
     We limit all terms considered to terms that are well-formed with
     respect to a set of declarations (fixed by the context; we will
-    drop constantly mentioning "w.r.t. a set of declarations"). In
-    particular, we only allow {i well-formed substitutions}:
-    substitutions that when applied to a well-formed term, return a
-    well-formed term:
+    drop constantly mentioning "w.r.t. a set of declarations").
 
-    A {i well-formed substitution} is defined by extending into a
-    function over terms in the standard way a finite mapping from
-    variables (terms whose head symbols are variable symbols) to
-    terms, requiring that [X(s)] is mapped to [t] only when [t ISA s].
+    The intent of the above definitions is to mix the ideas of
+    parametric polymorphism from type systems with a representational
+    variant of {i Typed Feature Structures} known from the literature,
+    for now reducing sharing constraints to syntactical
+    equality.
 
-    We define matching a pattern [p] against a ground term [t] (where
-    [p] and [t] are well-formed) as the problem of deciding [t ISA p]
-    by finding the substitution [r] from the definition of
-    [ISA]. (Groundness of [t] is not essential as we can rename its
-    variables to fresh constants.)
+    {3 "Unification Theory" for Hierarchical Terms}
 
+    We define {i well-formed substitutions} by extending into a
+    function over terms in the standard way a finite mapping from a
+    set of sharing variables to well-formed terms, requiring that
+    [X(s)] is mapped to [t] only when [t ISA s]. Additionally, all
+    appearances of a sharing variable in any term of the image of the
+    substitution have the same type. When applied to a well-formed
+    term, well-formed substitutions return a well-formed term.
+
+    We introduce an order on either well-formed or type-substitutions,
+    by saying that [S ISA R] when for all [t], [S(t) ISA R(t)].
+
+    We define {i isa-matching} a term [p] (called {i pattern}) against
+    a term [t] (where [p] and [t] are well-formed) as an algorithm to
+    decide [t ISA p] that returns a pair of substitutions: a type
+    subsitution [R] and a well-formed substitution where a sharing
+    variable in [p] is associated with a corresponding subterm in [t],
+    as required by [S(t) ISA R(p)] where [S] is a type-substitution
+    replacing each type-variable [?V] in [t] by a fresh constant [V( ;
+    )], and [R] is the smallest such substitution. The constants [V( ;
+    )] are only conceptual, the original variables [?V] appear if
+    needed in the result.
+
+    We define {i eq-matching} a pattern [p] against a term [t] as the
+    problem of finding a well-formed substitution [R_s] and a
+    type-substitution [R_t] such that [t = R_w(R_t(p))]. Note that if
+    eq-matching [p] against [t] exists, isa-matching also exists and
+    is the same pair of substitutions.
+
     We define {i glb-unification} ({i Greatest Lower Bound
-    Unification}) of two or more well-formed terms [t_1, ..., t_n] as:
-    given that there exist a well-formed term [t] and a well-formed
-    substitution [r], such that for all substitutions [s] such that
-    [s(r(t_i))] are all ground, for all [i], [s(t) ISA s(r(t_i))].
+    Unification}) of two well-formed terms [t_1, t_2] as the greatest
+    term [t] such that [f(;t,t) ISA f(;t_1,t_2)] (where [f] is an
+    arbitrary symbol) and variables of [t] are included in variables
+    of [t1,t2], together with the smallest type-substitution [R] such
+    that [f(;t,t) ISA R(f(;t_1,t_2))] and the well-formed substitution
+    with sharing variables in [f(;...
 
[truncated message content]