Merge pull request #1043 from andrew-johnson-4/phi-3

Phi 3

Cargo.toml

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

EXAMPLES/phi-types.lsts.out

@@ -1 +1,11 @@
-Error:
+Error: Function Application Yielded No Matches
+phi
+With Arguments Cons<FileState::Closed,FileState::Open>
+At EXAMPLES/phi-types.lsts line 4 column 1
+With Candidates:
+Arrow<Cons<FileState::Closed,FileState::Closed>,FileState::Closed>+
+Blob+
+GlobalVariable+
+Arrow<Cons<FileState::Open,FileState::Open>,FileState::Open>+
+Blob+
+GlobalVariable

PLATFORM/C/LIB/bool.lm

@@ -1,7 +1,3 @@
 
-fragment type Bool; size Bool 1;
-
-true := 1_u8;
-false := 0_u8;
-
-(declare-unop( into-branch-conditional Bool BranchConditional ( x ) ));
+true := 1_u64;
+false := 0_u64;

PLATFORM/C/LIB/io.lm

@@ -22,8 +22,11 @@ mktemp := λ: FFI(: template U8[]). (: () U8[]);
 wait := λ: FFI(: wstatus U32[]). (: () PID);
 fork := λ: FFI().(: () PID);
 
-fopen := λ: FFI(: fp String)(: mode String). (: () File[]+Phi<FileState::Open>);
-fclose := λ: FFI(: fio File[]+Phi<FileState::Open,FileState::Closed>). (: () U32);
+fopen := λ: FFI(: fp String)(: mode String). (: () IO::File+Phi<FileState::Open>);
+fclose := λ: FFI(: fio IO::File+Phi<FileState::Open,FileState::Closed>). (: () U32);
+
+phi := λ: Blob(: left FileState::Open)(: right FileState::Open). (: () FileState::Open);
+phi := λ: Blob(: left FileState::Closed)(: right FileState::Closed). (: () FileState::Closed);
 
 exit := λ(: x U64).(: (exit(as x U32)) Nil);
 

PLATFORM/C/LIB/list.lsts

