"Interface" instead of "interface:", and "Rec" can be used in type definition.

1 files changed, 86 insertions, 265 deletions

diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux
index 389635abc..c87b674f0 100644
--- a/stdlib/source/library/lux.lux
+++ b/stdlib/source/library/lux.lux
@@ -138,19 +138,20 @@
  ["None" "Some"]
  #1)
 
-... (type: .public #rec Type
-...   (#Primitive Text (List Type))
-...   (#Sum Type Type)
-...   (#Product Type Type)
-...   (#Function Type Type)
-...   (#Parameter Nat)
-...   (#Var Nat)
-...   (#Ex Nat)
-...   (#UnivQ (List Type) Type)
-...   (#ExQ (List Type) Type)
-...   (#Apply Type Type)
-...   (#Named Name Type)
-...   )
+... (type: .public Type
+...   (Rec Type
+...     (Variant
+...      (#Primitive Text (List Type))
+...      (#Sum Type Type)
+...      (#Product Type Type)
+...      (#Function Type Type)
+...      (#Parameter Nat)
+...      (#Var Nat)
+...      (#Ex Nat)
+...      (#UnivQ (List Type) Type)
+...      (#ExQ (List Type) Type)
+...      (#Apply Type Type)
+...      (#Named Name Type))))
 ("lux def type tagged" Type
  (9 #1 ["library/lux" "Type"]
     ({Type
@@ -194,9 +195,7 @@
        ("lux type check type" (9 #0 Type List)))}
      ("lux type check type" (9 #0 (4 #0 1) (4 #0 0)))))
  [dummy_location
-  (9 #1 (#Item [[dummy_location (7 #0 ["library/lux" "type_rec?"])]
-                [dummy_location (0 #0 #1)]]
-               #End))]
+  (9 #1 #End)]
  ["Primitive" "Sum" "Product" "Function" "Parameter" "Var" "Ex" "UnivQ" "ExQ" "Apply" "Named"]
  #1)
 
@@ -1399,11 +1398,12 @@
            (failure "Wrong syntax for $_")}
           tokens))
 
-... (interface: (Monad m)
-...   (: (All [a] (-> a (m a)))
-...      in)
-...   (: (All [a b] (-> (-> a (m b)) (m a) (m b)))
-...      then))
+... (type: (Monad m)
+...   (Interface
+...    (: (All [a] (-> a (m a)))
+...       in)
+...    (: (All [a b] (-> (-> a (m b)) (m a) (m b)))
+...       then)))
 ("lux def type tagged" Monad
  (#Named ["library/lux" "Monad"]
          (All [m]
@@ -2404,17 +2404,6 @@
                    (local_identifier$ ($_ text\composite "__gensym__" prefix (nat\encoded seed))))}
           state))
 
-(macro:' .public (Rec tokens)
-         ({(#Item [_ (#Identifier "" name)] (#Item body #End))
-           (let' [body' (|> body
-                            nested_quantification
-                            (with_replacements (list [name (` (#.Apply (~ (type_parameter 1)) (~ (type_parameter 0))))])))]
-                 (in_meta (list (` (#.Apply .Nothing (#.UnivQ #.End (~ body')))))))
-           
-           _
-           (failure "Wrong syntax for Rec")}
-          tokens))
-
 (macro:' .public (exec tokens)
          (list)
          ({(#Item value actions)
@@ -3367,7 +3356,7 @@
     (#Some [tokens' [slot type]])
 
     _
-    #.None))
+    #None))
 
 (def: un_paired
   (-> (List [Code Code]) (List Code))
@@ -3395,21 +3384,11 @@
     _
     (failure "Wrong syntax for Record")))
 
-(def: (recP tokens)
-  (-> (List Code) [(List Code) Bit])
-  (case tokens
-    (^ (list& [_ (#Tag ["" "rec"])] tokens'))
-    [tokens' #1]
-
-    _
-    [tokens #0]))
-
 (def: (typeP tokens)
-  (-> (List Code) (Maybe [Code Bit Text (List Text) (List [Code Code]) Code]))
+  (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) Code]))
   (|> (do maybe_monad
         [% (anyP tokens)
          .let' [[tokens export_policy] %]
-         .let' [[tokens rec?] (recP tokens)]
          % (local_declarationP tokens)
          .let' [[tokens [name parameters]] %]
          % (annotationsP tokens)
@@ -3417,42 +3396,35 @@
          % (anyP tokens)
          .let' [[tokens definition] %]
          _ (endP tokens)]
-        (in [export_policy rec? name parameters annotations definition]))
-      ... (^ (list _export_policy _rec _declaration _annotations _body))
+        (in [export_policy name parameters annotations definition]))
       ... (^ (list _export_policy _declaration _annotations _body))
       (maybe\else' (do maybe_monad
-                     [.let' [[tokens rec?] (recP tokens)]
-                      % (local_declarationP tokens)
+                     [% (local_declarationP tokens)
                       .let' [[tokens [name parameters]] %]
                       % (annotationsP tokens)
                       .let' [[tokens annotations] %]
                       % (anyP tokens)
                       .let' [[tokens definition] %]
                       _ (endP tokens)]
-                     (in [(` ..private) rec? name parameters annotations definition])))
-      ... (^ (list _rec _declaration _annotations _body))
+                     (in [(` ..private) name parameters annotations definition])))
       ... (^ (list _declaration _annotations _body))
       (maybe\else' (do maybe_monad
-                     [.let' [[tokens rec?] (recP tokens)]
-                      % (local_declarationP tokens)
+                     [% (local_declarationP tokens)
                       .let' [[tokens [name parameters]] %]
                       % (anyP tokens)
                       .let' [[tokens definition] %]
                       _ (endP tokens)]
-                     (in [(` ..private) rec? name parameters #End definition])))
-      ... (^ (list _rec _declaration _body))
+                     (in [(` ..private) name parameters #End definition])))
       ... (^ (list _declaration _body))
       (maybe\else' (do maybe_monad
                      [% (anyP tokens)
                       .let' [[tokens export_policy] %]
-                      .let' [[tokens rec?] (recP tokens)]
                       % (local_declarationP tokens)
                       .let' [[tokens [name parameters]] %]
                       % (anyP tokens)
                       .let' [[tokens definition] %]
                       _ (endP tokens)]
-                     (in [export_policy rec? name parameters #End definition])))
-      ... (^ (list _export_policy _rec _declaration _body))
+                     (in [export_policy name parameters #End definition])))
       ... (^ (list _export_policy _declaration _body))
       ))
 
@@ -3491,32 +3463,20 @@
 
 (macro: .public (type: tokens)
   (case (typeP tokens)
-    (#Some [export_policy rec? name args meta type_codes])
+    (#Some [export_policy name args meta type_codes])
     (do meta_monad
       [type+tags?? (..type_declaration type_codes)
        module_name current_module_name
        .let' [type_name (local_identifier$ name)
               [type tags??] type+tags??
               type' (: (Maybe Code)
-                       (if rec?
-                         (if (empty? args)
-                           (let [g!param (local_identifier$ "")
-                                 prime_name (local_identifier$ name)
-                                 type+ (with_replacements (list [name (` ((~ prime_name) .Nothing))])
-                                         type)]
-                             (#Some (` ((All (~ prime_name) [(~ g!param)] (~ type+))
-                                        .Nothing))))
-                           #None)
-                         (case args
-                           #End
-                           (#Some type)
+                       (case args
+                         #End
+                         (#Some type)
 
-                           _
-                           (#Some (` (.All (~ type_name) [(~+ (list\each local_identifier$ args))] (~ type)))))))
-              total_meta (let [meta (definition_annotations meta)
-                               meta (if rec?
-                                      (` (#.Item (~ (flag_meta "type_rec?")) (~ meta)))
-                                      meta)]
+                         _
+                         (#Some (` (.All (~ type_name) [(~+ (list\each local_identifier$ args))] (~ type))))))
+              total_meta (let [meta (definition_annotations meta)]
                            (` [(~ location_code)
                                (#.Record (~ meta))]))]]
       (case type'
@@ -3545,64 +3505,6 @@
     #None
     (failure "Wrong syntax for type:")))
 
-(def:' .private (interfaceP tokens)
-       (-> (List Code) (Maybe [Code Text (List Text) (List [Code Code]) (List Code)]))
-       (|> (do maybe_monad
-             [% (declarationP tokens)
-              .let' [[tokens [export_policy name parameters]] %]
-              % (annotationsP tokens)
-              .let' [[tokens annotations] %]]
-             (in [export_policy name parameters annotations tokens]))
-           ... (^ (list _export_policy _declaration _annotations _body))
-           ... (^ (list _declaration _annotations _body))
-           (maybe\else' (do maybe_monad
-                          [% (local_declarationP tokens)
-                           .let' [[tokens [name parameters]] %]]
-                          (in [(` ..private) name parameters #End tokens])))
-           ... (^ (list _declaration _body))
-           (maybe\else' (do maybe_monad
-                          [% (declarationP tokens)
-                           .let' [[tokens [export_policy name parameters]] %]]
-                          (in [export_policy name parameters #End tokens])))
-           ... (^ (list _export_policy _declaration _body))
-           ))
-
-(macro: .public (interface: tokens)
-  (case (interfaceP tokens)
-    (#Some [export_policy name args annotations methods])
-    (do meta_monad
-      [methods' (monad\each meta_monad expansion methods)
-       members (: (Meta (List [Text Code]))
-                  (monad\each meta_monad
-                              (: (-> Code (Meta [Text Code]))
-                                 (function (_ token)
-                                   (case token
-                                     (^ [_ (#Form (list [_ (#Text "lux type check")] type [_ (#Identifier ["" name])]))])
-                                     (in [name type])
-
-                                     _
-                                     (failure "Interfaces require typed members!"))))
-                              (list\conjoint methods')))
-       .let [def_name (local_identifier$ name)
-             interface_type (` (..Record
-                                (~ (record$ (list\each (: (-> [Text Code] [Code Code])
-                                                          (function (_ [module_name m_type])
-                                                            [(local_tag$ module_name) m_type]))
-                                                       members)))))
-             usage (case args
-                     #End
-                     def_name
-
-                     _
-                     (` ((~ def_name) (~+ (list\each local_identifier$ args)))))]]
-      (in_meta (list (` (..type: (~ export_policy)
-                          (~ usage)
-                          (~ (record$ annotations))
-                          (~ interface_type))))))
-
-    #None
-    (failure "Wrong syntax for interface:")))
-
 (template [<name> <to>]
   [(def: .public (<name> value)
      (-> (I64 Any) <to>)
@@ -3926,7 +3828,7 @@
                                                             code\encoded))))
     ))
 
-(def: (only p xs)
+(def: (list\only p xs)
   (All [a] (-> (-> a Bit) (List a) (List a)))
   (case xs
     #End
@@ -3934,8 +3836,8 @@
 
     (#Item x xs')
     (if (p x)
-      (#Item x (only p xs'))
-      (only p xs'))))
+      (#Item x (list\only p xs'))
+      (list\only p xs'))))
 
 (def: (is_member? cases name)
   (-> (List Text) Text Bit)
@@ -4377,7 +4279,7 @@
              (do meta_monad
                [*defs (exported_definitions module_name)
                 _ (test_referrals module_name *defs _defs)]
-               (in (..only (|>> (is_member? _defs) not) *defs)))
+               (in (..list\only (|>> (is_member? _defs) not) *defs)))
 
              #Ignore
              (in (list))
@@ -4643,47 +4545,6 @@
     _
     (failure "Wrong syntax for ^template")))
 
-(def: (baseline_column code)
-  (-> Code Nat)
-  (case code
-    (^template [<tag>]
-      [[[_ _ column] (<tag> _)]
-       column])
-    ([#Bit]
-     [#Nat]
-     [#Int]
-     [#Rev]
-     [#Frac]
-     [#Text]
-     [#Identifier]
-     [#Tag])
-
-    (^template [<tag>]
-      [[[_ _ column] (<tag> parts)]
-       (list\mix n/min column (list\each baseline_column parts))])
-    ([#Form]
-     [#Tuple])
-
-    [[_ _ column] (#Record pairs)]
-    (list\mix n/min column
-              (list\composite (list\each (|>> product\left baseline_column) pairs)
-                              (list\each (|>> product\right baseline_column) pairs)))
-    ))
-
-(type: Documentation_Fragment
-  (Variant
-   (#Documentation_Comment Text)
-   (#Documentation_Example Code)))
-
-(def: (documentation_fragment code)
-  (-> Code Documentation_Fragment)
-  (case code
-    [_ (#Text comment)]
-    (#Documentation_Comment comment)
-
-    _
-    (#Documentation_Example code)))
-
 (template [<name> <extension>]
   [(def: .public <name>
      (All [s] (-> (I64 s) (I64 s)))
@@ -4693,92 +4554,6 @@
   [-- "lux i64 -"]
   )
 
-(def: tag\encoded
-  (-> Name Text)
-  (|>> name\encoded
-       (text\composite "#")))
-
-(def: (repeated n x)
-  (All [a] (-> Int a (List a)))
-  (if ("lux i64 <" n +0)
-    (#Item x (repeated ("lux i64 +" -1 n) x))
-    #End))
-
-(def: (location_padding baseline [_ old_line old_column] [_ new_line new_column])
-  (-> Nat Location Location Text)
-  (if ("lux i64 =" old_line new_line)
-    (text\interposed "" (repeated (.int ("lux i64 -" old_column new_column)) " "))
-    (let [extra_lines (text\interposed "" (repeated (.int ("lux i64 -" old_line new_line)) ..\n))
-          space_padding (text\interposed "" (repeated (.int ("lux i64 -" baseline new_column)) " "))]
-      (text\composite extra_lines space_padding))))
-
-(def: (text\size x)
-  (-> Text Nat)
-  ("lux text size" x))
-
-(def: (updated_location [file line column] code_text)
-  (-> Location Text Location)
-  [file line ("lux i64 +" column (text\size code_text))])
-
-(def: (example_documentation prev_location baseline example)
-  (-> Location Nat Code [Location Text])
-  (case example
-    (^template [<tag> <encoded>]
-      [[new_location (<tag> value)]
-       (let [as_text (<encoded> value)]
-         [(updated_location new_location as_text)
-          (text\composite (location_padding baseline prev_location new_location)
-                          as_text)])])
-    ([#Bit        bit\encoded]
-     [#Nat        nat\encoded]
-     [#Int        int\encoded]
-     [#Frac       frac\encoded]
-     [#Text       text\encoded]
-     [#Identifier name\encoded]
-     [#Tag        tag\encoded])
-
-    (^template [<tag> <open> <close> <prep>]
-      [[group_location (<tag> parts)]
-       (let [[group_location' parts_text] (list\mix (function (_ part [last_location text_accum])
-                                                      (let [[part_location part_text] (example_documentation last_location baseline part)]
-                                                        [part_location (text\composite text_accum part_text)]))
-                                                    [(revised@ #column ++ group_location) ""]
-                                                    (<prep> parts))]
-         [(revised@ #column ++ group_location')
-          ($_ text\composite (location_padding baseline prev_location group_location)
-              <open>
-              parts_text
-              <close>)])])
-    ([#Form   "(" ")" |>]
-     [#Tuple  "[" "]" |>]
-     [#Record "{" "}" ..un_paired])
-
-    [new_location (#Rev value)]
-    ("lux io error" "@example_documentation Undefined behavior.")
-    ))
-
-(def: (fragment_documentation fragment)
-  (-> Documentation_Fragment Text)
-  (case fragment
-    (#Documentation_Comment comment)
-    (|> comment
-        (text\all_split_by ..\n)
-        (list\each (function (_ line) ($_ text\composite "... " line ..\n)))
-        (text\interposed ""))
-
-    (#Documentation_Example example)
-    (let [baseline (baseline_column example)
-          [location _] example
-          [_ text] (..example_documentation (with@ #column baseline location) baseline example)]
-      (text\composite text "\n\n"))))
-
-(macro: .public (example tokens)
-  (in_meta (list (` [(~ location_code)
-                     (#.Text (~ (|> tokens
-                                    (list\each (|>> ..documentation_fragment ..fragment_documentation))
-                                    (text\interposed "")
-                                    text$)))]))))
-
 (def: (interleaved xs ys)
   (All [a] (-> (List a) (List a) (List a)))
   (case xs
@@ -5557,3 +5332,49 @@
 
     _
     (..failure (..wrong_syntax_error (name_of ..try)))))
+
+(def: (methodP tokens)
+  (-> (List Code) (Maybe [(List Code) [Text Code]]))
+  (case tokens
+    (^ (list& [_ (#Form (list [_ (#Text "lux type check")] type [_ (#Identifier ["" name])]))]
+              tokens'))
+    (#Some [tokens' [name type]])
+
+    _
+    #None))
+
+(macro: .public (Interface tokens)
+  (do meta_monad
+    [methods' (monad\each meta_monad expansion tokens)]
+    (case (everyP methodP (list\conjoint methods'))
+      (#Some methods)
+      (in (list (` (..Tuple (~+ (list\each product\right methods))))
+                (tuple$ (list\each (|>> product\left text$) methods))))
+      
+      #None
+      (failure "Wrong syntax for Interface"))))
+
+(def: (recursive_type name body)
+  (-> Text Code Code)
+  (let [body' (|> body
+                  nested_quantification
+                  (with_replacements (list [name (` (#.Apply .Nothing (~ (type_parameter 0))))])))]
+    (` (#.Apply .Nothing (#.UnivQ #.End (~ body'))))))
+
+(macro: .public (Rec tokens)
+  (case tokens
+    (^ (list [_ (#Identifier "" name)] body))
+    (do meta_monad
+      [body' (expansion body)]
+      (case body'
+        (^ (list body' labels))
+        (in (list (..recursive_type name body') labels))
+
+        (^ (list body'))
+        (in (list (..recursive_type name body')))
+
+        _
+        (failure "Wrong syntax for Rec")))
+
+    _
+    (failure "Wrong syntax for Rec")))