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

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

Revision: 1725
          http://toss.svn.sourceforge.net/toss/?rev=1725&view=rev
Author:   lukaszkaiser
Date:     2012-06-15 21:24:23 +0000 (Fri, 15 Jun 2012)
Log Message:
-----------
First step in merging Term with TermType.

Modified Paths:
--------------
    trunk/Toss/Term/BuiltinLang.ml
    trunk/Toss/Term/ParseArcTest.ml
    trunk/Toss/Term/SyntaxDef.ml
    trunk/Toss/Term/SyntaxDefTest.ml
    trunk/Toss/Term/TRS.ml
    trunk/Toss/Term/Term.ml
    trunk/Toss/Term/TermTest.ml
    trunk/Toss/Term/TermType.ml
    trunk/Toss/Term/TermType.mli
    trunk/Toss/Term/TermTypeTest.ml

Modified: trunk/Toss/Term/BuiltinLang.ml
===================================================================
--- trunk/Toss/Term/BuiltinLang.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/BuiltinLang.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -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_type (list_name, [|t|])
-let list_tp_a = list_tp (Type_var "a")
+let list_tp t = TTerm (list_name, [|t|])
+let list_tp_a = list_tp (TVar ("a", [||], 0, [||]))
 
 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 (Type_var "a"); Str ","; Tp list_tp_a],
+let list_cons_sd = SDfun ([Tp (TVar ("a",[||],0,[||])); Str ","; Tp list_tp_a],
 			   list_tp_a)
 let list_cons_name = name_of_sd list_cons_sd
 
@@ -147,8 +147,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 (Type_var "a_1"); Str "be";
-  Tp (Type_var "a_1")], input_rewrite_rule_tp)
+let let_be_sd = SDfun ([Str "let"; Tp (TVar ("a_1",[||],0,[||])); Str "be";
+  Tp (TVar ("a_1",[||],0,[||]))], input_rewrite_rule_tp)
 let let_be_name = name_of_sd let_be_sd
 
 let priority_input_rewrite_rule_sd = SDtype ([Str "priority";
@@ -158,8 +158,9 @@
 let priority_input_rewrite_rule_tp = 
   type_of_sd priority_input_rewrite_rule_sd
 
-let let_major_be_sd = SDfun ([Str "let"; Str "major"; Tp (Type_var "a_1");
-  Str "be"; Tp (Type_var "a_1")], priority_input_rewrite_rule_tp)
+let let_major_be_sd = 
+  SDfun ([Str "let"; Str "major"; Tp (TVar ("a_1",[||],0,[||])); Str "be";
+          Tp (TVar ("a_1",[||],0,[||]))], priority_input_rewrite_rule_tp)
 let let_major_be_name = name_of_sd let_major_be_sd
 
 let fun_definition_sd = SDtype ([Str "fun"; Str "definition"])
@@ -184,43 +185,44 @@
 
 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_type (exception_cl_name, [|t|])
+let exception_cl_tp t = TTerm (exception_cl_name, [|t|])
 
 let exception_sd = 
-  SDfun ([Str "!"; Str "!"; Tp (Type_var "a"); Str "!";Str "!";],
-          exception_cl_tp (Type_var "other_than_a!"))
+  SDfun ([Str "!"; Str "!"; Tp (TVar ("a",[||],0,[||])); Str "!";Str "!";],
+          exception_cl_tp (TVar ("other_than_a!",[||],0,[||])))
 let exception_name = name_of_sd exception_sd
 
 let exn_ok_sd = 
-  SDfun ([Str "+"; Str "+"; Tp (Type_var "a"); Str "+";Str "+";],
-          exception_cl_tp (Type_var "a")) (* Here it should be a! *)
+  SDfun ([Str "+"; Str "+"; Tp (TVar ("a",[||],0,[||])); Str "+";Str "+";],
+          exception_cl_tp (TVar ("a",[||],0,[||]))) (* 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 (Type_var "b"); Str ")"],
-                         Type_var "b")
+let brackets_sd = SDfun ([Str "("; Tp (TVar ("b",[||],0,[||])); Str ")"],
+                         TVar ("b",[||],0,[||]))
 let brackets_name = name_of_sd brackets_sd
 
 
-let verbatim_sd = 
-  SDfun ([Str "<"; Str "|"; Tp (Type_var "b"); Str "|"; Str ">"], Type_var "b")
+let verbatim_sd = SDfun ([Str "<"; Str "|"; Tp (TVar ("b",[||],0,[||]));
+                          Str "|"; Str ">"], TVar ("b",[||],0,[||]))
 let verbatim_name = name_of_sd verbatim_sd
 
 
 let if_then_else_sd = SDfun ([Str "if"; Tp boolean_tp; Str "then";
-  Tp (Type_var "a"); Str "else"; Tp (Type_var "a")], Type_var "a")
+  Tp (TVar ("a",[||],0,[||])); Str "else"; 
+  Tp (TVar ("a",[||],0,[||]))], TVar ("a",[||],0,[||]))
 let if_then_else_name = name_of_sd if_then_else_sd
 
