Merge pull request #1134 from andrew-johnson-4/port-lm-to-lsts-fwelio

Port lm to lsts fwelio

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.20.32"
+version = "1.20.33"
 authors = ["Andrew <[email protected]>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

SRC/index-index.lm

@@ -5,6 +5,7 @@ import SRC/unit-types.lsts;
 import SRC/unit-ast.lsts;
 import SRC/unit-inference.lsts;
 import SRC/unit-fragments.lsts;
+import SRC/unit-globals.lsts;
 import SRC/unit-drivers.lsts;
 
 import SRC/index-definitions.lm;

SRC/index-types.lm

@@ -26,7 +26,6 @@ import SRC/is-class.lm;
 import SRC/is-only-child.lsts;
 import SRC/is-sized-array.lsts;
 import SRC/fields-of-tag.lm;
-import SRC/type-constructors.lm;
 import SRC/type-complex-fields.lm;
 import SRC/get-vararg-inner.lm;
 import SRC/maybe-specialize.lm;
@@ -66,7 +65,6 @@ import SRC/type-of-s.lm;
 import SRC/type-of-s-with-fields.lm;
 
 import SRC/typeof-lhs.lm;
-import SRC/typeof-tag.lm;
 import SRC/cons-head.lm;
 import SRC/cons-tail.lm;
 import SRC/parameter-number.lm;

SRC/infer-type-constructor.lm

@@ -21,8 +21,7 @@ infer-type-constructor := λ(: base-type Type)(: body AST). (: (
          (add-quick-prop( (t1(+( 'Tag::_s tag ))) (t3( 'Array_s base-type TAny )) (t2( 'CaseNumber_s (t1(to-string(index-of-tag tag))) )) ))
          (index-class-of-tag( tag base-type ))
          (index-fields-of-tag( tag base-type TAny (t1 'Nil_s) ))
-         (set type-constructors-index (.bind( type-constructors-index tag rtype )))
-         (set r 8_u64)
+         (set global-type-context (.bind( global-type-context tag rtype body )))
          (let constructor-tt (t2( 'Constructor_s (t1 tag) )))
       ))
       ( (App( (Lit( tag _ )) args )) (
@@ -48,9 +47,7 @@ infer-type-constructor := λ(: base-type Type)(: body AST). (: (
          (set-type-fields( base-type atype ))
          (index-class-of-tag( tag base-type ))
          (index-fields-of-tag( tag base-type base-type atype ))
-         (set type-constructors-index (.bind( type-constructors-index tag (t3( 'Arrow_s atype rtype )) )))
-         (set r 8_u64)
-         (let constructor-tt (t2( 'Constructor_s (t1 tag) )))
+         (set global-type-context (.bind( global-type-context tag (t3( 'Arrow_s atype rtype )) body )))
       ))
       ( ASTEOF () )
    ))

SRC/tctx-bind.lsts

@@ -0,0 +1,4 @@
+
+let .bind(tctx: TContext, k: CString, kt: Type, kv: AST): TContext = (
+   TCtxBind { close(tctx), k, kt, kv }
+);

SRC/typeof-tag.lsts

@@ -0,0 +1,4 @@
+
+let typeof-tag(tag: CString): Type = (
+   typeof-var-raw(ASTEOF, global-type-context, tag)
+);

SRC/unit-globals.lsts

@@ -0,0 +1,6 @@
+
+import SRC/typeof-tag.lsts;
+
+import SRC/tctx-bind.lsts;
+
+# global indexes