Merge pull request #1127 from andrew-johnson-4/infer-lm-struct-23mf

Infer lm struct 23mf

Cargo.toml

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

PLUGINS/BACKEND/C/compile-c.lm

@@ -16,7 +16,7 @@ plugins-backend-c-compile := λ . (: (
                   global-ctx k kt fragment
                )))
             ) (
-               (let clean-tt (without-representation kt))
+               (let clean-tt (.without-tag kt))
                (let mid (mangle-identifier( k clean-tt )))
                (set fragment (.set( fragment 'fragment-type_s (SAtom 'Global_s) )))
                (set fragment (.set( fragment 'expression_s (SAtom mid) )))

PLUGINS/BACKEND/C/compile-global.lm

@@ -76,7 +76,7 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
          (set assemble-text-section (SCons( (close assemble-text-section) (close text) )))
       )))
       ( t (
-         (let clean-tt (without-representation kt))
+         (let clean-tt (.without-tag kt))
          (let mid (mangle-identifier( k clean-tt )))
 
          (let e (compile-expr( ctx t 0_i64 Used )))

SRC/denormalize.lm

@@ -2,7 +2,6 @@
 denormalize := λ(: tt Type). (: (
    (set tt (with-size tt))
    (set tt (with-tag tt))
-   (set tt (with-platform-props tt))
    (set tt (enrich-quick-prop tt))
    tt
 ) Type);

SRC/index-types.lm

@@ -52,15 +52,12 @@ import SRC/has-forward.lm;
 import SRC/with-tag.lm;
 import SRC/with-phi.lsts;
 import SRC/with-size.lm;
-import SRC/with-platform-props.lm;
 
 import SRC/without-t.lm;
 import SRC/without-phi.lsts;
 import SRC/without-constructor.lm;
-import SRC/without-representation.lm;
 import SRC/without-size-unless-class.lm;
 import SRC/without-size.lm;
-import SRC/without-platform-props.lm;
 
 import SRC/with-only-class.lm;
 

SRC/infer-expr.lm

@@ -137,7 +137,7 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
             ( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) () )
             ( (TGround( 'Array_s (LCons( TAny (LCons( array-base LEOF )) )) )) (
                (maybe-specialize( 'open_s (typeof-var-raw( term tctx 'open_s )) deref-type ))
-               (set deref-type (&&( array-base (t1 'StackVariable_s) )))
+               (set deref-type array-base)
             ))
             ( _ (do-specialize( 'open_s (typeof-var-raw( term tctx 'open_s )) deref-type term )) )
          ))

SRC/infer-global-context.lm

@@ -50,7 +50,7 @@ infer-global-context-2 := λ(: td AST). (: (
       ( (Glb( k_t rhs )) (
          (infer-expr( global-type-context rhs Unscoped TAny Used ))
          (let rhst (normalize(typeof rhs)))
-         (let kt (&&( (without-representation rhst) (t1 'GlobalVariable_s) )))
+         (let kt (&&( rhst (t1 'GlobalVariable_s) )))
          (set global-type-context (TCtxBind(
             (close global-type-context) k kt td
          )))

SRC/infer-type-definition.lm

@@ -40,5 +40,7 @@ infer-type-definition := λ(: base-type Type)(: body AST)(: case-number U64). (:
          (t2( 'CaseNumber_s (t1 '0_s) ))
       ))
    ) ())
+   (add-quick-prop( (t3( 'Array_s base-type TAny )) TAny (t1 'LMStruct_s) ))
+   (add-quick-prop( base-type TAny (t1 'LMStruct_s) ))
    r
 ) U64);

SRC/normalize.lm

@@ -1,8 +1,6 @@
 
 normalize := λ(: tt Type). (: (
    (let rt tt)
-   (set rt (without-representation rt))
-   (set rt (without-platform-props rt))
    (set rt (.without-tag rt))
    # Sized can serve as a datatype if nothing else is available
    (set rt (without-size-unless-class rt))

SRC/without-tag.lsts

@@ -6,7 +6,14 @@ let .without-tag(tt: Type): Type = (
       TGround { tag:c"Constructor" } => TAny;
       TGround { tag:c"CaseNumber" } => TAny;
       TGround { tag:c"Raw" } => TAny;
-      TGround { tag:tag } => if tag.has-prefix(c"Tag::") then TAny else tt;
+      TGround { tag:c"LMStruct" } => TAny;
+      TGround { tag:c"Constant" } => TAny;
+      TGround { tag:c"Literal" } => TAny;
+      TGround { tag:c"LocalVariable" } => TAny;
+      TGround { tag:c"GlobalVariable" } => TAny;
+      TGround { tag:tag } => if tag.has-prefix(c"Tag::") then TAny
+                        else if tag.has-prefix(c"Field::") then TAny
+                        else tt;
       _ => tt;
    }
 );