Merge pull request #1199 from andrew-johnson-4/lm-to-lsts-fadwpw

Lm to lsts fadwpw

Cargo.toml

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

PLUGINS/BACKEND/C/compile-stack-call.lm

@@ -26,8 +26,6 @@ compile-stack-call := λ(: ctx FContext)(: f Fragment)(: function-name String)(:
 
          (set ictx (.set( ictx 'function-id_s (SAtom function-id) )))  
          (set ictx (.set( ictx 'function-name_s (SAtom function-name) )))
-         (set ictx (.set( ictx 'used_s (SAtom(to-string used)) )))
-         (set.type( ictx (t1( 'ImplicitContext_s )) ))
          (set ctx (.bind( ctx 'ictx_s (t1 'ImplicitContext_s) ictx )))
 
          (let args-tt (.type push-args))

PLUGINS/FRONTEND/LM/index-index.lm

@@ -15,4 +15,5 @@ import PLUGINS/FRONTEND/LM/parse-type.lm;
 import PLUGINS/FRONTEND/LM/parse.lm;
 import PLUGINS/FRONTEND/LM/lm-is-variable.lm;
 import PLUGINS/FRONTEND/LM/lm-type-of-s.lm;
+import PLUGINS/FRONTEND/LM/remove-parens.lm;
 

SRC/cons-tail.lm

@@ -1,14 +1,4 @@
 
-cons-tail := λ(: tt Type). (: (
-   (let r TAny)
-   (match tt (
-      ()
-      ( (TGround( 'Cons_s (LCons( tl (LCons( hd LEOF )) )) )) (set r tl) )
-      ( _ () )
-   ))
-   r
-) Type);
-
 cons-tail-or-self := λ(: tt Type). (: (
    (match tt (
       ()

SRC/index-ast.lm

@@ -1,5 +1,3 @@
 
-import SRC/plus.lm;
 import SRC/print.lm;
 import SRC/var-name-if-var.lm;
-import SRC/remove-parens.lm;

SRC/index-types.lm

@@ -34,7 +34,6 @@ import SRC/has-forward.lm;
 import SRC/type-of-s-with-fields.lm;
 
 import SRC/typeof-lhs.lm;
-import SRC/cons-head.lm;
 import SRC/cons-tail.lm;
 import SRC/apply.lm;
 import SRC/apply.lsts;
@@ -45,7 +44,6 @@ import SRC/try-specialize.lm;
 
 import SRC/unify-hint.lm;
 import SRC/infer-type-definition.lm;
-import SRC/cons-arity.lm;
 import SRC/typeof-var.lm;
 import SRC/typeof-var-raw.lm;
 

SRC/index-utility.lm

@@ -2,5 +2,3 @@
 import SRC/index-definitions.lm;
 
 import SRC/error-formatting.lm;
-import SRC/to-string.lm;
-import SRC/is-equal.lm;

SRC/plus.lsts

@@ -0,0 +1,11 @@
+
+let $"+"(l: AST, r: AST): AST = (
+   match r {
+      ASTEOF{} => ();
+      Seq{left=left,right=right} => (
+         l = l + left;
+         l = l + right;
+      );
+      re => l = Seq{close(l), close(re)};
+   }; l
+);

SRC/type-cmp.lsts

@@ -9,7 +9,7 @@ let cmp(left: Type, right: Type): Ord = (
       });
       TAnd{ left-left=left, left-right=right } => (match right {
          TAnd{ right-left=left, right-right=right } => (
-            cmp(left-left,right-left) && cmp(right-left, right-right);
+            cmp(left-left,right-left) && cmp(left-right, right-right);
          );
          _ => cmp($".0"(left), $".0"(right));
       });

SRC/unit-ast.lsts

@@ -8,3 +8,4 @@ import SRC/is-seq.lsts;
 import SRC/non-zero.lsts;
 import SRC/uuid.lsts;
 import SRC/smart-token-location.lsts;
+import SRC/plus.lsts;