(language) Nil is the type name for nil

Signed-off-by: Jerome Simeon <[email protected]>
accordproject · Aug 9, 2018 · edc2b06 · edc2b06
1 parent 4a00d24
commit edc2b06
Show file tree

Hide file tree

Showing 13 changed files with 16 additions and 16 deletions.
diff --git a/examples/helloworldstate/logic.ergo b/examples/helloworldstate/logic.ergo
@@ -24,7 +24,7 @@ contract HelloWorldState over TemplateModel {
     }
   }
 
-  clause init(request : MyRequest) : Nothing {
+  clause init(request : MyRequest) {
     set state State{
       counter: 0.0
     };

diff --git a/extraction/src/ErgoParser.mly b/extraction/src/ErgoParser.mly
@@ -205,7 +205,7 @@ clause:
 
 outtype:
 |
-  { ErgoCompiler.ergo_type_nothing (mk_provenance $startpos $endpos) }
+  { ErgoCompiler.ergo_type_nil (mk_provenance $startpos $endpos) }
 | COLON out = paramtype
   { out }
 
@@ -531,7 +531,7 @@ tname:
       | "Long" -> ErgoCompiler.ergo_type_long (mk_provenance $startpos $endpos)
       | "Integer" -> ErgoCompiler.ergo_type_integer (mk_provenance $startpos $endpos)
       | "DateTime" -> ErgoCompiler.ergo_type_dateTime (mk_provenance $startpos $endpos)
-      | "Nothing" -> ErgoCompiler.ergo_type_nothing (mk_provenance $startpos $endpos)
+      | "Nil" -> ErgoCompiler.ergo_type_nil (mk_provenance $startpos $endpos)
       | "Any" -> ErgoCompiler.ergo_type_any (mk_provenance $startpos $endpos)
       | _ ->
           ErgoCompiler.ergo_type_class_ref

diff --git a/mechanization/Common/Types/ErgoType.v b/mechanization/Common/Types/ErgoType.v
@@ -29,7 +29,7 @@ Section ErgoType.
 
     Inductive ergo_type :=
     | ErgoTypeAny : A -> ergo_type                               (**r any type *)
-    | ErgoTypeNothing : A -> ergo_type                           (**r nothing type *)
+    | ErgoTypeNil : A -> ergo_type                               (**r unit type *)
     | ErgoTypeBoolean : A -> ergo_type                           (**r bool atomic type *)
     | ErgoTypeString : A -> ergo_type                            (**r string atomic type *)
     | ErgoTypeDouble : A -> ergo_type                            (**r double atomic type *)
@@ -46,7 +46,7 @@ Section ErgoType.
     Definition type_annot (et:ergo_type) : A :=
       match et with
       | ErgoTypeAny a => a
-      | ErgoTypeNothing a => a
+      | ErgoTypeNil a => a
       | ErgoTypeBoolean a => a
       | ErgoTypeString a => a
       | ErgoTypeDouble a => a

diff --git a/mechanization/Common/Types/ErgoTypetoErgoCType.v b/mechanization/Common/Types/ErgoTypetoErgoCType.v
@@ -104,7 +104,7 @@ Section ErgoTypetoErgoCType.
   Fixpoint ergo_type_to_ergoc_type (t:laergo_type) : ergoc_type :=
     match t with
     | ErgoTypeAny _ => ttop
-    | ErgoTypeNothing _ => tunit
+    | ErgoTypeNil _ => tunit
     | ErgoTypeBoolean _ => tbool
     | ErgoTypeString _ => tstring
     | ErgoTypeDouble _ => tfloat

diff --git a/mechanization/Common/Utils/DataTypes.v b/mechanization/Common/Utils/DataTypes.v
@@ -140,7 +140,7 @@ Section DataTypes.
       match t with
       | Bottom₀ => "Nothing"%string
       | Top₀ => "Any"%string
-      | Unit₀ => "Unit"%string
+      | Unit₀ => "Nil"%string
       | Nat₀ => "Integer"%string
       | Float₀ => "Double"%string
       | Bool₀ => "Boolean"%string

diff --git a/mechanization/Compiler/ErgoCompiler.v b/mechanization/Compiler/ErgoCompiler.v
@@ -125,8 +125,8 @@ Module ErgoCompiler.
 
   Definition ergo_type_any prov : ergo_type
     := ErgoType.ErgoTypeAny prov.
-  Definition ergo_type_nothing prov : ergo_type
-    := ErgoType.ErgoTypeNothing prov.
+  Definition ergo_type_nil prov : ergo_type
+    := ErgoType.ErgoTypeNil prov.
   Definition ergo_type_boolean prov : ergo_type
     := ErgoType.ErgoTypeBoolean prov.
   Definition ergo_type_string prov : ergo_type

diff --git a/mechanization/Ergo/Lang/ErgoExpand.v b/mechanization/Ergo/Lang/ErgoExpand.v
@@ -131,7 +131,7 @@ Section ErgoExpand.
              (mkErgoTypeSignature
                 prov
                 (("request"%string, ErgoTypeClassRef prov default_request_absolute_name)::nil)
-                (ErgoTypeNothing prov)
+                (ErgoTypeNil prov)
                 None
                 (Some (ErgoTypeClassRef prov default_emits_absolute_name)))
              (Some init_body).

diff --git a/mechanization/ErgoC/Lang/ErgoCStdlib.v b/mechanization/ErgoC/Lang/ErgoCStdlib.v
@@ -31,7 +31,7 @@ Section ErgoCStdlib.
   Definition empty_sigc prov (params:list string) :=
     mkSigC
       (List.map (fun x => (x,ErgoTypeAny prov)) params)
-      (ErgoTypeNothing prov).
+      (ErgoTypeNil prov).
 
   Definition mk_naked_closure prov (params:list string) (body:ergoc_expr) : ergoc_function :=
     mkFuncC

diff --git a/mechanization/Translation/ErgoNameResolve.v b/mechanization/Translation/ErgoNameResolve.v
@@ -129,7 +129,7 @@ Section ErgoNameResolution.
              (t:lrergo_type) : eresult laergo_type :=
       match t with
       | ErgoTypeAny prov => esuccess (ErgoTypeAny prov)
-      | ErgoTypeNothing prov => esuccess (ErgoTypeNothing prov)
+      | ErgoTypeNil prov => esuccess (ErgoTypeNil prov)
       | ErgoTypeBoolean prov => esuccess (ErgoTypeBoolean prov)
       | ErgoTypeString prov => esuccess (ErgoTypeString prov)
       | ErgoTypeDouble prov => esuccess (ErgoTypeDouble prov)

diff --git a/mechanization/Translation/ErgotoErgoC.v b/mechanization/Translation/ErgotoErgoC.v
@@ -297,7 +297,7 @@ Section ErgotoErgoC.
         then
           ((current_time, (ErgoTypeDateTime prov))
              ::(this_contract, tem)
-             ::(this_state, ErgoTypeNothing prov)
+             ::(this_state, ErgoTypeNil prov)
              ::(this_emit, ErgoTypeArray prov emit_type)
              ::c.(clause_sig).(type_signature_params))
         else

diff --git a/packages/ergo-cli/lib/ergoc-lib.js b/packages/ergo-cli/lib/ergoc-lib.js
diff --git a/packages/ergo-cli/lib/ergotop.js b/packages/ergo-cli/lib/ergotop.js
diff --git a/packages/ergo-compiler/lib/ergo-core.js b/packages/ergo-compiler/lib/ergo-core.js