Merge pull request #1178 from andrew-johnson-4/lm-to-lsts-faewpq

Lm to lsts faewpq

Cargo.toml

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

PLATFORM/C/LIB/default.lm

@@ -35,6 +35,7 @@ import PLATFORM/C/LIB/s.lsts;
 import PLATFORM/C/LIB/tuple.lsts;
 import PLATFORM/C/LIB/list.lm;
 import PLATFORM/C/LIB/list.lsts;
+import PLATFORM/C/LIB/maybe.lsts;
 import PLATFORM/C/LIB/vector.lsts;
 import PLATFORM/C/LIB/hashtable.lm;
 import PLATFORM/C/LIB/hashtable.lsts;

PLATFORM/C/LIB/list.lm

@@ -1,5 +1,5 @@
 
-type List<x> LEOF | (LCons( x , List<x>[] )); zero List<x> LEOF;
+type List<x> LEOF | (LCons( head:x , tail:List<x>[] )); zero List<x> LEOF;
 
 cons := λ(: hd x)(: tl List<x>). (: (
    (set tl (LCons( hd (close tl) )))

PLATFORM/C/LIB/maybe.lsts

@@ -0,0 +1,24 @@
+
+type Maybe<x> = Some { content:x } | None;
+zero Maybe<x> = None;
+
+let .get-or(m: Maybe<x>, default: x): x = (
+   match m {
+      Some{content=content} => content;
+      None{} => default;
+   }
+);
+
+let .is-none(m: Maybe<x>): U64 = (
+   match m {
+      Some{} => false;
+      None{} => true;
+   }
+);
+
+let .is-some(m: Maybe<x>): U64 = (
+   match m {
+      Some{} => true;
+      None{} => false;
+   }
+);

PLUGINS/BACKEND/C/compile-c-typedef.lm

@@ -28,11 +28,11 @@ compile-c-typedef-ordinal := λ(: base-type Type). (: (
    ) ())
 ) Nil);
 
-continue-compile-c-typedefs-concrete := (: LEOF List<Tuple<Tuple<TContext,Type>,AST>>);
+continue-compile-c-typedefs-concrete := (: LEOF List<Tuple<Tuple<Maybe<List<Tuple<String,Type,AST>>>,Type>,AST>>);
 continue-compile-c-typedefs-count := 0_u64;
 try-continue-compile-c-typedefs := λ. (: (
    (let continue continue-compile-c-typedefs-concrete)
-   (set continue-compile-c-typedefs-concrete (: LEOF List<Tuple<Tuple<TContext,Type>,AST>>))
+   (set continue-compile-c-typedefs-concrete (: LEOF List<Tuple<Tuple<Maybe<List<Tuple<String,Type,AST>>>,Type>,AST>>))
    (while (non-zero continue) (
       (set continue-compile-c-typedefs-count (+( continue-compile-c-typedefs-count 1_u64 )))
       (if (>( continue-compile-c-typedefs-count 100_u64 )) (
@@ -48,7 +48,7 @@ try-continue-compile-c-typedefs := λ. (: (
          ))
       ))
       (set continue continue-compile-c-typedefs-concrete)
-      (set continue-compile-c-typedefs-concrete (: LEOF List<Tuple<Tuple<TContext,Type>,AST>>))
+      (set continue-compile-c-typedefs-concrete (: LEOF List<Tuple<Tuple<Maybe<List<Tuple<String,Type,AST>>>,Type>,AST>>))
    ))
 ) Nil);
 
