[Toss-devel-svn] SF.net SVN: toss:[1713] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1713] trunk/Toss
|
From: <luk...@us...> - 2012-05-21 22:07:09
|
Revision: 1713
http://toss.svn.sourceforge.net/toss/?rev=1713&view=rev
Author: lukaszkaiser
Date: 2012-05-21 22:07:00 +0000 (Mon, 21 May 2012)
Log Message:
-----------
Correcting Term functions, merging old docs.
Modified Paths:
--------------
trunk/Toss/Makefile
trunk/Toss/Term/.cvsignore
trunk/Toss/Term/Makefile
trunk/Toss/Term/TRS.ml
trunk/Toss/Term/TRS.mli
trunk/Toss/Term/TRSTest.ml
trunk/Toss/www/reference/Makefile
trunk/Toss/www/reference/reference.tex
Added Paths:
-----------
trunk/Toss/Term/lib/.cvsignore
trunk/Toss/Term/lib/arithmetics.trs
trunk/Toss/Term/lib/basic.trs
trunk/Toss/Term/lib/core.trs
trunk/Toss/Term/lib/lists.trs
trunk/Toss/Term/lib/sasha.trs
trunk/Toss/Term/tests/differentiation.trs
trunk/Toss/Term/tests/english.trs
trunk/Toss/Term/tests/entanglement.trs
trunk/Toss/Term/tests/fo_formula.trs
trunk/Toss/Term/tests/sasha_basic.trs
trunk/Toss/Term/tests/short_checks.trs
trunk/Toss/Term/tests/simple_algo.trs
trunk/Toss/www/reference/parser.tex
trunk/Toss/www/reference/rewriting.tex
trunk/Toss/www/reference/simplification.tex
trunk/Toss/www/reference/syntax_definitions.tex
trunk/Toss/www/reference/terms.tex
trunk/Toss/www/reference/types.tex
Removed Paths:
-------------
trunk/Toss/Term/lib/arithmetics.spg
trunk/Toss/Term/lib/basic.spg
trunk/Toss/Term/lib/core.spg
trunk/Toss/Term/lib/lists.spg
trunk/Toss/Term/lib/sasha.spg
trunk/Toss/Term/tests/differentiation.spg
trunk/Toss/Term/tests/english.spg
trunk/Toss/Term/tests/entanglement.spg
trunk/Toss/Term/tests/fo_formula.spg
trunk/Toss/Term/tests/sasha_basic.spg
trunk/Toss/Term/tests/short_checks.spg
trunk/Toss/Term/tests/simple_algo.spg
Property Changed:
----------------
trunk/Toss/Term/
trunk/Toss/Term/lib/
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Makefile 2012-05-21 22:07:00 UTC (rev 1713)
@@ -61,7 +61,7 @@
NAMEPATTERN = f$(subst .,_,$(subst -,_,$(subst /,_,$(basename $@))))
%.resource:
@echo -n 'let $(NAMEPATTERN) = "' >> Formula/Resources.ml
- @cat $(basename $@) | sed 's/"/\\"/g' >> Formula/Resources.ml
+ @cat $(basename $@) | sed 's/\\/\\\\/g' | sed 's/"/\\"/g' >> Formula/Resources.ml
@echo '"' >> Formula/Resources.ml
@echo '' >> Formula/Resources.ml
@echo 'let _ = files := ("$(basename $@)", $(NAMEPATTERN)) :: !files' \
@@ -72,6 +72,15 @@
TOSSEXFILES = $(shell find examples -name "*.toss")
TOSSEXRESC = $(addsuffix .resource, $(TOSSEXFILES))
+TRSPARSEDFILES = $(shell find Term/lib -name "*.trs.parsed")
+TRSPARSEDRESC = $(addsuffix .resource, $(TRSPARSEDFILES))
+
+TRSTESTFILES = $(shell find Term/tests -name "*.trs")
+TRSTESTRESC = $(addsuffix .resource, $(TRSTESTFILES))
+
+TRSTESTLOGFILES = $(shell find Term/tests -name "*.log")
+TRSTESTLOGRESC = $(addsuffix .resource, $(TRSTESTLOGFILES))
+
new_resource_file:
@echo "(* Automatically Constructed Resources *)" > Formula/Resources.ml
@echo "" >> Formula/Resources.ml
@@ -80,7 +89,7 @@
@echo "let get_file fn = List.assoc fn !files" >> Formula/Resources.ml
@echo "" >> Formula/Resources.ml
-all_resources: $(TOSSEXRESC) \
+all_resources: $(TOSSEXRESC) $(TRSPARSEDRESC) $(TRSTESTRESC) $(TRSTESTLOGRESC) \
GGP/tests/connect5-simpl.toss.resource \
GGP/tests/breakthrough-simpl.toss.resource \
GGP/examples/connect5.gdl.resource \
@@ -93,11 +102,23 @@
Formula/Resources.ml:
@make new_resource_file > /dev/null
+ @make allparsed
@make all_resources
EXTDEPS = caml_extensions/pa_let_try.cmo caml_extensions/pa_log.cmo Formula/Resources.ml
+MKPARSED = ./TRSTest.native -c -f -l "Term/lib"
+
+%.trs.parsed: %.trs
+ make ./Term/TRSTest.native
+ $(MKPARSED) -o $@ < $< > /dev/null
+
+allparsed: Term/lib/core.trs.parsed Term/lib/arithmetics.trs.parsed \
+ Term/lib/lists.trs.parsed Term/lib/basic.trs.parsed \
+ Term/lib/sasha.trs.parsed
+
+
# -------- MAIN OCAMLBUILD PART --------
OCB_LFLAG=-lflags -I,+js_of_ocaml,-I,+site-lib/js_of_ocaml,-g
@@ -176,6 +197,14 @@
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
./TossServer -fulltest Solver -v
+# Term tests
+TermTests: TossServer
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
+ ./TossServer -fulltest Term
+TermTestsVerbose: TossServer
+ OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
+ ./TossServer -fulltest Term -v
+
# Arena tests
ArenaTests: TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
@@ -251,3 +280,4 @@
rm -f *.cmx *.cmi *.o *.cmo *.a *.cmxa *.cma *.annot *~ TossServer
rm -f Formula/*~ Solver/*~ Arena/*~ Learn/*~ Play/*~ GGP/*~ Server/*~
rm -f caml_extensions/*.cmo caml_extensions/*.cmi Formula/Resources.ml
+ rm -f Term/lib/*.trs.parsed
Property changes on: trunk/Toss/Term
___________________________________________________________________
Modified: svn:ignore
- # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
speagram
*.mly.debug
*.cmx
*.cmo
*.cmi
*.annot
*~
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*~
Modified: trunk/Toss/Term/.cvsignore
===================================================================
--- trunk/Toss/Term/.cvsignore 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/.cvsignore 2012-05-21 22:07:00 UTC (rev 1713)
@@ -2,11 +2,4 @@
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
-speagram
-
-*.mly.debug
-*.cmx
-*.cmo
-*.cmi
-*.annot
*~
Modified: trunk/Toss/Term/Makefile
===================================================================
--- trunk/Toss/Term/Makefile 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/Makefile 2012-05-21 22:07:00 UTC (rev 1713)
@@ -1,14 +1,10 @@
-all: parsed
+all: coreparsed
-RUN = ../TRSTest.native -c -f -l "../Term/lib"
+MKPARSED = ../TRSTest.native -c -f -l "../Term/lib"
-parsed:
+coreparsed:
make -C .. ./Term/TRSTest.native
- $(RUN) -o lib/core.spg.parsed < lib/core.spg > /dev/null
- $(RUN) -o lib/arithmetics.spg.parsed < lib/arithmetics.spg > /dev/null
- $(RUN) -o lib/lists.spg.parsed < lib/lists.spg > /dev/null
- $(RUN) -o lib/basic.spg.parsed < lib/basic.spg > /dev/null
- $(RUN) -o lib/sasha.spg.parsed < lib/sasha.spg > /dev/null
+ $(MKPARSED) -o lib/core.trs.parsed < lib/core.trs > /dev/null
.PHONY:
Modified: trunk/Toss/Term/TRS.ml
===================================================================
--- trunk/Toss/Term/TRS.ml 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/TRS.ml 2012-05-21 22:07:00 UTC (rev 1713)
@@ -24,6 +24,7 @@
(string * term_type) list (* Objects with types for chronologic access *)
;;
+
(* -------------- GETTING SYNTAX DEFINITIONS OUT ---------------- *)
let syntax_defs_of_sys = function
@@ -121,21 +122,16 @@
let rec update_on_load_file k file sys bs =
- try
- let in_file = open_in (file ^ ".spg.parsed") in
- let rec process s =
- try
- let line = input_line in_file in
- if line = "" then process s else (
- (* print_endline ("parsing: " ^ line); *)
- let te = term_of_string line in
- s := update_on_term k te !s bs;
- process s
- )
- with End_of_file -> !s in
- process (ref bs)
- with
- Sys_error s -> raise (Sys_error s)
+ let rec process s = function
+ | [] -> !s
+ | line :: rest ->
+ if line = "" then process s rest else (
+ let te = term_of_string line in
+ s := update_on_term k te !s bs;
+ process s rest
+ ) in
+ let fname = file ^ ".trs.parsed" in
+ process (ref bs) (Aux.split_newlines (AuxIO.input_file fname))
and update_on_term k te sys bs =
try update_on_sd (decode_syntax_definition te) sys with
DECODE _ ->
@@ -469,7 +465,7 @@
brackets_rules; verbatim_rules; if_then_else_rules; preprocess_rules;
additional_xslt_rules; string_quote_rules];; (* eq_bool_rules *)
-let basic_system =
+let basic_system () =
let upd sys sd = update_on_sd sd sys in
let mem_rrs = (TermHashtbl.create 512, Hashtbl.create 512) in
let emptys = Sys ([], Hashtbl.create 512, mem_rrs, [], []) in
@@ -479,7 +475,7 @@
;;
let process_with_system lp verbose s str fail xml_out outprint =
- process_with_system_bs lp verbose s str fail xml_out basic_system outprint
+ process_with_system_bs lp verbose s str fail xml_out (basic_system()) outprint
;;
Modified: trunk/Toss/Term/TRS.mli
===================================================================
--- trunk/Toss/Term/TRS.mli 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/TRS.mli 2012-05-21 22:07:00 UTC (rev 1713)
@@ -29,7 +29,7 @@
val basic_sdefs : syntax_def list;;
-val basic_system : spg_system;;
+val basic_system : unit -> spg_system;;
(* -------- COMPLETE ONE STEP OF A SHELL ------- *)
Modified: trunk/Toss/Term/TRSTest.ml
===================================================================
--- trunk/Toss/Term/TRSTest.ml 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/TRSTest.ml 2012-05-21 22:07:00 UTC (rev 1713)
@@ -60,13 +60,13 @@
;;
let test fname =
- let s = ref (AuxIO.input_file ("./Term/tests/" ^ fname ^ ".spg")) in
+ let s = ref (AuxIO.input_file ("./Term/tests/" ^ fname ^ ".trs")) in
let read_s () = if !s = "" then raise End_of_file else (
let c = !s.[0] in s := String.sub !s 1 ((String.length !s)-1); c) in
let o = ref "" in
let print_o str = o := !o ^ str ^ "\n" in
run "./Term/lib" false "" "" "" true
- (ref basic_system) read_s true false (ref []) print_o;
+ (ref (basic_system ())) read_s true false (ref []) print_o;
assert_equal ~printer:(fun x -> x) (Aux.normalize_spaces (
AuxIO.input_file ("./Term/tests/" ^ fname ^ ".log")))
(Aux.normalize_spaces !o)
@@ -133,7 +133,7 @@
ignore (OUnit.run_test_tt ~verbose:true tests)
else (
let parsed_terms = ref [] in
- let basic_sys = ref basic_system in
+ let basic_sys = ref (basic_system ()) in
if !builtin_out then
let defs = String.concat "\n" (map pretty_print_sd basic_sdefs) in
print_endline ("// SPEAGRAM BUILT-IN DEFS.\n" ^ defs ^ "\n")
Property changes on: trunk/Toss/Term/lib
___________________________________________________________________
Added: svn:ignore
+ # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
# svn propset svn:ignore -F .cvsignore .
*.parsed
*~
Added: trunk/Toss/Term/lib/.cvsignore
===================================================================
--- trunk/Toss/Term/lib/.cvsignore (rev 0)
+++ trunk/Toss/Term/lib/.cvsignore 2012-05-21 22:07:00 UTC (rev 1713)
@@ -0,0 +1,6 @@
+# We are still using .cvsignore files as we find them easier to manage
+# than svn properties. Therefore if you change .cvsignore do the following.
+# svn propset svn:ignore -F .cvsignore .
+
+*.parsed
+*~
Deleted: trunk/Toss/Term/lib/arithmetics.spg
===================================================================
--- trunk/Toss/Term/lib/arithmetics.spg 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/lib/arithmetics.spg 2012-05-21 22:07:00 UTC (rev 1713)
@@ -1,462 +0,0 @@
-Load state library:/core.
-
-// BASIC NUMBER TYPES.
-
-// BINARY NUMEBERS.
-
-New type ''binary number''.
-New function ''0'' as binary number.
-New function ''1'' as binary number.
-New function binary number ''0'' as binary number.
-New function binary number ''1'' as binary number.
-
-// TYPE CAST TO ENFORCE NATURAL NUMBER TYPE.
-New function binary number ''as binary number'' as binary number.
-New variable b as binary number.
-Let b as binary number be b.
-Close context.
-
-// NATURAL NUMBERS.
-New type ''natural number''.
-New function ''0'' as natural number.
-New function ''1'' as natural number.
-New function ''2'' as natural number.
-New function ''3'' as natural number.
-New function ''4'' as natural number.
-New function ''5'' as natural number.
-New function ''6'' as natural number.
-New function ''7'' as natural number.
-New function ''8'' as natural number.
-New function ''9'' as natural number.
-New function natural number ''0'' as natural number.
-New function natural number ''1'' as natural number.
-New function natural number ''2'' as natural number.
-New function natural number ''3'' as natural number.
-New function natural number ''4'' as natural number.
-New function natural number ''5'' as natural number.
-New function natural number ''6'' as natural number.
-New function natural number ''7'' as natural number.
-New function natural number ''8'' as natural number.
-New function natural number ''9'' as natural number.
-
-// TYPE CAST TO ENFORCE NATURAL NUMBER TYPE.
-New function natural number ''as natural number'' as natural number.
-New variable n as natural number.
-Let n as natural number be n.
-Close context.
-
-// Standard numbers 0 and 1 are natural and not binary.
-See 0 as natural number preferred to different 0 as binary number.
-See 1 as natural number preferred to different 1 as binary number.
-
-
-// This number-append is necessary for division later.
-New function natural number ''@'' natural number as natural number.
-New variable varnat_a as natural number.
-New variable varnat_b as natural number.
-Let varnat_a @ 0 be varnat_a 0.
-Let varnat_a @ 1 be varnat_a 1.
-Let varnat_a @ 2 be varnat_a 2.
-Let varnat_a @ 3 be varnat_a 3.
-Let varnat_a @ 4 be varnat_a 4.
-Let varnat_a @ 5 be varnat_a 5.
-Let varnat_a @ 6 be varnat_a 6.
-Let varnat_a @ 7 be varnat_a 7.
-Let varnat_a @ 8 be varnat_a 8.
-Let varnat_a @ 9 be varnat_a 9.
-Let varnat_a @ (varnat_b 0) be (varnat_a @ varnat_b) 0.
-Let varnat_a @ (varnat_b 1) be (varnat_a @ varnat_b) 1.
-Let varnat_a @ (varnat_b 2) be (varnat_a @ varnat_b) 2.
-Let varnat_a @ (varnat_b 3) be (varnat_a @ varnat_b) 3.
-Let varnat_a @ (varnat_b 4) be (varnat_a @ varnat_b) 4.
-Let varnat_a @ (varnat_b 5) be (varnat_a @ varnat_b) 5.
-Let varnat_a @ (varnat_b 6) be (varnat_a @ varnat_b) 6.
-Let varnat_a @ (varnat_b 7) be (varnat_a @ varnat_b) 7.
-Let varnat_a @ (varnat_b 8) be (varnat_a @ varnat_b) 8.
-Let varnat_a @ (varnat_b 9) be (varnat_a @ varnat_b) 9.
-
-Close context.
-
-
-// ARITHMETIC FUNCTION DECLARATIONS.
-
-// BINARY NUMBERS.
-
-New variable n as binary number.
-New variable m as binary number.
-New variable k as binary number.
-New variable n' as binary number.
-New variable m' as binary number.
-New variable k' as binary number.
-
-New function binary number ''+'' binary number as binary number.
-See (n+(m0)) preferred to (n'+m')0.
-See (n+(m1)) preferred to (n'+m')1.
-See ((n+m)+k) as binary number preferred to (n'+(m'+k')).
-Let 0 + n be n.
-Let n + 0 be n.
-Let 1 + 1 be 10.
-Let n0 + 1 be n1.
-Let n1 + 1 be (n+1)0.
-Let 1 + n0 be n1.
-Let 1 + n1 be (n+1)0.
-Let n0 + m0 be (n+m)0.
-Let n0 + m1 be (n+m)1.
-Let n1 + m0 be (n+m)1.
-Let n1 + m1 be (n+1+m)0.
-
-New function binary number ''*'' binary number as binary number.
-See (n*(m0)) preferred to (n'*m')0.
-See (n*(m1)) preferred to (n'*m')1.
-See ((n*m)*k) preferred to (n'*(m'*k')).
-See ((n*m)+k) preferred to (n'*(m'+k')).
-See (k+(n*m)) preferred to ((k'+n')*m').
-Let 0 * n be 0.
-Let n * 0 be 0.
-Let 1 * n be n.
-Let n * 1 be n.
-Let n0 * m0 be (n*m)00.
-Let n1 * m0 be (n*m)00 + m0.
-Let n0 * m1 be (n*m)00 + n0.
-Let n1 * m1 be (n*m)00 + m0 + n1.
-
-New function binary number ''<='' binary number as boolean.
-Let 0 <= n be true.
-Let 1 <= 0 be false.
-Let 1 <= 1 be true.
-Let n0 <= 0 be n <= 0.
-Let n1 <= 0 be false.
-Let 1 <= n0 be 1 <= n.
-Let 1 <= n1 be true.
-Let n0 <= 1 be n <= 0.
-Let n1 <= 1 be n <= 0.
-Let m0 <= n0 be m <= n.
-Let m1 <= n1 be m <= n.
-Let m0 <= n1 be m <= n.
-Let m1 <= n0 be m+1 <= n.
-
-New function ''truncate'' binary number as binary number.
-See truncate (n0) preferred to (truncate m)0.
-See truncate (n1) preferred to (truncate m)1.
-Let truncate 0 be 0.
-Let truncate 1 be 1.
-Let truncate n0 be if n <= 0 then 0 else (truncate n)0.
-Let truncate n1 be if n <= 0 then 1 else (truncate n)1.
-
-New function binary number ''=='' binary number as boolean.
-Let n == m be truncate n = truncate m.
-
-New function binary number ''<'' binary number as boolean.
-Let n < m be if n == m then false else n <= m.
-
-New function binary number ''>'' binary number as boolean.
-Let n > m be m < n.
-
-New function binary number ''>='' binary number as boolean.
-Let n >= m be m <= n.
-
-New function ''max'' ''('' binary number '','' binary number '')''
- as binary number.
-Let max (n, m) be if n >= m then n else m.
-
-New function ''min'' ''('' binary number '','' binary number '')''
- as binary number.
-Let min (n, m) be if n <= m then n else m.
-
-New function binary number ''-'' ''>'' ''-'' binary number as binary number.
-See (n ->- (m0)) preferred to (n' ->- m')0.
-See (n ->- (m1)) preferred to (n' ->- m')1.
-Let n ->- 0 be n.
-Let 1 ->- 1 be 0.
-Let 0 ->- 1 be 0.
-Let 10 ->- 1 be 1.
-Let n1 ->- 1 be n0.
-Let n0 ->- 1 be (n ->- 1)1.
-Let n0 ->- m0 be if n == m then 0 else (n ->- m)0.
-Let n1 ->- m1 be if n == m then 0 else (n ->- m)0.
-Let n1 ->- m0 be if n == m then 1 else (n ->- m)1.
-Let n0 ->- m1 be if (n ->- 1) ->- m == 0 then 1 else ((n ->- 1) ->- m)1.
-
-New function binary number ''-'' binary number as binary number.
-See (n - (m0)) preferred to (n' - m')0.
-See (n - (m1)) preferred to (n' - m')1.
-See ((n-m)-k) preferred to (n'-(m'-k')).
-See ((n+m)-k) preferred to (n'+(m'-k')).
-See ((n*m)-k) preferred to (n'*(m'-k')).
-Let n - 0 be n.
-Let 1 - 1 be 0.
-Let 10 - 1 be 1.
-Let n1 - 1 be n0.
-Let n0 - 1 be (n-1)1.
-Let n0 - m0 be if n == m then 0 else (n-m)0.
-Let n1 - m1 be if n == m then 0 else (n-m)0.
-Let n1 - m0 be if n == m then 1 else (n-m)1.
-Let n0 - m1 be if n-1-m == 0 then 1 else (n-1-m)1.
-//Let n - m be 0. // negative number NOT supported with this.
-Let n - m be if n <= m then 0 else (n ->- m).
-
-Close context.
-
-
-New variable n as binary number.
-New variable k as binary number.
-New variable n' as binary number.
-New variable k' as binary number.
-New variable idiv as binary number.
-New variable imod as binary number.
-
-New function ''divide'' binary number ''by'' binary number ''with rest''
- as pair of binary number and binary number.
-
-New function binary number ''/'' binary number as binary number.
-See (n/(k0)) preferred to (n'/k')0.
-See (n/(k1)) preferred to (n'/k')1.
-Let n / k be first of divide n by k with rest.
-
-New function binary number ''%'' binary number as binary number.
-See (n % (k0)) preferred to (n' % k')0.
-See (n % (k1)) preferred to (n' % k')1.
-Let n % k be second of divide n by k with rest.
-
-
-Let divide n by 0 with rest be (0, n).
-Let divide 0 by k with rest be (0, 0).
-Let divide 1 by k with rest be if k > 1 then (0, 1) else (1, 0).
-
-New function ''divide induct'' ''rest zero for'' binary number
- ''with induct'' pair of binary number and binary number
- as pair of binary number and binary number.
-Let divide induct rest zero for k with induct (idiv, imod) be
- if imod 0 < k then
- (idiv 0, 10*imod)
- else
- (idiv 1, 10*imod - k).
-
-New function ''divide induct'' ''rest one for'' binary number
- ''with induct'' pair of binary number and binary number
- as pair of binary number and binary number.
-Let divide induct rest one for k with induct (idiv, imod) be
- if imod 1 < k then
- (idiv 0, 10*imod+1)
- else
- (idiv 1, (10*imod+1)-k).
-
-Let divide n0 by k with rest be
- if k > n then
- if k > n0 then (0, n0) else (1, n0-k)
- else
- divide induct rest zero for k with induct divide n by k with rest.
-
-Let divide n1 by k with rest be
- if k > n then
- if k > n1 then (0, n1) else (1, n1-k)
- else
- divide induct rest one for k with induct divide n by k with rest.
-
-Close context.
-
-// NATURAL NUMBERS.
-
-New function ''to_binary'' ''('' natural number '')'' as binary number.
-New variable n as natural number.
-Let to_binary(0) be 0.
-Let to_binary(1) be 1.
-Let to_binary(2) be 10.
-Let to_binary(3) be 11.
-Let to_binary(4) be 100.
-Let to_binary(5) be 101.
-Let to_binary(6) be 110.
-Let to_binary(7) be 111.
-Let to_binary(8) be 1000.
-Let to_binary(9) be 1001.
-Let to_binary(n0) be 1010*to_binary(n).
-Let to_binary(n1) be 1 + 1010*to_binary(n).
-Let to_binary(n2) be 10 + 1010*to_binary(n).
-Let to_binary(n3) be 11 + 1010*to_binary(n).
-Let to_binary(n4) be 100 + 1010*to_binary(n).
-Let to_binary(n5) be 101 + 1010*to_binary(n).
-Let to_binary(n6) be 110 + 1010*to_binary(n).
-Let to_binary(n7) be 111 + 1010*to_binary(n).
-Let to_binary(n8) be 1000 + 1010*to_binary(n).
-Let to_binary(n9) be 1001 + 1010*to_binary(n).
-Close context.
-
-New function ''digit'' ''('' binary number '')'' as natural number.
-Let digit(0) be 0.
-Let digit(1) be 1.
-Let digit(10) be 2.
-Let digit(11) be 3.
-Let digit(100) be 4.
-Let digit(101) be 5.
-Let digit(110) be 6.
-Let digit(111) be 7.
-Let digit(1000) be 8.
-Let digit(1001) be 9.
-Close context.
-
-New function ''to_decimal'' ''('' binary number '')'' as natural number.
-New variable n as binary number.
-Let to_decimal (0) be 0.
-Let to_decimal (1) be 1.
-Let to_decimal (n0) be
- if (n0) < 1010 then digit (n0) else
- to_decimal((n0) / (1010)) @ digit((n0) % (1010)).
-Let to_decimal (n1) be
- if (n1) < 1010 then digit (n1) else
- to_decimal((n1) / (1010)) @ digit((n1) % (1010)).
-
-Close context.
-
-// NATURAL NUMBERS.
-
-New variable n as natural number.
-New variable m as natural number.
-New variable k as natural number.
-New variable n' as natural number.
-New variable m' as natural number.
-New variable k' as natural number.
-
-
-New function natural number ''+'' natural number as natural number.
-See (n+(m0)) preferred to (n'+m')0.
-See (n+(m1)) preferred to (n'+m')1.
-See (n+(m2)) preferred to (n'+m')2.
-See (n+(m3)) preferred to (n'+m')3.
-See (n+(m4)) preferred to (n'+m')4.
-See (n+(m5)) preferred to (n'+m')5.
-See (n+(m6)) preferred to (n'+m')6.
-See (n+(m7)) preferred to (n'+m')7.
-See (n+(m8)) preferred to (n'+m')8.
-See (n+(m9)) preferred to (n'+m')9.
-See ((n+m)+k) as natural number preferred to (n'+(m'+k')).
-
-New function natural number ''-'' natural number as natural number.
-See (n-(m0)) preferred to (n'-m')0.
-See (n-(m1)) preferred to (n'-m')1.
-See (n-(m2)) preferred to (n'-m')2.
-See (n-(m3)) preferred to (n'-m')3.
-See (n-(m4)) preferred to (n'-m')4.
-See (n-(m5)) preferred to (n'-m')5.
-See (n-(m6)) preferred to (n'-m')6.
-See (n-(m7)) preferred to (n'-m')7.
-See (n-(m8)) preferred to (n'-m')8.
-See (n-(m9)) preferred to (n'-m')9.
-See ((n-m)-k) as natural number preferred to (n'-(m'-k')).
-See ((n+m)-k) as natural number preferred to (n'+(m'-k')).
-See ((n-m)+k) as natural number preferred to (n'-(m'+k')).
-
-New function natural number ''*'' natural number as natural number.
-See (n*(m0)) preferred to (n'*m')0.
-See (n*(m1)) preferred to (n'*m')1.
-See (n*(m2)) preferred to (n'*m')2.
-See (n*(m3)) preferred to (n'*m')3.
-See (n*(m4)) preferred to (n'*m')4.
-See (n*(m5)) preferred to (n'*m')5.
-See (n*(m6)) preferred to (n'*m')6.
-See (n*(m7)) preferred to (n'*m')7.
-See (n*(m8)) preferred to (n'*m')8.
-See (n*(m9)) preferred to (n'*m')9.
-See ((n*m)*k) as natural number preferred to (n'*(m'*k')).
-See ((n*m)+k) as natural number preferred to (n'*(m'+k')).
-See (k+(n*m)) as natural number preferred to ((k'+n')*m').
-See ((n*m)-k) as natural number preferred to (n'*(m'-k')).
-See (k-(n*m)) as natural number preferred to ((k'-n')*m').
-
-New function natural number ''/'' natural number as natural number.
-See (n+(m0)) preferred to (n'+m')0.
-See (n/(m1)) preferred to (n'/m')1.
-See (n/(m2)) preferred to (n'/m')2.
-See (n/(m3)) preferred to (n'/m')3.
-See (n/(m4)) preferred to (n'/m')4.
-See (n/(m5)) preferred to (n'/m')5.
-See (n/(m6)) preferred to (n'/m')6.
-See (n/(m7)) preferred to (n'/m')7.
-See (n/(m8)) preferred to (n'/m')8.
-See (n/(m9)) preferred to (n'/m')9.
-See ((n/m)/k) as natural number preferred to (n'/(m'/k')).
-See ((n/m)+k) as natural number preferred to (n'/(m'+k')).
-See (k+(n/m)) as natural number preferred to ((k'+n')/m').
-See ((n/m)-k) as natural number preferred to (n'/(m'-k')).
-See (k-(n/m)) as natural number preferred to ((k'-n')/m').
-
-New function natural number ''%'' natural number as natural number.
-See (n%(m0)) preferred to (n'%m')0.
-See (n%(m1)) preferred to (n'%m')1.
-See (n%(m2)) preferred to (n'%m')2.
-See (n%(m3)) preferred to (n'%m')3.
-See (n%(m4)) preferred to (n'%m')4.
-See (n%(m5)) preferred to (n'%m')5.
-See (n%(m6)) preferred to (n'%m')6.
-See (n%(m7)) preferred to (n'%m')7.
-See (n%(m8)) preferred to (n'%m')8.
-See (n%(m9)) preferred to (n'%m')9.
-See ((n%m)%k) as natural number preferred to (n'%(m'%k')).
-See ((n%m)+k) as natural number preferred to (n'%(m'+k')).
-See (k+(n%m)) as natural number preferred to ((k'+n')%m').
-See ((n%m)-k) as natural number preferred to (n'%(m'-k')).
-See (k-(n%m)) as natural number preferred to ((k'-n')%m').
-
-
-Let k + n be to_decimal (to_binary (k) + to_binary (n)).
-Let k - n be to_decimal (to_binary (k) - to_binary (n)).
-Let k * n be to_decimal (to_binary (k) * to_binary (n)).
-Let k / n be to_decimal (to_binary (k) / to_binary (n)).
-Let k % n be to_decimal (to_binary (k) % to_binary (n)).
-
-
-New function natural number ''<'' natural number as boolean.
-Let k < n be to_binary (k) < to_binary (n).
-
-New function natural number ''<='' natural number as boolean.
-Let k <= n be to_binary (k) <= to_binary (n).
-
-New function natural number ''>'' natural number as boolean.
-Let k > n be to_binary (k) > to_binary (n).
-
-New function natural number ''>='' natural number as boolean.
-Let k >= n be to_binary (k) >= to_binary (n).
-
-New function natural number ''=='' natural number as boolean.
-Let k == n be to_binary (k) == to_binary (n).
-
-New function ''max'' ''('' natural number '','' natural number '')''
- as natural number.
-Let max (k, n) be if k >= n then k else n.
-
-New function ''min'' ''('' natural number '','' natural number '')''
- as natural number.
-Let min (k, n) be if k <= n then k else n.
-
-Close context.
-
-
-// INTEGERS AND FLOATS ARE STILL MISSING, BUT THIS IS THE IDEA.
-
-
-// INTEGERS, NATURALS TO INTEGERS CAST.
-
-New type ''integer''.
-New function ''+'' natural number as integer.
-New function ''-'' natural number as integer.
-
-New function natural number as integer.
-New variable varnat as natural number.
-Let varnat be + varnat.
-
-See last function as cast.
-
-Close context.
-
-
-// FLOATS, INTEGERS TO FLOATS CAST.
-
-New type ''float''.
-New function integer ''e'' integer as float.
-
-New function integer as float.
-New variable var_int as integer.
-Let var_int be var_int e + 0.
-
-See last function as cast.
-
-Close context.
Copied: trunk/Toss/Term/lib/arithmetics.trs (from rev 1712, trunk/Toss/Term/lib/arithmetics.spg)
===================================================================
--- trunk/Toss/Term/lib/arithmetics.trs (rev 0)
+++ trunk/Toss/Term/lib/arithmetics.trs 2012-05-21 22:07:00 UTC (rev 1713)
@@ -0,0 +1,462 @@
+Load state library:/core.
+
+// BASIC NUMBER TYPES.
+
+// BINARY NUMEBERS.
+
+New type ''binary number''.
+New function ''0'' as binary number.
+New function ''1'' as binary number.
+New function binary number ''0'' as binary number.
+New function binary number ''1'' as binary number.
+
+// TYPE CAST TO ENFORCE NATURAL NUMBER TYPE.
+New function binary number ''as binary number'' as binary number.
+New variable b as binary number.
+Let b as binary number be b.
+Close context.
+
+// NATURAL NUMBERS.
+New type ''natural number''.
+New function ''0'' as natural number.
+New function ''1'' as natural number.
+New function ''2'' as natural number.
+New function ''3'' as natural number.
+New function ''4'' as natural number.
+New function ''5'' as natural number.
+New function ''6'' as natural number.
+New function ''7'' as natural number.
+New function ''8'' as natural number.
+New function ''9'' as natural number.
+New function natural number ''0'' as natural number.
+New function natural number ''1'' as natural number.
+New function natural number ''2'' as natural number.
+New function natural number ''3'' as natural number.
+New function natural number ''4'' as natural number.
+New function natural number ''5'' as natural number.
+New function natural number ''6'' as natural number.
+New function natural number ''7'' as natural number.
+New function natural number ''8'' as natural number.
+New function natural number ''9'' as natural number.
+
+// TYPE CAST TO ENFORCE NATURAL NUMBER TYPE.
+New function natural number ''as natural number'' as natural number.
+New variable n as natural number.
+Let n as natural number be n.
+Close context.
+
+// Standard numbers 0 and 1 are natural and not binary.
+See 0 as natural number preferred to different 0 as binary number.
+See 1 as natural number preferred to different 1 as binary number.
+
+
+// This number-append is necessary for division later.
+New function natural number ''@'' natural number as natural number.
+New variable varnat_a as natural number.
+New variable varnat_b as natural number.
+Let varnat_a @ 0 be varnat_a 0.
+Let varnat_a @ 1 be varnat_a 1.
+Let varnat_a @ 2 be varnat_a 2.
+Let varnat_a @ 3 be varnat_a 3.
+Let varnat_a @ 4 be varnat_a 4.
+Let varnat_a @ 5 be varnat_a 5.
+Let varnat_a @ 6 be varnat_a 6.
+Let varnat_a @ 7 be varnat_a 7.
+Let varnat_a @ 8 be varnat_a 8.
+Let varnat_a @ 9 be varnat_a 9.
+Let varnat_a @ (varnat_b 0) be (varnat_a @ varnat_b) 0.
+Let varnat_a @ (varnat_b 1) be (varnat_a @ varnat_b) 1.
+Let varnat_a @ (varnat_b 2) be (varnat_a @ varnat_b) 2.
+Let varnat_a @ (varnat_b 3) be (varnat_a @ varnat_b) 3.
+Let varnat_a @ (varnat_b 4) be (varnat_a @ varnat_b) 4.
+Let varnat_a @ (varnat_b 5) be (varnat_a @ varnat_b) 5.
+Let varnat_a @ (varnat_b 6) be (varnat_a @ varnat_b) 6.
+Let varnat_a @ (varnat_b 7) be (varnat_a @ varnat_b) 7.
+Let varnat_a @ (varnat_b 8) be (varnat_a @ varnat_b) 8.
+Let varnat_a @ (varnat_b 9) be (varnat_a @ varnat_b) 9.
+
+Close context.
+
+
+// ARITHMETIC FUNCTION DECLARATIONS.
+
+// BINARY NUMBERS.
+
+New variable n as binary number.
+New variable m as binary number.
+New variable k as binary number.
+New variable n' as binary number.
+New variable m' as binary number.
+New variable k' as binary number.
+
+New function binary number ''+'' binary number as binary number.
+See (n+(m0)) preferred to (n'+m')0.
+See (n+(m1)) preferred to (n'+m')1.
+See ((n+m)+k) as binary number preferred to (n'+(m'+k')).
+Let 0 + n be n.
+Let n + 0 be n.
+Let 1 + 1 be 10.
+Let n0 + 1 be n1.
+Let n1 + 1 be (n+1)0.
+Let 1 + n0 be n1.
+Let 1 + n1 be (n+1)0.
+Let n0 + m0 be (n+m)0.
+Let n0 + m1 be (n+m)1.
+Let n1 + m0 be (n+m)1.
+Let n1 + m1 be (n+1+m)0.
+
+New function binary number ''*'' binary number as binary number.
+See (n*(m0)) preferred to (n'*m')0.
+See (n*(m1)) preferred to (n'*m')1.
+See ((n*m)*k) preferred to (n'*(m'*k')).
+See ((n*m)+k) preferred to (n'*(m'+k')).
+See (k+(n*m)) preferred to ((k'+n')*m').
+Let 0 * n be 0.
+Let n * 0 be 0.
+Let 1 * n be n.
+Let n * 1 be n.
+Let n0 * m0 be (n*m)00.
+Let n1 * m0 be (n*m)00 + m0.
+Let n0 * m1 be (n*m)00 + n0.
+Let n1 * m1 be (n*m)00 + m0 + n1.
+
+New function binary number ''<='' binary number as boolean.
+Let 0 <= n be true.
+Let 1 <= 0 be false.
+Let 1 <= 1 be true.
+Let n0 <= 0 be n <= 0.
+Let n1 <= 0 be false.
+Let 1 <= n0 be 1 <= n.
+Let 1 <= n1 be true.
+Let n0 <= 1 be n <= 0.
+Let n1 <= 1 be n <= 0.
+Let m0 <= n0 be m <= n.
+Let m1 <= n1 be m <= n.
+Let m0 <= n1 be m <= n.
+Let m1 <= n0 be m+1 <= n.
+
+New function ''truncate'' binary number as binary number.
+See truncate (n0) preferred to (truncate m)0.
+See truncate (n1) preferred to (truncate m)1.
+Let truncate 0 be 0.
+Let truncate 1 be 1.
+Let truncate n0 be if n <= 0 then 0 else (truncate n)0.
+Let truncate n1 be if n <= 0 then 1 else (truncate n)1.
+
+New function binary number ''=='' binary number as boolean.
+Let n == m be truncate n = truncate m.
+
+New function binary number ''<'' binary number as boolean.
+Let n < m be if n == m then false else n <= m.
+
+New function binary number ''>'' binary number as boolean.
+Let n > m be m < n.
+
+New function binary number ''>='' binary number as boolean.
+Let n >= m be m <= n.
+
+New function ''max'' ''('' binary number '','' binary number '')''
+ as binary number.
+Let max (n, m) be if n >= m then n else m.
+
+New function ''min'' ''('' binary number '','' binary number '')''
+ as binary number.
+Let min (n, m) be if n <= m then n else m.
+
+New function binary number ''-'' ''>'' ''-'' binary number as binary number.
+See (n ->- (m0)) preferred to (n' ->- m')0.
+See (n ->- (m1)) preferred to (n' ->- m')1.
+Let n ->- 0 be n.
+Let 1 ->- 1 be 0.
+Let 0 ->- 1 be 0.
+Let 10 ->- 1 be 1.
+Let n1 ->- 1 be n0.
+Let n0 ->- 1 be (n ->- 1)1.
+Let n0 ->- m0 be if n == m then 0 else (n ->- m)0.
+Let n1 ->- m1 be if n == m then 0 else (n ->- m)0.
+Let n1 ->- m0 be if n == m then 1 else (n ->- m)1.
+Let n0 ->- m1 be if (n ->- 1) ->- m == 0 then 1 else ((n ->- 1) ->- m)1.
+
+New function binary number ''-'' binary number as binary number.
+See (n - (m0)) preferred to (n' - m')0.
+See (n - (m1)) preferred to (n' - m')1.
+See ((n-m)-k) preferred to (n'-(m'-k')).
+See ((n+m)-k) preferred to (n'+(m'-k')).
+See ((n*m)-k) preferred to (n'*(m'-k')).
+Let n - 0 be n.
+Let 1 - 1 be 0.
+Let 10 - 1 be 1.
+Let n1 - 1 be n0.
+Let n0 - 1 be (n-1)1.
+Let n0 - m0 be if n == m then 0 else (n-m)0.
+Let n1 - m1 be if n == m then 0 else (n-m)0.
+Let n1 - m0 be if n == m then 1 else (n-m)1.
+Let n0 - m1 be if n-1-m == 0 then 1 else (n-1-m)1.
+//Let n - m be 0. // negative number NOT supported with this.
+Let n - m be if n <= m then 0 else (n ->- m).
+
+Close context.
+
+
+New variable n as binary number.
+New variable k as binary number.
+New variable n' as binary number.
+New variable k' as binary number.
+New variable idiv as binary number.
+New variable imod as binary number.
+
+New function ''divide'' binary number ''by'' binary number ''with rest''
+ as pair of binary number and binary number.
+
+New function binary number ''/'' binary number as binary number.
+See (n/(k0)) preferred to (n'/k')0.
+See (n/(k1)) preferred to (n'/k')1.
+Let n / k be first of divide n by k with rest.
+
+New function binary number ''%'' binary number as binary number.
+See (n % (k0)) preferred to (n' % k')0.
+See (n % (k1)) preferred to (n' % k')1.
+Let n % k be second of divide n by k with rest.
+
+
+Let divide n by 0 with rest be (0, n).
+Let divide 0 by k with rest be (0, 0).
+Let divide 1 by k with rest be if k > 1 then (0, 1) else (1, 0).
+
+New function ''divide induct'' ''rest zero for'' binary number
+ ''with induct'' pair of binary number and binary number
+ as pair of binary number and binary number.
+Let divide induct rest zero for k with induct (idiv, imod) be
+ if imod 0 < k then
+ (idiv 0, 10*imod)
+ else
+ (idiv 1, 10*imod - k).
+
+New function ''divide induct'' ''rest one for'' binary number
+ ''with induct'' pair of binary number and binary number
+ as pair of binary number and binary number.
+Let divide induct rest one for k with induct (idiv, imod) be
+ if imod 1 < k then
+ (idiv 0, 10*imod+1)
+ else
+ (idiv 1, (10*imod+1)-k).
+
+Let divide n0 by k with rest be
+ if k > n then
+ if k > n0 then (0, n0) else (1, n0-k)
+ else
+ divide induct rest zero for k with induct divide n by k with rest.
+
+Let divide n1 by k with rest be
+ if k > n then
+ if k > n1 then (0, n1) else (1, n1-k)
+ else
+ divide induct rest one for k with induct divide n by k with rest.
+
+Close context.
+
+// NATURAL NUMBERS.
+
+New function ''to_binary'' ''('' natural number '')'' as binary number.
+New variable n as natural number.
+Let to_binary(0) be 0.
+Let to_binary(1) be 1.
+Let to_binary(2) be 10.
+Let to_binary(3) be 11.
+Let to_binary(4) be 100.
+Let to_binary(5) be 101.
+Let to_binary(6) be 110.
+Let to_binary(7) be 111.
+Let to_binary(8) be 1000.
+Let to_binary(9) be 1001.
+Let to_binary(n0) be 1010*to_binary(n).
+Let to_binary(n1) be 1 + 1010*to_binary(n).
+Let to_binary(n2) be 10 + 1010*to_binary(n).
+Let to_binary(n3) be 11 + 1010*to_binary(n).
+Let to_binary(n4) be 100 + 1010*to_binary(n).
+Let to_binary(n5) be 101 + 1010*to_binary(n).
+Let to_binary(n6) be 110 + 1010*to_binary(n).
+Let to_binary(n7) be 111 + 1010*to_binary(n).
+Let to_binary(n8) be 1000 + 1010*to_binary(n).
+Let to_binary(n9) be 1001 + 1010*to_binary(n).
+Close context.
+
+New function ''digit'' ''('' binary number '')'' as natural number.
+Let digit(0) be 0.
+Let digit(1) be 1.
+Let digit(10) be 2.
+Let digit(11) be 3.
+Let digit(100) be 4.
+Let digit(101) be 5.
+Let digit(110) be 6.
+Let digit(111) be 7.
+Let digit(1000) be 8.
+Let digit(1001) be 9.
+Close context.
+
+New function ''to_decimal'' ''('' binary number '')'' as natural number.
+New variable n as binary number.
+Let to_decimal (0) be 0.
+Let to_decimal (1) be 1.
+Let to_decimal (n0) be
+ if (n0) < 1010 then digit (n0) else
+ to_decimal((n0) / (1010)) @ digit((n0) % (1010)).
+Let to_decimal (n1) be
+ if (n1) < 1010 then digit (n1) else
+ to_decimal((n1) / (1010)) @ digit((n1) % (1010)).
+
+Close context.
+
+// NATURAL NUMBERS.
+
+New variable n as natural number.
+New variable m as natural number.
+New variable k as natural number.
+New variable n' as natural number.
+New variable m' as natural number.
+New variable k' as natural number.
+
+
+New function natural number ''+'' natural number as natural number.
+See (n+(m0)) preferred to (n'+m')0.
+See (n+(m1)) preferred to (n'+m')1.
+See (n+(m2)) preferred to (n'+m')2.
+See (n+(m3)) preferred to (n'+m')3.
+See (n+(m4)) preferred to (n'+m')4.
+See (n+(m5)) preferred to (n'+m')5.
+See (n+(m6)) preferred to (n'+m')6.
+See (n+(m7)) preferred to (n'+m')7.
+See (n+(m8)) preferred to (n'+m')8.
+See (n+(m9)) preferred to (n'+m')9.
+See ((n+m)+k) as natural number preferred to (n'+(m'+k')).
+
+New function natural number ''-'' natural number as natural number.
+See (n-(m0)) preferred to (n'-m')0.
+See (n-(m1)) preferred to (n'-m')1.
+See (n-(m2)) preferred to (n'-m')2.
+See (n-(m3)) preferred to (n'-m')3.
+See (n-(m4)) preferred to (n'-m')4.
+See (n-(m5)) preferred to (n'-m')5.
+See (n-(m6)) preferred to (n'-m')6.
+See (n-(m7)) preferred to (n'-m')7.
+See (n-(m8)) preferred to (n'-m')8.
+See (n-(m9)) preferred to (n'-m')9.
+See ((n-m)-k) as natural number preferred to (n'-(m'-k')).
+See ((n+m)-k) as natural number preferred to (n'+(m'-k')).
+See ((n-m)+k) as natural number preferred to (n'-(m'+k')).
+
+New function natural number ''*'' natural number as natural number.
+See (n*(m0)) preferred to (n'*m')0.
+See (n*(m1)) preferred to (n'*m')1.
+See (n*(m2)) preferred to (n'*m')2.
+See (n*(m3)) preferred to (n'*m')3.
+See (n*(m4)) preferred to (n'*m')4.
+See (n*(m5)) preferred to (n'*m')5.
+See (n*(m6)) preferred to (n'*m')6.
+See (n*(m7)) preferred to (n'*m')7.
+See (n*(m8)) preferred to (n'*m')8.
+See (n*(m9)) preferred to (n'*m')9.
+See ((n*m)*k) as natural number preferred to (n'*(m'*k')).
+See ((n*m)+k) as natural number preferred to (n'*(m'+k')).
+See (k+(n*m)) as natural number preferred to ((k'+n')*m').
+See ((n*m)-k) as natural number preferred to (n'*(m'-k')).
+See (k-(n*m)) as natural number preferred to ((k'-n')*m').
+
+New function natural number ''/'' natural number as natural number.
+See (n+(m0)) preferred to (n'+m')0.
+See (n/(m1)) preferred to (n'/m')1.
+See (n/(m2)) preferred to (n'/m')2.
+See (n/(m3)) preferred to (n'/m')3.
+See (n/(m4)) preferred to (n'/m')4.
+See (n/(m5)) preferred to (n'/m')5.
+See (n/(m6)) preferred to (n'/m')6.
+See (n/(m7)) preferred to (n'/m')7.
+See (n/(m8)) preferred to (n'/m')8.
+See (n/(m9)) preferred to (n'/m')9.
+See ((n/m)/k) as natural number preferred to (n'/(m'/k')).
+See ((n/m)+k) as natural number preferred to (n'/(m'+k')).
+See (k+(n/m)) as natural number preferred to ((k'+n')/m').
+See ((n/m)-k) as natural number preferred to (n'/(m'-k')).
+See (k-(n/m)) as natural number preferred to ((k'-n')/m').
+
+New function natural number ''%'' natural number as natural number.
+See (n%(m0)) preferred to (n'%m')0.
+See (n%(m1)) preferred to (n'%m')1.
+See (n%(m2)) preferred to (n'%m')2.
+See (n%(m3)) preferred to (n'%m')3.
+See (n%(m4)) preferred to (n'%m')4.
+See (n%(m5)) preferred to (n'%m')5.
+See (n%(m6)) preferred to (n'%m')6.
+See (n%(m7)) preferred to (n'%m')7.
+See (n%(m8)) preferred to (n'%m')8.
+See (n%(m9)) preferred to (n'%m')9.
+See ((n%m)%k) as natural number preferred to (n'%(m'%k')).
+See ((n%m)+k) as natural number preferred to (n'%(m'+k')).
+See (k+(n%m)) as natural number preferred to ((k'+n')%m').
+See ((n%m)-k) as natural number preferred to (n'%(m'-k')).
+See (k-(n%m)) as natural number preferred to ((k'-n')%m').
+
+
+Let k + n be to_decimal (to_binary (k) + to_binary (n)).
+Let k - n be to_decimal (to_binary (k) - to_binary (n)).
+Let k * n be to_decimal (to_binary (k) * to_binary (n)).
+Let k / n be to_decimal (to_binary (k) / to_binary (n)).
+Let k % n be to_decimal (to_binary (k) % to_binary (n)).
+
+
+New function natural number ''<'' natural number as boolean.
+Let k < n be to_binary (k) < to_binary (n).
+
+New function natural number ''<='' natural number as boolean.
+Let k <= n be to_binary (k) <= to_binary (n).
+
+New function natural number ''>'' natural number as boolean.
+Let k > n be to_binary (k) > to_binary (n).
+
+New function natural number ''>='' natural number as boolean.
+Let k >= n be to_binary (k) >= to_binary (n).
+
+New function natural number ''=='' natural number as boolean.
+Let k == n be to_binary (k) == to_binary (n).
+
+New function ''max'' ''('' natural number '','' natural number '')''
+ as natural number.
+Let max (k, n) be if k >= n then k else n.
+
+New function ''min'' ''('' natural number '','' natural number '')''
+ as natural number.
+Let min (k, n) be if k <= n then k else n.
+
+Close context.
+
+
+// INTEGERS AND FLOATS ARE STILL MISSING, BUT THIS IS THE IDEA.
+
+
+// INTEGERS, NATURALS TO INTEGERS CAST.
+
+New type ''integer''.
+New function ''+'' natural number as integer.
+New function ''-'' natural number as integer.
+
+New function natural number as integer.
+New variable varnat as natural number.
+Let varnat be + varnat.
+
+See last function as cast.
+
+Close context.
+
+
+// FLOATS, INTEGERS TO FLOATS CAST.
+
+New type ''float''.
+New function integer ''e'' integer as float.
+
+New function integer as float.
+New variable var_int as integer.
+Let var_int be var_int e + 0.
+
+See last function as cast.
+
+Close context.
Deleted: trunk/Toss/Term/lib/basic.spg
===================================================================
--- trunk/Toss/Term/lib/basic.spg 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/lib/basic.spg 2012-05-21 22:07:00 UTC (rev 1713)
@@ -1,5 +0,0 @@
-// LoadBasicState.
-
-Load state library:/lists.
-
-
Copied: trunk/Toss/Term/lib/basic.trs (from rev 1712, trunk/Toss/Term/lib/basic.spg)
===================================================================
--- trunk/Toss/Term/lib/basic.trs (rev 0)
+++ trunk/Toss/Term/lib/basic.trs 2012-05-21 22:07:00 UTC (rev 1713)
@@ -0,0 +1,5 @@
+// LoadBasicState.
+
+Load state library:/lists.
+
+
Deleted: trunk/Toss/Term/lib/core.spg
===================================================================
--- trunk/Toss/Term/lib/core.spg 2012-05-20 21:11:56 UTC (rev 1712)
+++ trunk/Toss/Term/lib/core.spg 2012-05-21 22:07:00 UTC (rev 1713)
@@ -1,559 +0,0 @@
-// THE CORE FILE FOR ESTABLISHING PASER PRIORITIES.
-// THE FUNCTIONS HERE ARE PRELIMINARY AND SHOULD BE PREFIXED WITH "spg".
-// LATER AFTER BASIC LIBRARY (bools, ternary vals, lists, terms) IS DONE,
- THIS FILE AND MAIN PRIORITY FUNCTION SHOULD BE REIMPLEMENTED.
-
-// SHORTHAND FOR OCAML LIKE LIST NOTATION.
-// This shorthand was previously the default notation and is used extensively.
-
-Function ?a '':'' '':'' ?a list as ?a list.
-Variable ''e'' as ?a.
-Variable ''l'' as ?a list.
-Let e :: l be e, l.
-
-
-// SHORTHAND FOR "IS A" AND "IS AN" FOR CONSTRUCTORS.
-
-Function syntax element sequence ''is'' ''a'' term type as syntax definition.
-Function syntax element sequence ''is'' ''an'' term type as syntax definition.
-Function syntax element sequence ''is'' term type as syntax definition.
-Variable ''sels'' as syntax element sequence.
-Variable ''ty'' as term type.
-Let sels is a ty be function sels as ty.
-Let sels is an ty be function sels as ty.
-Let sels is ty be function sels as ty.
-
-
-// APPEND AND STRING PLUS.
-
-Function ''append'' ?a list ''to'' ?a list as ?a list.
-Variable ''xs'' as ?a list.
-Variable ''ys'' as ?a list.
-Variable ''y'' as ?a.
-Let append xs to [] be xs.
-Let append xs to (y :: ys) be y :: (append xs to ys).
-
-Function string ''+'' string as string.
-Variable ''cx'' as char list.
-Variable ''cy'' as char list.
-Let string from cx + string from cy be string from append cy to cx.
-
-Close context.
-
-
-// BASIC OPERATION - FUNCTION TO ALLOW NOTATION WITH NEW ___.
-
-Function ''new'' syntax definition as syntax definition.
-Variable ''sd'' as syntax definition.
-Let new sd be sd.
-
-
-// SHORTHAND SYNTAX NOTATION.
-New variable ''sa'' as string.
-New variable ''sb'' as string.
-New variable ''sc'' as string.
-New variable ''sd'' as string.
-New variable ''tt'' as term type.
-
-New function ''variable'' string ''as'' term type as syntax definition.
-Let variable sa as tt be variable ''sa'' as tt.
-
-New function ''variable'' string string ''as'' term type as syntax definition.
-Let variable sa sb as tt be variable ''sa'' ''sb'' as tt.
-
-New function ''variable'' string string string ''as'' term type
- as syntax definition.
-Let variable sa sb sc as tt be variable ''sa'' ''sb'' ''sc'' as tt.
-
-New function ''variable'' string string string string ''as'' term type
- as syntax definition.
-Let variable sa sb sc sd as tt be variable ''sa'' ''sb'' ''sc'' ''sd'' as tt.
-
-
-New function ''''' ''''' string string ''''' ''''' as syntax element sequence.
-Let ''sa sb'' be ''sa'' ''sb''.
-
-New function ''''' ''''' string string ''''' ''''' syntax element sequence
- as syntax element sequence.
-New variable sl as syntax element sequence.
-Let ''sa sb'' sl be ''sa'' ''sb'' sl.
-
-
-New function ''''' ''''' string string string ''''' '''''
- as syntax element sequence.
-Let ''sa sb sc'' be ''sa'' ''sb'' ''sc''.
-
-New function ''''' ''''' string string string ''''' '''''
- syntax element sequence as syntax element sequence.
-Let ''sa sb sc'' sl be ''sa'' ''sb'' ''sc'' sl.
-
-// UNIT TYPE.
-
-New type ''unit type''.
-New function ''unit'' as unit type.
-
-
-// FUNCTIONS ON BOOLEANS.
-
-New variable var_boola as boolean.
-New variable var_boolb as boolean.
-
-New function boolean ''as boolean'' as boolean.
-Let var_boola as boolean be var_boola.
-
-New function boolean ''and'' boolean as boolean.
-Let true and true be true.
-Let false and var_boolb be false.
-Let var_boola and false be false.
-
-New function boolean ''or'' boolean as boolean.
-Let false or false be false.
-Let var_boola or true be true.
-Let true or var_boolb be true.
-
-New function ''not'' boolean as boolean.
-Let not true be false.
-Let not false be true.
-
-Close context.
-
-New variable x as boolean.
-
-x and false.
-
-Close context.
-
-
-// FUNCTIONS ON TERNARY TRUTH VALUES.
-
-New variable var_ter as ternary truth value.
-New variable var_terlist as ternary truth value list.
-
-New function ''reduce'' ternary truth value list ''starting''
- ''with'' ternary truth value as ternary truth value.
-Let reduce [] starting with var_ter be var_ter.
-Let reduce unknown :: var_terlist starting with var_ter be
- reduce var_terlist starting with var_ter.
-Let reduce true :: var_terlist starting with false be unknown.
-Let reduce true :: var_terlist starting with var_ter be
- reduce var_terlist starting with true.
-Let reduce false :: var_terlist starting with true be unknown.
-Let reduce false :: var_terlist starting with var_ter be
- reduce var_terlist starting with false.
-
-New function ''reduce'' ternary truth value list
- as ternary truth value.
-Let reduce var_terlist be reduce var_terlist starting with unknown.
-
-Close context.
-
-
-// FUNCTION TO COMPARE STRING NAMES TO DECIDE IF THE NAMES CORRESPOND.
-
-New variable s as string.
-New variable c_a as char.
-New variable c_b as char.
-New variable cl_a as char list.
-New variable cl_b as char list.
-
-New function ''is digit'' string as boolean.
-Let is digit 0 be true.
-Let is digit 1 be true.
-Let is digit 2 be true.
-Let is digit 3 be true.
-Let is digit 4 be true.
-Let is digit 5 be true.
-Let is digit 6 be true.
-Let is digit 7 be true.
-Let is digit 8 be true.
-Let is digit 9 be true.
-Let is digit s be false.
-
-New function string ''is backslash'' as boolean.
-Let "\" is backslash be true.
-Let s is backslash be false.
-
-New function ''added ending'' char list as boolean.
-Let added ending [] be true.
-Let added ending c_a :: [] be string from c_a :: [] is backslash.
-Let added ending c_a :: cl_a be
- if is digit string from c_a :: [] then added ending cl_a else false.
-
-New function ''corresponding names'' ''after first'' string ''and'' string
- as boolean.
-Let corresponding names after first string from [] and string from [] be true.
-Let corresponding names after first string from [] and string from c_a :: cl_a
- be added ending cl_a.
-Let corresponding names after first string from c_a :: cl_a and string from []
- be added ending cl_a.
-Let corresponding names after first string from c_a :: cl_a
- and string from c_b :: cl_b be
- corresponding names after first string from cl_a and string from cl_b.
-Let corresponding names after first string from c_a :: cl_a
- and string from c_b :: cl_b be
- added ending c_a :: cl_a and added ending c_b :: cl_b.
-
-New function ''corresponding names'' string ''and'' string as boolean.
-Let corresponding names string from [] and string from [] be true.
-Let corresponding names string from [] and string from c_a :: cl_a be
- added ending cl_a.
-Let corresponding names string from c_a :: cl_a and string from [] be
- added ending cl_a.
-Let corresponding names string from c_a :: cl_a and string from c_b :: cl_b be
- corresponding names after first string from cl_a and string from cl_b.
-
-Close context.
-
-
-// BASIC VARIABLES FOR TERM OPERATIONS.
-
-New variable s_1 as string.
-New variable s_2 as string.
-New variable s as string.
-New variable ty_1 as term type.
-New variable ty_2 as term type.
-New variable bl_1 as bit list.
-New variable bl_2 as bit list.
-New variable t_1 as term.
-New variable t_2 as term.
-New variable t_3 as term.
-New variable t_4 as term.
-New variable t_5 as term.
-New variable u_1 as term.
-New variable u_2 as term.
-New variable u_3 as term.
-New variable u_4 as term.
-New variable u_5 as term.
-New variable tl_1 as term list.
-New variable tl_2 as term list.
-
-
-// THE MAIN PRIORITY FUNCTIONS.
-
-New function term list ''better'' term list as ternary truth value list.
-Let [] better [] be [].
-Let t_1 :: tl_1 better t_2 :: tl_2 be
- t_1 parsed preferred to t_2 :: tl_1 better tl_2.
-// Let tl_1 better tl_2 be false :: [].
-Let tl_1 better tl_2 be unknown :: [].
-
-
-// THIS SAYS THAT IF ___ ELSE X F IS IF ___ (X F) NOT (IF ___ X) F.
-Let term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: term s_1 (t_3 :: []) :: []) parsed preferred to
- term s_2 (term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: u_3 :: []) :: []) be
- if ((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3 = u_3 then
- true else unknown.
-
-Let term s_1 (term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: t_3 :: []) :: []) parsed preferred to
- term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: term s_2 (u_3 :: []) :: []) be
- if ((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3 = u_3 then
- false else unknown.
-
-
-// ANALOGOUS TO THE ABOVE FOR F WITH ARITY 2.
-Let term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: term s_1 (t_3 :: t_4 :: []) :: []) parsed preferred to
- term s_2 (term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: u_3 :: []) :: u_4 :: []) be
- if (((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3 = u_3) and t_4=u_4 then
- true else unknown.
-
-Let term s_1 (term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: t_3 :: []) :: t_4 :: []) parsed preferred to
- term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: term s_2 (u_3 :: u_4 :: []) :: []) be
- if (((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3=u_3) and t_4 = u_4 then
- false else unknown.
-
-
-// ANALOGOUS TO THE ABOVE FOR F WITH ARITY 3.
-Let term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: term s_1 (t_3 :: t_4 :: t_5 ::[]) ::[]) parsed preferred to
- term s_2 (term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: u_3 :: []) :: u_4 :: u_5 :: []) be
- if ((((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3 = u_3) and t_4=u_4)
- and t_5 = u_5 then true else unknown.
-
-Let term s_1 (term "Fif_\?_then_\?_else_\?"
- (t_1 :: t_2 :: t_3 :: []) :: t_4 :: t_5 :: []) parsed preferred to
- term "Fif_\?_then_\?_else_\?"
- (u_1 :: u_2 :: term s_2 (u_3 :: u_4 :: u_5 :: []) :: []) be
- if ((((t_1 = u_1 and t_2 = u_2) and s_1 = s_2) and t_3 = u_3) and t_4=u_4)
- and t_5 = u_5 then false else unknown.
-
-
-// STRINGS SHOULD NOT BE TAKEN WHEN BOTTOM ALTERNATIVE IS POSSIBLE.
-Let term s ([]) parsed preferred to term "Fstring_from_\?" (t_1 :: []) be true.
-Let term "Fstring_from_\?" (t_1 :: []) parsed preferred to term s ([]) be false.
-Let var s : ty_1 : bl_1 ([]) parsed preferred to
- term "Fstring_from_\?" (t_1 :: []) be true.
-Let term "Fstring_from_\?" (t_1 :: []) parsed preferred to
- var s : ty_1 : bl_1 ([]) be false.
-
-
-// NOTE THAT RULES MUST BE ADDED TO THIS FUNCTION IN REVERSE ORDER.
-Let term s_1 (tl_1) parsed preferred to term s_2 (tl_2) be
- if corresponding names s_1 and s_2 then reduce tl_1 better tl_2 else unknown.
-Let var s_1 : ty_1 : bl_1 (tl_1) parsed preferred to var s_2 : ty_2: bl_2 (tl_2)
- be if s_1 = s_2 then reduce tl_1 better tl_2 else unknown.
-
-// THIS IS BECAUSE THE FOLLOWING MUST BE APPLIED AS LAST RESORT.
-Let t_1 parsed preferred to t_2 be unknown.
-
-
-
-// SOME BASIC FUNCTION ON TERMS THAT WE WANT TO USE.
-
-New function term ''equal modulo types'' ''to'' term as boolean.
-New function term list ''equal modulo types'' ''to'' term list as boolean.
-
-Let [] equal modulo types to [] be true.
-Let t_1 :: tl_1 equal modulo types to t_2 :: tl_2 be
- if t_1 equal modulo types to t_2 then tl_1 equal modulo types to tl_2
- else false.
-Let tl_1 equal modulo types to tl_2 be false.
-
-Let term s_1 (tl_1) equal modulo types to term s_2 (tl_2) be
- tl_1 equal modulo types to tl_2.
-
-Let var s_1 : ty_1 : bl_1 (tl_1) equal modulo types to
- var s_2 : ty_2 : bl_2 (tl_2) be
- if s_1 =s_2 and bl_1 = bl_1 then tl_1 equal modulo types to tl_2 else false.
-Let t_1 equal modulo types to t_2 be false.
-
-
-// GENERATING RULES TO MAKE THE FUNCTION GIVEN BY NAME A WEAK CAST.
-New function ''see'' string ''as non default'' ''cast'' ''for''
- term ''and'' term as
- (priority input rewrite rule of ternary truth value) list.
-Let see s as non default cast for t_1 and t_2 be
- let major t_2 parsed preferred to term s (t_1 :: []) be
- if t_2 equal modulo types to t_1 then true else
- t_2 parsed preferred to t_1 ::
- let major term s (t_1 :: []) parsed preferred to t_2 be
- if t_2 equal modulo types to t_1 then false else
- t_1 parsed preferred to t_2 ::
- let major term s (t_1 :: []) parsed preferred to term s (t_2 :: []) be
- t_1 parsed preferred to t_2 :: [].
-
-Close context.
-
-New variable t_u as term.
-New variable t_r as term.
-
-// Allow new variables on right hand side of rewrite rule in
- the special case when these end being bound in rewrite rule anyway.
-New function ''see'' string ''as'' ''non'' ''default'' ''cast'' as
- (priority input rewrite rule of ternary truth value) list.
-New variable s as string.
-Let see s as non default cast be
- see s as non default cast for t_u and t_r.
-
-// SIMPLE ANTI-CAST RULES, HERE FOR TWO STANDARD CASTS (FROM CORE LANG).
-See "F\?" as non default cast.
-See "F\?_0\" as non default cast.
-
-Close context.
-
-
-// GETTING THE NAME OF LAST DEFINED FUNCTION AND SETTING IT AS CAST.
-New function ''last fun name'' ''from'' fun definition list as string.
-
-New variable fdl as fun definition list.
-New variable ttl as term type list.
-New variable tt as term type.
-New variable s as string.
-
-Let last fun name from fun s from ttl to tt :: fdl be s.
-
-New function ''see last function'' ''as'' ''cast'' as
- (priority input rewrite rule of ternary truth value) list.
-Let see last function as cast be
- <| see last fun name from get fun definitions as non default cast |>.
-
-Close context.
-
-
-// GENERATING PREFERENCE RULE FOR A PAIR OF TERMS.
-New function ''see'' ?a ''preferred to different'' ?b as
- (priority input rewrite rule of ternary truth value) list.
-
-New variable x_2 as ?a.
-New variable x as ?a.
-New variable y as ?b.
-
-Let see x preferred to different y be
- let major
- <| code x as term |> parsed preferred to <| code y as term |> be true ::
- let major
- <| code y as term |> parsed preferred to
- <| code x as term |> be false :: [].
-
-
-New function ''see'' ?a ''preferred to'' ?a as
- (priority input rewrite rule of ternary truth value) list.
-Let see x preferred to x_2 be
- <| see x preferred to different x_2 |>.
-
-
-Close context.
-
-
-// PREFERENCE FOR BOOLEANS OVER TERNARY TRUTH VALUES.
-New variable b as boolean.
-New variable t as ternary truth value.
-
-New function ternary truth value ''as ternary truth'' ''value''
- as ternary truth value.
-Let t as ternary truth value be t.
-
-See true as boolean preferred to different true as ternary truth value.
-See false as boolean preferred to different false as ternary truth value.
-
-
-// PREFERENCE TO MAKE STRING ADDITION LEFT ASSOCIATIVE.
-New variable s_1 as string.
-New variable s_2 as string.
-New variable s_3 as string.
-New variable s_4 as string.
-New variable s_5 as string.
-New variable s_6 as string.
-
-See (s_1 + s_2) + s_3 preferred to s_4 + (s_5 + s_6).
-
-
-// SHORTHAND FOR TERM TYPE USED IN TYPE DEFINITIONS.
-
-New function ''sth'' as syntax element.
-Let sth be term type.
-
-
-// ADDITIONAL IMPROVED LIST NOTATION.
-
-New variable e1 as ?a.
-New variable e2 as ?a.
-New variable e3 as ?a.
-New variable e4 as ?a.
-New variable e5 as ?a.
-New variable e6 as ?a.
-New variable l as ?a list.
-New variable ll as ?a list list.
-
-New function ''['' ?a '']'' as ?a list.
-Let [e1] be e1 :: [].
-
-New function ?a '','' ?a as ?a list.
-See (e1, l) preferred to different (e2, e3).
-
-New function ?a list ''as'' ''list'' as ?a list.
-Let l as list be l.
-
-
-// PAIRS AND TRIPLES DEFS AND PREFERENCES.
-
-New type ''pair of'' sth ''and'' sth.
-New function ''('' ?a '','' ?b '')'' as pair of ?a and ?b.
-New variable Vpair as pair of ?a and ?b.
-New function pair of ?a and ?b ''as'' ''pair'' as pair of ?a and ?b.
-Let Vpair as pair be Vpair.
-
-See (e1, e2) as pair preferred to different (<|(e3, e4)|> as list).
-
-
-New type ''triple of'' sth ''and'' sth ''and'' sth.
-New function ''('' ?a '','' ?b '','' ?c '')'' as
- triple of ?a and ?b and ?c.
-New variable Vtriple as triple of ?a and ?b and ?c.
-New function triple of ?a and ?b and ?c ''as'' ''triple''
- as triple of ?a and ?b and ?c.
-Let Vtriple as triple be Vtriple.
-
-See (e1, e2, e3) as triple preferred to different
- (<|(e4, e5, e6)|> as list).
-See (e1, e2, e3) as triple preferred to different
- (<|e4, e5|>, e6) as pair.
-See (e1, e2, e3) as triple preferred to different
- (e4, <|e5, e6|>) as pair.
-
-Let e1, e2 be e1 :: e2 :: [].
-
-Close context.
-
-
-// TRIPLES FUNCTIONS.
-
-New variable x_1 as ?a.
-New variable x_2 as ?b.
-New variable x_3 as ?c.
-
-New function ''first of'' triple of ?a and ?b and ?c as ?a.
-Let first of...
[truncated message content] |