-let eq_bool_sd = SDfun ([Tp (Type_var "a"); Str "="; Tp (Type_var "a")],
-      boolean_tp)
+let eq_bool_sd = SDfun ([Tp (TVar ("a",[||],0,[||])); Str "=";
+                         Tp (TVar ("a",[||],0,[||]))], 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 (Type_var "a");
+let code_as_term_sd = SDfun ([Str "code"; Tp (TVar ("a",[||],0,[||]));
   Str "as"; Str "term"], term_tp)
 let code_as_term_name = name_of_sd code_as_term_sd
 
@@ -276,12 +278,13 @@
 let set_command_tp = type_of_sd set_command_sd
 
 let set_prop_sd = SDfun ([Str "set"; Tp (string_tp); Str "of";
-  Tp (Type_var "a"); Str "to"; Tp (Type_var "b")], set_command_tp)
+  Tp (TVar ("a",[||],0,[||])); Str "to";
+  Tp (TVar ("b",[||],0,[||]))], set_command_tp)
 let set_prop_name = name_of_sd set_prop_sd
 
 
-let preprocess_sd = 
-  SDfun ([Str "#"; Str "#"; Str "#"; Tp (Type_var "p")], Type_var "q")
+let preprocess_sd =  SDfun ([Str "#"; Str "#"; Str "#";
+                       Tp (TVar ("p",[||],0,[||]))], TVar ("q",[||],0,[||]))
 let preprocess_name = name_of_sd preprocess_sd
 
 

