Update ast subtrees

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "lambda_mountain"
-version = "1.20.63"
+version = "1.21.14"
 authors = ["Andrew <andrew@subarctic.org>"]
 license = "MIT"
 description = "Typed Macro Assembler (backed by Coq proofs-of-correctness)"

SRC/index-types.lm

@@ -25,7 +25,6 @@ import SRC/typeof-var-raw.lm;
 import SRC/typecheck.lm;
 import SRC/specialize.lm;
 import SRC/infer-type-constructor.lm;
-import SRC/infer-global-context.lm;
 import SRC/assert-well-typed.lm;
 import SRC/assert-one-typed.lm;
 import SRC/infer-ctx.lm;

SRC/infer-global-terms.lsts

@@ -0,0 +1,78 @@
+
+let infer-global-terms(term: AST): AST = (
+   match term {
+      Seq{} => (
+         let seqs = mk-vector(type(AST));
+         while non-zero(term) { match term {
+            Seq{l=left, r=right} => (
+               seqs = seqs.push(r);
+               term = l;
+            );
+         }};
+         let def-i = seqs.length;
+         while def-i > 0 {
+            def-i = def-i - 1;
+            let r = seqs[def-i];
+            let new-r = infer-global-terms(r);
+            if not(is(r,new-r)) then { seqs[def-i] = new-r; };
+         };
+         term = ASTEOF;
+         let def-order-i = seqs.length;
+         while def-order-i > 0 {
+            def-order-i = def-order-i - 1;
+            term = term + seqs[def-order-i];
+         };
+      );
+      Glb{val:Abs{}} => ();
+      Glb{k=key, rhs=val} => (
+         (_, let new-rhs) = std-infer-expr((None :: TContext?), rhs, false, Used, TAny);
+         if not(is(rhs,new-rhs)) then term = mk-glb(k, new-rhs);
+         let kt = normalize(typeof(rhs)) && t1(c"GlobalVariable");
+         global-type-context = global-type-context.bind(k.key, kt, term);
+         mark-global-as-seen(k.key, kt, TAny);
+         ascript-normal(term, kt);
+         maybe-apply-global-callable(c"mov", t3(c"Cons",kt,kt), term);
+      );
+      _ => ();
+   }; term
+);
+
+let infer-global-context(term: AST): Nil = (
+   match term {
+      Seq{} => (
+         let seqs = mk-vector(type(AST));
+         while term.is-seq { match term {
+            Seq{l=left, r=right} => (
+               seqs = seqs.push(r);
+               if l.is-seq
+               then term = l
+               else (term = ASTEOF; seqs = seqs.push(l));
+            );
+         }};
+         let def-i = seqs.length;
+         while def-i > 0 {
+            def-i = def-i - 1;
+            infer-global-context(seqs[def-i]);
+         };
+      );
+      Typedef{ lhs:Lit{base-type=key}, case-constructors=rhs } => (
+         # TODO: remove when LM frontend is removed
+         let bt = parse-type(base-type);
+         infer-type-definition(bt, case-constructors, 0);
+      );
+      Typedef{ lhs:AType{bt=tt}, case-constructors=rhs } => (
+         infer-type-definition(bt, case-constructors, 0);
+      );
+      Glb{ k=key, frhs=val:Abs{lhs=lhs, rhs:App{left:Lit{key:c":"}, right:App{rhs=left, right:AType{return-type=tt}}}, misc-tt=tt} } => (
+         if misc-tt.is-t(c"TypedMacro") then bind-new-macro(k.key, frhs)
+         else {
+            let ft = t3(c"Arrow", typeof-lhs(lhs), return-type) && misc-tt;
+            mark-global-as-seen(k.key, ft, misc-tt);
+            ascript-normal(term, ft);
+            ascript-normal(frhs, ft);
+            global-type-context = global-type-context.bind(k.key, ft, term);
+         };
+      );
+      _ => ();
+   }
+);

SRC/specialize.lm

