Merge pull request #911 from andrew-johnson-4/call-cpp

Call cpp
andrew-johnson-4 · Nov 6, 2024 · a13e359 · a13e359
2 parents 3857b7d + e0051e0
commit a13e359
Show file tree

Hide file tree

Showing 19 changed files with 18,484 additions and 18,135 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.18.6"
+version = "1.18.7"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

diff --git a/Makefile b/Makefile
@@ -1,6 +1,6 @@
 
 dev: install-production
-	lm --c tests/regress/function-pointers.lm
+	lm --c tests/regress/exec.lm
 	cc tmp.c
 	./a.out
 	echo $?

diff --git a/PLATFORM/C/LIB/array.lm b/PLATFORM/C/LIB/array.lm
@@ -1,4 +1,12 @@
 
+const-cons := λ: Blob(: es x...). (: (
+   (:expression(
+      '{_s (for-arg (e in es) (
+         (:expression e) ',_s
+       )) 'NULL}_s
+   ))
+) Array<x,CONST>);
+
 (declare-binop( [] Array<base-type,?> U64 base-type ('\[_l x '[_l y ']\]_l) ));
 (declare-ternop( set[] Array<base-type,?> U64 base-type base-type ('\[_l x '[_l y ']=_l z \]_l) ));
 (declare-binop( + Array<base-type,?> U64 Array<base-type,?> ('\[_l x '+_l y '\]_l) ));

diff --git a/PLATFORM/C/LIB/io.lm b/PLATFORM/C/LIB/io.lm
@@ -10,6 +10,7 @@ fopen := λ: FFI(: fp U8[])(: mode U8[]). (: () File[]);
 fread := λ: FFI(: buff ?[])(: size U64)(: count U64)(: f File[]). (: () U64);
 fwrite := λ: FFI(: buff ?[])(: size U64)(: count U64)(: f File[]). (: () U64);
 fclose := λ: FFI(: f File[]). (: () U32);
+execvp := λ: FFI(: file U8[])(: argv U8[][]). (: () U32);
 
 exit := λ(: x U64).(: (exit(as x U32)) Nil);
 

diff --git a/PLATFORM/C/LIB/tuple.lm b/PLATFORM/C/LIB/tuple.lm
@@ -1,5 +1,5 @@
 
-type Tuple<x,y> (Tuple( x , y ));
+type Tuple<x,y> (Tuple( first:x , second:y ));
 
 == := λ(: l Tuple<x,y>)(: r Tuple<x,y>). (: (
    (let return 0_u64)

diff --git a/PLUGINS/BACKEND/C/compile-c-text-header.lm b/PLUGINS/BACKEND/C/compile-c-text-header.lm
@@ -1,4 +1,4 @@
 
 compile-c-text-header := λ. (: (
-   (SAtom '\oinclude\s<stdio.h>\n\oinclude\s<stdlib.h>\n\oinclude\s<string.h>\n\n_s)
+   (SAtom '\oinclude\s<stdio.h>\n\oinclude\s<stdlib.h>\n\oinclude\s<string.h>\n\oinclude\s<unistd.h>\n\n_s)
 ) S);
diff --git a/PLUGINS/BACKEND/C/compile-data-header.lm b/PLUGINS/BACKEND/C/compile-data-header.lm
diff --git a/PLUGINS/BACKEND/C/compile-expr-direct.lm b/PLUGINS/BACKEND/C/compile-expr-direct.lm
@@ -68,22 +68,6 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
       ( (App( (Lit( ':_s _ )) (App( t (AType tt) )) )) (
          (set e (compile-expr( ctx t stack-offset used )))
       ))
-      ( (App( (Var( 'gensym-label_s _ )) (Var( id _ )) )) (
-         (set ctx (fragment-context::bind(
-            ctx id (t1 'Label_s) (fragment::label( (uuid()) ))
-         )))
-         (set.context( e (close ctx) ))
-         (set.type( e (denormalize(t1 'Nil_s)) ))
-      ))
-      ( (App( (Var( 'label_s _ )) (Var( id _ )) )) (
-         (let l (fragment-context::lookup( ctx id (t1 'Label_s) term )))
-         (let prog (SCons(
-            (close(fragment::get( l 'expression_s )))
-            (close(SAtom ':\n_s))
-         )))
-         (set e (fragment::set( e 'program_s prog )))
-         (set.type( e (denormalize(t1 'Nil_s)) ))
-      ))
       ( (App( (Var( 'scope_s _ )) t )) (
          (set e (compile-expr( ctx t stack-offset Tail )))
          (set.context( e (close ctx) ))
@@ -188,37 +172,72 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
          (let bind-offset (-( stack-offset (as size I64) )))
          (let fr (fragment::local-variable( bind-offset rtype )))
          (set ctx (fragment-context::bind( ctx lhs rtype fr )))
-         (set e (compile-expr( ctx rhs stack-offset Used )))
-         (set e (fragment::set( e 'frame_s (
-            (+(
-               (fragment::get( e 'frame_s ))
+         (let prepost (mangle-c-declaration rtype))
+         (if (is-const-array rtype) (
+            (set e (compile-expr( ctx rhs stack-offset Used )))
+            (set e (fragment::set( e 'expression_s (
                (+(
                   (+(
-                     (mangle-c-type rtype)
+                     (.first prepost)
                      (SAtom '\s_s)
                   ))
                   (+(
                      (fragment::get( fr 'expression_s ))
-                     (SAtom '\:\n_s)
+                     (+(
+                        (+(
+                           (.second prepost)
+                           (SAtom '=_s)
+                        ))
+                        (+(
+                           (fragment::get( e 'expression_s ))
+                           (SAtom '\:\n_s)
+                        ))
+                     ))
                   ))
                ))
-            ))
-         ))))
-         (set e (fragment::set( e 'expression_s (
-            (+(
-               (+(
-                  (SAtom '\[{_s)
-                  (fragment::get( fr 'expression_s ))
+            ))))
+         ) (
+            (match rhs (
+               ()
+               ( (App( (Lit( ':_s _ )) (App( (Var( '__uninitialized_s _ )) (AType tt) )) )) () )
+               ( _ (
+                  (set e (compile-expr( ctx rhs stack-offset Used )))
+                  (set e (fragment::set( e 'expression_s (
+                     (+(
+                        (+(
+                           (SAtom '\[{_s)
+                           (fragment::get( fr 'expression_s ))
+                        ))
+                        (+(
+                           (SAtom '=_s)
+                           (+(
+                              (fragment::get( e 'expression_s ))
+                              (SAtom '\:\[{}\]\:}\]\n_s)
+                           ))
+                        ))
+                     ))
+                  ))))
                ))
+            ))
+            (set e (fragment::set( e 'frame_s (
                (+(
-                  (SAtom '=_s)
+                  (fragment::get( e 'frame_s ))
                   (+(
-                     (fragment::get( e 'expression_s ))
-                     (SAtom '\:\[{}\]\:}\]\n_s)
+                     (+(
+                        (.first prepost)
+                        (SAtom '\s_s)
+                     ))
+                     (+(
+                        (fragment::get( fr 'expression_s ))
+                        (+(
+                           (.second prepost)
+                           (SAtom '\:\n_s)
+                        ))
+                     ))
                   ))
                ))
-            ))
-         ))))
+            ))))
+         ))
          (set.context( e (close ctx) ))
          (set.type( e (typeof term) ))
       ))

diff --git a/PLUGINS/BACKEND/C/compile-text-header.lm b/PLUGINS/BACKEND/C/compile-text-header.lm
diff --git a/PLUGINS/BACKEND/C/index-index.lm b/PLUGINS/BACKEND/C/index-index.lm
@@ -18,11 +18,9 @@ import PLUGINS/BACKEND/C/never-as-expr-type.lm;
 import PLUGINS/BACKEND/C/compile-c-function-args.lm;
 import PLUGINS/BACKEND/C/compile-c-text-header.lm;
 import PLUGINS/BACKEND/C/compile-c-typedef.lm;
-import PLUGINS/BACKEND/C/compile-data-header.lm;
 import PLUGINS/BACKEND/C/compile-exit-cleanup.lm;
 import PLUGINS/BACKEND/C/compile-finish.lm;
 import PLUGINS/BACKEND/C/compile-program-ordered.lm;
-import PLUGINS/BACKEND/C/compile-text-header.lm;
 import PLUGINS/BACKEND/C/compile-write.lm;
 import PLUGINS/BACKEND/C/initialize-c-struct.lm;
 import PLUGINS/BACKEND/C/cc-args.lm;
@@ -34,3 +32,4 @@ import PLUGINS/BACKEND/C/escape-string.lm;
 import PLUGINS/BACKEND/C/fragment::chain.lm;
 import PLUGINS/BACKEND/C/fragment::local-variable.lm;
 import PLUGINS/BACKEND/C/fragment::label.lm;
+import PLUGINS/BACKEND/C/is-const-array.lm;
diff --git a/PLUGINS/BACKEND/C/is-const-array.lm b/PLUGINS/BACKEND/C/is-const-array.lm
@@ -0,0 +1,11 @@
+
+is-const-array := λ(: tt Type). (: (
+   (let r 0_u64)
+   (match tt (
+      ()
+      ( (TAnd( t1 t2 )) (set r (||( (is-const-array( t1 )) (is-const-array( t2 )) ))) )
+      ( (TGround( 'Array_s (LCons( (TGround( 'CONST_s _ )) (LCons( array-base _ )) )) )) (set r 1_u64) )
+      ( _ () )
+   ))
+   r
+) U64);
diff --git a/PLUGINS/BACKEND/C/mangle-c-type.lm b/PLUGINS/BACKEND/C/mangle-c-type.lm
@@ -37,3 +37,42 @@ mangle-c-type-internal := λ(: tt Type). (: (
    ))
    r
 ) S);
+
+mangle-c-declaration := λ(: tt Type). (: (
+   (set tt (normalize tt))
+   (let r (mangle-c-declaration-internal tt))
+   r
+) Tuple<S,S>);
+
+mangle-c-declaration-internal := λ(: tt Type). (: (
+   (let pre SNil)
+   (let post SNil)
+   (match tt (
+      ()
+      ( (TGround( 'Array_s (LCons( (TGround( 'CONST_s _ )) (LCons( array-base _ )) )) )) (
+         (let rst (mangle-c-declaration-internal array-base))
+         (set pre (.first rst))
+         (set post (+(
+            (.second rst)
+            (SAtom '[]_s)
+         )))
+      ))
+      ( (TGround( 'Array_s (LCons( (TGround( index _ )) (LCons( array-base _ )) )) )) (
+         (let rst (mangle-c-declaration-internal array-base))
+         (set pre (.first rst))
+         (set post (+(
+            (.second rst)
+            (+( (+( (SAtom '[_s) (SAtom index) )) (SAtom ']_s) ))
+         )))
+      ))
+      ( _ (
+         (set pre (mangle-c-type tt))
+      ))
+   ))
+   (Tuple( pre post ))
+) Tuple<S,S>);
+
+
+
+
+
diff --git a/SRC/infer-expr.lm b/SRC/infer-expr.lm
@@ -139,7 +139,16 @@ infer-expr := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type)(:
                (exit-error( 'Variable\sName\sIs\sAlready\sBound\sIn\sOuter\sScope_s term ))
             ) ())
          ) ())
-         (infer-expr( tctx rhs Unscoped TAny Tail ))
+         (match rhs (
+            ()
+            ( (App( (Lit( ':_s _ )) (App( (@( u (Var( '__uninitialized_s _ )) )) (AType tt) )) )) (
+               (ascript-normal( u tt ))
+               (ascript-normal( rhs tt ))
+            ))
+            ( _ (
+               (infer-expr( tctx rhs Unscoped TAny Tail ))
+            ))
+         ))
          (let tt (typeof rhs))
          (if (non-zero tt) () (
             (exit-error( 'Unable\sto\sinfer\stype\sof\sexpression_s rhs ))

diff --git a/SRC/type-of-s-with-fields.lm b/SRC/type-of-s-with-fields.lm
@@ -12,12 +12,12 @@ type-of-s-with-fields := λ(: base-type Type)(: tag String)(: compound AST)(: fi
                (add-alias(
                   (clone-rope(SCons( (close(SAtom '._s)) (close(SAtom fn)) )))
                   (clone-rope(SCons( (close(SAtom '._s)) (close(SAtom(to-string field-index))) )))
-                  (t3( 'Arrow_s (and( (t1 tag) base-type )) ft ))
+                  (t3( 'Arrow_s (and( (t2( 'Tag_s (t1 tag) )) base-type )) ft ))
                ))
                (add-alias(
                   (clone-rope(SCons( (close(SAtom 'set._s)) (close(SAtom fn)) )))
                   (clone-rope(SCons( (close(SAtom 'set._s)) (close(SAtom(to-string field-index))) )))
-                  (t3( 'Arrow_s (t3( 'Cons_s (and( (t1 tag) base-type )) ft )) (t1 'Nil_s) ))
+                  (t3( 'Arrow_s (t3( 'Cons_s (and( (t2( 'Tag_s (t1 tag) )) base-type )) ft )) (t1 'Nil_s) ))
                ))
                (set nt ft)
             ))
@@ -33,12 +33,12 @@ type-of-s-with-fields := λ(: base-type Type)(: tag String)(: compound AST)(: fi
                (add-alias(
                   (clone-rope(SCons( (close(SAtom '._s)) (close(SAtom fn)) )))
                   (clone-rope(SCons( (close(SAtom '._s)) (close(SAtom(to-string field-index))) )))
-                  (t3( 'Arrow_s (and( (t1 tag) base-type )) ft ))
+                  (t3( 'Arrow_s (and( (t2( 'Tag_s (t1 tag) )) base-type )) ft ))
                ))
                (add-alias(
                   (clone-rope(SCons( (close(SAtom 'set._s)) (close(SAtom fn)) )))
                   (clone-rope(SCons( (close(SAtom 'set._s)) (close(SAtom(to-string field-index))) )))
-                  (t3( 'Arrow_s (t3( 'Cons_s (and( (t1 tag) base-type )) ft )) (t1 'Nil_s) ))
+                  (t3( 'Arrow_s (t3( 'Cons_s (and( (t2( 'Tag_s (t1 tag) )) base-type )) ft )) (t1 'Nil_s) ))
                ))
               (set nt ft)
             ))

diff --git a/SRC/with-size.lm b/SRC/with-size.lm
@@ -40,6 +40,12 @@ with-size-recurse := λ(: tt Type). (: (
       ( (TGround( 'CaseNumber_s _ )) () )
       ( (TGround( 'Fields_s _ )) () )
       ( (TGround( 'FieldsSized_s _ )) () )
+      ( (TGround( 'Array_s (LCons( array-index (LCons( array-base LEOF )) )) )) (
+         (set tt (TGround( 'Array_s (close(cons(
+            array-index
+            (cons( (with-size array-base) (: LEOF List<Type>) ))
+         ))) )))
+      ))
       ( (TGround( tag ps )) (
          (set tt (TGround( tag (close(with-size ps)) )))
       ))