Merge pull request #1136 from andrew-johnson-4/port-lm-to-lsts-faaelk

Port lm to lsts faaelk

Cargo.toml

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

SRC/class-info-index.lsts

@@ -0,0 +1,11 @@
+
+type StructLayout = LM1Style | CStyle;
+
+type ClassInfo = ClassInfo { layout: StructLayout };
+let class-info-index = {} :: HashtableEq<Tuple<CString,U64>,ClassInfo>;
+
+let add-class-info(cls: Type, info: ClassInfo): Nil = (
+   class-info-index = class-info-index.bind( cls.ground-tag-and-arity, info );
+);
+
+let .is-class(cls: Type): U64 = class-info-index.has(cls.ground-tag-and-arity);

SRC/class-of-tag.lm

@@ -3,16 +3,7 @@ tag-to-class-index := (: (HashtableEq( 0_u64 0_u64 (as 0_u64 Tuple<String,Type>[
 
 index-class-of-tag := λ(: tag String)(: class Type). (: (
    (set tag-to-class-index (.bind( tag-to-class-index tag class )))
-   (match class (
-      ()
-      ( (TGround( cls _ )) (
-         (set class-to-yes-index (.bind( class-to-yes-index cls 1_u64 )))
-      ))
-      ( _ (
-         (print 'Unexpected\sClass\sIn\sindex-class-of-tag:\s_s)(print class)(print '\n_s)
-         (exit 1_u64)
-      ))
-   ))
+   (add-class-info( class (ClassInfo( LM1Style )) ))
 ) Nil);
 
 class-of-tag := λ(: tag String). (: (

SRC/ground-tag-and-arity.lsts

@@ -0,0 +1,17 @@
+
+let .ground-tag-and-arity(tt: Type): (CString,U64) = (
+   match tt {
+      TGround { tag:c"Array", parameters:[_.. array-base..] } => (
+         let ga = array-base.ground-tag-and-arity;
+         ( ga.first, ga.second + 1000 )
+      );
+      TGround { tag:c"Sized" } => (c"", 9999999);
+      TGround { tag=tag, parameters=parameters } => (tag, parameters.length);
+      TAny {} => (c"?", 0);
+      TVar {} => (c"", 9999999);
+      TAnd { left=left, right=right } => (
+         let lga = left.ground-tag-and-arity;
+         if lga.second==9999999 then right.ground-tag-and-arity else lga
+      );
+   }
+);

SRC/index-ast.lm

@@ -1,5 +1,4 @@
 
-import SRC/is-lm-struct.lm;
 import SRC/plus.lm;
 import SRC/print.lm;
 import SRC/var-name-if-var.lm;

SRC/index-types.lm

@@ -22,7 +22,6 @@ import SRC/class-only-child.lm;
 import SRC/index-of-tag.lm;
 import SRC/size-of-class.lm;
 import SRC/class-of-tag.lm;
-import SRC/is-class.lm;
 import SRC/is-only-child.lsts;
 import SRC/is-sized-array.lsts;
 import SRC/fields-of-tag.lm;

SRC/infer-type-definition.lm

@@ -2,7 +2,6 @@
 infer-type-definition := λ(: base-type Type)(: body AST)(: case-number U64). (: (
    # This works but is too slow
    (mark-class-exists( (tag-of base-type) ))
-   (mark-is-lm-struct( (tag-of base-type) ))
    (let r 0_u64)
    (match body (
       ()

SRC/quick-prop.lsts

@@ -1,23 +1,6 @@
 
 let quick-prop = {} :: HashtableEq<(CString,U64),List<(Type,Type)>>;
 
-let .ground-tag-and-arity(tt: Type): (CString,U64) = (
-   match tt {
-      TGround { tag:c"Array", parameters:[_.. array-base..] } => (
-         let ga = array-base.ground-tag-and-arity;
-         ( ga.first, ga.second + 1000 )
-      );
-      TGround { tag:c"Sized" } => (c"", 9999999);
-      TGround { tag=tag, parameters=parameters } => (tag, parameters.length);
-      TAny {} => (c"?", 0);
-      TVar {} => (c"", 9999999);
-      TAnd { left=left, right=right } => (
-         let lga = left.ground-tag-and-arity;
-         if lga.second==9999999 then right.ground-tag-and-arity else lga 
-      );
-   }
-);
-
 let add-quick-prop(pre: Type, pat: Type, post: Type): Nil = (
    let key = pre.ground-tag-and-arity;
    let val = quick-prop.lookup(key, ([] :: List<(Type,Type)>));

SRC/unit-globals.lsts

@@ -4,3 +4,4 @@ import SRC/typeof-tag.lsts;
 import SRC/tctx-bind.lsts;
 
 # global indexes
+import SRC/class-info-index.lsts;

SRC/unit-types.lsts

@@ -11,6 +11,7 @@ import SRC/p.lsts;
 import SRC/range.lsts;
 import SRC/domain.lsts;
 import SRC/arity.lsts;
+import SRC/ground-tag-and-arity.lsts;
 import SRC/slot.lsts;
 
 # Boolean Queries

SRC/with-only-class.lm

@@ -10,7 +10,7 @@ with-only-class := λ(: tt Type). (: (
          (if (non-zero rc) (set rt rc) ())
       ))
       ( (TGround( tag _ )) (
-         (if (is-class tag) (
+         (if (.is-class tt) (
             (if (not(is-fragment tag)) (
                (set rt tt)
             ) ())