Merge pull request #933 from andrew-johnson-4/lsts-collections-2

Lsts collections 2
andrew-johnson-4 · Nov 13, 2024 · 3a407e3 · 3a407e3
2 parents c3b845b + 1ec9d1c
commit 3a407e3
Show file tree

Hide file tree

Showing 9 changed files with 19,734 additions and 19,694 deletions.
diff --git a/BOOTSTRAP/cli.c b/BOOTSTRAP/cli.c
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.19.5"
+version = "1.19.6"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

diff --git a/PLATFORM/C/LIB/hashtable.lm b/PLATFORM/C/LIB/hashtable.lm
@@ -71,12 +71,15 @@ type HashtableIs<k,v> (HashtableIs( occupied:U64 , capacity:U64 , contents:Tuple
    default
 ) v);
 
-type HashtableEq<k,v> (HashtableEq( occupied:U64 , capacity:U64 , contents:Tuple<k,v>[] ));
+type HashtableEq<k,v> (HashtableEq( occupied:U64 , capacity:U64 , contents:Tuple<k,v>[] )); # | MEOF;
 
 .bind := λ(: table HashtableEq<k,v>)(: key k)(: value v). (: (
-   (let occupied (.3 table))
-   (let capacity (.2 table))
-   (let contents (.1 table))
+   #(if (is( table (: MEOF HashtableEq<k,v>) )) (
+   #   (set table (HashtableEq( 0_u64 0_u64 (as 0_u64 Tuple<k,v>[]) )))
+   #) ())
+   (let occupied (.3(as table Tag<HashtableEq>)))
+   (let capacity (.2(as table Tag<HashtableEq>)))
+   (let contents (.1(as table Tag<HashtableEq>)))
    (if (>=( (*( occupied 3_u64 )) capacity )) (
       (let new-capacity (max( 1000_u64 (*( occupied 30_u64 )) )))
       (let new-sizeof (*( (sizeof Tuple<k,v>) new-capacity )))
@@ -121,9 +124,9 @@ type HashtableEq<k,v> (HashtableEq( occupied:U64 , capacity:U64 , contents:Tuple
 ) U64);
 
 .lookup := λ(: table HashtableEq<k,v>)(: key k)(: default v). (: (
-   (let capacity (.2 table))
+   (let capacity (.2(as table Tag<HashtableEq>)))
    (if (==( capacity 0_u64 )) () (
-      (let contents (.1 table))
+      (let contents (.1(as table Tag<HashtableEq>)))
       (let replacing 0_u64)
       (let ki (%( (deep-hash key) capacity )))
       (let old-kv ([]( contents ki )))
@@ -142,3 +145,7 @@ type HashtableEq<k,v> (HashtableEq( occupied:U64 , capacity:U64 , contents:Tuple
    ))
    default
 ) v);
+
+map::cons := λ(: key k)(: val v)(: tl HashtableEq<k,v>). (: (
+   (.bind( tl key val ))
+) HashtableEq<k,v>);
diff --git a/PLATFORM/C/LIB/list.lm b/PLATFORM/C/LIB/list.lm
@@ -6,6 +6,11 @@ cons := λ(: hd x)(: tl List<x>). (: (
    tl
 ) List<x>);
 
+list::cons := λ(: hd x)(: tl List<x>). (: (
+   (set tl (LCons( hd (close tl) )))
+   tl
+) List<x>);
+
 head := λ(: l List<x>). (: (
    (match l (
       ()

diff --git a/PLUGINS/BACKEND/C/compile-c-typedef.lm b/PLUGINS/BACKEND/C/compile-c-typedef.lm
@@ -5,22 +5,24 @@ compile-c-typedef-concrete-ordinal := λ(: base-type Type). (: (
    (let base-uuid (uuid()))
    (set index-c-type-ordinal (.bind( index-c-type-ordinal base-type base-uuid )))
    (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom 'typedef\sstruct\s_s)) )))
-   (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom base-uuid)) )))
+   (set assemble-header-section (SCons( (close assemble-header-section) (close(mangle-c-type base-type)) )))
    (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\s_s)) )))
-   (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom base-uuid)) )))
+   (set assemble-header-section (SCons( (close assemble-header-section) (close(mangle-c-type base-type)) )))
    (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\:\n_s)) )))
 ) Nil);
 
 compile-c-typedef-ordinal := λ(: base-type Type). (: (
-   (if (is-open base-type) () (
-      (compile-c-typedef-concrete-ordinal( base-type ))
-   ))
-   (match base-type (
-      ()
-      ( (TGround( tag ts )) (
-         (let k (Tuple( tag (.length ts) )))
-         (for-each (vt in (.lookup( concrete-type-instances-index k (: LEOF List<Type>) ))) (
-            (compile-c-typedef-concrete-ordinal( vt ))
+   (if (is-fragment base-type) () (
+      (if (is-open base-type) () (
+         (compile-c-typedef-concrete-ordinal( base-type ))
+      ))
+      (match base-type (
+         ()
+         ( (TGround( tag ts )) (
+            (let k (Tuple( tag (.length ts) )))
+            (for-each (vt in (.lookup( concrete-type-instances-index k (: LEOF List<Type>) ))) (
+               (compile-c-typedef-concrete-ordinal( vt ))
+            ))
          ))
       ))
    ))
@@ -118,7 +120,7 @@ compile-c-typedef-concrete := λ(: tctx TContext)(: base-type Type)(: body AST).
       ) (
          (set is-cstruct-hard-compiled-index (.bind( is-cstruct-hard-compiled-index base-type 1_u64 )))
          (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom 'struct\s_s)) )))
-         (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom base-uuid)) )))
+         (set assemble-header-section (SCons( (close assemble-header-section) (close(mangle-c-type base-type)) )))
          (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '{\n_s)) )))
          (set assemble-header-section (SCons( (close assemble-header-section) (close(SAtom '\tlong\sfield_0\:\n_s)) )))
          (if has-case (
@@ -131,16 +133,18 @@ compile-c-typedef-concrete := λ(: tctx TContext)(: base-type Type)(: body AST).
 ) Nil);
 
 compile-c-typedef := λ(: base-type Type)(: body AST). (: (
-   (if (is-open base-type) () (
-      (compile-c-typedef-concrete( TCtxEOF base-type body ))
-   ))
-   (match base-type (
-      ()
-      ( (TGround( tag ts )) (
-         (let k (Tuple( tag (.length ts) )))
-         (for-each (vt in (.lookup( concrete-type-instances-index k (: LEOF List<Type>) ))) (
-            (let tctx (unify( base-type vt )))
-            (compile-c-typedef-concrete( tctx vt body ))
+   (if (is-fragment base-type) () (
+      (if (is-open base-type) () (
+         (compile-c-typedef-concrete( TCtxEOF base-type body ))
+      ))
+      (match base-type (
+         ()
+         ( (TGround( tag ts )) (
+            (let k (Tuple( tag (.length ts) )))
+            (for-each (vt in (.lookup( concrete-type-instances-index k (: LEOF List<Type>) ))) (
+               (let tctx (unify( base-type vt )))
+               (compile-c-typedef-concrete( tctx vt body ))
+            ))
          ))
       ))
    ))

diff --git a/PLUGINS/BACKEND/C/compile-constructor.lm b/PLUGINS/BACKEND/C/compile-constructor.lm
@@ -2,12 +2,11 @@
 compile-constructor := λ(: ctx FContext)(: tag-name String)(: return-type Type)(: args-type Type)(: args AST)(: offset I64). (: (
    (let r (fragment::new()))
    (let bare-ordinal (with-only-class return-type))
-   (let c-type-name (.lookup( index-c-type-ordinal (normalize bare-ordinal) 'UnknownCTypename_s )))
    (let case-number (index-of-tag tag-name))
    (set r (initialize-c-struct( ctx args case-number 1_u64 )))
    (set r (fragment::set( r 'expression_s (
       (+(
-         (+( (+( (SAtom '\[{_s) (SAtom c-type-name) )) (SAtom '\srvalue={.field_0=_s) ))
+         (+( (+( (SAtom '\[{_s) (mangle-c-type(normalize bare-ordinal)) )) (SAtom '\srvalue={.field_0=_s) ))
          (+( (+( (SAtom(to-string case-number)) (fragment::get( r 'expression_s )) )) (SAtom '}\:rvalue\:}\]_s) ))
       ))
    ))))

diff --git a/PLUGINS/BACKEND/C/mangle-c-type.lm b/PLUGINS/BACKEND/C/mangle-c-type.lm
@@ -36,7 +36,10 @@ mangle-c-type-internal := λ(: tt Type). (: (
          ) (
             (let c-type-name (.lookup( index-c-type-ordinal tt 'UnknownCTypename_s )))
             (if (==( c-type-name 'UnknownCTypename_s )) () (
-               (set r (SAtom c-type-name))
+               (set r (+(
+                  (SAtom 'LM__s)
+                  (mangle-identifier tt)
+               )))
             ))
          ))
       ))

diff --git a/PLUGINS/FRONTEND/LSTS/lsts-parse.lm b/PLUGINS/FRONTEND/LSTS/lsts-parse.lm
@@ -292,10 +292,7 @@ lsts-parse-map := λ(: tokens List<Token>). (: (
             (set term (App(
                (close(Var( 'map::cons_s (with-location( (token::new 'map::cons_s) loc )) )))
                (close(App(
-                  (close(App(
-                     (close(Var( 'Tuple_s (with-location( (token::new 'Tuple_s) loc )) )))
-                     (close(App( (close item) (close mapped) )))
-                  )))
+                  (close(App( (close item) (close mapped) )))
                   (close term)
                )))
             )))

diff --git a/SRC/infer-expr.lm b/SRC/infer-expr.lm
@@ -191,9 +191,30 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          (match l (
             ()
             ( (Var( l-fname _ )) (
+               (if (==( l-fname 'list::cons_s )) (
+                  (match r (
+                     ()
+                     ( (App( k m )) (
+                        (infer-expr( tctx k Unscoped TAny Call ))
+                        (infer-expr( tctx m Unscoped (t2( 'List_s (typeof k) )) Used ))
+                     ))
+                     ( _ () )
+                  ))
+               ) ())
+               (if (==( l-fname 'map::cons_s )) (
+                  (match r (
+                     ()
+                     ( (App( kv m )) (
+                        (infer-expr( tctx kv Unscoped TAny Call ))
+                        (infer-expr( tctx m Unscoped (t3( 'HashtableEq_s (p2(typeof kv)) (p1(typeof kv)) )) Used ))
+                     ))
+                     ( _ () )
+                  ))
+               ) ())
                (if (is( used Unused )) (set r-used Unused) ())
                (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
                (if (is-arrow(typeof l)) (set r-used Call) ())
+               (let r-hint TAny)
                (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
                (let lt-fname (find-alias( l-fname (typeof r) )))
                (let ftrt (apply-or-cons-and-specialize(