change naming convention of files -- back to lisp-case

TODO.md

@@ -1,2 +1,18 @@
+change naming convention -- back to lisp-case -- use -t for types
+
+ambr @Type @type-t
+ambr Nat nat-t
+ambr List list-t
+ambr DiffList diff-list-t
+ambr Trivial trivial-t
+
+ambs @Type
+ambs Nat
+ambs List
+ambs DiffList
+
+add define- to statement keywords
+
+drop @ from builtin
 static import should handled by an extra pass -- instead of injecting a `Loader` to `Mod`
 `NodeId` vs `Node` -- instead of `Node` vs `NodeEntry` -- the same for `HalfEdge`

examples/builtin/run-only-top-port.i

@@ -1,4 +1,4 @@
-require "../datatypes/Nat.i"
+require "../datatypes/nat.i"
 
 one one add
 one one add

examples/datatypes/Bin.i → examples/datatypes/bin.i

@@ -163,7 +163,7 @@ end
 import
   Nat, zero, add1,
   natErase, natDup
-from "./Nat.i"
+from "./nat.i"
 
 node natDouble
   Nat :target!

examples/datatypes/Bin.test.i → examples/datatypes/bin.test.i

@@ -1,4 +1,4 @@
-require "./Bin.i"
+require "./bin.i"
 
 bend b1 b1 b0                                // = 0b110 = 4+2 = 6
 zero add1 add1 add1 add1 add1 add1 add1 ntob // 8 Nat -> 8 Bin

examples/datatypes/DiffList.i → examples/datatypes/diff-list.i

@@ -1,4 +1,4 @@
-require "List.i"
+require "list.i"
 
 // Concatenation of lists is performed in linear time
 // with respect to its first argument.

examples/datatypes/DiffList.test.i → examples/datatypes/diff-list.test.i

@@ -1,5 +1,5 @@
-require "DiffList.i"
-require "Trivial.i"
+require "diff-list.i"
+require "trivial.i"
 
 claim oneTwoSoles -- Trivial DiffList end
 

examples/datatypes/List.test.i → examples/datatypes/list.test.i

@@ -1,5 +1,5 @@
-require "List.i"
-require "Trivial.i"
+require "list.i"
+require "trivial.i"
 
 claim sixSoles -- Trivial List end
 

examples/datatypes/Nat.test.i → examples/datatypes/nat.test.i

@@ -1,6 +1,6 @@
-require "Nat.i"
-require "Nat.i"
-require "Nat.i" // Multiple `require` is fine.
+require "nat.i"
+require "nat.i"
+require "nat.i" // multiple `require` is fine.
 
 zero zero add @inspect @run @inspect
 two @inspect @run @inspect

examples/module/define-rule-for-non-own-node.error.i

@@ -1,4 +1,4 @@
-import Nat, zero, add1, add from "../datatypes/Nat.i"
+import Nat, zero, add1, add from "../datatypes/nat.i"
 
 rule zero add
   (add)-addend

examples/module/define-rule-for-non-own-node.error.i.err

@@ -1,14 +1,14 @@
 [checkRuleIsAboutOwnNode] To define a rule, one of the node must be owned by this module.
 
   loading module url: examples/module/define-rule-for-non-own-node.error.i
-  first node module url: examples/datatypes/Nat.i
-  second node module url: examples/datatypes/Nat.i
+  first node module url: examples/datatypes/nat.i
+  second node module url: examples/datatypes/nat.i
 
 [DefineRule.execute] I fail to define rule.
 
   rule nodes: zero add
 
-  1 |import Nat, zero, add1, add from "../datatypes/Nat.i"
+  1 |import Nat, zero, add1, add from "../datatypes/nat.i"
   2 |
   3 |rule zero add
   4 |  (add)-addend

examples/module/import.i

@@ -1,3 +1,3 @@
-import zero, one, add from "../datatypes/Nat.i"
+import zero, one, add from "../datatypes/nat.i"
 
 zero one add @inspect @run @inspect

examples/module/require-already-defined.error.i

@@ -1,3 +1,3 @@
 type Nat -- @Type end
 
-require "../datatypes/Nat.i"
+require "../datatypes/nat.i"

examples/module/require-already-defined.error.i.err

@@ -4,9 +4,9 @@
 
 [Require.execute] I fail to require module.
 
-  path: "../datatypes/Nat.i"
+  path: "../datatypes/nat.i"
 
  1 |type Nat -- @Type end
  2 |
- 3 |require "../datatypes/Nat.i"
+ 3 |require "../datatypes/nat.i"
  4 |

examples/module/require.i

@@ -1,3 +1,3 @@
-require "../datatypes/Nat.i"
+require "../datatypes/nat.i"
 
 zero one add @inspect @run @inspect