@@ -147,7 +147,7 @@ compile-c-typedef := λ(: base-type Type)(: body AST). (: (
    (set compile-c-type-body-of-base-type (.bind( compile-c-type-body-of-base-type (tag-of base-type) (Tuple( base-type body )) )))
    (if (.is-lm-struct base-type) (
       (if (.is-open base-type) () (
-         (compile-c-typedef-concrete( TCtxEOF base-type body ))
+         (compile-c-typedef-concrete( (: None TContext) base-type body ))
       ))
       (match base-type (
          ()

SRC/apply.lsts

@@ -45,16 +45,14 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
          let fpt = sft.domain;
          let ctx = unify(fpt, parameters);
          let phi-ctx = ctx;
-         while non-zero(phi-ctx) { match phi-ctx {
-            TCtxBind { rst=ctx, key:c"Phi::Transition", typ=typ, term:Var{ pid=key } } => (
-               phi-types = cons( Tuple{ pid, typ }, phi-types );
-               phi-ctx = rst;
-            );
-            TCtxBind { rst=ctx, key=key, typ=typ } => (
-               phi-ctx = rst;
-            );
-            _ => (phi-ctx = TCtxEOF {};);
-         } };
+         for phi-row in phi-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+            match phi-row {
+               Tuple{ first:c"Phi::Transition", typ=second, third:Var{pid=key} } => (
+                  phi-types = cons( Tuple{ pid, typ }, phi-types );
+               );
+               _ => ();
+            }
+         };
          let closed-type = substitute( ctx, sft );
          function-type = closed-type;
          if not(r.is-t( c"Error: Did Not Close Before Specialization")) {

SRC/ast-definitions.lsts

@@ -17,3 +17,5 @@ zero AST = ASTEOF;
 
 # constructor with a default argument
 let $"App"(left: AST[], right: AST[]): AST = App { false, left, right };
+
+type TContext is Maybe<List<Tuple<CString,Type,AST>>>;

SRC/ctx-union.lsts

@@ -0,0 +1,8 @@
+
+let union(ctx: FContext, tctx: TContext): FContext = (
+   let r = ctx;
+   for Tuple{ k=first, vt=second } in tctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      r = FCtxBind{ close(r), k, TAny, mk-fragment() };
+   };
+   r
+);

SRC/fctx-lookup.lsts

@@ -49,14 +49,15 @@ let .lookup(ctx: FContext, k: CString, kt: Type, sloc: AST, hard: U64): Fragment
       );
    }};
    if not(non-zero(found)) && hard {
-      print("Context::lookup \{k} : "); print(kt); print("\nCandidates:\n");
+      print("Context::lookup \{k} : \{kt}\nCandidates:\n");
       while non-zero(original-ctx) { match original-ctx {
          FCtxBind { remainder=remainder, ctx-k=k, ctx-kt=kt } => (
-            if k==ctx-k { print("\{k} : "); print(kt); print("\n"); };
+            if k==ctx-k { print("\{k} : \{ctx-kt}\n"); };
             original-ctx = remainder;
          );
       }};
-      print("Context::lookup Could Not Find Symbol\n"); exit(1);
+      print("Context::lookup Could Not Find Symbol at \{sloc.location}\n");
+      exit(1);
    };
    r
 );

SRC/index-definitions.lm

@@ -20,7 +20,7 @@ type MacroList MEOF | (MSeq( MacroList[] , Macro )); zero MacroList MEOF;
 
 type ParsePartial (PME( AST , List<Token> )); # term, remainder
 
-type StackToSpecialize (StackToSpecialize( String , Type , TContext , Type ));
+type StackToSpecialize (StackToSpecialize( String , Type , Maybe<List<Tuple<String,Type,AST>>> , Type ));
 
 type ApplyResult (ApplyResult( function-type:Type , return-type:Type , phi-types:List<Tuple<String,Type>> ));
 

SRC/index-types.lm

@@ -57,3 +57,5 @@ import SRC/assert-well-typed.lm;
 import SRC/assert-one-typed.lm;
 import SRC/infer-ctx.lm;
 import SRC/infer-tctx.lm;
+
+import SRC/ctx-union.lsts;

SRC/infer-expr.lm

@@ -38,6 +38,7 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
       ))
       ( (Glb( k v )) () ) # globals should already be inferred by now
       ( (App( (Lit( ':_s _ )) (App( (Lit( _ _ )) (AType tt) )) )) (
+         (set tt (.rewrite-type-alias tt))
          (add-concrete-type-instance tt)
          (match term (
             ()
@@ -60,6 +61,7 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          ))
       ))
       ( (App( (Lit( ':_s _ )) (App( t (AType tt) )) )) (
+         (set tt (.rewrite-type-alias tt))
          (set tctx (infer-expr( tctx t Unscoped tt used )))
          (let inner-tt (typeof t))
          (if (non-zero inner-tt) (
@@ -92,6 +94,7 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          (ascript-normal( term (typeof t) ))
       ))
       ( (App( (Var( 'as_s _ )) (App( t (AType tt) )) )) (
+         (set tt (.rewrite-type-alias tt))
          (add-concrete-type-instance tt)
          (set tctx (infer-expr( tctx t Unscoped TAny used )))
          (let inner-tt (typeof t))

SRC/infer-global-context.lm

@@ -33,13 +33,13 @@ infer-global-context-2 := λ(: td AST). (: (
       ( (Glb( k_t (@( frhs (Abs( lhs (App( (Lit( ':_s _ )) (App( rhs (AType rhst) )) )) tlt )) )) )) (
       ))
       ( (Glb( k_t rhs )) (
-         (infer-expr( TCtxEOF rhs Unscoped TAny Used ))
+         (infer-expr( (: None TContext) rhs Unscoped TAny Used ))
          (let rhst (normalize(typeof rhs)))
          (let kt (&&( rhst (t1 'GlobalVariable_s) )))
          (set global-type-context (.bind( global-type-context k kt td )))
          (mark-global-as-seen( k kt TAny ))
          (ascript-normal( td kt ))
-         (maybe-specialize( 'mov_s (typeof-var-raw( rhs TCtxEOF 'mov_s )) (t3( 'Cons_s kt kt )) ))
+         (maybe-specialize( 'mov_s (typeof-var-raw( rhs (: None TContext) 'mov_s )) (t3( 'Cons_s kt kt )) ))
       ))
       ( _ () )
    ))

SRC/inference-definitions.lsts

@@ -1,5 +1,2 @@
 
-type TContext = TCtxEOF | TCtxNil
-              | TCtxBind { ctx: TContext[], key: CString, typ: Type, term: AST };
-zero TContext = TCtxEOF;
 

SRC/phi-merge.lsts

@@ -2,54 +2,38 @@
 let phi-merge(ctx: TContext, weak-ctx: TContext): TContext = (
    let iter-ctx = ctx;
    let left-phi-ids = [] :: List<CString>;
-   while non-zero(iter-ctx) { match iter-ctx {
-      TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-         left-phi-ids = left-phi-ids + typ.phi-ids;
-         iter-ctx = rst;
-      );
-      _ => (iter-ctx = TCtxEOF {});
-   }};
+   for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      left-phi-ids = left-phi-ids + typ.phi-ids;
+   };
    iter-ctx = weak-ctx;
    let right-phi-ids = [] :: List<CString>;
-   while non-zero(iter-ctx) { match iter-ctx {
-      TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-         right-phi-ids = right-phi-ids + typ.phi-ids;
-         iter-ctx = rst;
-      );
-      _ => (iter-ctx = TCtxEOF {});
-   }};
+   for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      right-phi-ids = right-phi-ids + typ.phi-ids;
+   };
    for lid in left-phi-ids.unique {
       if right-phi-ids.contains(lid) {
          iter-ctx = ctx;
          let left-key = c"";
          let left-typ = TAny {};
          let left-term = ASTEOF {};
-         while non-zero(iter-ctx) { match iter-ctx {
-            TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-               if typ.contains-phi(lid) {
-                  left-key = key;
-                  left-typ = typ.get-phi(lid);
-                  left-term = term;
-                  iter-ctx = TCtxEOF {};
-               } else {
-                  iter-ctx = rst;
-               }
-            );
-            _ => (iter-ctx = TCtxEOF {});
-         }};
+         let found = false;
+         for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+            if not(found) && typ.contains-phi(lid) {
+               left-key = key;
+               left-typ = typ.get-phi(lid);
+               left-term = term;
+               found = true;
+            };
+         };
          iter-ctx = weak-ctx;
          let right-typ = TAny {};
-         while non-zero(iter-ctx) { match iter-ctx {
-            TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-               if typ.contains-phi(lid) {
-                  right-typ = typ.get-phi(lid);
-                  iter-ctx = TCtxEOF {};
-               } else {
-                  iter-ctx = rst;
-               }
-            );
-            _ => (iter-ctx = TCtxEOF {});
-         }};
+         found = false;
+         for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+            if not(found) && typ.contains-phi(lid) {
+               right-typ = typ.get-phi(lid);
+               found = true;
+            };
+         };
          let merge-result = apply-blame(c"phi", typeof-var-raw(left-term, ctx, c"phi"), t3(c"Cons", left-typ, right-typ), 0, left-term);
          if not(left-typ == merge-result.return-type) {
             ctx = ctx.bind( left-key, t3(c"Phi", t1(lid), merge-result.return-type), left-term );
@@ -62,54 +46,38 @@ let phi-merge(ctx: TContext, weak-ctx: TContext): TContext = (
 let phi-override(ctx: TContext, weak-ctx: TContext): TContext = (
    let iter-ctx = ctx;
    let left-phi-ids = [] :: List<CString>;
-   while non-zero(iter-ctx) { match iter-ctx {
-      TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-         left-phi-ids = left-phi-ids + typ.phi-ids;
-         iter-ctx = rst;
-      );
-      _ => (iter-ctx = TCtxEOF {});
-   }};
+   for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      left-phi-ids = left-phi-ids + typ.phi-ids;
+   };
    iter-ctx = weak-ctx;
    let right-phi-ids = [] :: List<CString>;
-   while non-zero(iter-ctx) { match iter-ctx {
-      TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-         right-phi-ids = right-phi-ids + typ.phi-ids;
-         iter-ctx = rst;
-      );
-      _ => (iter-ctx = TCtxEOF {});
-   }};
+   for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      right-phi-ids = right-phi-ids + typ.phi-ids;
+   };
    for lid in left-phi-ids.unique {
       if right-phi-ids.contains(lid) {
          iter-ctx = ctx;
          let left-key = c"";
          let left-typ = TAny {};
          let left-term = ASTEOF {};
-         while non-zero(iter-ctx) { match iter-ctx {
-            TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-               if typ.contains-phi(lid) {
-                  left-key = key;
-                  left-typ = typ.get-phi(lid);
-                  left-term = term;
-                  iter-ctx = TCtxEOF {};
-               } else {
-                  iter-ctx = rst;
-               }
-            );
-            _ => (iter-ctx = TCtxEOF {});
-         }};
+         let found = false;
+         for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+            if not(found) && typ.contains-phi(lid) {
+               left-key = key;
+               left-typ = typ.get-phi(lid);
+               left-term = term;
+               found = true;
+            };
+         };
          iter-ctx = weak-ctx;
          let right-typ = TAny {};
-         while non-zero(iter-ctx) { match iter-ctx {
-            TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-               if typ.contains-phi(lid) {
-                  right-typ = typ.get-phi(lid);
-                  iter-ctx = TCtxEOF {};
-               } else {
-                  iter-ctx = rst;
-               }
-            );
-            _ => (iter-ctx = TCtxEOF {});
-         }};
+         found = false;
+         for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+            if not(found) && typ.contains-phi(lid) {
+               right-typ = typ.get-phi(lid);
+               found = true;
+            };
+         };
          if not(left-typ == right-typ) {
             ctx = ctx.bind( left-key, t3(c"Phi", t1(lid), right-typ), left-term );
          };

SRC/phi-transition.lsts

@@ -1,17 +1,13 @@
 
 let phi-transition(ctx: TContext, phi-id: CString, phi-new-type: Type): TContext = (
    let iter-ctx = ctx;
-   while non-zero(iter-ctx) { match iter-ctx {
-      TCtxBind { rst=ctx, key=key, typ=typ, term=term } => (
-         if typ.contains-phi(phi-id) {
-            ctx = ctx.bind( key, typ.replace-phi(phi-id, phi-new-type), term );
-            iter-ctx = TCtxEOF {};
-         } else {
-            iter-ctx = rst;
-         }
-      );
-      _ => (iter-ctx = TCtxEOF {});
-   }};
+   let found = false;
+   for Tuple{ key=first, typ=second, term=third } in iter-ctx.get-or([] :: List<Tuple<CString,Type,AST>>) {
+      if not(found) && typ.contains-phi(phi-id) {
+         ctx = ctx.bind( key, typ.replace-phi(phi-id, phi-new-type), term );
+         found = true;
+      };
+   };
    ctx
 );
 

SRC/specialize.lm

@@ -16,7 +16,7 @@ specialize := λ(: key String)(: ft Type)(: unify-ctx TContext)(: result-type Ty
       (if (non-zero term) (
          (let special-term (substitute( unify-ctx term )))
          (infer-global-context( special-term ))
-         (infer-expr( TCtxEOF special-term Unscoped TAny Used ))
+         (infer-expr( (: None TContext) special-term Unscoped TAny Used ))
          (set ast-parsed-program (Seq(
             (close ast-parsed-program)
             (close special-term)

SRC/substitute.lm

@@ -125,38 +125,36 @@ substitute := λ(: tctx TContext)(: t AST). (: (
             (close(Lit( v (unique vtk) )))
             (close(AType( (substitute( tctx vt )) )))
          ))) )))
-         (while (non-zero tctx) (match tctx (
-            ()
-            ( TCtxNil (set tctx TCtxEOF) )
-            ( (TCtxBind( rst tk tv ta )) (
-               (if (==( tk v )) (
-                  (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
-                     (close(substitute( tctx ta )))
-                     (close(AType( (substitute( tctx vt )) )))
-                  ))) )))
-                  (set tctx TCtxEOF)
-               ) (set tctx rst))
-            ))
-         )))
+         (let found 0_u64)
+         (for-each ( (Tuple( tk tv ta )) in
+             (.get-or( tctx (: LEOF List<Tuple<String,Type,AST>>) ))
+         ) (
+            (if (&&( (not found) (==( tk v )) )) (
+               (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
+                  (close(substitute( tctx ta )))
+                  (close(AType( (substitute( tctx vt )) )))
+               ))) )))
+               (set found 1_u64)
+            ) ())
+         ))
       ))
       ( (App( (Lit( ':_s ctk )) (App( (Var( v vtk )) (AType vt) )) )) (
          (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
             (close(Var( v (unique vtk) )))
             (close(AType( (substitute( tctx vt )) )))
          ))) )))
-         (while (non-zero tctx) (match tctx (
-            ()
-            ( TCtxNil (set tctx TCtxEOF) )
-            ( (TCtxBind( rst tk tv ta )) (
-               (if (==( tk v )) (
-                  (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
-                     (close(substitute( tctx ta )))
-                     (close(AType( (substitute( tctx vt )) )))
-                  ))) )))
-                  (set tctx TCtxEOF)
-               ) (set tctx rst))
-            ))
-         )))
+         (let found 0_u64)
+         (for-each ( (Tuple( tk tv ta )) in
+             (.get-or( tctx (: LEOF List<Tuple<String,Type,AST>>) ))
+         ) (
+            (if (&&( (not found) (==( tk v )) )) (
+               (set t (App( (close(Lit( ':_s (unique ctk) ))) (close(App(
+                  (close(substitute( tctx ta )))
+                  (close(AType( (substitute( tctx vt )) )))
+               ))) )))
+               (set found 1_u64)
+            ) ())
+         ))
       ))
       ( (Lit( v vtk )) (set t (Lit( v (unique vtk) ))) )
       ( (Var( v vtk )) (set t (Var( v (unique vtk) ))) )

SRC/tctx-and.lsts

@@ -0,0 +1,4 @@
+
+let $"&&"(lctx: TContext, rctx: TContext): TContext = (
+   if lctx.is-none then lctx else if rctx.is-none then rctx else union(lctx, rctx)
+);

SRC/tctx-bind.lsts

@@ -6,5 +6,5 @@ let .bind(tctx: HashtableEq<CString,List<Tuple<Type,AST>>>, k: CString, kt: Type
 );
 
 let .bind(tctx: TContext, k: CString, kt: Type, kv: AST): TContext = (
-   TCtxBind{ close(tctx), k, kt, kv }
+   Some{ cons(Tuple{k, kt, kv}, tctx.get-or([] :: List<Tuple<CString,Type,AST>>)) };
 );

SRC/tctx-substitute.lm

@@ -17,16 +17,15 @@ substitute := λ(: tctx TContext)(: tt Type). (: (
    (match tt (
       ()
       ( (TVar v) (
-         (while (non-zero tctx) (match tctx (
-            ()
-            ( TCtxNil (set tctx TCtxEOF) )
-            ( (TCtxBind( rst tk tv _ )) (
-               (if (==( tk v )) (
-                  (set tt tv)
-                  (set tctx TCtxEOF)
-               ) (set tctx rst))
-            ))
-         )))
+         (let found 0_u64)
+         (for-each ( (Tuple( tk tv _ )) in
+             (.get-or( tctx (: LEOF List<Tuple<String,Type,AST>>) ))
+         ) (
+            (if (&&( (not found) (==( tk v )) )) (
+               (set tt tv)
+               (set found 1_u64)
+            ) ())
+         ))
       ))
       ( (TGround( tag pars )) (
          (set tt (TGround(

SRC/tctx-union.lsts

@@ -0,0 +1,5 @@
+
+let union(lctx: TContext, rctx: TContext): TContext = (
+   Some{ rctx.get-or([] :: List<Tuple<CString,Type,AST>>) +
+         lctx.get-or([] :: List<Tuple<CString,Type,AST>>) }
+);

SRC/type-alias-index.lsts

@@ -6,11 +6,13 @@ let add-type-alias(lt: Type, rt: Type): Nil = (
 );
 let .rewrite-type-alias(lt: Type): Type = (
    match lt {
-      TGround{} => (
+      TGround{ tag=tag, parameters=parameters } => (
          let lt-rt = type-alias-index.lookup( lt.ground-tag-and-arity, Tuple{ TAny, TAny } );
          if non-zero(lt-rt.first) {
             let tctx = unify(lt-rt.first, lt);
             if non-zero(tctx) { lt = substitute(tctx, lt-rt.second); };
+         } else {
+            lt = TGround{ tag, close(parameters.rewrite-type-alias) };
          };
          lt
       );
@@ -24,3 +26,10 @@ let .rewrite-type-alias(lt: Type): Type = (
       _ => lt;
    }
 );
+let .rewrite-type-alias(lt: List<Type>): List<Type> = (
+   match lt {
+      LCons{ head=head, tail=tail } => cons( head.rewrite-type-alias, tail.rewrite-type-alias );
+      _ => lt;
+   }
+);
+

SRC/typecheck.lm

@@ -26,7 +26,7 @@ typecheck := λ. (: (
          (set ordered-type-exprs rst)
       ))
    )))
-   (infer-expr( TCtxEOF ast-parsed-program Unscoped TAny Used ))
+   (infer-expr( (: None TContext) ast-parsed-program Unscoped TAny Used ))
    (while (non-zero stack-to-specialize) (match stack-to-specialize (
       ()
       ( (LCons( (StackToSpecialize( function-name ft unify-ctx special-type )) rst )) (

SRC/typeof-tag.lsts

@@ -1,4 +1,4 @@
 
 let typeof-tag(tag: CString): Type = (
-   typeof-var-raw(ASTEOF, TCtxEOF, tag)
+   typeof-var-raw(ASTEOF, None :: TContext, tag)
 );

SRC/typeof-var-raw.lm

@@ -1,30 +1,24 @@
 
 typeof-var-raw := λ(: sloc AST)(: tctx TContext)(: vname String). (: (
    (let found (find-alias-type vname))
-   (while (non-zero tctx) (match tctx (
-      ()
-      ( TCtxNil (set tctx TCtxEOF) )
-      ( (TCtxBind( rst k vt _ )) (
-         (if (==( k vname )) (
-            (if (non-zero found) (
-               (if (.is-arrow vt) (
-                  (set found (&&( found vt )))
-               ) (
-                  (set found vt)
-               ))
-            ) (
-               (set found vt)
-            ))
+   (let continue 1_u64)
+   (for-each ( (Tuple( k vt _ )) in 
+               (.get-or( tctx (: LEOF List<Tuple<String,Type,AST>>) )) ) (
+      (if (&&( continue (==( k vname )) )) (
+         (if (non-zero found) (
             (if (.is-arrow vt) (
-               (set tctx rst)
+               (set found (&&( found vt )))
             ) (
-               (set tctx TCtxEOF)
+               (set found vt)
             ))
          ) (
-            (set tctx rst)
+            (set found vt)
          ))
-      ))
-   )))
+         (if (not(.is-arrow vt)) (
+            (set continue 0_u64)
+         ) ())
+      ) ())
+   )) 
    (for-each ((Tuple( kt t )) in (.lookup( global-type-context vname (: LEOF List<Tuple<Type,AST>>) ))) (
       (if (non-zero found) (
          (if (.is-arrow found) (

SRC/unify.lm

@@ -1,66 +1,54 @@
 
 unify := λ(: fpt Type)(: pt Type). (: (
-   (let ctx TCtxEOF)
+   (let ctx (: None TContext))
    (if (can-unify( fpt pt )) (
       (set ctx (unify-inner( fpt pt )))
    ) ())
    ctx
 ) TContext);
 
 unify-inner := λ(: fpt Type)(: pt Type). (: (
-   (let ctx TCtxEOF)
+   (let ctx (: None TContext))
+   (let yes (Some( (: LEOF List<Tuple<String,Type,AST>>) )))
    (match (Tuple( fpt pt )) (
       ()
       ( (Tuple( TAny _ )) (
-         (set ctx TCtxNil)
+         (set ctx yes)
       ))
       ( (Tuple( (TVar( ltv )) (TGround( tg LEOF )) )) (
          (set ctx (.bind(
-            TCtxEOF
+            ctx
             ltv
             (normalize pt)
             (Lit( tg (mk-token tg) ))
          )))
       ))
       ( (Tuple( (TGround( 'Any_s _ )) _ )) (
-         (set ctx TCtxNil)
+         (set ctx yes)
       ))
       ( (Tuple( (TVar( ltv )) rt )) (
          (set ctx (.bind(
-            TCtxEOF
+            ctx
             ltv
             (normalize pt)
             ASTEOF
          )))
       ))
       ( (Tuple( (TAnd( lt1 lt2 )) rt )) (
-         (match (Tuple( (unify-inner( lt1 rt )) (unify-inner( lt2 rt )) )) (
-            ()
-            ( (Tuple( TCtxEOF _ )) () )
-            ( (Tuple( _ TCtxEOF )) () )
-            ( (Tuple( lctx rctx )) (
-               (set ctx (union( lctx rctx )))
-            ))
-         ))
+         (set ctx (&&( (unify-inner( lt1 rt )) (unify-inner( lt2 rt )) )))
       ))
       ( (Tuple( lt (TAnd( rt1 rt2 )) )) (
-         (match (Tuple( (unify-inner( lt rt1 )) (unify-inner( lt rt2 )) )) (
-            ()
-            ( (Tuple( TCtxEOF TCtxEOF )) () )
-            ( (Tuple( lctx TCtxEOF )) (set ctx lctx) )
-            ( (Tuple( TCtxEOF rctx )) (set ctx rctx) )
-            ( (Tuple( lctx rctx )) (
-               (set ctx (union( lctx rctx )))
-            ))
-         ))
+         (set ctx (union( (unify-inner( lt rt1 )) (unify-inner( lt rt2 )) )))
       ))
 
       # Literal Constants
       ( (Tuple(
          (TGround( 'CONST_s LEOF ))
          (TGround( c LEOF ))
       )) (
-         (if (||( (.is-digit c) (==( c 'CONST_s )) )) (set ctx TCtxNil) ())
+         (if (||( (.is-digit c) (==( c 'CONST_s )) )) (
+            (set ctx yes)
+         ) ())
       ))
 
       # Phi Types
@@ -70,14 +58,12 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
       )) (
          (if (==( from_phi state_phi )) (
             (set ctx (.bind(
-               TCtxEOF
+               ctx
                'Phi::Transition_s
                to_phi
                (Var( id_phi (mk-token id_phi) ))
             )))
-         ) (
-            TCtxEOF
-         ))
+         ) ())
       ))
 
       # Varargs
@@ -89,7 +75,7 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
          (TGround( 'Cons_s (LCons( rp1 (LCons( rpr LEOF )) )) ))
       )) (
          (if (can-unify( lp1 rp1 )) (
-            (set ctx (and(
+            (set ctx (&&(
                (unify-inner( lpr rpr ))
                (unify-inner( lp1 rp1 ))
             )))
@@ -105,7 +91,7 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
          rp1
       )) (
          (if (can-unify( lp1 rp1 )) (
-            (set ctx (and(
+            (set ctx (&&(
                (unify-inner( lp1 rp1 ))
                (unify-inner( lpr (t1 'Nil_s) ))
             )))
@@ -118,7 +104,7 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
          (TGround( 'Cons_s (LCons( rp1 (LCons( rpr LEOF )) )) ))
       )) (
          (if (can-unify( lp1 rp1 )) (
-            (set ctx (and(
+            (set ctx (&&(
                (unify-inner( fpt rpr ))
                (unify-inner( lp1 rp1 ))
             )))
@@ -135,11 +121,6 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
          (set ctx (unify-inner( lp1 rp1 )))
       ))
 
-      ( (Tuple( (TGround( 'GT_s (LCons( (TGround( lbase LEOF )) LEOF )) )) (TGround( rbase LEOF )) )) (
-         (if (>( (to-i64 rbase) (to-i64 lbase) )) (
-            (set ctx TCtxNil)
-         ) ())
-      ))
       ( (Tuple( (TGround( ltn lps )) (TGround( rtn rps )) )) (
          (if (==( ltn rtn )) (
             (set ctx (unify( lps rps )))
@@ -151,10 +132,11 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
 ) TContext);
 
 unify := λ(: fpt List<Type>)(: pt List<Type>). (: (
-   (let ctx TCtxEOF)
+   (let ctx (: None TContext))
+   (let yes (Some( (: LEOF List<Tuple<String,Type,AST>>) )))
    (match (Tuple( fpt pt )) (
       ()
-      ( (Tuple( LEOF LEOF )) (set ctx TCtxNil) )
+      ( (Tuple( LEOF LEOF )) (set ctx yes))
       ( (Tuple( (LCons( lp1 lps )) (LCons( rp1 rps )) )) (
          (set ctx (unify( lp1 rp1 )))
          (if (non-zero ctx) (

SRC/union.lm

@@ -16,17 +16,3 @@ union := λ(: l Context)(: r Context). (: (
    return
 ) Context);
 
-union := λ(: ctx FContext)(: tctx TContext). (: (
-   (let r ctx)
-   (while (non-zero tctx) (match tctx (
-      ()
-      ( TCtxNil (set tctx TCtxEOF) )
-      ( (TCtxBind( rst k vt _ )) (
-         (set r (FCtxBind(
-            (close r) k TAny (mk-fragment())
-         )))
-         (set tctx rst)
-      ))
-   )))
-   r
-) FContext);

SRC/unit-inference.lsts

@@ -10,8 +10,8 @@ import SRC/inference-definitions.lsts;
 import SRC/can-unify.lsts;
 import SRC/unify.lm;
 import SRC/tctx-substitute.lm;
-import SRC/tctx-union.lm;
-import SRC/tctx-and.lm;
+import SRC/tctx-union.lsts;
+import SRC/tctx-and.lsts;
 import SRC/tctx-bind.lsts;
 
 # corollaries