Merge pull request #1164 from andrew-johnson-4/cleanup-lm-to-lsts

Cleanup lm to lsts

Cargo.toml

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

PLUGINS/BACKEND/C/compile-c.lm

@@ -27,9 +27,8 @@ plugins-backend-c-compile := λ . (: (
                   )))
                ) (
                   (let repr-tt (&&( clean-tt (t1 'GlobalVariable_s) )))
-                  (set.type( fragment (without-constructor repr-tt) ))
                   (set global-ctx (.bind(
-                     global-ctx k (without-constructor repr-tt) fragment
+                     global-ctx k repr-tt fragment
                   )))
                ))
             ))

PLUGINS/BACKEND/C/compile-destructure-args.lm

@@ -9,7 +9,7 @@ compile-destructure-args := λ(: tt Type)(: ctx FContext)(: lhs AST)(: offset I6
             (if is-fragment (
                (set kt (denormalize kt))
             ) (
-               (set kt (maybe-local-variable(denormalize kt)))
+               (set kt (&&( (normalize(denormalize kt)) (t1 'LocalVariable_s) )))
             ))
             (set ctx (.bind(
                ctx k kt (fragment::local-variable( 0_i64 kt ))
@@ -20,7 +20,7 @@ compile-destructure-args := λ(: tt Type)(: ctx FContext)(: lhs AST)(: offset I6
          (if is-fragment (
             (set kt (denormalize kt))
          ) (
-            (set kt (maybe-local-variable(denormalize kt)))
+            (set kt (&&( (normalize(denormalize kt)) (t1 'LocalVariable_s) )))
          ))
          (set ctx (.bind(
             ctx k kt (fragment::local-variable( 0_i64 kt ))

PLUGINS/BACKEND/C/mangle-identifier.lm

@@ -82,7 +82,7 @@ mangle-identifier := λ(: k String)(: kt Type). (: (
       (close(mangle-identifier k))
       (close(SCons(
          (close(SAtom( '_CL__s )))
-         (close(mangle-identifier(without-phi(normalize kt))))
+         (close(mangle-identifier(normalize kt)))
       )))
    )))
    (clone-rope cs)

SRC/index-types.lm

@@ -18,7 +18,6 @@ import SRC/index-of-tag.lm;
 import SRC/is-sized-array.lsts;
 import SRC/get-vararg-inner.lm;
 import SRC/maybe-specialize.lm;
-import SRC/maybe-local-variable.lm;
 
 import SRC/is-constructor.lm;
 
@@ -41,8 +40,6 @@ import SRC/with-phi.lsts;
 import SRC/with-size.lm;
 
 import SRC/without-t.lm;
-import SRC/without-phi.lsts;
-import SRC/without-constructor.lm;
 import SRC/without-size-unless-class.lm;
 import SRC/without-size.lm;
 

SRC/infer-ctx.lm

@@ -3,14 +3,14 @@ infer-ctx := λ(: tctx TContext)(: lhs AST). (: (
    (match lhs (
       ()
       ( (App( (Lit( ':_s _ )) (App( (Var( v vtk )) (AType tt) )) )) (
-         (set tt (maybe-local-variable(denormalize tt)))
+         (set tt (&&( (normalize(denormalize tt)) (t1 'LocalVariable_s) )))
          (set tctx (TCtxBind(
             (close tctx) v tt (Var( v vtk ))
          )))
          (set tctx (infer-tctx( tctx tt )))
       ))
       ( (App( ps (App( (Lit( ':_s _ )) (App( (Var( v vtk )) (AType tt) )) )) )) (
-         (set tt (maybe-local-variable(denormalize tt)))
+         (set tt (&&( (normalize(denormalize tt)) (t1 'LocalVariable_s) )))
          (set tctx (TCtxBind(
             (close tctx) v tt (Var( v vtk ))
          )))

SRC/infer-expr.lm

@@ -164,7 +164,7 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          (if (non-zero tt) () (
             (exit-error( 'Unable\sto\sinfer\stype\sof\sexpression_s rhs ))
          ))
-         (set tt (maybe-local-variable(without-constructor tt)))
+         (set tt (&&( (normalize tt) (t1 'LocalVariable_s) )))
          (match term (
             ()
             ( (App( (Abs( lname-var _ _ )) _ )) (

SRC/normalize.lsts

@@ -7,7 +7,6 @@ let normalize(tt: Type): Type = (
       ct = tt.rewrite-type-alias;
       ct = ct.without-tag;
       ct = without-size-unless-class(ct);
-      ct = without-phi(ct);
       ct = weaken-quick-prop(ct);
       normalize-cache = normalize-cache.bind(tt, ct);
       ct

SRC/quick-prop.lsts

@@ -39,6 +39,11 @@ let enrich-quick-prop(base: Type, pre: Type): Type = (
 
 let weaken-quick-prop-index = {} :: HashtableEq<(CString,U64),List<(Type,Type)>>;
 
+# core implicit weakening rules
+add-weaken-quick-prop( t2(c"Phi",TAny), t2(c"Phi",TAny), t2(c"Phi",TAny) );
+add-weaken-quick-prop( t2(c"Constructor",TAny), t2(c"Constructor",TAny), t2(c"Constructor",TAny) );
+add-weaken-quick-prop( t2(c"CaseNumber",TAny), t2(c"CaseNumber",TAny), t2(c"CaseNumber",TAny) );
+
 let add-weaken-quick-prop(pre: Type, pat: Type, post: Type): Nil = (
    let key = pre.ground-tag-and-arity;
    let val = weaken-quick-prop-index.lookup(key, ([] :: List<(Type,Type)>));