Merge pull request #1497 from andrew-johnson-4/infer-expr-allow-tree-edits

Infer expr allow tree edits

Author: andrew-johnson-4

BOOTSTRAP/cli.c

@@ -1,6 +1,7 @@
 
 assert-one-typed := λ(: term AST). (: (
    (if (non-zero(typeof term)) () (
+      (print 'Assert\sOne\s_s)(print term)(print '\n_s)
       (exit-error( 'Unable\sto\sinfer\stype\sof\sexpression_s term ))
    ))
 ) Nil);

SRC/assert-one-typed.lm

@@ -1,7 +1,7 @@
 
 type CompileMode ModeParse | ModePreprocess | ModeTypecheck | ModeCompile;
 
-type IsUsed Used | Unused | Tail | Return | Call | C;
+type IsUsed Used | Unused | Tail | Return | Call;
 type IsScoped Scoped | Unscoped;
 
 type FContext FCtxEOF | (FCtxBind( remainder:FContext[] , k:String , kt:Type , kv:Fragment )); zero FContext FCtxEOF;

SRC/index-definitions.lm

@@ -5,7 +5,6 @@ import SRC/quick-prop.lsts;
 
 import SRC/substitute.lm;
 import SRC/cons-root.lsts;
-import SRC/infer-expr.lm;
 import SRC/is-special.lm;
 import SRC/global-is-seen.lm;
 import SRC/index-of-tag.lm;

SRC/index-types.lm

@@ -37,7 +37,8 @@ infer-global-context-2 := λ(: td AST). (: (
       ( (Glb( k (@( frhs (Abs( lhs (App( (Lit( ':_s _ )) (App( rhs (AType rhst) )) )) tlt )) )) )) (
       ))
       ( (Glb( k rhs )) (
-         (infer-expr( (: None Maybe<TContext>) rhs Unscoped TAny Used ))
+         (let tctx-rhs (std-infer-expr( (: None Maybe<TContext>) rhs false Used TAny )))
+         # TODO: make this rewrite terms if the subtree has changes
          (let rhst (normalize(typeof rhs)))
          (let kt (&&( rhst (t1 'GlobalVariable_s) )))
          (set global-type-context (.bind( global-type-context (.key k) kt td )))

SRC/infer-expr.lm

@@ -3,6 +3,10 @@ let mk-app(f: AST, a: AST): AST = (
    App{ close(f), close(a) }
 );
 
+let mk-cons-or-app(is-cons: U64, f: AST, a: AST): AST = (
+   App{ is-cons, close(f), close(a) }
+);
+
 let mk-cons(f: AST, a: AST): AST = (
    App{ true, close(f), close(a) }
 );
@@ -26,3 +30,6 @@ let mk-abs(l: AST, r: AST, t: Type): AST = (
 let mk-meta(l: AST): AST = (
    Meta{ close(l) }
 );
+
+let mk-nil(): AST = ASTNil{};
+let mk-eof(): AST = ASTEOF{};

SRC/infer-global-context.lm

@@ -15,7 +15,7 @@ specialize := λ(: key String)(: ft Type)(: unify-ctx Maybe<TContext>)(: result-
          (mark-as-special( key result-type ))
          (let special-term (substitute( unify-ctx term )))
          (infer-global-context( special-term ))
-         (infer-expr( (: None Maybe<TContext>) special-term Unscoped (t1 'Specialize_s) Used ))
+         (let tctx-special (std-infer-expr( (: None Maybe<TContext>) special-term false Used TAny )))
          (set global-type-context (.bind( global-type-context key (typeof special-term) special-term )))
          (set ast-parsed-program (Seq(
             (close ast-parsed-program)

SRC/mk-app.lsts

@@ -19,7 +19,7 @@ let std-apply-macro(tctx: Maybe<TContext>, mname: CString, margs: AST): (TContex
          peeped = mtype;
       };
    };
-   let peeped-type = std-infer-peeped-arguments(tctx, margs, peep-holes);
+   (let peeped-type, _) = std-infer-peeped-arguments(tctx, margs, peep-holes);
 
    let matched = [] :: List<(Type,AST)>;
    for Tuple{mtype=first, mterm=third} in row {
@@ -45,20 +45,24 @@ let std-apply-macro(tctx: Maybe<TContext>, mname: CString, margs: AST): (TContex
    std-apply-macro-candidates(tctx, mname, margs, candidates);
 );
 
-let std-infer-peeped-arguments(tctx: Maybe<TContext>, t: AST, peep: Type): Type = (
+let std-infer-peeped-arguments(tctx: Maybe<TContext>, t: AST, peep: Type): (Type, AST) = (
    match peep {
       TGround{tag:c"Cons", parameters:[p2.. p1..]} => (
          match t {
-            App{left=left, right=right} => (
-               t3(c"Cons",
-                  std-infer-peeped-arguments(tctx, left, p1),
-                  std-infer-peeped-arguments(tctx, right, p2)
-               )
+            App{is-cons=is-cons, left=left, right=right} => (
+               (let lt, let new-left) = std-infer-peeped-arguments(tctx, left, p1);
+               (let rt, let new-right) = std-infer-peeped-arguments(tctx, right, p2);
+               if not(is(left,new-left)) || not(is(right,new-right))
+               then t = mk-cons-or-app(is-cons,new-left,new-right);
+               (t3(c"Cons",lt,rt), t)
             );
             _ => fail("std-infer-peeped-arguments expected cons term: \{t}\n");
          }
       );
-      TAny{} => ta;
-      _ => ( infer-expr(tctx, t, Unscoped, TAny, Used); typeof(t) );
+      TAny{} => (ta, t);
+      _ => (
+         (_, t) = std-infer-expr(tctx, t, false, Used, TAny);
+         (typeof(t), t);
+      );
    }
 );