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

Phi types

Cargo.toml

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

EXAMPLES/phi-types.lsts

@@ -0,0 +1,11 @@
+
+import LIB/default.lm;
+
+let fp = fopen(c"input-file.txt", c"r") :: File;
+
+# The type system doesn't know that this is always true
+# So fclose may or may not be called
+# This creates an error because the φ-type can't be merged
+if true {
+   fclose(fp);
+};

EXAMPLES/phi-types.lsts.out

@@ -0,0 +1 @@
+Error:

Makefile

@@ -1,6 +1,6 @@
 
 dev: install-production
-	lm tests/regress/propositional-types.lsts
+	lm EXAMPLES/phi-types.lsts
 	cc -O3 tmp.c
 	./a.out
 

PLUGINS/FRONTEND/LSTS/lsts-parse.lsts

@@ -90,7 +90,7 @@ let lsts-parse-type(tokens: List<Token>): Tuple<Type,List<Token>> = (
       };
       lsts-parse-expect(c")", tokens); tokens = tail(tokens);
       TGround { c"Tuple", close(args) };
-   } else if lsts-is-ident-head(lsts-parse-head(tokens)) {
+   } else if lsts-is-ident-head(lsts-parse-head(tokens)) && not(lsts-is-reserved-word(lsts-parse-head(tokens))) {
       let varname = lsts-parse-head(tokens); tokens = tail(tokens);
       TVar { varname }
    } else {

PLUGINS/FRONTEND/LSTS/lsts-tokenize.lm

@@ -4,6 +4,18 @@ lsts-tokenize := λ(: fp String). (: (
    (lsts-tokenize-string(fp text))
 ) List<Token>);
 
+lsts-is-reserved-word := λ(: text String). (: (
+   (let r 0_u64)
+   (if (==( text 'if_s )) (set r 1_u64) ()) # $
+   (if (==( text 'then_s )) (set r 1_u64) ()) # $
+   (if (==( text 'else_s )) (set r 1_u64) ()) # $
+   (if (==( text 'let_s )) (set r 1_u64) ()) # $
+   (if (==( text 'while_s )) (set r 1_u64) ()) # $
+   (if (==( text 'for_s )) (set r 1_u64) ()) # $
+   (if (==( text 'type_s )) (set r 1_u64) ()) # $
+   r
+) U64);
+
 lsts-is-ident-head := λ(: text String). (: (
    (let r 0_u64)
    (if (&&( (>=( (head-string text) 48_u8 )) (<=( (head-string text) 57_u8 )) )) (set r 1_u64) ())  # 0-9