@@ -16,6 +16,7 @@ specialize := λ(: key String)(: ft Type)(: unify-ctx Maybe<TContext>)(: result-
          (let special-term (substitute( unify-ctx term )))
          (infer-global-context( special-term ))
          (let tctx-special (std-infer-expr( (: None Maybe<TContext>) special-term false Used TAny )))
+         (set special-term (.second tctx-special))
          (set global-type-context (.bind( global-type-context key (typeof special-term) special-term )))
          (set ast-parsed-program (Seq(
             (close ast-parsed-program)

SRC/std-apply-macro.lsts

@@ -19,7 +19,7 @@ let std-apply-macro(tctx: Maybe<TContext>, mname: CString, margs: AST): (TContex
          peeped = mtype;
       };
    };
-   (let peeped-type, _) = std-infer-peeped-arguments(tctx, margs, peep-holes);
+   (let peeped-type, margs) = std-infer-peeped-arguments(tctx, margs, peep-holes);
 
    let matched = [] :: List<(Type,AST)>;
    for Tuple{mtype=first, mterm=third} in row {

SRC/std-infer-expr.lsts

@@ -14,6 +14,7 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
       );
       App{o-t=left:Var{key:c"open"}, r=right} => (
          (tctx, let new-r) = std-infer-expr(tctx, r, false, Used, TAny);
+         if not(is(r,new-r)) then { r = new-r; term = mk-app(o-t, r); };
          let deref-type = typeof(r);
          match deref-type.slot(c"Array") {
             TGround{tag:c"Array", parameters:[_.. TAny{}..]} => ();
@@ -36,38 +37,47 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
       );
       App{szof=left:Var{key:c"scope"}, r=right} => (
          (_, let new-r) = std-infer-expr(tctx, r, true, Tail, TAny);
+         if not(is(r,new-r)) then { r = new-r; term = mk-app(szof, r); };
          ascript-normal(term, typeof(r));
       );
-      App{left:Lit{key:c":"}, right:App{t=left,right:AType{tt=tt}}} => (
+      App{asc=left:Lit{key:c":"}, right:App{t=left,right:AType{tt=tt}}} => (
          tt = tt.rewrite-type-alias;
          add-concrete-type-instance(tt);
          match t {
             Lit{} => ();
-            _ => ((tctx, let new-t) = std-infer-expr(tctx, t, false, Tail, tt));
+            _ => (
+               (tctx, let new-t) = std-infer-expr(tctx, t, false, Tail, tt);
+               if not(is(t,new-t)) then { t = new-t; term = mk-app(asc, mk-app(t, mk-atype(tt))); };
+            );
          };
          ascript-normal(t, tt);
          ascript-normal(term, tt);
          if tt.is-t(c"SmartString") then maybe-apply-global-callable(c"intern", tt, term);
       );
-      App{left:Var{key:c"as"}, right:App{t=left,right:AType{tt=tt}}} => (
+      App{asc=left:Var{key:c"as"}, right:App{t=left,right:AType{tt=tt}}} => (
          tt = tt.rewrite-type-alias;
          add-concrete-type-instance(tt);
          (tctx, let new-t) = std-infer-expr(tctx, t, false, used, TAny);
+         if not(is(t,new-t)) then { t = new-t; term = mk-app(asc, mk-app(t, mk-atype(tt))); };
          let inner-tt = typeof(t);
          if tt.tag.has-prefix(c"Tag::") then tt = tt && inner-tt
          else tt = tt && inner-tt.with-only-class;
          ascript-normal(term, tt);
       );
-      App{left:App{ left:App{ left:Var{key:c"if"}, cond=right }, t=right }, f=right} => (
+      App{left:App{ left:App{ ifv=left:Var{key:c"if"}, cond=right }, t=right }, f=right} => (
          if is-scoped {
             (let tctx-inner, let new-cond) = std-infer-expr(tctx, cond, false, Used, TAny);
             (_, let new-t) = std-infer-expr(tctx-inner, t, false, Tail, TAny);
             (_, let new-f) = std-infer-expr(tctx, f, false, Tail, TAny);
+            if not(is(cond,new-cond)) || not(is(t,new-t)) || not(is(f,new-f))
+            then { term = mk-app(mk-app(mk-app(ifv,new-cond),new-t),new-f) };
          } else {
             (tctx, let new-cond) = std-infer-expr(tctx, cond, false, Used, TAny);
             (let tctx-t, let new-t) = std-infer-expr(tctx, t, false, Tail, TAny);
             (_, let new-f) = std-infer-expr(tctx, f, false, Tail, TAny);
             tctx = tctx-t;
+            if not(is(cond,new-cond)) || not(is(t,new-t)) || not(is(f,new-f))
+            then { term = mk-app(mk-app(mk-app(ifv,new-cond),new-t),new-f) };
          };
          ascript-normal(term, typeof(t)); # TODO: use MGU to merge true and false branches
       );
@@ -77,32 +87,32 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
       Typedef{} => ();
       AType{tt=tt} => ascript-normal(term, tt);
       Seq{} => (
-         let seqs = [] :: List<AST>;
-         let is-diff = false as U64;
-         while term.is-seq { match term {
+         let seqs = mk-vector(type(AST));
+         while non-zero(term) { match term {
             Seq{l=left, r=right} => (
-               (tctx, let new-r) = std-infer-expr(tctx, r, false, Used, hint);
-               is-diff = is-diff || not(is(r,new-r));
-               seqs = cons(new-r,seqs);
-               term = l;
+               seqs = seqs.push(r);
+               term = l
             );
          }};
-         if is-diff {
-            term = ASTEOF;
-            for r in seqs {
-               if non-zero(term)
-               then term = mk-seq(term, r)
-               else term = r
-            };
-         }
+         let def-i = seqs.length;
+         while def-i > 0 {
+            def-i = def-i - 1;
+            let r = seqs[def-i];
+            (_, let new-r) = std-infer-expr(tctx, seqs[def-i], false, Used, hint);
+            if not(is(r,new-r)) then { seqs[def-i] = new-r; };
+         };
+         term = ASTEOF;
+         let def-order-i = seqs.length;
+         while def-order-i > 0 {
+            def-order-i = def-order-i - 1;
+            term = term + seqs[def-order-i]
+         };
       );
       Glb{key=key, val=val} => (
-         # TODO: remove after infer-expr.lm is ported
-         #(tctx, let new-val) = std-infer-expr(tctx, val, false, Used);
-         #if not(is(val,new-val)) then term = mk-glb(key, val);
          let rough-tt = typeof(term);
          if rough-tt.is-arrow && not(rough-tt.is-open) {
             (_, let new-val) = std-infer-expr(tctx, val, is-scoped, Used, TAny);
+            if not(is(val,new-val)) then { term = mk-glb(key,new-val); };
          };
       );
       Var{key=key, token=token} => (
@@ -119,9 +129,11 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
             }
          }
       );
-      Abs{lhs=lhs, rhs=rhs:App{left:Lit{key:c":"},right:App{inner-rhs=left, right:AType{return-type=tt}}}, misc-tt=tt} => (
+      Abs{lhs=lhs, rhs=rhs:App{asc=left:Lit{key:c":"},right:App{inner-rhs=left, right:AType{return-type=tt}}}, misc-tt=tt} => (
          tctx = infer-ctx(tctx, lhs);
          (_, let new-inner-rhs) = std-infer-expr(tctx, inner-rhs, false, Tail, return-type);
+         if not(is(inner-rhs,new-inner-rhs))
+         then { inner-rhs = new-inner-rhs; term = mk-abs(lhs, mk-app(asc,mk-app(inner-rhs,mk-atype(return-type))), misc-tt) };
          if not(misc-tt.is-t(c"Blob")) && not(misc-tt.is-t(c"C-FFI")) then ascript-normal(inner-rhs, return-type);
          ascript-normal(rhs, return-type);
          let domain-tt = typeof-lhs(lhs);
@@ -131,20 +143,23 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
          if is-cons {
             (tctx, let new-l) = std-infer-expr(tctx, l, false, Used, TAny);
             (tctx, let new-r) = std-infer-expr(tctx, r, false, Used, TAny);
+            if not(is(l,new-l)) || not(is(r,new-r)) then { term = mk-cons(new-l, new-r) };
             ascript-normal(term, if is(used, Tail) then typeof(r) else t3(c"Cons", typeof(l), typeof(r)));
          } else {
             let rt = TAny;
             if var-name-if-var(l)==c"list::cons" { match r {
                App{k=left, m=right} => (
                   (_, let new-k) = std-infer-expr(tctx, k, false, Call, TAny);
                   (_, let new-m) = std-infer-expr(tctx, m, false, Used, t2(c"List",normalize(typeof(k))));
+                  if not(is(k,new-k)) || not(is(m,new-m)) then { r = mk-cons(new-k, new-m) };
                );
                _ => ();
             }};
             if var-name-if-var(l)==c"map::cons" { match r {
                App{kv=left, m=right} => (
                   (_, let new-kv) = std-infer-expr(tctx, kv, false, Call, TAny);
                   (_, let new-m) = std-infer-expr(tctx, m, false, Used, t3(c"HashtableEq",normalize(typeof(kv)).r2,normalize(typeof(kv)).r1));
+                  if not(is(kv,new-kv)) || not(is(m,new-m)) then { r = mk-cons(new-kv, new-m) };
                );
                _ => ();
             }};
@@ -155,8 +170,10 @@ let std-infer-expr(tctx: Maybe<TContext>, term: AST, is-scoped: Bool, used: IsUs
                (tctx, let new-l) = std-infer-expr(tctx, l, false, used, TAny);
                if typeof(l).is-arrow {
                   (tctx, let new-r) = std-infer-expr(tctx, r, false, Call, TAny);
+                  if not(is(l,new-l)) || not(is(r,new-r)) then { l = new-l; r = new-r; term = mk-app(l,r); };
                } else {
                   (tctx, let new-r) = std-infer-expr(tctx, r, false, Used, TAny);
+                  if not(is(l,new-l)) || not(is(r,new-r)) then { l = new-l; r = new-r; term = mk-app(l,r); };
                };
                rt = if typeof(l).is-arrow && non-zero(var-name-if-var-or-lit(l)) {
                   apply-global-callable(var-name-if-var-or-lit(l), typeof(r), term);

SRC/typecheck.lm

@@ -1,30 +1,9 @@
 
 typecheck := λ. (: (
-   (let p ast-parsed-program)
-   (let ordered-type-exprs ASTEOF)
-   (while (non-zero p) (match p (
-      ()
-      ( (Seq( rst r )) (
-         (set ordered-type-exprs (Seq( (close ordered-type-exprs) (close r) )))
-         (set p rst)
-      ))
-   )))
-   (let preordered-type-exprs ordered-type-exprs)
-   (while (non-zero preordered-type-exprs) (match preordered-type-exprs (
-      ()
-      ( (Seq( rst r )) (
-         (infer-global-context( r ))
-         (set preordered-type-exprs rst)
-      ))
-   )))
-   (while (non-zero ordered-type-exprs) (match ordered-type-exprs (
-      ()
-      ( (Seq( rst r )) (
-         (infer-global-context-2( r ))
-         (set ordered-type-exprs rst)
-      ))
-   )))
+   (infer-global-context ast-parsed-program)
+   (set ast-parsed-program (infer-global-terms ast-parsed-program))
    (let tctx-ast (std-infer-expr( (: None Maybe<TContext>) ast-parsed-program false Used TAny )))
+   (set ast-parsed-program (.second tctx-ast))
    (while (non-zero stack-to-specialize) (match stack-to-specialize (
       ()
       ( (LCons( (StackToSpecialize( function-name ft unify-ctx special-type )) rst )) (

SRC/unit-orphans.lsts

@@ -16,3 +16,4 @@ import SRC/macro-table.lsts;
 import SRC/std-apply-macro.lsts;
 import SRC/std-apply-macro-candidates.lsts;
 import SRC/std-direct-destructure-macro.lsts;
+import SRC/infer-global-terms.lsts;