Modified: trunk/Toss/Term/ParseArcTest.ml
===================================================================
--- trunk/Toss/Term/ParseArcTest.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/ParseArcTest.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -10,13 +10,14 @@
     (fun () ->
       let elem_eq res e = assert_equal ~printer:(fun x -> x) res (elem_str e) in
       let type_decls_list = [
-	(list_cons_name, Fun_type ([|Type_var "a"; list_tp_a|], list_tp_a));
+	(list_cons_name, TTerm (TermType.fun_type_name, 
+                            [|TVar ("a",[||],0,[||]); 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"], Type_var "a") in
+      let var_x_a_sd = SDvar ([Str "x"], TVar ("a",[||],0,[||])) 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 -> Arc (sd, (name_of_sd sd), [], 0)) sdefs in
@@ -44,13 +45,14 @@
   "parse" >::
     (fun () ->
       let type_decls_list = [
-	(list_cons_name, Fun_type ([|Type_var "a"; list_tp_a|], list_tp_a));
+	(list_cons_name, TTerm (TermType.fun_type_name,
+                             [|TVar ("a",[||],0,[||]); 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"], Type_var "a") in
+      let var_x_a_sd = SDvar ([Str "x"], TVar ("a",[||],0,[||])) 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 -> (sd, name_of_sd sd)) sdefs_basic in

Modified: trunk/Toss/Term/SyntaxDef.ml
===================================================================
--- trunk/Toss/Term/SyntaxDef.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/SyntaxDef.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -71,22 +71,23 @@
     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 = List.concat (List.map (function Str _ -> [] | Tp _ -> ["a"]) sel) in
-    let arg_of s1 s2 = Type_var (s1 ^ "_" ^ s2) in
+    let arg_of s1 s2 = TVar (s1 ^ "_" ^ s2, [||], 0, [||]) in
     let args = List.map2 arg_of s (numbers (List.length s)) in
-    Term_type (name_of_sd sd, of_list args)
+    TTerm (name_of_sd sd, of_list args)
   | _ -> failwith "type of sd on non-type definition"
 
 
 (* Type used in type declaration for a syntax definition. *)
 let sd_type sd = 
   let types_of_sels s = List.map (function Str _ -> [] | Tp ty -> [ty]) s in
-  let ts = of_list (List.flatten (types_of_sels (syntax_elems_of_sd sd))) in
+  let ts = List.flatten (types_of_sels (syntax_elems_of_sd sd)) in
   match sd with
     | SDtype _ -> None
-    | SDfun (sel, ty)-> Some (if (length ts = 0) then ty else Fun_type (ts, ty))
-    | SDvar (sel, ty)-> Some (if (length ts = 0) then ty else Fun_type (ts, ty))
+    | SDfun (sel, ty)-> Some (if (ts = []) then ty else
+        TTerm (TermType.fun_type_name, of_list (ts @ [ty])))
+    | SDvar (sel, ty)-> Some (if (ts = []) then ty else 
+        TTerm (TermType.fun_type_name, of_list (ts @ [ty])))
 
-
 (* Functional syntax definition corresponding to a given one. *)
 let func_sd_of_sd sd =
   let change = function Tp _ -> [Str "{"; Str "}"] | x -> [x] in
@@ -214,13 +215,16 @@
   else [Some (n)]
 
 let rec display_type = function
-  | Type_var n -> "?" ^ n
-  | Term_type (n, a) ->
+  | TVar (n, [||], 0, [||]) -> "?" ^ n
+  | TVar _ -> failwith "display_type on non-type variable"
+  | TTerm (n, arr) when n = TermType.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)    
+  | TTerm (n, a) ->
+    let args = List.map display_type (Array.to_list a) in
     display_sd (split_sdef_name n) args
-  | Fun_type (a, r) ->
-    let args = List.map display_type (Array.to_list a) in
-    "(" ^ (String.concat ", " args) ^ ") --> " ^ (display_type r)
 
 let pretty_print_sd sd =
   let pretty_print_se = function
@@ -248,9 +252,8 @@
       !is_ok
     ) in
   let flat_grammar_name_of_type = function
-    | Term_type (n, _) -> "$" ^ String.sub n 1 ((String.length n) - 1)
-    | Fun_type _ -> "$@fun"
-    | Type_var _ -> "$@object" in
+    | TTerm (n, _) -> "$" ^ String.sub n 1 ((String.length n) - 1)
+    | 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-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/SyntaxDefTest.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -5,7 +5,7 @@
 let tests = "SyntaxDef" >::: [
   "name of sd" >::
     (fun () ->
-      let sel1 = [Str "[list]"; Str "of"; Tp (Type_var "a")] in
+      let sel1 = [Str "[list]"; Str "of"; Tp (TVar ("a",[||],0,[||]))] 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,8 @@
 	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 (Type_var "a");Str "kot@"] in
+			Str "\\\\";Str "maa\\"; Tp (TVar ("a",[||],0,[||]));
+                        Str "kot@"] in
       test_split "Tala\\_ma\\_kota" "Sala_ma_kota" sd1;
       test_split "T\\\\atala_\\__\\\\?_m\\\\\\_a_\\\\\\\\_maa\\\\_\\?_kot\\at"
 	"S\\@ala|S_|S\\?|Sm\\_a|S\\\\|Smaa\\|N|Skot@" sd2;

Modified: trunk/Toss/Term/TRS.ml
===================================================================
--- trunk/Toss/Term/TRS.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/TRS.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -150,7 +150,10 @@
   let elem_of_td (n, ty) = 
     if n.[0] = c then
       match ty with
-	| Fun_type (a, r) -> [(n, Array.to_list a, r)]
+	| TTerm (name, arr) when name = TermType.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)]
 	| _ -> [(n, [], ty)]
     else [] in
   flatten (map elem_of_td tdecls)
@@ -200,10 +203,13 @@
   
 let is_better sys te1 te2 =
   let query = Term (preferred_to_name, [|code_term te1; code_term te2|]) in
+  let report i = 
+    LOG 1 "%s prefered to %s ? %i" (term_to_string te1) (term_to_string te2) i;
+    i in
   match normalise_with_sys sys query with
-    | Term (n, [||]) when n = ternary_true_name -> 1
-    | Term (n, [||]) when n = ternary_false_name -> -1
-    | te -> 0
+    | Term (n, [||]) when n = ternary_true_name -> report 1
+    | Term (n, [||]) when n = ternary_false_name -> report (-1)
+    | te -> report 0
 
 let is_best sys ht terms te =
   let cmp a b = 
@@ -232,6 +238,7 @@
   | t :: tes ->
     (* we rehash terms here because often first or first-parsed is best *)
     let terms = t :: (rev tes) in
+    LOG 1 "finding best of %i" (List.length terms);
     let best = filter (is_best sys (Hashtbl.create 64) terms) terms in
     remove_bracket_duplicates best
 
@@ -326,7 +333,7 @@
   match in_pair with
     | (te, _) when is_some (decode_sd_opt te) -> msg (
       match decode_syntax_definition te with
-        |SDtype (sels) -> "New class " ^ (msg_for_sels sels) ^ " declared."
+        | SDtype (sels) -> "New class " ^ (msg_for_sels sels) ^ " declared."
 	| SDfun (sels, _) -> "New function " ^ (msg_for_sels sels) ^" declared."
 	| SDvar (sels, _) -> "New variable " ^ (msg_for_sels sels) ^" declared."
     ) ""

Modified: trunk/Toss/Term/Term.ml
===================================================================
--- trunk/Toss/Term/Term.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/Term.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -118,12 +118,15 @@
 
 
 let rec code_term_type = function
-  | Type_var name -> Term (term_type_var_name, [|code_string name|])
-  | Fun_type (args_types, return_type) ->
+  | TVar (name, [||], 0, [||])-> Term (term_type_var_name, [|code_string name|])
+  | TVar _ -> failwith "code_term_type: non-type variable"
+  | TTerm (name, arr) when name = TermType.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, [|
       code_list code_term_type (to_list args_types);
       code_term_type return_type|])
-  | Term_type (name, args) ->
+  | TTerm (name, args) ->
     Term (term_type_cons_name, [|
       code_string name;
       code_list code_term_type (to_list args)|])
@@ -131,13 +134,13 @@
 
 let rec decode_term_type = function
   | Term (s, [|coded_name|]) when s = term_type_var_name ->
-    Type_var (decode_string coded_name)
+    TVar (decode_string coded_name, [||], 0, [||])
   | Term (s, [|coded_1; coded_2|]) when s = term_type_fun_name ->
-    Fun_type (of_list (decode_list decode_term_type coded_1),
-              decode_term_type coded_2)
+    TTerm (TermType.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_type (decode_string coded_1,
-               of_list (decode_list decode_term_type coded_2))
+    TTerm (decode_string coded_1,
+           of_list (decode_list decode_term_type coded_2))
   | _ -> raise (DECODE "term_type")
 
 
@@ -233,15 +236,15 @@
 let code_type_definition (name, arity) =
   let rec var = function
     | 0 -> []
-    | i -> Type_var ("a_" ^ (string_of_int i)) :: (var (i-1)) in
+    | i -> TVar ("a_" ^ (string_of_int i), [||], 0, [||]) :: (var (i-1)) in
   Term (type_of_name,
-        [|code_term_type (Term_type (name, of_list (var arity)))|])
+        [|code_term_type (TTerm (name, of_list (var arity)))|])
 
 
 let decode_type_definition = function
   | Term (n, [|ty|]) when n = type_of_name ->
     (match (decode_term_type ty) with
-        Term_type (name, args) -> (name, Array.length args)
+        TTerm (name, args) -> (name, Array.length args)
       | _ -> raise (DECODE "type definition 1")
     )     
   | _ -> raise (DECODE "type definition 2")
@@ -364,17 +367,19 @@
 (* --- Display terms and types as XML --- *)
 
 let rec display_type_xml = function
-  | Type_var n -> "<type_var>" ^ (make_xml_compatible n) ^ "</type_var>"
-  | Term_type (n, a) ->
+  | TVar (n, [||], 0, [||]) ->
+    "<type_var>" ^ (make_xml_compatible n) ^ "</type_var>"
+  | TVar _ -> failwith "display_type_xml: non-type variable"
+  | TTerm (n, a) ->
     "<type class=\"" ^ (make_xml_compatible n) ^ "\">\n" ^
       (String.concat "\n" (List.map display_type_xml (to_list a))) ^
       "\n</type>"
-  | Fun_type (a, r) ->
+(*  | Fun_type (a, r) ->
     "<funtype>\n<funtype-arg-types>\n" ^
       (String.concat "\n" (List.map display_type_xml (to_list a))) ^
       "\n</funtype-arg-types>\n<funtype-return-type>\n" ^
       (display_type_xml r) ^
-      "</funtype-return-type>\n</funtype>"
+      "</funtype-return-type>\n</funtype>" *)
 
 
 let rec display_term_xml = function
@@ -504,7 +509,9 @@
     let ((i, uni_sack, ty_decls), arg_tys) = fold_left type_sack (i ,[]) a in
     (match (suffix i (Hashtbl.find ty_decls n), List.rev arg_tys) with
       |	(ty, []) -> ((i+1, uni_sack, ty_decls), ty :: itys)
-      | (Fun_type (at, r), rt) -> 
+      | (TTerm (n, arr), rt) when n = TermType.fun_type_name -> 
+        let l = Array.length arr in
+        let (at, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
 	(try ((i+1, (List.combine (to_list at) rt) @ uni_sack, ty_decls), 
 	      r :: itys)
 	 with Invalid_argument _-> raise (NOT_WELL_TYPED "type_sack, term,i.a")
@@ -516,7 +523,9 @@
     let real_var_type = if code_degree = 0 then var_type else term_tp in
     (match (real_var_type, List.rev arg_tys) with
       | (ty, []) -> ((i+1, uni_sack, ty_decls), ty :: itys)
-      | (Fun_type (at, r), rt) -> 
+      | (TTerm (n, arr), rt) when n = TermType.fun_type_name -> 
+        let l = Array.length arr in
+        let (at, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
 	(try ((i+1, (List.combine (to_list at) rt) @ uni_sack, ty_decls),
 	      r :: itys)
 	 with Invalid_argument _-> raise (NOT_WELL_TYPED "type_sack, var, i.a")
@@ -549,20 +558,22 @@
 (* --- Rules for special built-in functions --- *)
 
 let brackets_rules = 
-  [(Term (brackets_name, [|Var ("x", Type_var "a", 0, [||])|]),
-    Var ("x", Type_var "a", 0, [||]))]
+  [(Term (brackets_name, [|Var ("x", TVar ("a",[||],0,[||]), 0, [||])|]),
+    Var ("x", TVar ("a",[||],0,[||]), 0, [||]))]
 let verbatim_rules = 
-  [(Term (verbatim_name, [|Var ("x", Type_var "a", 0, [||])|]),
-    Var ("x", Type_var "a", 0, [||]))]
+  [(Term (verbatim_name, [|Var ("x", TVar ("a",[||],0,[||]), 0, [||])|]),
+    Var ("x", TVar ("a",[||],0,[||]), 0, [||]))]
 let if_then_else_rules = [
   (Term (if_then_else_name, [|code_bool true;
-       Var ("x", Type_var "a", 0, [||]); Var ("y", Type_var "a", 0, [||])|]),
-   Var ("x", Type_var "a", 0, [||]));
+       Var ("x", TVar ("a",[||],0,[||]), 0, [||]);
+       Var ("y", TVar ("a",[||],0,[||]), 0, [||])|]),
+   Var ("x", TVar ("a",[||],0,[||]), 0, [||]));
   (Term (if_then_else_name, [|code_bool false;
-       Var ("x", Type_var "a", 0, [||]); Var ("y", Type_var "a", 0, [||])|]),
-   Var ("y", Type_var "a", 0, [||]))]
+       Var ("x", TVar ("a",[||],0,[||]), 0, [||]);
+       Var ("y", TVar ("a",[||],0,[||]), 0, [||])|]),
+   Var ("y", TVar ("a",[||],0,[||]), 0, [||]))]
 
-let varx_te = Var ("x", Type_var "p", 0, [||])
+let varx_te = Var ("x", TVar ("p",[||],0,[||]), 0, [||])
 let preprocess_rules = [(Term (preprocess_name, [|varx_te|]), varx_te)]
 
 let string_quote_rules = 

Modified: trunk/Toss/Term/TermTest.ml
===================================================================
--- trunk/Toss/Term/TermTest.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/TermTest.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -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_type ("ala", [| |]) in
-      let tt2 = Term_type ("bolek", [|tt1; tt1|]) in
-      let tt3 = Fun_type ([|tt1; tt2|], tt1) in
-      let tt4 = Type_var "zmienna" in
+      let tt1 = TTerm ("ala", [| |]) in
+      let tt2 = TTerm ("bolek", [|tt1; tt1|]) in
+      let tt3 = TTerm (TermType.fun_type_name, [|tt1; tt2; tt1|]) in
+      let tt4 = TVar ("zmienna",[||],0,[||]) in
       test_code_decode_tt tt1;
       test_code_decode_tt tt2;
       test_code_decode_tt tt3;
@@ -26,7 +26,7 @@
       let term1 = Term ("ala", [| |]) in
       let term2 = Term ("bolek", [|term1|]) in
       let term3 = Term ("cynik", [|term1; term2|]) in
-      let term4 = Var ("zmienna", Type_var "a1", 0, [| |]) in
+      let term4 = Var ("zmienna", TVar ("a1",[||],0,[||]), 0, [| |]) in
       test_code_decode_te term1;
       test_code_decode_te term2;
       test_code_decode_te term3;
@@ -52,10 +52,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 (Type_var "eee") in
+      let se2 = SyntaxDef.Tp (TVar ("eee",[||],0,[||])) in
       let sd1 = SyntaxDef.SDtype [se1; se2] in
-      let sd2 = SyntaxDef.SDfun ([se2; se1; se1], Term_type ("aaa",[| |])) in
-      let sd3 = SyntaxDef.SDvar ([se2; se2; se1; se1], Term_type("qza",[||])) in
+      let sd2 = SyntaxDef.SDfun ([se2; se1; se1], TTerm ("aaa",[| |])) in
+      let sd3 = SyntaxDef.SDvar ([se2; se2; se1; se1], TTerm("qza",[||])) in
       test_code_decode_sd sd1;
       test_code_decode_sd sd2;
       test_code_decode_sd sd3;
@@ -94,13 +94,15 @@
   "type reconstruction" >::
     (fun () ->
       let list_tp_a = BuiltinLang.list_tp_a in
-      let typesl = [("cons", Fun_type ([|Type_var "a"; list_tp_a|], list_tp_a));
+      let typesl = [("cons", TTerm (TermType.fun_type_name, 
+                                    [|TVar ("a",[||],0,[||]); list_tp_a;
+                                      list_tp_a|]));
 		    ("nil", list_tp_a);
 		    ("true", BuiltinLang.boolean_tp);
-		    ("1", Term_type ("int", [||]))] in
+		    ("1", TTerm ("int", [||]))] in
       let types = Hashtbl.create 5 in
       List.iter (fun (a, b) -> Hashtbl.add types a b) typesl;
-      let var_x_a = Var ("x", Type_var "a", 0, [||]) in
+      let var_x_a = Var ("x", TVar ("a",[||],0,[||]), 0, [||]) in
       let te1 = Term ("cons", [|var_x_a; Term ("nil", [||])|]) in
       let te2 = Term ("cons", [|Term ("true", [||]); te1|]) in
       let te3 = Term ("cons", [|Term ("1", [||]); te1|]) in

Modified: trunk/Toss/Term/TermType.ml
===================================================================
--- trunk/Toss/Term/TermType.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/TermType.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -5,16 +5,15 @@
 
 (* The type of term types. *)
 type term_type = 
-  | Term_type of string * term_type array 
-  | Fun_type of term_type array * term_type
-  | Type_var of string
+  | TTerm of string * term_type array 
+  | TVar of string * term_type array * int * term_type array
 
+let fun_type_name = "fffuuunnntyppe"
 
 (* Suffix type variables to rename them. *)
 let rec suffix i = function
-  | Term_type (n, a) -> Term_type (n, map (fun t -> suffix i t) a)
-  | Fun_type (a, r) -> Fun_type (map (fun t -> suffix i t) a, suffix i r)
-  | Type_var n -> Type_var (n ^ "._." ^ (string_of_int i))
+  | TTerm (n, a) -> TTerm (n, map (fun t -> suffix i t) a)
+  | TVar (n, a, b, c) -> TVar (n ^ "._." ^ (string_of_int i), a, b, c)
 
 
 (* --- Type Unification --- *)
@@ -28,12 +27,11 @@
 (* Application of substitutions. *)
 let rec apply subst tp =
   let rec apply_var v = function
-    | [] -> Type_var v
+    | [] -> TVar (v, [||], 0, [||])
     | (n, ty) :: ss -> if (v = n) then ty else apply_var v ss in
   match tp with
-    | Type_var n -> apply_var n subst
-    | Term_type (n, a) -> Term_type (n, map (apply subst) a)
-    | Fun_type (a, r) -> Fun_type (map (apply subst) a, apply subst r)
+    | TVar (n, _, _, _) -> apply_var n subst
+    | TTerm (n, a) -> TTerm (n, map (apply subst) a)
 
 exception UNIFY
 
@@ -47,19 +45,23 @@
    where this algorithm is explained and similar code is given for terms. *)
 let rec mgu = function
   | ([], subst) -> subst
-  | ((Type_var v, tp) :: tps, subst) ->
-    if (Type_var v = tp) then mgu (tps, subst) else elim (v, tp, tps, subst)
-  | ((tp, Type_var v) :: tps, subst) -> elim (v, tp, tps, subst)
-  | ((Term_type (f, ts), Term_type (g, rs)) :: tps, subst) ->
-    if f = g then mgu ((combine ts rs) @ tps, subst) else raise UNIFY
-  | ((Fun_type (a1, r1), Fun_type (a2, r2)) :: tps, subst) ->
-    mgu ((r1, r2) :: ((combine a1 a2) @ tps), subst)
-  | _ -> raise UNIFY
+  | ((TVar (v, [||], 0, [||]) as var, tp) :: tps, subst) ->
+    if (var = tp) then mgu (tps, subst) else elim (v, tp, tps, subst)
+  | ((tp, TVar (v, [||], 0, [||])) :: tps, subst) -> elim (v, tp, tps, subst)
+  | ((TVar _, _) :: _, _) -> failwith "non-type var in type mgu (left)"
+  | ((_, TVar _) :: _, _) -> failwith "non-type var in type mgu (right)"
+  | ((TTerm (f, ts), TTerm (g, rs)) :: tps, subst) ->
+    if f = g then if f = fun_type_name then (
+        let l1, l2 = Array.length ts, Array.length rs in
+        let (a1, r1) = (Array.sub ts 0 (l1-1), ts.(l1-1)) in
+        let (a2, r2) = (Array.sub rs 0 (l2-1), rs.(l2-1)) in
+        mgu ((r1, r2) :: ((combine a1 a2) @ tps), subst)
+    ) else
+        mgu ((combine ts rs) @ tps, subst) else raise UNIFY
 and elim (v, tp, tps, subst) = 
   let rec occurs s = function
-    | Type_var n -> s = n
-    | Term_type (_, a) -> exists (occurs s) a
-    | Fun_type (a, r) -> (occurs s r) || exists (occurs s) a in
+    | TVar (n, _, _, _) -> s = n
+    | TTerm (_, a) -> exists (occurs s) a in
   if occurs v tp then raise UNIFY else 
     let app = apply [(v, tp)] in
     let new_tps = List.map (fun (t1,t2) -> (app t1, app t2)) tps in
@@ -74,17 +76,21 @@
   let type_array_to_string ta =
     String.concat ", " (to_list (map type_to_string ta)) in
   match tp with
-    | Type_var n -> "@? " ^ n
-    | Term_type (n, a) -> 
-      if (length a = 0) then n else
-	n ^ " (" ^ (type_array_to_string a) ^ ")"
-    | Fun_type (a, r) -> 
+    | TVar (n, [||], 0, [||]) -> "@? " ^ n
+    | TVar _ -> failwith "non-type var in type_to_string"
+    | TTerm (n, arr) when n = fun_type_name -> 
+      let l = Array.length arr in
+      let (a, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
       if (length a = 0) then
 	"@F (" ^ (type_to_string r) ^ ")"
       else
 	"@F (" ^ (type_to_string r) ^ ", " ^ (type_array_to_string a) ^ ")"
+    | TTerm (n, a) -> 
+      if (length a = 0) then n else
+	n ^ " (" ^ (type_array_to_string a) ^ ")"
 
 
+
 (* Lexer for types and terms. *)
 let split_to_list str =
   let split_space s = Aux.split_spaces s in
@@ -113,15 +119,15 @@
   split_special r1
 
 let rec parse_type = function
-  | (Aux.Delim "@?") :: (Aux.Text n) :: rest -> (Type_var n, rest)
+  | (Aux.Delim "@?") :: (Aux.Text n) :: rest -> (TVar (n, [||], 0, [||]), rest)
   | (Aux.Delim "@F") :: rest ->
     (match parse_list rest with
       | ([], cont) -> failwith "Function w/o return type." 
-      | (r :: a, cont) -> (Fun_type (of_list a, r), cont)
+      | (r :: a, cont) -> (TTerm (fun_type_name, of_list (a @ [r])), cont)
     )
   | (Aux.Text n) :: rest -> 
     let (args, cont) = parse_list rest in
-    (Term_type (n, of_list args), cont)
+    (TTerm (n, of_list args), cont)
   | _ -> failwith "parse_type: no parse"
 and parse_list = function
   | (Aux.Delim "(") :: rest ->

Modified: trunk/Toss/Term/TermType.mli
===================================================================
--- trunk/Toss/Term/TermType.mli	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/TermType.mli	2012-06-15 21:24:23 UTC (rev 1725)
@@ -3,10 +3,10 @@
 
 (** The type of term types. *)
 type term_type = 
-  | Term_type of string * term_type array 
-  | Fun_type of term_type array * term_type
-  | Type_var of string
+  | TTerm of string * term_type array 
+  | TVar of string * term_type array * int * term_type array
 
+val fun_type_name : string
 
 (** Suffix all type variables, useful for renaming. *)
 val suffix : int -> term_type -> term_type

Modified: trunk/Toss/Term/TermTypeTest.ml
===================================================================
--- trunk/Toss/Term/TermTypeTest.ml	2012-06-15 15:23:31 UTC (rev 1724)
+++ trunk/Toss/Term/TermTypeTest.ml	2012-06-15 21:24:23 UTC (rev 1725)
@@ -4,8 +4,8 @@
 let tests = "TermType" >::: [
   "mgu" >::
     (fun () ->
-      let t = Term_type ("ala", [| Type_var("x"); Term_type("pies", [||]) |]) in
-      let s = Term_type ("ala", [| Term_type("kot", [||]); Type_var("y") |]) in
+      let t = TTerm ("ala", [| TVar("x",[||],0,[||]); TTerm("pies", [||]) |]) in
+      let s = TTerm ("ala", [| TTerm("kot", [||]); TVar("y",[||],0,[||]) |]) in
       let subst_str subst = String.concat ", " (List.map (fun (s, tp) ->
 	s ^ " <- " ^ (type_to_string tp)) subst) in
       assert_equal ~printer:(fun x -> x) "y <- pies, x <- kot" 

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