Merge pull request #753 from andrew-johnson-4/more-doca-types-2

More doca types 2

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.16.36"
+version = "1.16.37"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

LIB/default-stdlib.lm

@@ -26,6 +26,23 @@ type Tuple<x,y> (Tuple( x , y ));
    return
 ) U64);
 
+== := λ(: lt List<x>)(: rt List<x>). (: (
+   (let r 0_u64)
+   (match (Tuple( lt rt )) (
+      ()
+      ( (Tuple( LEOF LEOF )) (set r 1_u64) )
+      ( (Tuple( (LCons( ltr lt1 )) (LCons( rtr rt1 )) )) (
+         (if (==( lt1 rt1 )) (
+            (if (==( ltr rtr )) (
+               (set r 1_u64)
+            ) ())
+         ) ())
+      ))
+      ( _ () )
+   ))
+   r
+) U64);
+
 deep-hash := λ(: l Tuple<x,y>). (: (
    (let return 0_u64)
    (match l (

SRC/alias.lm

@@ -12,7 +12,7 @@ find-alias := λ(: from String)(: pars Type). (: (
          ()
          ( (Tuple(
               (Tuple( alt-from alt-to ))
-              (TGround( 'Arrow_s (TypeSeq( (TypeSeq( TypeEOF alt-domain )) _ )) ))
+              (TGround( 'Arrow_s (LCons( _ (LCons( alt-domain LEOF )) )) ))
            )) (
             (if (&&( (==( from alt-from )) (can-unify( alt-domain pars )) )) (
                (set to alt-to)

SRC/index-types.lm

@@ -20,5 +20,7 @@ import SRC/domain.lm;
 import SRC/range.lm;
 import SRC/t.lm;
 import SRC/p.lm;
+import SRC/tag-of.lm;
+import SRC/is-open.lm;
 
 import SRC/typecheck.lm;

SRC/infer-expr.lm

@@ -139,8 +139,8 @@ infer-expr := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type)(:
          (let deref-type (typeof r))
          (match (slot( deref-type 'Array_s )) (
             ()
-            ( (TGround( 'Array_s (TypeSeq( (TypeSeq( TypeEOF TAny )) _ )) )) () )
-            ( (TGround( 'Array_s (TypeSeq( (TypeSeq( TypeEOF array-base )) TAny )) )) (
+            ( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) () )
+            ( (TGround( 'Array_s (LCons( TAny (LCons( array-base LEOF )) )) )) (
                (set deref-type (and( array-base (t1 'StackVariable_s) )))
             ))
             ( _ () )

SRC/is-open.lm

@@ -0,0 +1,27 @@
+
+is-open := λ(: tt Type). (: (
+   (let r 0_u64)
+   (match tt (
+      ()
+      ( TAny (set r 1_u64) )
+      ( (TVar _) (set r 1_u64) )
+      ( (TAnd( lt rt )) (
+         (if (is-open lt) (set r 1_u64) ())
+         (if (is-open rt) (set r 1_u64) ())
+      ))
+      ( (TGround( 'Array_s (LCons( _ (LCons( _ LEOF )) )) )) () )
+      ( (TGround( 'Field_s (LCons( _ (LCons( base-type LEOF )) )) )) (
+         (set r (is-open base-type))
+      ))
+      ( (TGround( _ pars )) (
+         (while (non-zero pars) (match pars (
+            ()
+            ( (LCons( p1 rst )) (
+               (if (is-open p1) (set r 1_u64) ())
+               (set pars rst)
+            ))
+         )))
+      ))
+   ))
+   r
+) U64);

SRC/mangle-identifier.lm

@@ -54,7 +54,7 @@ mangle-identifier := λ(: kt Type). (: (
          (set r (mangle-identifier tv))
          (while (non-zero ps) (match ps (
             ()
-            ( (TypeSeq( rst p1 )) (
+            ( (LCons( p1 rst )) (
                (set r (SCons( (close r) (close(mangle-identifier p1)) )))
                (set ps rst)
             )))

SRC/p.lm

@@ -1,8 +1,8 @@
 
-p := λ(: tt TypeList)(: default Type)(: i U64). (: (
+p := λ(: tt List<Type>)(: default Type)(: i U64). (: (
    (match tt (
       ()
-      ( (TypeSeq( rst pt )) ((if (==( i 0_u64 ))
+      ( (LCons( pt rst )) ((if (==( i 0_u64 ))
          (set default pt)
          (set default (p( rst default (-( i 1_u64 )) )))
       )))

SRC/stable-ast.lm

@@ -9,8 +9,7 @@ config-assemble-mode         := (: AssembleGNU AssembleMode);
 type CompileMode ModeTokenize | ModeParse | ModePreprocess | ModeTypecheck | ModeCompile;
 config-mode                  := (: ModeCompile CompileMode);
 
-type Type TAny | (TVar String) | (TGround( String , TypeList[] )) | (TAnd( Type[] , Type[] )); zero Type TAny;
-type TypeList TypeEOF | (TypeSeq( TypeList[] , Type )); zero TypeList TypeEOF;
+type Type TAny | (TVar String) | (TGround( String , List<Type>[] )) | (TAnd( Type[] , Type[] )); zero Type TAny;
 
 type SourceLocation (SourceLocation( String , U64 , U64 ));
 type Token (Token( String , U64 , SourceLocation ));
@@ -31,7 +30,6 @@ type TContext TCtxEOF | TCtxNil | (TCtxBind( TContext[] , String , Type , AST ))
 type FContext FCtxEOF | (FCtxBind( FContext[] , String , Type , Fragment )); zero FContext FCtxEOF;
 
 type STypeList STEOF | (STSeq( STypeList[] , S , Type )); zero STypeList STEOF;
-type ATypeList ATEOF | (ATSeq( ATypeList[] , AST , Type )); zero ATypeList ATEOF;
 type StringTypeList StrTEOF | (StrTSeq( StringTypeList[] , String , Type )); zero StringTypeList StrTEOF;
 
 type StringList SLEOF | (SLSeq( StringList[] , String )); zero StringList SLEOF;
@@ -238,11 +236,11 @@ serialize-ast := λ(: t AST). (: (
    ))
 ) Nil);
 
-serialize-ast := λ(: tt TypeList). (: (match tt (
+serialize-ast := λ(: tt List<Type>). (: (match tt (
    ()
-   ( TypeEOF () )
-   ( (TypeSeq( TypeEOF p1 )) (serialize-ast p1) )
-   ( (TypeSeq( rst p1 )) (
+   ( LEOF () )
+   ( (LCons( p1 LEOF )) (serialize-ast p1) )
+   ( (LCons( p1 rst )) (
       (print '\[App\s\[_s)
       (serialize-ast rst)
       (print '\s_s)
@@ -269,7 +267,7 @@ serialize-ast := λ(: tt Type). (: (match tt (
       (print '\]\]_s)
       (print '\]\]_s)
    ))
-   ( (TGround( tag TypeEOF )) (
+   ( (TGround( tag LEOF )) (
       (print '\[Literal\s_s)
       (print tag)
       (print '\]_s)
@@ -341,7 +339,7 @@ print := λ(: tt Type). (: (match tt (
    ()
    ( TAny (print '?_s) )
    ( (TVar( vn )) (print vn) )
-   ( (TGround( tag TypeEOF )) (print tag) )
+   ( (TGround( tag LEOF )) (print tag) )
    ( (TAnd( lt rt )) (
       (if (is-arrow lt) (
          (print lt)
@@ -361,11 +359,11 @@ print := λ(: tt Type). (: (match tt (
    ))
 )) Nil);
 
-print := λ(: tt TypeList). (: (match tt (
+print := λ(: tt List<Type>). (: (match tt (
    ()
-   ( TypeEOF () )
-   ( (TypeSeq( TypeEOF p1 )) (print p1) )
-   ( (TypeSeq( rst p1 )) (
+   ( LEOF () )
+   ( (LCons( p1 LEOF )) (print p1) )
+   ( (LCons( p1 rst )) (
       (print rst)
       (print ',_s)
       (print p1)

SRC/stable-blob.lm

@@ -83,7 +83,7 @@ blob-call := λ(: ctx FContext)(: function-name String)(: args AST). (: (
 blob-bind-one := λ(: ctx FContext)(: k String)(: kt Type)(: arg Fragment). (: (
    (match kt (
       ()
-      ( (TGround( '..._s (TypeSeq( TypeEOF p1 )) )) (
+      ( (TGround( '..._s (LCons( p1 LEOF )) )) (
          (if (can-unify( p1 (fragment::get-type arg) )) (
             (set ctx (fragment-context::bind-vararg(
                ctx k kt arg
@@ -144,7 +144,7 @@ blob-args := λ(: ctx FContext)(: rval AST). (: (
    (let r FLEOF)
    (match (slot( (typeof rval) 'Cons_s )) (
       ()
-      ( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (
+      ( (TGround( 'Cons_s (LCons( p2 (LCons( p1 LEOF )) )) )) (
          (match rval (
             ()
             ( (App( le re )) (

SRC/stable-codegen.lm

@@ -56,7 +56,7 @@ compile-destructure-args := λ(: tt Type)(: ctx FContext)(: lhs AST)(: offset I6
       ( (App( rst (App( (Lit( ':_s _ )) (App( (Var( k _ )) (AType kt) )) )) )) (
          (match (slot( tt 'Cons_s )) (
             ()
-            ( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF rst-tt )) p2 )) )) (
+            ( (TGround( 'Cons_s (LCons( p2 (LCons( rst-tt LEOF )) )) )) (
                (set ctx (compile-destructure-args( rst-tt ctx rst offset )))
                (let rst-sz (sizeof-aligned rst-tt))
                (let rst-offset (-( offset (as rst-sz I64) )))
@@ -155,7 +155,7 @@ compile-push-rvalue := λ(: ctx FContext)(: rval AST)(: offset I64)(: count U64)
    (let r (fragment::new()))
    (match (slot( (typeof rval) 'Cons_s )) (
       ()
-      ( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (
+      ( (TGround( 'Cons_s (LCons( p2 (LCons( p1 LEOF )) )) )) (
          (match rval (
             ()
             ( (App( le re )) (
@@ -208,7 +208,7 @@ compile-fragment-args := λ(: ctx FContext)(: function-args-type Type)(: rval AS
    (let r FLEOF)
    (match (slot( (typeof rval) 'Cons_s )) (
       ()
-      ( (TGround( 'Cons_s (TypeSeq( (TypeSeq( TypeEOF p1 )) p2 )) )) (
+      ( (TGround( 'Cons_s (LCons( p2 (LCons( p1 LEOF )) )) )) (
          (match rval (
             ()
             ( (App( le re )) (
@@ -439,8 +439,8 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
          (let tt (typeof t))
          (match (slot( tt 'Array_s )) (
             ()
-            ( (TGround( 'Array_s (TypeSeq( (TypeSeq( TypeEOF TAny )) _ )) )) () )
-            ( (TGround( 'Array_s (TypeSeq( (TypeSeq( TypeEOF inner-tt )) TAny )) )) (
+            ( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) () )
+            ( (TGround( 'Array_s (LCons( TAny (LCons( inner-tt LEOF )) )) )) (
                (let e1 (fragment::set-type( e (denormalize tt) )))
                (let e2 (fragment::new()))
                (set e2 (fragment::set( e2 'expression_s (SAtom '0_s) )))

SRC/stable-context.lm

@@ -22,7 +22,7 @@ fragment-context::lookup := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AST
          (if (==( k rk )) (
             (match (slot( rt 'Arrow_s )) (
                ()
-               ( (TGround( 'Arrow_s (TypeSeq( (TypeSeq( TypeEOF domaint )) ranget )) )) (
+               ( (TGround( 'Arrow_s (LCons( ranget (LCons( domaint LEOF )) )) )) (
                   (if (can-unify( domaint kt )) (
                      (if (non-zero found) (
                         (if (can-unify( found domaint )) (
@@ -69,7 +69,7 @@ fragment-context::lookups := λ(: ctx FContext)(: k String)(: kt Type)(: sloc AS
          (if (==( k rk )) (
             (match (slot( rt 'Arrow_s )) (
                ()
-               ( (TGround( 'Arrow_s (TypeSeq( (TypeSeq( TypeEOF domaint )) ranget )) )) (
+               ( (TGround( 'Arrow_s (LCons( ranget (LCons( domaint LEOF )) )) )) (
                   (if (can-unify( domaint kt )) (
                      (if (non-zero found) (
                         (if (can-unify( found domaint )) (

SRC/stable-parse.lm

@@ -60,7 +60,7 @@ parse-lambda := λ(: tokens List<Token>). (: (
 parse-type-comma-sep := λ(: tt String). (: (
    (let buff SNil)
    (let depth 0_u64)
-   (let base TypeEOF)
+   (let base (: LEOF List<Type>))
    (while (head-string tt) (
       (match (head-string tt) (
          ()
@@ -72,9 +72,9 @@ parse-type-comma-sep := λ(: tt String). (: (
       ))
       (if (==( depth 0_u64 )) (
          (if (==( (head-string tt) 44_u8 )) (
-            (set base (TypeSeq(
-               (close base)
+            (set base (cons(
                (parse-type(clone-rope buff))
+               base
             )))
             (set buff SNil)
          ) (
@@ -91,12 +91,12 @@ parse-type-comma-sep := λ(: tt String). (: (
       ))
       (set tt (tail-string tt))
    ))
-   (set base (TypeSeq(
-      (close base)
+   (set base (cons(
       (parse-type(clone-rope buff))
+      base
    )))
    base
-) TypeList);
+) List<Type>);
 
 parse-type := λ(: tt String). (: (
    (let is-vararg False_u8)
@@ -120,7 +120,7 @@ parse-type := λ(: tt String). (: (
          (if (==( (head-string tt) 43_u8 )) (
             (match base-type (
                ()
-               ( (TGround( 'Nil_s TypeEOF )) (
+               ( (TGround( 'Nil_s LEOF )) (
                   (let bt (parse-type-single (clone-rope buff)))
                   (set base-type bt)
                ))
@@ -149,7 +149,7 @@ parse-type := λ(: tt String). (: (
    (if (non-zero buff) (
       (match base-type (
          ()
-         ( (TGround( 'Nil_s TypeEOF )) (
+         ( (TGround( 'Nil_s LEOF )) (
             (let bt (parse-type-single (clone-rope buff)))
             (set base-type bt)
          ))
@@ -162,8 +162,8 @@ parse-type := λ(: tt String). (: (
       ))
    ) ())
    (if (==( is-vararg True_u8 )) (
-      (set base-type (TGround( '..._s (close(TypeSeq(
-         (close TypeEOF) base-type
+      (set base-type (TGround( '..._s (close(cons(
+         base-type (: LEOF List<Type>)
       ))))))
    ) ())
    base-type
@@ -287,7 +287,7 @@ parse-type-single := λ(: tt String). (: (
                      ) (
                         (set base-type (TGround(
                            (clone-rope buff)
-                           (close TypeEOF)
+                           (close(: LEOF List<Type>))
                         )))
                      ))
                   ))
@@ -307,7 +307,7 @@ parse-type-single := λ(: tt String). (: (
                      ) (
                         (set base-type (TGround(
                            (clone-rope buff)
-                           (close TypeEOF)
+                           (close(: LEOF List<Type>))
                         )))
                      ))
                   ))
@@ -351,7 +351,7 @@ parse-type-single := λ(: tt String). (: (
                ))
                ( 60_u8 (match base-type (
                   ()
-                  ( (TGround( tag TypeEOF )) (
+                  ( (TGround( tag LEOF )) (
                      (set base-type (TGround(
                         tag
                         (close(parse-type-comma-sep(clone-rope buff)))
@@ -391,7 +391,7 @@ parse-type-single := λ(: tt String). (: (
          ) (
             (set base-type (TGround(
                (clone-rope buff)
-               (close TypeEOF)
+               (close(: LEOF List<Type>))
             )))
          ))
       ))
@@ -559,8 +559,8 @@ parse-toplevel := λ(: tokens List<Token>). (: (
                suffix
                (TAnd(
                   (close(TAnd(
-                     (close(TGround( 'Constant_s (close TypeEOF) )))
-                     (close(TGround( 'Literal_s (close TypeEOF) )))
+                     (close(TGround( 'Constant_s (close(: LEOF List<Type>)) )))
+                     (close(TGround( 'Literal_s (close(: LEOF List<Type>)) )))
                   )))
                   (close(parse-type atype))
                ))