Merge pull request #1156 from andrew-johnson-4/implied-types

Implied types

Cargo.toml

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

PLATFORM/C/LIB/array.lm

@@ -3,7 +3,7 @@ null := λ: Blob(). (: (
    (:expression NULL_l)
 ) Array<?,?>);
 
-const-cons := λ: Blob(: es x...). (: (
+vararg-cons := λ: Blob(: es x...). (: (
    (:expression(
       '{_l (for-arg (e in es) (
          (:expression e) ',_l

PLATFORM/C/LIB/bool.lsts

@@ -1,3 +1,5 @@
 
+type Bool is U64;
+
 let true = 1;
 let false = 0;

PLATFORM/C/LIB/u32.lsts

@@ -1,4 +1,6 @@
 
+type U32 => U64;
+
 declare-binop( $"!=", raw-type(U32), raw-type(U32), raw-type(U64), ( l"("; x; l"!="; y; l")"; ) );
 declare-binop( $"==", raw-type(U32), raw-type(U32), raw-type(U64), ( l"("; x; l"=="; y; l")"; ) );
 declare-binop( $"<",  raw-type(U32), raw-type(U32), raw-type(U64), ( l"("; x; l"<"; y; l")"; ) );

PLUGINS/FRONTEND/LSTS/lsts-parse.lsts

@@ -489,12 +489,20 @@ let lsts-parse-typedef(tokens: List<Token>): List<Token> = (
    tokens = base-rest.second;
    match tokens {
       [Token{key:c"is"}.. rest] => (
-         lsts-parse-expect(c"is", tokens); tokens = tail(tokens);
+         tokens = rest;
          let rt-rest = lsts-parse-type(tokens);
          tokens = rt-rest.second;
          lsts-parse-expect(c";", tokens); tokens = tail(tokens);
          add-type-alias(base-rest.first, rt-rest.first);
       );
+      [Token{key:c"="}.. Token{key:c">"}.. rest] => (
+         tokens = rest;
+         let rt-rest = lsts-parse-type(tokens);
+         tokens = rt-rest.second;
+         lsts-parse-expect(c";", tokens); tokens = tail(tokens);
+         add-quick-prop(base-rest.first, base-rest.first, rt-rest.first);
+         add-weaken-quick-prop(base-rest.first, rt-rest.first, rt-rest.first);
+      );
       _ => (
          lsts-parse-expect(c"=", tokens); tokens = tail(tokens);
          let case-rest = lsts-parse-typedef-case(tokens);

SRC/apply.lsts

@@ -33,7 +33,7 @@ let apply(function-name: CString, function-type: Type, parameters: Type, do-spec
       rs = reduce-plural(rs);
    };
    let phi-types = [] :: List<Tuple<CString,Type>>;
-   if rs.length > 1 && not(function-type.is-t( c"Hook" )) {
+   if rs.length > 1 {
       r = t1(c"Error: Function Application Yielded An Irreducible Plurality Of Matches");
       function-type = head(rs);
       for candidate in tail(rs) {

SRC/denormalize.lsts

@@ -0,0 +1,25 @@
+
+let denormalize-arrow(pt: Type): Type = (
+   match pt {
+      TAnd{ left=left, right=right } => denormalize-arrow(left) && denormalize-arrow(right);
+      TGround{tag:c"Arrow", parameters:[rng.. dom..]} => (
+         t3( c"Arrow", denormalize-cons(dom), rng )
+      );
+      TGround{tag:c"Array", parameters:[rng.. dom..]} => (
+         t3( c"Array", denormalize-arrow(dom), rng )
+      );
+      TGround{} => denormalize(pt);
+      _ => pt;
+   }
+);
+
+let denormalize-cons(pt: Type): Type = (
+   match pt {
+      TAnd{ left=left, right=right } => denormalize-cons(left) && denormalize-cons(right);
+      TGround{tag:c"Cons", parameters:[rng.. dom..]} => (
+         t3( c"Cons", denormalize-cons(dom), denormalize-cons(rng) )
+      );
+      TGround{} => denormalize(pt);
+      _ => pt;
+   }
+);

SRC/fctx-lookup.lsts

@@ -25,16 +25,17 @@ let .lookup(ctx: FContext, k: CString, kt: Type, sloc: AST, hard: U64): Fragment
             } else {
                if ctx-kt.is-arrow {
                   let domaint = ctx-kt.domain;
+                  let domaind = denormalize(ctx-kt.domain);
                   let ranget = ctx-kt.range;
                   if can-unify( domaint, kt ) {
                      if non-zero(found) {
-                        if can-unify(found,domaint) {
+                        if can-unify(found,domaind) {
                            r = ctx-kv;
-                           found = domaint;
+                           found = domaind;
                         }
                      } else {
                         r = ctx-kv;
-                        found = domaint;
+                        found = domaind;
                      }
                   };
                   ctx = remainder;

SRC/index-types.lm

@@ -48,6 +48,7 @@ import SRC/without-size.lm;
 
 import SRC/normalize.lm;
 import SRC/denormalize.lm;
+import SRC/denormalize.lsts;
 import SRC/type-of-s.lm;
 import SRC/type-of-s-with-fields.lm;
 

SRC/normalize.lm

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

SRC/quick-prop.lsts

@@ -36,3 +36,34 @@ let enrich-quick-prop(base: Type, pre: Type): Type = (
    };
    pre
 );
+
+let weaken-quick-prop-index = {} :: HashtableEq<(CString,U64),List<(Type,Type)>>;
+
+let add-weaken-quick-prop(pre: Type, pat: Type, post: Type): Nil = (
+   let key = pre.ground-tag-and-arity;
+   let val = weaken-quick-prop-index.lookup(key, ([] :: List<(Type,Type)>));
+   val = cons( (pat,post), val );
+   weaken-quick-prop-index = weaken-quick-prop-index.bind( key, val );
+);
+
+let weaken-quick-prop(base: Type): Type = (
+   weaken-quick-prop(base, base)
+);
+
+let weaken-quick-prop(base: Type, pre: Type): Type = (
+   match pre {
+      TGround {} => (
+         for Tuple { lt=first, rt=second } in weaken-quick-prop-index.lookup( pre.ground-tag-and-arity, ([] :: List<(Type,Type)>) ) {
+            if can-unify(lt, base) then (
+               base = remove-info(base, rt);
+            );
+         };
+      );
+      TAnd { lt=left, rt=right } => (
+         base = weaken-quick-prop(base, lt);
+         base = weaken-quick-prop(base, rt);
+      );
+      _ => ();
+   };
+   base
+);

SRC/reduce-plural.lm

@@ -1,50 +1,55 @@
 
-reduce-plural := λ(: pts List<Type>). (: (
-   (let r (: LEOF List<Type>))
+reduce-plural := λ(: dpts List<Type>). (: (
+   (let pts (: LEOF List<Tuple<Type,Type>>))
+   (for-each (pt in dpts) (
+      (set pts (cons( (Tuple( (denormalize-arrow pt) pt )) pts )))
+   ))
+   (set pts (.reverse pts))
+   (let r (: LEOF List<Tuple<Type,Type>>))
    (let maybe-constructor pts)
    (while (non-zero maybe-constructor) (match maybe-constructor (
       ()
-      ( (LCons( try tlt )) (
+      ( (LCons( (Tuple( try-denormal try )) tlt )) (
          (if (is-constructor try) (
-            (set r (cons( try r )))
+            (set r (cons( (Tuple( try-denormal try )) r )))
          ) ())
          (set maybe-constructor tlt)
       ))
    )))
-   (if (non-zero r) (set pts (: LEOF List<Type>)) ())
+   (if (non-zero r) (set pts (: LEOF List<Tuple<Type,Type>>)) ())
    (while (non-zero pts) (match pts (
       ()
-      ( (LCons( try tlt )) (
+      ( (LCons( (Tuple( try-denormal try )) tlt )) (
          (set pts tlt)
-         (for-each (tst in tlt) (
+         (for-each ((Tuple( tst-denormal tst )) in tlt) (
             (if (non-zero try) (
-               (if (can-unify( (.domain try) (.domain tst) )) (
+               (if (can-unify( (.domain try-denormal) (.domain tst-denormal) )) (
                   (set try TAny)
                ) ())
             ) ())
          ))
          (if (non-zero try) (
-            (set r (cons( try r )))
+            (set r (cons( (Tuple( try-denormal try )) r )))
          ) ())
       ))
    )))
    (set pts r)
-   (set r (: LEOF List<Type>))
+   (let return (: LEOF List<Type>))
    (while (non-zero pts) (match pts (
       ()
-      ( (LCons( try tlt )) (
+      ( (LCons( (Tuple( try-denormal try )) tlt )) (
          (set pts tlt)
-         (for-each (tst in tlt) (
+         (for-each ((Tuple( tst-denormal tst )) in tlt) (
             (if (non-zero try) (
-               (if (can-unify( (.domain try) (.domain tst) )) (
+               (if (can-unify( (.domain try-denormal) (.domain tst-denormal) )) (
                   (set try TAny)
                ) ())
             ) ())
          ))
          (if (non-zero try) (
-            (set r (cons( try r )))
+            (set return (cons( try return )))
          ) ())
       ))
    )))
-   r
+   return
 ) List<Type>);

SRC/remove-info.lsts

@@ -0,0 +1,15 @@
+
+let remove-info(base: Type, rm: Type): Type = (
+   match base {
+      TAnd{ left=left, right=right } => (
+         let new-left = remove-info(left, rm);
+         let new-right = remove-info(right, rm);
+         if is(left,new-left) && is(right,new-right) then base
+         else (left && right);
+      );
+      TGround{} => (
+         if can-unify(rm,base) then TAny else base
+      );
+      _ => base;
+   }
+);

SRC/unit-inference.lsts

@@ -15,3 +15,4 @@ import SRC/tctx-and.lm;
 
 # corollaries
 import SRC/quick-prop.lsts;
+import SRC/remove-info.lsts;

tests/regress/exec.lm

@@ -5,7 +5,7 @@ main := λ. (: (
    (let tmp (as (mktemp(as (clone-rope(SAtom '/tmp/lm.tmp.XXXXXX_s)) U8[])) U8[]))
    (let p (fork()))
    (if (==( (as p U64) 0_u64 )) (
-      (let argv (const-cons(
+      (let argv (vararg-cons(
           (as 'cpp_s U8[])
           (as '-include_s U8[])
           (as 'stdio.h_s U8[])

tests/regress/type-alias.lsts

@@ -5,11 +5,21 @@ import LIB/default.lm;
 
 let f(x: U64): U64 = x + x;
 let g(x: USize): U64 = x + x + 1;
+let h(x: U32): U64 = 1;
+let h(x: U64): U64 = 2;
+let i(x: U64): U64 = 1;
+let i(x: U32): U64 = 2;
 
 print(f(1));     # normal
 print(f(1_sz));  # alias
-#print(f(1_u32)); # inference
+print(f(1_u32)); # inference
 
 print(g(1));     # normal
 print(g(1_sz));  # alias
-#print(g(1_u32)); # inference
+print(g(1_u32)); # inference
+
+print(h(1_u32)); # inference
+print(h(1_u64)); # inference
+
+print(i(1_u32)); # inference
+print(i(1_u64)); # inference

tests/regress/type-alias.lsts.out

@@ -1 +1 @@
-2233
+2223331221