[Toss-devel-svn] SF.net SVN: toss:[1726] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1726] trunk/Toss
|
From: <luk...@us...> - 2012-06-16 17:01:27
|
Revision: 1726
http://toss.svn.sourceforge.net/toss/?rev=1726&view=rev
Author: lukaszkaiser
Date: 2012-06-16 17:01:17 +0000 (Sat, 16 Jun 2012)
Log Message:
-----------
Merging TermType and Term, rest of old Term are now in Coding.
Modified Paths:
--------------
trunk/Toss/Server/Tests.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/Term/BuiltinLang.ml
trunk/Toss/Term/BuiltinLang.mli
trunk/Toss/Term/BuiltinLangTest.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/SyntaxDef.mli
trunk/Toss/Term/SyntaxDefTest.ml
trunk/Toss/Term/TRS.ml
trunk/Toss/Term/TRS.mli
trunk/Toss/Term/TRSTest.ml
Added Paths:
-----------
trunk/Toss/Term/Coding.ml
trunk/Toss/Term/Coding.mli
trunk/Toss/Term/CodingTest.ml
trunk/Toss/Term/Term.ml
trunk/Toss/Term/Term.mli
trunk/Toss/Term/TermTest.ml
Removed Paths:
-------------
trunk/Toss/Term/Term.ml
trunk/Toss/Term/Term.mli
trunk/Toss/Term/TermTest.ml
trunk/Toss/Term/TermType.ml
trunk/Toss/Term/TermType.mli
trunk/Toss/Term/TermTypeTest.ml
Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Server/Tests.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -14,10 +14,10 @@
]
let term_tests = "Term", [
- "TermTypeTest", [TermTypeTest.tests];
+ "TermTest", [TermTest.tests];
"SyntaxDefTest", [SyntaxDefTest.tests];
"BuiltinLangTest", [BuiltinLangTest.tests];
- "TermTest", [TermTest.tests];
+ "CodingTest", [CodingTest.tests];
"RewritingTest", [RewritingTest.tests];
"ParseArcTest", [ParseArcTest.tests];
"TRSTest", [TRSTest.tests; TRSTest.bigtests];
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Solver/Structure.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -529,17 +529,17 @@
let trs_set_struc s = function
| ("addrel", te_rel, te_arglist) ->
- let rname = Term.decode_string te_rel in
- let args = Term.decode_list Term.term_to_string te_arglist in
+ let rname = Coding.decode_string te_rel in
+ let args = Coding.decode_list Coding.term_to_string te_arglist in
let (struc, args) = List.fold_left (fun (st, a) e ->
let (s1, i) = find_or_new_elem st e in (s1, i :: a)) (s, []) args in
add_rel struc rname (Array.of_list (List.rev args))
| (str, te, arg) when String.length str > 3 && String.sub str 0 3 = "fun" ->
let fname = String.sub str 3 ((String.length str) - 3) in
- let (struc, i) = find_or_new_elem s (Term.term_to_string te) in
- let v = Term.decode_bit_list arg in
+ let (struc, i) = find_or_new_elem s (Coding.term_to_string te) in
+ let v = Coding.decode_bit_list arg in
add_fun struc fname (i, float v)
- | _-> raise (Term.DECODE "Structure.trs_set_struc not a structure update set")
+ | _-> raise (Coding.DECODE "Structure.trs_set_struc not a struc update set")
let struc_from_trs str =
let (o, trs, _) = TRS.run_shell_str str in
Modified: trunk/Toss/Term/BuiltinLang.ml
===================================================================
--- trunk/Toss/Term/BuiltinLang.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/BuiltinLang.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,6 +1,6 @@
(* Basic Built-in TRS Language Syntax. *)
-open TermType
+open Term
open SyntaxDef
@@ -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 = TTerm (list_name, [|t|])
-let list_tp_a = list_tp (TVar ("a", [||], 0, [||]))
+let list_tp t = Term (list_name, [||], [|t|])
+let list_tp_a = list_tp (Var ("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 (TVar ("a",[||],0,[||])); Str ","; Tp list_tp_a],
+let list_cons_sd = SDfun ([Tp (Var ("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 (TVar ("a_1",[||],0,[||])); Str "be";
- Tp (TVar ("a_1",[||],0,[||]))], input_rewrite_rule_tp)
+let let_be_sd = SDfun ([Str "let"; Tp (Var ("a_1",[||],0,[||])); Str "be";
+ Tp (Var ("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";
@@ -159,8 +159,8 @@
type_of_sd priority_input_rewrite_rule_sd
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)
+ SDfun ([Str "let"; Str "major"; Tp (Var ("a_1",[||],0,[||])); Str "be";
+ Tp (Var ("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"])
@@ -185,44 +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 = TTerm (exception_cl_name, [|t|])
+let exception_cl_tp t = Term (exception_cl_name, [||], [|t|])
let exception_sd =
- SDfun ([Str "!"; Str "!"; Tp (TVar ("a",[||],0,[||])); Str "!";Str "!";],
- exception_cl_tp (TVar ("other_than_a!",[||],0,[||])))
+ SDfun ([Str "!"; Str "!"; Tp (Var ("a",[||],0,[||])); Str "!";Str "!";],
+ exception_cl_tp (Var ("other_than_a!",[||],0,[||])))
let exception_name = name_of_sd exception_sd
let exn_ok_sd =
- SDfun ([Str "+"; Str "+"; Tp (TVar ("a",[||],0,[||])); Str "+";Str "+";],
- exception_cl_tp (TVar ("a",[||],0,[||]))) (* Here it should be a! *)
+ SDfun ([Str "+"; Str "+"; Tp (Var ("a",[||],0,[||])); Str "+";Str "+";],
+ exception_cl_tp (Var ("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 (TVar ("b",[||],0,[||])); Str ")"],
- TVar ("b",[||],0,[||]))
+let brackets_sd = SDfun ([Str "("; Tp (Var ("b",[||],0,[||])); Str ")"],
+ Var ("b",[||],0,[||]))
let brackets_name = name_of_sd brackets_sd
-let verbatim_sd = SDfun ([Str "<"; Str "|"; Tp (TVar ("b",[||],0,[||]));
- Str "|"; Str ">"], TVar ("b",[||],0,[||]))
+let verbatim_sd = SDfun ([Str "<"; Str "|"; Tp (Var ("b",[||],0,[||]));
+ Str "|"; Str ">"], Var ("b",[||],0,[||]))
let verbatim_name = name_of_sd verbatim_sd
let if_then_else_sd = SDfun ([Str "if"; Tp boolean_tp; Str "then";
- Tp (TVar ("a",[||],0,[||])); Str "else";
- Tp (TVar ("a",[||],0,[||]))], TVar ("a",[||],0,[||]))
+ Tp (Var ("a",[||],0,[||])); Str "else";
+ Tp (Var ("a",[||],0,[||]))], Var ("a",[||],0,[||]))
let if_then_else_name = name_of_sd if_then_else_sd
-let eq_bool_sd = SDfun ([Tp (TVar ("a",[||],0,[||])); Str "=";
- Tp (TVar ("a",[||],0,[||]))], boolean_tp)
+let eq_bool_sd = SDfun ([Tp (Var ("a",[||],0,[||])); Str "=";
+ Tp (Var ("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 (TVar ("a",[||],0,[||]));
+let code_as_term_sd = SDfun ([Str "code"; Tp (Var ("a",[||],0,[||]));
Str "as"; Str "term"], term_tp)
let code_as_term_name = name_of_sd code_as_term_sd
@@ -278,13 +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 (TVar ("a",[||],0,[||])); Str "to";
- Tp (TVar ("b",[||],0,[||]))], set_command_tp)
+ Tp (Var ("a",[||],0,[||])); Str "to";
+ Tp (Var ("b",[||],0,[||]))], set_command_tp)
let set_prop_name = name_of_sd set_prop_sd
let preprocess_sd = SDfun ([Str "#"; Str "#"; Str "#";
- Tp (TVar ("p",[||],0,[||]))], TVar ("q",[||],0,[||]))
+ Tp (Var ("p",[||],0,[||]))], Var ("q",[||],0,[||]))
let preprocess_name = name_of_sd preprocess_sd
Modified: trunk/Toss/Term/BuiltinLang.mli
===================================================================
--- trunk/Toss/Term/BuiltinLang.mli 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/BuiltinLang.mli 2012-06-16 17:01:17 UTC (rev 1726)
@@ -7,7 +7,7 @@
val bit_sd : syntax_def
val bit_name : string
-val bit_tp : TermType.term_type
+val bit_tp : Term.term
val bit_0_cons_sd : syntax_def
val bit_0_cons_name : string
val bit_1_cons_sd : syntax_def
@@ -15,18 +15,18 @@
val char_sd : syntax_def
val char_name : string
-val char_tp : TermType.term_type
+val char_tp : Term.term
val char_cons_sd : syntax_def
val char_cons_name : string
val term_type_sd : syntax_def
val term_type_name : string
-val term_type_tp : TermType.term_type
+val term_type_tp : Term.term
val list_sd : syntax_def
val list_name : string
-val list_tp : TermType.term_type -> TermType.term_type
-val list_tp_a : TermType.term_type
+val list_tp : Term.term -> Term.term
+val list_tp_a : Term.term
val list_nil_sd : syntax_def
val list_nil_name : string
val list_cons_sd : syntax_def
@@ -34,13 +34,13 @@
val string_sd : syntax_def
val string_name : string
-val string_tp : TermType.term_type
+val string_tp : Term.term
val string_cons_sd : syntax_def
val string_cons_name : string
val boolean_sd : syntax_def
val boolean_name : string
-val boolean_tp : TermType.term_type
+val boolean_tp : Term.term
val boolean_true_sd : syntax_def
val boolean_true_name : string
val boolean_false_sd : syntax_def
@@ -48,7 +48,7 @@
val ternary_truth_value_sd : syntax_def
val ternary_truth_value_name : string
-val ternary_truth_value_tp : TermType.term_type
+val ternary_truth_value_tp : Term.term
val ternary_true_sd : syntax_def
val ternary_true_name : string
val ternary_unknown_sd : syntax_def
@@ -65,21 +65,21 @@
val syntax_element_sd : syntax_def
val syntax_element_name : string
-val syntax_element_tp : TermType.term_type
+val syntax_element_tp : Term.term
val syntax_element_str_sd : syntax_def
val syntax_element_str_name : string
val syntax_element_tp_sd : syntax_def
val syntax_element_tp_name : string
val syntax_element_list_sd : syntax_def
val syntax_element_list_name : string
-val syntax_element_list_tp : TermType.term_type
+val syntax_element_list_tp : Term.term
val syntax_element_list_elem_sd : syntax_def
val syntax_element_list_elem_name : string
val syntax_element_list_cons_sd : syntax_def
val syntax_element_list_cons_name : string
val syntax_definition_sd : syntax_def
val syntax_definition_name : string
-val syntax_definition_tp : TermType.term_type
+val syntax_definition_tp : Term.term
val syntax_definition_type_sd : syntax_def
val syntax_definition_type_name : string
val syntax_definition_fun_sd : syntax_def
@@ -92,34 +92,34 @@
val term_sd : syntax_def
val term_name : string
-val term_tp : TermType.term_type
+val term_tp : Term.term
val term_var_cons_sd : syntax_def
val term_var_cons_name : string
val term_term_cons_sd : syntax_def
val term_term_cons_name : string
val rewrite_rule_sd : syntax_def
val rewrite_rule_name : string
-val rewrite_rule_tp : TermType.term_type
+val rewrite_rule_tp : Term.term
val rewrite_rule_cons_sd : syntax_def
val rewrite_rule_cons_name : string
val input_rewrite_rule_sd : syntax_def
val input_rewrite_rule_name : string
-val input_rewrite_rule_tp : TermType.term_type
+val input_rewrite_rule_tp : Term.term
val let_be_sd : syntax_def
val let_be_name : string
val priority_input_rewrite_rule_sd : syntax_def
val priority_input_rewrite_rule_name : string
-val priority_input_rewrite_rule_tp : TermType.term_type
+val priority_input_rewrite_rule_tp : Term.term
val let_major_be_sd : syntax_def
val let_major_be_name : string
val fun_definition_sd : syntax_def
val fun_definition_name : string
-val fun_definition_tp : TermType.term_type
+val fun_definition_tp : Term.term
val fun_definition_cons_sd : syntax_def
val fun_definition_cons_name : string
val type_definition_sd : syntax_def
val type_definition_name : string
-val type_definition_tp : TermType.term_type
+val type_definition_tp : Term.term
val type_of_sd_sd : syntax_def
val type_of_name : string
@@ -165,7 +165,7 @@
val outside_paths_sd : syntax_def
val outside_paths_name : string
-val outside_paths_tp : TermType.term_type
+val outside_paths_tp : Term.term
val path_library_sd : syntax_def
val path_library_name : string
@@ -175,26 +175,20 @@
val load_command_sd : syntax_def
val load_command_name : string
-val load_command_tp : TermType.term_type
+val load_command_tp : Term.term
val load_file_sd : syntax_def
val load_file_name : string
val sys_commands_sd : syntax_def
val sys_commands_name : string
-val sys_commands_tp : TermType.term_type
+val sys_commands_tp : Term.term
val close_context_sd : syntax_def
val close_context_name : string
-(*val remove_command_sd : syntax_def
-val remove_command_name : string
-val remove_command_tp : TermType.term_type
-val system_remove_sd : syntax_def
-val system_remove_name : string*)
-
val set_command_sd : syntax_def
val set_command_name : string
-val set_command_tp : TermType.term_type
+val set_command_tp : Term.term
val set_prop_sd : syntax_def
val set_prop_name : string
Modified: trunk/Toss/Term/BuiltinLangTest.ml
===================================================================
--- trunk/Toss/Term/BuiltinLangTest.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/BuiltinLangTest.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,12 +1,12 @@
open OUnit
-open TermType
+open Term
open BuiltinLang
let tests = "BuiltinLang" >::: [
"type names" >::
(fun () ->
let test_type_name res tp =
- assert_equal ~printer:(fun x -> x) res (TermType.type_to_string tp) in
+ assert_equal ~printer:(fun x -> x) res (Term.type_to_string tp) in
test_type_name "T\\?_list (@? a)" list_tp_a;
test_type_name "Tbit" bit_tp;
test_type_name "Tchar" char_tp;
Copied: trunk/Toss/Term/Coding.ml (from rev 1725, trunk/Toss/Term/Term.ml)
===================================================================
--- trunk/Toss/Term/Coding.ml (rev 0)
+++ trunk/Toss/Term/Coding.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -0,0 +1,502 @@
+(* Contains the type of typed terms, functions calculating type and
+ reconstruction for a term and printing and parsing for terms. *)
+
+open Array
+open Aux
+
+open Term
+open SyntaxDef
+open BuiltinLang
+
+
+(* --- Coding basic things as Terms --- *)
+
+exception DECODE of string
+exception CODE of string
+
+let rec code_list f = function
+ | [] -> Term (list_nil_name, [||], [||])
+ | x :: xs -> Term (list_cons_name, [||], [|f (x); code_list f xs|])
+
+
+let rec decode_list f = function
+ | Term (n, _, [||]) when n = list_nil_name -> []
+ | Term (n, _, [|x; xs|]) when n = list_cons_name -> (f x):: (decode_list f xs)
+ | _ -> raise (DECODE "list")
+
+
+let decode_list_opt f l = try Some (decode_list f l) with DECODE _ -> None
+
+let rec int_to_bits = function
+ | 0 -> [0]
+ | 1 -> [1]
+ | i -> if i mod 2 = 0 then 0 :: int_to_bits (i/2) else 1 :: int_to_bits (i/2)
+
+
+let bits_to_int i =
+ let rec bits_to_int_rec start = function
+ | [] -> 0
+ | x :: xs -> x * start + bits_to_int_rec (2*start) xs in
+ bits_to_int_rec 1 i
+
+
+let code_bit = function
+ | 0 -> Term (bit_0_cons_name, [||], [||])
+ | 1 -> Term (bit_1_cons_name, [||], [||])
+ | _ -> failwith "not bit while coding bit"
+
+
+let decode_bit = function
+ | Term (n, _, [||]) when n = bit_0_cons_name -> 0
+ | Term (n, _, [||]) when n = bit_1_cons_name -> 1
+ | _ -> raise (DECODE "bit")
+
+let decode_bit_list bl = bits_to_int (decode_list decode_bit bl)
+
+let code_char c =
+ let bits = int_to_bits (Char.code c) in
+ let rec zeros i = if i <= 0 then [] else 0 :: zeros (i-1) in
+ let eight_bits = bits @ zeros (8 - List.length bits) in
+ Term (char_cons_name, [||], of_list (List.map code_bit eight_bits))
+
+let decode_char = function
+ | Term (n, _, bits) when n = char_cons_name ->
+ Char.chr (bits_to_int (to_list (map decode_bit bits)))
+ | _ -> raise (DECODE "char")
+
+let code_string s =
+ let rec char_list i = if i < 0 then [] else s.[i] :: char_list (i-1) in
+ let chars = List.rev (char_list ((String.length s) - 1)) in
+ let char_term = code_list code_char chars in
+ Term (string_cons_name, [||], [|char_term|])
+
+
+let decode_string t =
+ let rec string_of_list_i s i = function
+ | [] -> s
+ | x :: xs -> (s.[i] <- x; string_of_list_i s (i+1) xs) in
+ let string_of_list l = string_of_list_i (String.create (List.length l)) 0 l in
+ match t with
+ | Term (n, _, [|c|]) when n = string_cons_name ->
+ string_of_list (decode_list decode_char c)
+ | _ -> raise (DECODE "string")
+
+
+let decode_string_opt t = try Some (decode_string t) with DECODE _ -> None
+
+
+let code_bool = function
+ | true -> Term (boolean_true_name, [||], [||])
+ | false -> Term (boolean_false_name, [||], [||])
+
+
+let decode_bool = function
+ | Term (n, _, [||]) when n = boolean_true_name -> true
+ | Term (n, _, [||]) when n = boolean_false_name -> false
+ | _ -> raise (DECODE "bool")
+
+
+let rec code_term_type = function
+ | Var (name, [||], 0, [||])->
+ Term (term_type_var_name, [||], [|code_string name|])
+ | Var _ -> failwith "code_term_type: non-type 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, [||], [|
+ code_list code_term_type (to_list args_types);
+ code_term_type return_type|])
+ | Term (name, [||], args) ->
+ Term (term_type_cons_name, [||], [|
+ code_string name;
+ code_list code_term_type (to_list args)|])
+ | Term _ -> failwith "code_term_type: non-type term"
+
+
+let rec decode_term_type = function
+ | Term (s, _, [|coded_name|]) when s = term_type_var_name ->
+ Var (decode_string coded_name, [||], 0, [||])
+ | Term (s, _, [|coded_1; coded_2|]) when s = term_type_fun_name ->
+ 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, [||],
+ of_list (decode_list decode_term_type coded_2))
+ | _ -> raise (DECODE "term_type")
+
+
+let decode_term_type_opt t =
+ try Some (decode_term_type t) with DECODE _ -> None
+
+
+let rec code_term = function
+ | Var (name, var_types, deg, args) ->
+ Term (term_var_cons_name, [||],
+ [|code_string name;
+ code_term_type var_types.(0);
+ code_list code_bit (int_to_bits deg);
+ code_list code_term (to_list args)|])
+ | Term (name, _, args) ->
+ Term (term_term_cons_name, [||], [|code_string name;
+ code_list code_term (to_list args)|])
+
+
+let rec code_term_incr_vars = function
+ | Var (name, var_type, deg, args) ->
+ Var (name, var_type, deg+1, map code_term_incr_vars args)
+ | Term (name, _, args) ->
+ Term (term_term_cons_name, [||], [|
+ code_string name; code_list code_term_incr_vars (to_list args)|])
+
+
+let rec decode_term = function
+ | Term (s, _, [|coded_name; coded_type; coded_deg; coded_args|])
+ when s = term_var_cons_name ->
+ Var (decode_string coded_name,
+ [|decode_term_type coded_type|],
+ bits_to_int (decode_list decode_bit coded_deg),
+ of_list (decode_list decode_term coded_args))
+ | Term (s, _, [|coded_name; coded_args|])
+ when s = term_term_cons_name ->
+ Term (decode_string coded_name, [||],
+ of_list (decode_list decode_term coded_args))
+ | _ -> raise (DECODE "term")
+
+
+let decode_term_opt t = try Some (decode_term t) with DECODE _ -> None
+
+
+type rewrite_rule = term * term
+
+
+let code_rewrite_rule (left, right) =
+ Term (rewrite_rule_cons_name, [||], [|code_term left; code_term right|])
+
+
+let decode_rewrite_rule = function
+ | Term (n, _, [|left; right|]) when n = rewrite_rule_cons_name ->
+ (decode_term left, decode_term right)
+ | _ -> raise (DECODE "rewrite rule")
+
+
+let code_input_rewrite_rule (left, right) =
+ Term (let_be_name, [||], [|left; right|])
+
+
+let decode_input_rewrite_rule = function
+ | Term (n, _, [|left; right|]) when n = let_be_name -> (left, right)
+ | _ -> raise (DECODE "input rewrite rule")
+
+
+let code_priority_input_rewrite_rule (left, right) =
+ Term (let_major_be_name, [||], [|left; right|])
+
+
+let decode_priority_input_rewrite_rule = function
+ | Term (n, [||], [|left; right|]) when n = let_major_be_name -> (left, right)
+ | _ -> raise (DECODE "priority input rewrite rule")
+
+
+type fun_definition = string * Term.term list * Term.term
+
+let code_fun_definition (name, args_types, return_type) =
+ Term (fun_definition_cons_name, [||], [|
+ code_string name;
+ code_list code_term_type args_types;
+ code_term_type return_type|])
+
+
+let decode_fun_definition = function
+ | Term (n, _, [|name; args; ret|]) when n = fun_definition_cons_name ->
+ (decode_string name, decode_list decode_term_type args,
+ decode_term_type ret)
+ | _ -> raise (DECODE "function definition")
+
+
+type type_definition = string * int
+
+let code_type_definition (name, arity) =
+ let rec var = function
+ | 0 -> []
+ | i -> Var ("a_" ^ (string_of_int i), [||], 0, [||]) :: (var (i-1)) in
+ Term (type_of_name, [||],
+ [|code_term_type (Term (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 (name, [||], args) -> (name, Array.length args)
+ | _ -> raise (DECODE "type definition 1")
+ )
+ | _ -> raise (DECODE "type definition 2")
+
+
+let code_syntax_element = function
+ | Str s -> Term (syntax_element_str_name, [||], [|code_string s|])
+ | Tp tt -> Term (syntax_element_tp_name, [||], [|code_term_type tt|])
+
+
+let decode_syntax_element = function
+ | Term (s, _, [|strt|]) when s = syntax_element_str_name ->
+ Str (decode_string strt)
+ | Term (s, _, [|tt|]) when s = syntax_element_tp_name ->
+ Tp (decode_term_type tt)
+ | _ -> raise (DECODE "syntax element")
+
+
+let rec code_syntax_element_list = function
+ | [se] -> Term (syntax_element_list_elem_name, [||],
+ [|code_syntax_element se|])
+ | se :: ses -> Term (syntax_element_list_cons_name, [||],
+ [|code_syntax_element se; code_syntax_element_list ses|])
+ | [] -> raise (CODE "syntax element list")
+
+
+let rec decode_syntax_element_list = function
+ | Term (name, _, [|coded_se|]) when name = syntax_element_list_elem_name ->
+ [decode_syntax_element coded_se]
+ | Term (name, _, [|coded_se; coded_ses|])
+ when name = syntax_element_list_cons_name ->
+ (decode_syntax_element coded_se) :: (decode_syntax_element_list coded_ses)
+ | _ -> raise (DECODE "syntax element list")
+
+
+let code_syntax_definition = function
+ | SDtype se ->
+ Term (syntax_definition_type_name, [||], [|code_syntax_element_list se|])
+ | SDfun (se, res_ty) ->
+ Term (syntax_definition_fun_name, [||],
+ [|code_syntax_element_list se; code_term_type res_ty|])
+ | SDvar (se, res_ty) ->
+ Term (syntax_definition_var_name, [||],
+ [|code_syntax_element_list se; code_term_type res_ty|])
+
+
+let decode_syntax_definition = function
+ | Term (str, _, [|t1|]) when str = syntax_definition_type_name ->
+ SDtype (decode_syntax_element_list t1)
+ | Term (str, _, [|t1; t2|]) ->
+ let se = decode_syntax_element_list t1 in
+ let res_ty = decode_term_type t2 in
+ if str = syntax_definition_fun_name then SDfun (se, res_ty) else
+ if str = syntax_definition_var_name then SDvar (se, res_ty) else
+ raise (DECODE "syntax definition 1")
+ | _ -> raise (DECODE "syntax definition 2")
+
+
+
+(* --- Term matching and substitutions --- *)
+
+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))
+ 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, [||]), 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
+
+
+(* Application of term substitutions (only flat functional substitutes). *)
+let rec apply_s substs = function
+ | Var (n, _, d, [||]) as t ->
+ (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, t, deg, a) ->
+ try (
+ let raw_result =
+ match (List.assoc n substs) with
+ | Term (name, [||], [||]) ->
+ Term (name, [||], map (apply_s substs) a)
+ | Var (name, ty, d, [||]) ->
+ Var (name, ty, d, 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, t, deg, map (apply_s substs) a)
+
+
+(* --- Nice Term display based on Syntax Definitions --- *)
+
+let is_some = function Some _ -> true | None -> false
+
+let rec display_term = function
+ | te when is_some (decode_string_opt te) ->
+ "\"" ^ (decode_string te) ^ "\""
+ | te when is_some (decode_list_opt (fun x -> x) te) ->
+ let str_list = List.map display_term (decode_list (fun x -> x) te) in
+ "["^ (String.concat ", " str_list) ^ "]"
+ | Term (n, _, a) ->
+ let args = List.map display_term (Array.to_list a) in
+ display_sd (split_sdef_name n) args
+ | Var (n, _, _, a) ->
+ let args = List.map display_term (Array.to_list a) in
+ display_sd (split_sdef_name n) args
+
+
+(* --- Display terms and types as XML --- *)
+
+let rec display_type_xml = function
+ | Var (n, [||], 0, [||]) ->
+ "<type_var>" ^ (make_xml_compatible n) ^ "</type_var>"
+ | Var _ -> failwith "display_type_xml: non-type variable"
+ | Term (n, _, a) ->
+ "<type class=\"" ^ (make_xml_compatible n) ^ "\">\n" ^
+ (String.concat "\n" (List.map display_type_xml (to_list a))) ^
+ "\n</type>"
+
+let rec display_term_xml = function
+ | te when is_some (decode_string_opt te) ->
+ "<term-string>" ^ (make_xml_compatible (decode_string te)) ^
+ "</term-string>"
+ | te when is_some (decode_list_opt (fun x -> x) te) ->
+ let str_list = List.map display_term_xml (decode_list (fun x -> x) te) in
+ "<term-list>"^ (String.concat " " str_list) ^ "</term-list>"
+ | Term (n, _, a) ->
+ "<term class=\"" ^ (make_xml_compatible n) ^ "\">\n" ^
+ (String.concat "\n" (List.map display_term_xml (to_list a))) ^
+ "\n</term>"
+ | Var (n, ty, deg, a) ->
+ "<term-variable class=\"" ^ (make_xml_compatible n) ^
+ "\" deg=\"" ^ (string_of_int deg) ^ "\">" ^
+ (String.concat "" (List.map display_term_xml (to_list a))) ^
+ "<term-variable-type>"^(display_type_xml ty.(0))^"</term-variable-type>" ^
+ "</term-variable>"
+
+
+
+(* --- Term parsing and printing --- *)
+
+(* Printing terms. *)
+let rec term_to_string term =
+ let term_array_to_string ta =
+ String.concat ", " (to_list (map term_to_string ta)) in
+ match term with
+ | _ when is_some (decode_string_opt term) ->
+ let s = (match (decode_string_opt term) with Some s -> s | None -> "") in
+ "@`" ^ (Aux.normalize_spaces s) ^ "@`"
+ | _ when is_some (decode_list_opt (fun x -> x) term) ->
+ (match (decode_list_opt (fun x -> x) term) with None -> ""
+ | Some l -> "@L["^ (String.concat ", " (List.map term_to_string l))^"]")
+ | _ when is_some (decode_term_type_opt term) ->
+ (match (decode_term_type_opt term) with None -> ""
+ | Some ty -> "@Y " ^ (type_to_string ty))
+ | _ when is_some (decode_term_opt term) ->
+ (match (decode_term_opt term) with None -> ""
+ | Some te -> "@T " ^ (term_to_string te))
+ | Var (v, t, d, [||]) ->
+ "@V [" ^ v ^ " @: " ^ (type_to_string t.(0)) ^
+ " @: "^ string_of_int (d) ^ " ]"
+ | Var (v, t, d, a) ->
+ "@V [" ^ v ^ " @: " ^ (type_to_string t.(0)) ^
+ " @: "^ string_of_int (d) ^ " ] (" ^
+ (term_array_to_string a) ^ " )"
+ | Term (n, [||], [||]) -> n
+ | Term (n, [||], a) ->
+ n ^ " (" ^ (term_array_to_string a) ^ " )"
+ | Term _ -> failwith "term_to_string: stored types not supported yet"
+
+
+(* Parser for terms. *)
+let rec parse_term = function
+ | (Delim "@`") :: rest ->
+ (match parse_text_list rest with
+ | (s, (Delim "@`") :: cont) ->
+ (if s = "" then code_string "" else
+ code_string (String.sub s 0 ((String.length s) - 1))), cont
+ | _ -> failwith "parse_term: string not closed"
+ )
+ | (Delim "@L") :: (Delim "[") :: rest ->
+ (match parse_term_list rest with
+ | (l, (Delim "]") :: cont) -> (code_list (fun x -> x) l, cont)
+ | _ -> failwith "parse_term: list not closed"
+ )
+ | (Delim "@Y") :: rest ->
+ let (ty, cont) = parse_type rest in
+ (code_term_type ty, cont)
+ | (Delim "@T") :: rest ->
+ let (te, cont) = parse_term rest in
+ (code_term te, cont)
+ | (Delim "@V") :: (Delim "[") :: (Text v) :: (Delim "@:") :: rest ->
+ (match parse_type rest with
+ | (ty, (Delim "@:") :: (Text deg) :: (Delim "]") :: cont) ->
+ let (l, c) = parse_bracketed_list cont in
+ (Var (v, [|ty|], int_of_string (deg), of_list l), c)
+ | _ -> failwith "parse_term: var not closed"
+ )
+ | (Text n) :: rest ->
+ let (l, cont) = parse_bracketed_list rest in
+ (Term (n, [||], of_list l), cont)
+ | _ -> failwith "parse_term: bad start"
+and parse_text_list = function
+ | (Text n) :: rest ->
+ let (tl, c) = parse_text_list rest in (n ^ " " ^ tl, c)
+ | (Delim "(") :: rest ->
+ let (tl, c) = parse_text_list rest in ("(" ^ tl, c)
+ | (Delim ")") :: rest ->
+ let (tl, c) = parse_text_list rest in (")" ^ tl, c)
+ | (Delim "[") :: rest ->
+ let (tl, c) = parse_text_list rest in ("[" ^ tl, c)
+ | (Delim "]") :: rest ->
+ let (tl, c) = parse_text_list rest in ("]" ^ tl, c)
+ | (Delim ",") :: rest ->
+ let (tl, c) = parse_text_list rest in ("," ^ tl, c)
+ | l -> ("", l)
+and parse_bracketed_list = function
+ | (Delim "(") :: rest ->
+ (match parse_term_list rest with
+ | (l, (Delim ")") :: cont) -> (l, cont)
+ | _ -> failwith "parse_bracketed_list: not closed"
+ )
+ | l -> ([], l)
+and parse_term_list l =
+ try let (te, cont) = parse_term l in
+ let (lst, c) = parse_term_list_delim cont in
+ (te :: lst, c)
+ with _ -> ([], l)
+and parse_term_list_delim = function
+ | (Delim ",") :: rest ->
+ let (l, cont) = parse_term_list rest in (l, cont)
+ | l -> ([], l)
+
+let term_of_string s =
+ let (te, cont) = parse_term (split_to_list s) in
+ if cont = [] then te else failwith "term_of_string: incomplete parse"
+
+
+(* --- Rules for special built-in functions --- *)
+
+let brackets_rules =
+ [(Term (brackets_name, [||], [|Var ("x", [|Var("a",[||],0,[||])|],0,[||])|]),
+ Var ("x", [|Var ("a",[||],0,[||])|], 0, [||]))]
+let verbatim_rules =
+ [(Term (verbatim_name, [||], [|Var ("x",[|Var ("a",[||],0,[||])|],0,[||])|]),
+ Var ("x", [|Var ("a",[||],0,[||])|], 0, [||]))]
+let if_then_else_rules = [
+ (Term (if_then_else_name, [||], [|code_bool true;
+ Var ("x", [|Var ("a",[||],0,[||])|], 0, [||]);
+ Var ("y", [|Var ("a",[||],0,[||])|], 0, [||])|]),
+ Var ("x", [|Var ("a",[||],0,[||])|], 0, [||]));
+ (Term (if_then_else_name, [||], [|code_bool false;
+ Var ("x", [|Var ("a",[||],0,[||])|], 0, [||]);
+ Var ("y", [|Var ("a",[||],0,[||])|], 0, [||])|]),
+ Var ("y", [|Var ("a",[||],0,[||])|], 0, [||]))]
+
+let varx_te = Var ("x", [|Var ("p",[||],0,[||])|], 0, [||])
+let preprocess_rules = [(Term (preprocess_name, [||], [|varx_te|]), varx_te)]
+
+let string_quote_rules =
+ [(Term (string_quote_name, [||], [|Var ("s", [|string_tp|], 0, [||])|]),
+ Var ("s", [|string_tp|], 0, [||]))]
+
+let additional_xslt_rules =
+ [(Term (additional_xslt_name, [||], [||]), code_string " ")]
Copied: trunk/Toss/Term/Coding.mli (from rev 1725, trunk/Toss/Term/Term.mli)
===================================================================
--- trunk/Toss/Term/Coding.mli (rev 0)
+++ trunk/Toss/Term/Coding.mli 2012-06-16 17:01:17 UTC (rev 1726)
@@ -0,0 +1,87 @@
+(** Contains the type of typed terms, functions calculating type and
+ reconstruction for a term, and printing and parsing for terms. *)
+
+(** {2 Coding basic things as Terms and decoding them} *)
+
+open SyntaxDef
+open Term
+
+(** Thrown when decoding fails. *)
+exception DECODE of string
+
+val code_list : ('a -> term) -> 'a list -> term
+val decode_list : (term -> 'a) -> term -> 'a list
+val decode_list_opt : (term -> 'a) -> term -> 'a list option
+val int_to_bits : int -> int list
+val bits_to_int : int list -> int
+val code_bit : int -> term
+val decode_bit : term -> int
+val decode_bit_list : term -> int
+val code_char : char -> term
+val decode_char : term -> char
+val code_string : string -> term
+val decode_string : term -> string
+val decode_string_opt : term -> string option
+val code_bool : bool -> term
+val decode_bool : term -> bool
+val code_term_type : term -> term
+val decode_term_type : term -> term
+val code_term : term -> term
+val code_term_incr_vars : term -> term
+val decode_term : term -> term
+
+(** {2 Rewriting rules and definitions, their coding and decoding} *)
+
+(** The type of Rewriting Rules. *)
+type rewrite_rule = term * term
+
+val code_rewrite_rule : rewrite_rule -> term
+val decode_rewrite_rule : term -> rewrite_rule
+val code_input_rewrite_rule : rewrite_rule -> term
+val decode_input_rewrite_rule : term -> rewrite_rule
+val code_priority_input_rewrite_rule : rewrite_rule -> term
+val decode_priority_input_rewrite_rule : term -> rewrite_rule
+
+(** The type of Function Definitions. *)
+type fun_definition = string * term list * term
+
+val code_fun_definition : fun_definition -> term
+val decode_fun_definition : term -> fun_definition
+
+(** The type of Type Definitons *)
+type type_definition = string * int
+
+val code_type_definition : type_definition -> term
+val decode_type_definition : term -> type_definition
+val decode_syntax_element : term -> SyntaxDef.syntax_elem
+val code_syntax_element_list : SyntaxDef.syntax_elem list -> term
+val decode_syntax_element_list : term -> SyntaxDef.syntax_elem list
+val code_syntax_definition : SyntaxDef.syntax_def -> term
+val decode_syntax_definition : term -> SyntaxDef.syntax_def
+
+
+(** {2 Term Matching} *)
+
+val matches : (string * term) list ref -> term * term -> bool
+val apply_s : (string * term) list -> term -> term
+
+
+(** {2 Term Display, printing and parsing} *)
+
+val display_term : term -> string
+val display_type_xml : term -> string
+val display_term_xml : term -> string
+
+val term_to_string : term -> string
+val parse_term : Aux.split_result list -> term * Aux.split_result list
+val term_of_string : string -> term
+
+
+(** {2 Rewriting Rules for special built-in functions} *)
+
+val brackets_rules : (term * term) list
+val verbatim_rules : (term * term) list
+val if_then_else_rules : (term * term) list
+val preprocess_rules : (term * term) list
+val additional_xslt_rules : (term * term) list
+val string_quote_rules : (term * term) list
Copied: trunk/Toss/Term/CodingTest.ml (from rev 1725, trunk/Toss/Term/TermTest.ml)
===================================================================
--- trunk/Toss/Term/CodingTest.ml (rev 0)
+++ trunk/Toss/Term/CodingTest.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -0,0 +1,115 @@
+open OUnit
+open Term
+open Coding
+
+let tests = "Term" >::: [
+ "coding term types" >::
+ (fun () ->
+ 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", [||], [||]) in
+ let tt2 = Term ("bolek", [||], [|tt1; tt1|]) in
+ let tt3 = Term (Term.fun_type_name, [||], [|tt1; tt2; tt1|]) in
+ let tt4 = Var ("zmienna",[||],0,[||]) in
+ test_code_decode_tt tt1;
+ test_code_decode_tt tt2;
+ test_code_decode_tt tt3;
+ test_code_decode_tt tt4;
+ );
+
+ "coding terms" >::
+ (fun () ->
+ 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 term1 = Term ("ala", [||], [||]) in
+ let term2 = Term ("bolek", [||], [|term1|]) in
+ let term3 = Term ("cynik", [||], [|term1; term2|]) in
+ let term4 = Var ("zmienna", [|Var ("a1",[||],0,[||])|], 0, [| |]) in
+ test_code_decode_te term1;
+ test_code_decode_te term2;
+ test_code_decode_te term3;
+ test_code_decode_te term4;
+ );
+
+ "coding type definitions" >::
+ (fun () ->
+ let test_code_decode_td td =
+ let td1 = decode_type_definition (code_type_definition td) in
+ assert_equal ~printer:(fun x -> "type definition test") td td1 in
+ let td0 = ("numerek", 0) in
+ let td1 = ("listek", 1) in
+ let td2 = ("parka", 2) in
+ test_code_decode_td td0;
+ test_code_decode_td td1;
+ test_code_decode_td td2;
+ );
+
+ "coding syntax definitions" >::
+ (fun () ->
+ let test_code_decode_sd sd =
+ 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,[||])) in
+ let sd1 = SyntaxDef.SDtype [se1; se2] 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;
+ );
+
+ "display term" >::
+ (fun () ->
+ let test_display_term res te =
+ assert_equal ~printer:(fun x -> x) res (display_term te) in
+ test_display_term "[true, false, true]"
+ (code_list code_bool [true; false; true]);
+ test_display_term "\"ala ma kota\"" (code_string "ala ma kota");
+ test_display_term "type ''\"tp\"''"
+ (code_syntax_definition (SyntaxDef.SDtype ([SyntaxDef.Str "tp"])));
+ );
+
+ "parsing and printing" >::
+ (fun () ->
+ let testpp s = assert_equal ~printer:(fun x -> x) s
+ (term_to_string (term_of_string s)) in
+ testpp "ala";
+ testpp "ala (a )";
+ testpp "ala (a, b )";
+ testpp "@V [x @: @? a @: 0 ]";
+ testpp "@V [x @: @? a @: 0 ] (p )";
+ testpp "@V [x @: @? a @: 0 ] (p, q )";
+ testpp "@`kota ma ala@`";
+ testpp "pies (@`kota ma ala@` )";
+ testpp "a (pies (@`kota ma ala@` ), pies )";
+ testpp "a (b (c, d ), e )";
+ testpp "@L[]";
+ testpp "@L[a]";
+ testpp "@L[a, b]";
+ );
+
+ "type reconstruction" >::
+ (fun () ->
+ let list_tp_a = BuiltinLang.list_tp_a in
+ let typesl = [("cons", Term (Term.fun_type_name, [||],
+ [|Var ("a",[||],0,[||]); list_tp_a;
+ list_tp_a|]));
+ ("nil", list_tp_a);
+ ("true", BuiltinLang.boolean_tp);
+ ("1", Term ("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", [|Var ("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
+ let test_tt res te = assert_equal ~printer:(fun x -> x) res
+ (type_to_string (type_of_term types te)) in
+ test_tt "T\\?_list (@? a._.6)" te1;
+ test_tt "T\\?_list (Tboolean)" te2;
+ test_tt "T\\?_list (int)" te3;
+ );
+]
Modified: trunk/Toss/Term/ParseArc.ml
===================================================================
--- trunk/Toss/Term/ParseArc.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/ParseArc.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -2,9 +2,8 @@
and checks if terms are well-typed when closing arcs. *)
open List
-open TermType
+open Term
open SyntaxDef
-open Term
(* The type of elements created during parsing.
@@ -12,13 +11,13 @@
Type is kept together with each term not to recalculate it too often. *)
type parser_elem =
| Token of string
- | Typed_term of term_type * term
+ | Typed_term of term * term
(* Print a parser elem. *)
let elem_str = function
| Token s -> "Tok " ^ s
| Typed_term (tp, te) ->
- "Te " ^ (term_to_string te) ^ " : " ^ (type_to_string tp)
+ "Te " ^ (Coding.term_to_string te) ^ " : " ^ (type_to_string tp)
(* The type of incomplete arcs that appear during parsing;
@@ -91,7 +90,7 @@
Throws NOT_CLOSED if closing fails. *)
let match_of_tok = function
| (Str _, _) -> []
- | (Tp _, Token s) -> [code_string s]
+ | (Tp _, Token s) -> [Coding.code_string s]
| (Tp _, Typed_term (_, te)) -> [te]
let close_arc type_decls = function
@@ -99,13 +98,14 @@
let elems = syntax_elems_of_sd sd in
let args = flatten (map match_of_tok (combine elems (rev l))) in
let res_term = (match sd with
- | SDtype _ -> Term (BuiltinLang.term_type_cons_name,
- [|code_string n; code_list (fun x -> x) args|])
- | SDfun _ -> Term (n, Array.of_list args)
+ | SDtype _ ->
+ Term (BuiltinLang.term_type_cons_name, [||],
+ [|Coding.code_string n; Coding.code_list (fun x -> x) args|])
+ | SDfun _ -> Term (n, [||], Array.of_list args)
| SDvar (_, _) ->
(match sd_type sd with
| None -> failwith "variable syntax definition w/o type"
- | Some (ty) -> Var (n, ty, 0, Array.of_list args) )
+ | Some (ty) -> Var (n, [|ty|], 0, Array.of_list args) )
) in
(try (Typed_term (type_of_term type_decls res_term, res_term), spos)
with NOT_WELL_TYPED _ -> raise NOT_CLOSED)
Modified: trunk/Toss/Term/ParseArc.mli
===================================================================
--- trunk/Toss/Term/ParseArc.mli 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/ParseArc.mli 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,13 +1,13 @@
(** Contains the bottom-up chart-based parser that uses syntax definitions
and checks if terms are well-typed when closing arcs. **)
-open TermType
+open Term
open SyntaxDef
(** Elements used in the parser. *)
type parser_elem =
| Token of string
- | Typed_term of term_type * Term.term
+ | Typed_term of term * Term.term
(** Print a parser elem. *)
val elem_str : parser_elem -> string
@@ -24,14 +24,14 @@
(** Closes all arcs from the given list that can be closed
and returns the elements together with starting positions. *)
-val close_arc_list : (string, term_type) Hashtbl.t ->
+val close_arc_list : (string, term) Hashtbl.t ->
parser_arc list -> (parser_elem * int) list
-val parse_to_array : (string, term_type) Hashtbl.t ->
+val parse_to_array : (string, term) Hashtbl.t ->
(syntax_def * string) list -> string list -> (parser_elem * int) list array
-val parse : (string, term_type) Hashtbl.t -> (syntax_def * string) list ->
+val parse : (string, term) Hashtbl.t -> (syntax_def * string) list ->
string list -> parser_elem list
val split_input_string : string -> string list
Modified: trunk/Toss/Term/ParseArcTest.ml
===================================================================
--- trunk/Toss/Term/ParseArcTest.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/ParseArcTest.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,23 +1,22 @@
open OUnit
-open TermType
+open Term
open SyntaxDef
open BuiltinLang
open ParseArc
let tests = "ParseArc" >::: [
-
"extend and close arc list" >::
(fun () ->
let elem_eq res e = assert_equal ~printer:(fun x -> x) res (elem_str e) in
let type_decls_list = [
- (list_cons_name, TTerm (TermType.fun_type_name,
- [|TVar ("a",[||],0,[||]); list_tp_a; list_tp_a|]));
+ (list_cons_name, Term (Term.fun_type_name, [||],
+ [|Var ("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"], TVar ("a",[||],0,[||])) in
+ let var_x_a_sd = SDvar ([Str "x"], Var ("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
@@ -45,14 +44,14 @@
"parse" >::
(fun () ->
let type_decls_list = [
- (list_cons_name, TTerm (TermType.fun_type_name,
- [|TVar ("a",[||],0,[||]); list_tp_a; list_tp_a|]));
+ (list_cons_name, Term (Term.fun_type_name, [||],
+ [|Var ("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"], TVar ("a",[||],0,[||])) in
+ let var_x_a_sd = SDvar ([Str "x"], Var ("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/Rewriting.ml
===================================================================
--- trunk/Toss/Term/Rewriting.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/Rewriting.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,7 +1,6 @@
(* Contains the functions responsible for rewriting and normalization. *)
open List
-open TermType
open SyntaxDef
open BuiltinLang
open Term
@@ -14,7 +13,7 @@
let is_left_linear (lhs, _) =
let rec vars = function
- | Term (_, a) -> List.concat (Array.to_list (Array.map vars a))
+ | 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
let vs = List.sort String.compare (vars lhs) in
let rec has_duplicates = function [] | [_] -> false
@@ -25,11 +24,11 @@
let add_first_rule (Rules (rrs)) rr =
if is_left_linear rr then Rules (rr :: rrs) else
- failwith ("Non linear: " ^ (Term.display_term (fst rr)))
+ failwith ("Non linear: " ^ (Coding.display_term (fst rr)))
let add_last_rule (Rules (rrs)) rr =
if is_left_linear rr then Rules (rrs @ [rr]) else
- failwith ("Non linear: " ^ (Term.display_term (fst rr)))
+ failwith ("Non linear: " ^ (Coding.display_term (fst rr)))
(* --- Rewriting with Clash Detection --- *)
@@ -42,32 +41,32 @@
functions on the left side, but we do not check it dynamically here. *)
let check_clash_match (term1, term2) =
let rec check_clash_match_in = function
- | (Term (n1, a1), Term (n2, a2))
+ | (Term (n1, _, a1), Term (n2, _, a2))
when (n1 = n2) && (Array.length a1 = Array.length a2) ->
let update (clash, substs) t1 t2 =
let (new_clash, new_substs) = check_clash_match_in (t1, t2) in
(clash || new_clash, new_substs @ substs) in
Aux.array_fold_left2 update (false, []) a1 a2
- | (Term (n1, _), Term (n2, [||])) when (n1 = n2) ->
+ | (Term (n1, _, _), Term (n2, _, [||])) when (n1 = n2) ->
raise NO_MATCH (* used cons vs. functional cons *)
- | (Term (n1, _), Term (n2, _)) when (n1 = n2) ->
+ | (Term (n1, _, _), Term (n2, _, _)) when (n1 = n2) ->
failwith "curried functions not supported (yet?)"
- | (Term (n1, _), Term (n2, _)) -> (* when (n2.[0] != 'F') *)
+ | (Term (n1, _, _), Term (n2, _, _)) -> (* when (n2.[0] != 'F') *)
raise NO_MATCH
| (Term _, _) ->
(true, [])
| (Var (n, _, d, [||]), t2) ->
- (false, [(n, (d, fn_apply d decode_term t2))])
+ (false, [(n, (d, fn_apply d Coding.decode_term t2))])
| (Var _, _) ->
failwith "functional var on left side of rr" in
match (term1, term2) with (* now term1 = f (args) *)
- | (Term (n1, a1), Term (n2, a2))
+ | (Term (n1, _, a1), Term (n2, _, a2))
when (n1 = n2) && (Array.length a1 = Array.length a2) ->
let update (clash, substs) t1 t2 =
let (new_clash, new_substs) = check_clash_match_in (t1, t2) in
(clash || new_clash, new_substs @ substs) in
Aux.array_fold_left2 update (false, []) a1 a2
- | (Term (n1, _), Term (n2, [||])) when (n1 = n2) ->
+ | (Term (n1, _, _), Term (n2, _, [||])) when (n1 = n2) ->
raise NO_MATCH (* non-0-arg fun and functional term *)
| _ -> failwith "rewriting not this function"
@@ -87,7 +86,7 @@
let (clash, substs) = check_clash_match (left, term) in
if clash then term else
let (merge_clash, merged_substs) = merge_substs substs in
- if merge_clash then term else apply_s merged_substs right
+ if merge_clash then term else Coding.apply_s merged_substs right
(* The final rewrite function that takes care of function names in terms. *)
let rewrite (Rules (rules)) term =
@@ -100,14 +99,14 @@
(* --- Normalisation --- *)
let rec normalise_special_id_one name = function
- | Term (n, [|a|]) when n = name -> a
- | Term (n, a) -> Term (n, Array.map (normalise_special_id_one name) a)
+ | Term (n, _, [|a|]) when n = name -> a
+ | Term (n, t, a) -> Term (n, t, Array.map (normalise_special_id_one name) a)
| Var (n, ty, d, a) ->
Var (n, ty, d, 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, a) -> Term (n, Array.map (normalise_special_id_all name) a)
+ | 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, ty, d, a) ->
Var (n, ty, d, Array.map (normalise_special_id_all name) a)
@@ -115,12 +114,12 @@
let normalise_verbatim = normalise_special_id_one verbatim_name
let rec normalise_special rr_spec = function
- | Term (n, [|a|]) as te when n = verbatim_name -> te
- | Term (n, a) when n.[0] = 'F' ->
- let normalised = Term (n, Array.map (normalise_special rr_spec) a) in
+ | Term (n, _, [|a|]) as te when n = verbatim_name -> te
+ | Term (n, t, a) when n.[0] = 'F' ->
+ let normalised = Term (n, t, Array.map (normalise_special rr_spec) a) in
rr_spec normalised
- | Term (n, a) ->
- Term (n, Array.map (normalise_special rr_spec) a)
+ | Term (n, t, a) ->
+ Term (n, t, Array.map (normalise_special rr_spec) a)
| Var (n, ty, d, a) ->
Var (n, ty, d, Array.map (normalise_special rr_spec) a)
@@ -137,24 +136,24 @@
(steps := !steps + fst (res); snd (res))) th_arr in
(!steps, res_arr)
and basic_normalise rr rr_spec m = function
- | Term (n, [|Term (f, a); r|]) when n = let_major_be_name ->
+ | Term (n, t, [|Term (f, ft, a); r|]) when n = let_major_be_name ->
let (steps_l, na) = basic_normalise_arr rr rr_spec m a in
let (steps_r, rs) = basic_normalise rr rr_spec m r in
- (steps_l + steps_r, Term (n, [|Term (f, na); rs|]))
- | Term (n, [|a|]) as te when n = verbatim_name -> (0, te)
- | Term (nm, [|c; y; n|]) when nm = if_then_else_name ->
+ (steps_l + steps_r, Term (n, t, [|Term (f, ft, na); rs|]))
+ | Term (n, _, [|a|]) as te when n = verbatim_name -> (0, te)
+ | Term (nm, nt, [|c; y; n|]) when nm = if_then_else_name ->
let (steps_c, norm_cond) = basic_normalise rr rr_spec m c in
- let norm_cond_te = Term (nm, [|norm_cond; y; n|]) in
+ let norm_cond_te = Term (nm, nt, [|norm_cond; y; n|]) in
let rewritten = rr norm_cond_te in
if (rewritten = norm_cond_te) then
- (steps_c, Term (nm, [|norm_cond; normalise_special rr_spec y;
- normalise_special rr_spec n|]))
+ (steps_c, Term (nm, nt, [|norm_cond; normalise_special rr_spec y;
+ normalise_special rr_spec n|]))
else
let (steps, res) = basic_normalise rr rr_spec m rewritten in
(steps + steps_c + 1, res)
- | Term (n, a) when n.[0] = 'F' ->
+ | Term (n, t, a) when n.[0] = 'F' ->
(let (prev_steps, prev_res) = basic_normalise_arr rr rr_spec m a in
- let nmlized = Term (n, prev_res) in
+ let nmlized = Term (n, t, prev_res) in
let found= try Some (TermHashtbl.find m nmlized) with Not_found -> None in
match found with Some (r) -> (prev_steps, r) | None ->
let rewritten = rr nmlized in
@@ -167,9 +166,9 @@
(TermHashtbl.add m nmlized res; (0, res))
else (prev_steps + steps + 1, res)
)
- | Term (n, a) ->
+ | Term (n, t, a) ->
let (steps, res) = basic_normalise_arr rr rr_spec m a in
- (steps, Term (n, res))
+ (steps, Term (n, t, res))
| Var (n, ty, d, a) ->
let (steps, res) = basic_normalise_arr rr rr_spec m a in
(steps, Var (n, ty, d, res))
@@ -178,9 +177,9 @@
let normalise mem rules is_special rewrite_special inp_term =
let term = normalise_brackets inp_term in
let rr = function
- | Term (n, a) as te when (is_special n) ->
+ | Term (n, _, a) as te when (is_special n) ->
rewrite_special (normalise_verbatim te)
- | Term (n, a) as te ->
+ | Term (n, _, a) as te ->
(try rewrite (Hashtbl.find rules n) te with Not_found -> te)
| te -> te in
let (_, normalised) =
Modified: trunk/Toss/Term/RewritingTest.ml
===================================================================
--- trunk/Toss/Term/RewritingTest.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/RewritingTest.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -1,7 +1,8 @@
open OUnit
+open Term
open BuiltinLang
-open Term
open Rewriting
+open Coding
let tests = "Rewriting" >::: [
"rewrite" >::
@@ -9,24 +10,24 @@
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", boolean_tp, 0, [||]) in
- let var_y_b = Var ("y", boolean_tp, 0, [||]) in
- let rr1 =
- (Term ("Fand", [|code_bool true; code_bool true|]), code_bool true) in
- let rr2 = (Term ("Fand", [|var_x_b; var_y_b|]), code_bool false) in
- let t1 = Term ("Fand", [|code_bool true; code_bool true|]) in
+ let var_x_b = Var ("x", [|boolean_tp|], 0, [||]) in
+ let var_y_b = Var ("y", [|boolean_tp|], 0, [||]) in
+ let rr1 =
+ (Term ("Fand",[||],[|code_bool true;code_bool true|]),code_bool true) in
+ let rr2 = (Term ("Fand", [||], [|var_x_b; var_y_b|]), code_bool false) in
+ let t1 = Term ("Fand", [||], [|code_bool true; code_bool true|]) in
test_rr [rr1; rr2] "Ftrue" t1;
- let t2 = Term ("Fand", [|code_bool true; code_bool false|]) in
+ let t2 = Term ("Fand", [||], [|code_bool true; code_bool false|]) in
test_rr [rr1; rr2] "Ffalse" t2;
- let t3 = Term ("Fand", [|code_bool false; code_bool true|]) in
+ let t3 = Term ("Fand", [||], [|code_bool false; code_bool true|]) in
test_rr [rr1; rr2] "Ffalse" t3;
- let t4 = Term ("Fand", [|code_bool false; code_bool false|]) in
+ let t4 = Term ("Fand", [||], [|code_bool false; code_bool false|]) in
test_rr [rr1; rr2] "Ffalse" t4;
- let t5 = Term ("Fand", [|code_bool false; var_x_b|]) in
+ let t5 = Term ("Fand", [||], [|code_bool false; var_x_b|]) in
test_rr [rr1; rr2] "Ffalse" t5;
- let t6 = Term ("Fand", [|code_bool true; var_x_b|]) in
+ let t6 = Term ("Fand", [||], [|code_bool true; var_x_b|]) in
test_rr [rr1; rr2] "Fand (Ftrue, @V [x @: Tboolean @: 0 ] )" t6;
- let t7 = Term ("Fand", [|var_x_b; var_y_b|]) in
+ let t7 = Term ("Fand", [||], [|var_x_b; var_y_b|]) in
test_rr [rr1; rr2] ("Fand (@V [x @: Tboolean @: 0 ], " ^
"@V [y @: Tboolean @: 0 ] )") t7;
);
@@ -38,22 +39,22 @@
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", boolean_tp, 0, [||]) in
- let var_y_b = Var ("y", boolean_tp, 0, [||]) in
+ let var_x_b = Var ("x", [|boolean_tp|], 0, [||]) in
+ let var_y_b = Var ("y", [|boolean_tp|], 0, [||]) in
let rr1 =
- (Term ("Fand", [|code_bool true; code_bool true|]), code_bool true) in
- let rr2 = (Term ("Fand", [|var_x_b; var_y_b|]), code_bool false) in
+ (Term ("Fand",[||],[|code_bool true;code_bool true|]),code_bool true) in
+ let rr2 = (Term ("Fand", [||], [|var_x_b; var_y_b|]), code_bool false) in
let rrs = ("Fand", [rr1; rr2]) in
- let t1 = Term ("Fand", [|code_bool true; code_bool true|]) in
+ let t1 = Term ("Fand", [||], [|code_bool true; code_bool true|]) in
test_ne rrs "Ftrue" t1;
- let t2 = Term ("Fand", [|code_bool true; t1|]) in
+ let t2 = Term ("Fand", [||], [|code_bool true; t1|]) in
test_ne rrs "Ftrue" t2;
- let t3 = Term ("Fand", [|var_x_b; t1|]) in
+ let t3 = Term ("Fand", [||], [|var_x_b; t1|]) in
test_ne rrs "Fand (@V [x @: Tboolean @: 0 ], Ftrue )" t3;
- let t4 = Term (if_then_else_name, [|var_x_b; t1; t1|]) in
+ let t4 = Term (if_then_else_name, [||], [|var_x_b; t1; t1|]) in
test_ne rrs ("Fif_\\?_then_\\?_else_\\? (@V [x @: Tboolean @: 0 ], Fand "^
"(Ftrue, Ftrue ), Fand (Ftrue, Ftrue ) )") t4;
- let t5 = Term ("Ckot", [|var_x_b; t1; t1|]) in
+ let t5 = Term ("Ckot", [||], [|var_x_b; t1; t1|]) in
test_ne rrs "Ckot (@V [x @: Tboolean @: 0 ], Ftrue, Ftrue )" t5;
);
]
Modified: trunk/Toss/Term/SyntaxDef.ml
===================================================================
--- trunk/Toss/Term/SyntaxDef.ml 2012-06-15 21:24:23 UTC (rev 1725)
+++ trunk/Toss/Term/SyntaxDef.ml 2012-06-16 17:01:17 UTC (rev 1726)
@@ -4,17 +4,17 @@
open Array
open Aux
-open TermType
+open Term
(* The type of syntax elements. *)
-type syntax_elem = Str of string | Tp of term_type
+type syntax_elem = Str of string | Tp of term
(* The type of syntax definitions. *)
type syntax_def =
| SDtype of syntax_elem list
- | SDfun of syntax_elem list * term_type
- | SDvar of syntax_elem list * term_type
+ | SDfun of syntax_elem list * term
+ | SDvar of syntax_elem list * term
(* --- Basic functions for Syntax Definitions, generating names --- *)
@@ -71,9 +71,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 = List.concat (List.map (function Str _ -> [] | Tp _ -> ["a"]) sel) in
- let arg_of s1 s2 = TVar (s1 ^ "_" ^ s2, [||], 0, [||]) in
+ let arg_of s1 s2 = Var (s1 ^ "_" ^ s2, [||], 0, [||]) in
let args = List.map2 arg_of s (numbers (List.length s)) in
- TTerm (name_of_sd sd, of_list args)
+ Term (name_of_sd sd, [||], of_list args)
| _ -> failwith "type of sd on non-type definition"
@@ -84,9 +84,9 @@
match sd with
| SDtype _ -> None
| SDfun (sel, ty)-> Some (if (ts = []) then ty else
- TTerm (TermType.fun_type_name, of_list (ts @ [ty])))
+ Term (Term.fun_type_name, [||], of_list (ts @ [ty])))
| SDvar (sel, ty)-> Some (if (ts = []) then ty else
- TTerm (TermType.fun_type_name, of_list (ts @ [...
[truncated message content] |
