Merge pull request #1124 from andrew-johnson-4/port-more-lm-to-lsts-2…

…lkfm Port more lm to lsts 2lkfm
andrew-johnson-4 · Jan 19, 2025 · 41b7710 · 41b7710
2 parents 7d3fb5a + 8762d88
commit 41b7710
Show file tree

Hide file tree

Showing 262 changed files with 22,419 additions and 31,088 deletions.
diff --git a/BOOTSTRAP/cli.c b/BOOTSTRAP/cli.c
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.20.26"
+version = "1.20.27"
 authors = ["Andrew <[email protected]>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

diff --git a/PLUGINS/BACKEND/C/compile-c.lm b/PLUGINS/BACKEND/C/compile-c.lm
@@ -26,7 +26,7 @@ plugins-backend-c-compile := λ . (: (
                      global-ctx k kt fragment
                   )))
                ) (
-                  (let repr-tt (+( clean-tt (t1 'GlobalVariable_s) )))
+                  (let repr-tt (&&( clean-tt (t1 'GlobalVariable_s) )))
                   (set.type( fragment (without-constructor repr-tt) ))
                   (set global-ctx (fragment-context::bind(
                      global-ctx k (without-constructor repr-tt) fragment

diff --git a/PLUGINS/BACKEND/C/compile-expr-direct.lm b/PLUGINS/BACKEND/C/compile-expr-direct.lm
@@ -33,7 +33,7 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
                   (set guid (uuid()))
                   (set e (.set( e 'expression_s (SAtom guid) )))
                   (set compile-smart-string-index (.bind( compile-smart-string-index val guid )))
-                  (let lit (Lit( val (token::new val) )))
+                  (let lit (Lit( val (mk-token val) )))
                   (ascript-normal( lit (t1 'String_s) ))
                   (let intern-ss (compile-stack-calls( ctx 'intern_s TAny (typeof term) lit stack-offset Used )))
                   (set assemble-header-section (+(

diff --git a/PLUGINS/BACKEND/GNU-X86/alias.lm b/PLUGINS/BACKEND/GNU-X86/alias.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/align.lm b/PLUGINS/BACKEND/GNU-X86/align.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/and.lm b/PLUGINS/BACKEND/GNU-X86/and.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/apply-or-cons-and-specialize.lm b/PLUGINS/BACKEND/GNU-X86/apply-or-cons-and-specialize.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/apply-plural.lm b/PLUGINS/BACKEND/GNU-X86/apply-plural.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/apply.lm b/PLUGINS/BACKEND/GNU-X86/apply.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/arity.lm b/PLUGINS/BACKEND/GNU-X86/arity.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/as-constant.lm b/PLUGINS/BACKEND/GNU-X86/as-constant.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/ascript-normal.lm b/PLUGINS/BACKEND/GNU-X86/ascript-normal.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/ascript.lm b/PLUGINS/BACKEND/GNU-X86/ascript.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/assert-one-typed.lm b/PLUGINS/BACKEND/GNU-X86/assert-one-typed.lm
diff --git a/PLUGINS/BACKEND/GNU-X86/assert-well-typed.lm b/PLUGINS/BACKEND/GNU-X86/assert-well-typed.lm