@@ -15,3 +15,27 @@ let cmp(ls: List<x>, rs: List<x>): I64 = (
 let $"<"(ls: List<x>, rs: List<x>): U64 = (
    cmp(ls, rs) < $"0_i64"
 );
+
+let to-smart-string(ls: List<x>): String = (
+   let s = "[";
+   let si = 0;
+   for l in ls {
+      if si > 0 {
+         s = s + ",";
+      };
+      s = s + to-smart-string(l);
+      si = si + 1;
+   };
+   s = s + "]";
+   s
+);
+
+let .unique(ls: List<x>): List<x> = (
+   let rs = [] :: List<x>;
+   for l in ls {
+      if not(rs.contains(l)) {
+         rs = cons(l, rs);
+      }
+   };
+   rs
+);

PLATFORM/C/LIB/tuple.lm

@@ -31,5 +31,5 @@ deep-hash := λ(: l Tuple<x,y>). (: (
 ) U64);
 
 print := λ(: l Tuple<x,y>). (: (
-   (print '\[_s)(print (.first l))(print ',_s)(print (.second l))(print '\n_s)
+   (print '\[_s)(print (.first l))(print ',_s)(print (.second l))(print '\]_s)
 ) Nil);

PLUGINS/BACKEND/C/mangle-identifier.lm

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

SRC/apply-or-cons-and-specialize.lm

@@ -1,26 +1,28 @@
 
 apply-or-cons-and-specialize := λ(: function-name String)(: ft Type)(: pt Type)(: blame AST). (: (
-   (let r (Tuple( TAny TAny )))
+   (let r (ApplyResult( TAny TAny (: LEOF List<Tuple<String,Type>>) )))
    (if (is-arrow ft) (
       (set r (apply-blame( function-name ft pt 1_u64 blame )))
    ) (
       (if (&&( (non-zero ft) (non-zero pt) )) (
-         (set r (Tuple(
+         (set r (ApplyResult(
             ft
             (t3( 'Cons_s ft pt ))
+            (: LEOF List<Tuple<String,Type>>)
          )))
       ) ())
    ))
    r
-) Tuple<Type,Type>);
+) ApplyResult);
 
 apply-cons :=  λ(: function-name String)(: ft Type)(: pt Type)(: blame AST). (: (
-   (let r (Tuple( TAny TAny )))
+   (let r (ApplyResult( TAny TAny (: LEOF List<Tuple<String,Type>>) )))
    (if (&&( (non-zero ft) (non-zero pt) )) (
-      (set r (Tuple(
+      (set r (ApplyResult(
          ft
          (t3( 'Cons_s ft pt ))
+         (: LEOF List<Tuple<String,Type>>)
       )))
    ) ())
    r
-) Tuple<Type,Type>);
+) ApplyResult);

SRC/apply-plural.lm

@@ -13,6 +13,7 @@ apply-plural := λ(: function-name String)(: ft Type)(: pt Type). (: (
          (TGround( 'Arrow_s (LCons( frt (LCons( fpt LEOF )) )) ))
          LEOF )) )) )) (
          (if (can-unify( fpt pt )) (
+            (print 'Unified\n_s)
             (set r (cons( ft r )))
          ) ())
       ))

SRC/apply.lm

@@ -1,6 +1,6 @@
 apply := λ(: function-name String)(: ft Type)(: pt Type)(: blame AST). (: (
    (apply-blame( function-name ft pt 0_u64 blame ))
-) Tuple<Type,Type>);
+) ApplyResult);
 
 apply := λ(: ctx Context)(: term AST). (: (
    (let return term)

SRC/apply.lsts

@@ -1,37 +1,38 @@
 
-let apply-blame(function-name: CString, function-type: Type, parameters: Type, do-specialize: U64, blame: AST): Tuple<Type,Type> = (
+let apply-blame(function-name: CString, function-type: Type, parameters: Type, do-specialize: U64, blame: AST): ApplyResult = (
    let r = apply(function-name, function-type, parameters, do-specialize);
-   if not(non-zero(r.second)) {
+   if not(non-zero(r.return-type)) {
       fail("Function Application Yielded No Matches\n"
            "\{function-name}\n"
            "With Arguments \{parameters}\n"
            "At \{location-of(blame)}\n"
            "With Candidates:\n"
            "\{function-type.pretty}\n")
    };
-   if is-t(r.second, c"Error: Did Not Close Before Specialization") {
+   if is-t(r.return-type, c"Error: Did Not Close Before Specialization") {
       fail("Application\sDid\sNot\sClose\sBefore\sSpecialization:\n"
            "Function \{function-name}: \{function-type}\n"
            "Argument \{parameters}\n"
            "At \{location-of(blame)}\n");
    };
-   if is-t(r.second, c"Error: Function Application Yielded An Irreducible Plurality Of Matches") {
+   if is-t(r.return-type, c"Error: Function Application Yielded An Irreducible Plurality Of Matches") {
       fail("Function Application Yielded An Irreducible Plurality Of Matches\n"
            "\{function-name}\n"
            "With Arguments \{parameters}\n"
            "At \{location-of(blame)}\n"
            "Matched Candidates:\n"
-           "\{r.first.pretty}\n")
+           "\{function-type.pretty}\n")
    };
    r
 );
 
-let apply(function-name: CString, function-type: Type, parameters: Type, do-specialize: U64): Tuple<Type,Type> = (
+let apply(function-name: CString, function-type: Type, parameters: Type, do-specialize: U64): ApplyResult = (
    let r = TAny {};
    let rs = apply-plural(function-name, function-type, parameters);
    if not(is-t( function-type, c"Hook" )) {
       rs = reduce-plural(rs);
    };
+   let phi-types = [] :: List<Tuple<CString,Type>>;
    if rs.length > 1 && not(is-t( function-type, c"Hook" )) {
       r = t1(c"Error: Function Application Yielded An Irreducible Plurality Of Matches");
       function-type = head(rs);
@@ -43,6 +44,17 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
          let frt = range(sft);
          let fpt = domain(sft);
          let ctx = normalize(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 {};);
+         } };
          let closed-type = substitute( ctx, sft );
          function-type = closed-type;
          if not(is-t( r, c"Error: Did Not Close Before Specialization")) {
@@ -59,6 +71,6 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
          r = and(r, cons-root(parameters));
       };
    };
-   Tuple { function-type, r }
+   ApplyResult { function-type, r, phi-types }
 );
 

SRC/can-unify.lm

@@ -40,7 +40,7 @@ can-unify := λ(: fpt Type)(: pt Type). (: (
          (TGround( 'Phi_s (LCons( (TGround( to_phi _ )) (LCons( (TGround( from_phi _ )) LEOF )) )) ))
          (TGround( 'Phi_s (LCons( (TGround( state_phi _ )) (LCons( (TGround( id_phi _ )) LEOF )) )) ))
       )) (
-         (==( from_phi state_phi ))
+         (set r (==( from_phi state_phi )))
       ))
 
       # Varargs

SRC/index-definitions.lm

@@ -17,7 +17,7 @@ type IsUsed Used | Unused | Tail | Return | Call;
 type IsScoped Scoped | Unscoped;
 
 type Context CtxEOF | CtxNil | (CtxBind( Context[] , String , AST )); zero Context CtxEOF;
-type TContext TCtxEOF | TCtxNil | (TCtxBind( TContext[] , String , Type , AST )); zero TContext TCtxEOF;
+type TContext TCtxEOF | TCtxNil | (TCtxBind( ctx:TContext[] , key:String , typ:Type , term:AST )); zero TContext TCtxEOF;
 type FContext FCtxEOF | (FCtxBind( FContext[] , String , Type , Fragment )); zero FContext FCtxEOF;
 
 type STypeList STEOF | (STSeq( STypeList[] , S , Type )); zero STypeList STEOF;
@@ -35,4 +35,7 @@ type ParsePartial (PME( AST , List<Token> )); # term, remainder
 
 type StackToSpecialize (StackToSpecialize( String , Type , TContext , Type ));
 
+type ApplyResult (ApplyResult( function-type:Type , return-type:Type , phi-types:List<Tuple<String,Type>> ));
+
 import SRC/to-smart-string.lm;
+

SRC/index-types.lm

@@ -10,6 +10,8 @@ import SRC/is-and.lsts;
 import SRC/index-concrete-type-instances.lm;
 import SRC/type-index.lm;
 import SRC/infer-expr.lm;
+import SRC/phi-transition.lsts;
+import SRC/phi-merge.lsts;
 import SRC/alias.lm;
 import SRC/class-exists.lm;
 import SRC/is-parameter-flat.lm;
@@ -59,10 +61,12 @@ import SRC/has-infinite.lm;
 import SRC/has-forward.lm;
 
 import SRC/with-tag.lm;
+import SRC/with-phi.lsts;
 import SRC/with-size.lm;
 import SRC/with-platform-props.lm;
 
 import SRC/without-tag.lm;
+import SRC/without-phi.lsts;
 import SRC/without-constructor.lm;
 import SRC/without-representation.lm;
 import SRC/without-size-unless-class.lm;

SRC/infer-expr.lm

@@ -30,16 +30,13 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          (infer-expr( tctx r Unscoped TAny Used ))
       ))
       ( (Typedef( _ _ )) () )
-      ( (Glb( k v )) (
+      ( (Glb( k (@( v (Abs( _ )) )) )) (
          (if (is-open(typeof term)) () (
             (infer-expr( tctx v Unscoped TAny Used ))
             (let vt (typeof v))
-            (if (is-arrow vt) () (
-               (let gt (and( (t1 'GlobalVariable_s) (without-representation vt) )))
-               (maybe-specialize( 'mov_s (typeof-var-raw( term tctx 'mov_s )) (t3( 'Cons_s vt gt )) ))
-            ))
          ))
       ))
+      ( (Glb( k v )) () ) # globals should already be inferred by now
       ( (App( (Lit( ':_s _ )) (App( (Lit( _ _ )) (AType tt) )) )) (
          (add-concrete-type-instance tt)
          (match term (
@@ -97,14 +94,18 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          (ascript-normal( term (t1 'Nil_s) ))
       ))
       ( (App( (App( (App( (Var( 'if_s _ )) cond )) t )) f )) (
-         (if (is( scoped Scoped )) (
+         (if (is( scoped Scoped )) (scope(
             (let tctx-inner (infer-expr( tctx cond Unscoped TAny Used )))
-            (infer-expr( tctx-inner t Unscoped TAny Tail ))
-         ) (
+            (let tctx-weak-t (infer-expr( tctx-inner t Unscoped TAny Tail )))
+            (let tctx-t (phi-override( tctx tctx-weak-t )))
+            (let tctx-f (infer-expr( tctx f Unscoped TAny Tail )))
+            (set tctx (phi-merge( tctx-t tctx-f )))
+         )) (
             (set tctx (infer-expr( tctx cond Unscoped TAny Used )))
-            (set tctx (infer-expr( tctx t Unscoped TAny Tail )))
+            (let tctx-t (infer-expr( tctx t Unscoped TAny Tail )))
+            (let tctx-f (infer-expr( tctx f Unscoped TAny Tail )))
+            (set tctx (phi-merge( tctx-t tctx-f )))
          ))
-         (infer-expr( tctx f Unscoped TAny Tail ))
          (ascript-normal( term (guess-representation(without-representation(typeof t))) ))
       ))
       ( (App( (Var( 'as_s _ )) (App( t (AType tt) )) )) (
@@ -132,8 +133,9 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
          ))
       ))
       ( (App( (Var( 'scope_s _ )) r )) (
-         (infer-expr( tctx r Scoped TAny Tail ))
+         (let weak-ctx (infer-expr( tctx r Scoped TAny Tail )))
          (ascript-normal( term (typeof r) ))
+         (set tctx (phi-override( tctx weak-ctx )))
       ))
       ( (App( (Var( 'open_s _ )) r )) (
          (set tctx (infer-expr( tctx r Unscoped TAny Used )))
@@ -219,36 +221,45 @@ infer-expr-one := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type
                (let r-hint TAny)
                (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
                (let lt-fname (find-alias( l-fname (typeof r) )))
-               (let ftrt (apply-or-cons-and-specialize(
+               (let apply-result (apply-or-cons-and-specialize(
                   lt-fname
                   (typeof-var-raw( term tctx lt-fname ))
                   (typeof r)
                   term
                )))
-               (let function-type (.2 ftrt))
-               (ascript-normal( l function-type ))
-               (set rt (.1 ftrt))
+               (ascript-normal( l (.function-type apply-result) ))
+               (set rt (.return-type apply-result))
+               (if (non-zero (.phi-types apply-result)) (
+                  (for-each ((Tuple( phi-id phi-new-type )) in (.phi-types apply-result)) (
+                     (set tctx (phi-transition( tctx phi-id phi-new-type )))
+                  ))
+               ) ())
             ))
             ( _ (
                (if (is( used Unused )) (set r-used Unused) ())
                (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
                (if (is-arrow(typeof l)) (set r-used Call) ())
                (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
-               (let ftrt (apply-cons(
+               (let apply-result (apply-cons(
                   (var-name-if-var l)
                   (typeof l)
                   (typeof r)
                   term
                )))
                (if (head-string(var-name-if-var l)) (
-                  (set ftrt (apply-or-cons-and-specialize(
+                  (set apply-result (apply-or-cons-and-specialize(
                      (var-name-if-var l)
                      (typeof l)
                      (typeof r)
                      term
                   )))
                ) ())
-               (set rt (.1 ftrt))
+               (set rt (.return-type apply-result))
+               (if (non-zero (.phi-types apply-result)) (
+                  (for-each ((Tuple( phi-id phi-new-type )) in (.phi-types apply-result)) (
+                     (set tctx (phi-transition( tctx phi-id phi-new-type )))
+                  ))
+               ) ())
             ))
          ))
          (if (is( l-used Unused )) (

SRC/infer-global-context.lm

@@ -54,10 +54,11 @@ infer-global-context-2 := λ(: td AST). (: (
          (let rhst (normalize(typeof rhs)))
          (let kt (and( (without-representation rhst) (t1 'GlobalVariable_s) )))
          (set global-type-context (TCtxBind(
-            (close global-type-context) k kt ASTEOF
+            (close 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 global-type-context 'mov_s )) (t3( 'Cons_s kt kt )) ))
       ))
       ( _ () )
    ))

SRC/normalize.lm

@@ -6,6 +6,7 @@ normalize := λ(: tt Type). (: (
    (set rt (without-tag rt))
    # Sized can serve as a datatype if nothing else is available
    (set rt (without-size-unless-class rt))
+   (set rt (with-phi rt))
    rt
 ) Type);