Merge pull request #1040 from andrew-johnson-4/phi-types-2

Phi types 2

Cargo.toml

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

EXAMPLES/phi-types.lsts

@@ -1,7 +1,7 @@
 
 import LIB/default.lm;
 
-let fp = fopen(c"input-file.txt", c"r") :: File;
+let fp = fopen(c"input-file.txt", c"r");
 
 # The type system doesn't know that this is always true
 # So fclose may or may not be called

PLATFORM/C/LIB/bool.lm

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

PLATFORM/C/LIB/default.lm

@@ -5,6 +5,7 @@ import PLATFORM/C/LIB/blob.lm;
 import PLATFORM/C/LIB/primitives.lm;
 import PLATFORM/C/LIB/field-accessors.lm;
 import PLATFORM/C/LIB/sized.lm;
+import PLATFORM/C/LIB/bool.lm;
 import PLATFORM/C/LIB/u8.lm;
 import PLATFORM/C/LIB/i8.lm;
 import PLATFORM/C/LIB/u16.lm;

PLATFORM/C/LIB/io.lm

@@ -22,6 +22,9 @@ 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);
+
 exit := λ(: x U64).(: (exit(as x U32)) Nil);
 
 fail := λ(: msg String)(: loc String). (: (

PLUGINS/BACKEND/C/compile-global.lm

@@ -79,14 +79,14 @@ compile-global-c := λ(: ctx FContext)(: k String)(: term AST). (: (
          (set text (SCons( (close text) (close(SAtom '}\n_s)) )))
          (set assemble-text-section (SCons( (close assemble-text-section) (close text) )))
       )))
-      ( (App( (Lit( ':_s ltok )) (App( t (AType tt) )) )) (
+      ( t (
          (let clean-tt (without-representation kt))
          (let mid (mangle-identifier( k clean-tt )))
 
          (let e (compile-expr( ctx t 0_i64 Used )))
 
          (let text SNil)
-         (match tt (
+         (match (slot( kt 'Array_s )) (
             ()
             ( (TGround( 'Array_s (LCons( _ (LCons(
                  (TGround( 'Arrow_s (LCons( ranget (LCons( domaint _ )) )) )) _

SRC/apply.lsts

@@ -7,7 +7,7 @@ let apply-blame(function-name: CString, function-type: Type, parameters: Type, d
            "With Arguments \{parameters}\n"
            "At \{location-of(blame)}\n"
            "With Candidates:\n"
-           "\{function-type}\n")
+           "\{function-type.pretty}\n")
    };
    if is-t(r.second, c"Error: Did Not Close Before Specialization") {
       fail("Application\sDid\sNot\sClose\sBefore\sSpecialization:\n"
@@ -21,7 +21,7 @@ let apply-blame(function-name: CString, function-type: Type, parameters: Type, d
            "With Arguments \{parameters}\n"
            "At \{location-of(blame)}\n"
            "Matched Candidates:\n"
-           "\{r.first}\n")
+           "\{r.first.pretty}\n")
    };
    r
 );

SRC/can-unify.lm

@@ -35,6 +35,14 @@ can-unify := λ(: fpt Type)(: pt Type). (: (
          (if r () (set r (can-unify( lt rt2 ))))
       ))
 
+      # Phi Types
+      ( (Tuple(
+         (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 ))
+      ))
+
       # Varargs
       ( (Tuple(
          (TGround( 'Cons_s (LCons(

SRC/infer-global-context.lm

@@ -40,18 +40,25 @@ infer-global-context := λ(: td AST). (: (
             td
          )))
       ))
-      ( (Glb( k_t (App( (Lit( ':_s _ )) (App( rhs (AType rhst) )) )) )) (
-         (add-concrete-type-instance rhst)
+      ( _ () )
+   ))
+) Nil);
+
+infer-global-context-2 := λ(: td AST). (: (
+   (match td (
+      ()
+      ( (Glb( k_t (@( frhs (Abs( lhs (App( (Lit( ':_s _ )) (App( rhs (AType rhst) )) )) tlt )) )) )) (
+      ))
+      ( (Glb( k_t rhs )) (
+         (infer-expr( global-type-context rhs Unscoped TAny Used ))
+         (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
          )))
          (mark-global-as-seen( k kt TAny ))
          (ascript-normal( td kt ))
       ))
-      ( (Glb( _ _ )) (
-         (exit-error( 'Global\sBindings\sMust\sBe\sAscripted_s td ))
-      ))
       ( _ () )
    ))
 ) Nil);

SRC/to-smart-string.lm

@@ -32,3 +32,36 @@ to-smart-string := λ(: tt Type). (: (
    ))
 ) SmartString);
 
+.pretty := λ(: tt Type). (: (
+   (match tt (
+      ()
+      ( TAny (intern '?_s))
+      ( (TVar v) (to-smart-string v) )
+      ( (TGround( tg ps )) (
+         (let r (to-smart-string tg))
+         (if (>( (.length ps) 0_u64 )) (
+            (set r (+( r (intern '<_s) )))
+            (let ri 0_u64)
+            (for-each (p in ps) (
+               (if (>( ri 0_u64 )) (
+                  (set r (+( r (intern ',_s) )))
+               ) ())
+               (set ri (+( ri 1_u64 )))
+               (set r (+( r (to-smart-string p) )))
+            ))
+            (set r (+( r (intern '>_s) )))
+         ) ())
+         r
+      ))
+      ( (TAnd( lt rt )) (
+         (+( 
+            (.pretty lt)
+            (+(
+               (intern '+\n_s)
+               (.pretty rt)
+            ))
+         ))
+      ))
+   ))
+) SmartString);
+

SRC/typecheck.lm

@@ -11,10 +11,18 @@ typecheck := λ. (: (
          (set p rst)
       ))
    )))
-   (while (non-zero ordered-type-exprs) (match ordered-type-exprs (
+   (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)
       ))
    )))

SRC/unify.lm

@@ -55,6 +55,23 @@ unify-inner := λ(: fpt Type)(: pt Type). (: (
          ))
       ))
 
+      # Phi Types
+      ( (Tuple(
+         (TGround( 'Phi_s (LCons( to_phi (LCons( (TGround( from_phi _ )) LEOF )) )) ))
+         (TGround( 'Phi_s (LCons( (TGround( state_phi _ )) (LCons( (TGround( id_phi _ )) LEOF )) )) ))
+      )) (
+         (if (==( from_phi state_phi )) (
+            (set ctx (TCtxBind(
+               (close TCtxEOF)
+               id_phi
+               to_phi
+               (Lit( 'Phi::Transition_s (token::new 'Phi::Transition_s) ))
+            )))
+         ) (
+            TCtxEOF
+         ))
+      ))
+
       # Varargs
       ( (Tuple(
          (TGround( 'Cons_s (LCons(

tests/regress/propositional-types.lsts

@@ -3,7 +3,7 @@ import LIB/default.lm;
 
 type A = A { x: U64 };
 
-let a = A { 1 } :: A;
+let a = A { 1 };
 
 let prop quick-prop(a: A): B = ();