Merge pull request #813 from andrew-johnson-4/remove-remaining-untype…

…d-fragments

Remove remaining untyped fragments

Cargo.toml

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

LIB/default-rules.lm

@@ -4,6 +4,9 @@ fragment type ReservedWord; atom suffix ReservedWord _r;
 macro ( ('let x y) )
       ( (λ x . ()) y );
 
+macro ( ('set lhs rhs) )
+      ( (mov( rhs lhs )) );
+
 macro ( ('for-each (item 'in iter) loop) ) (
    (let (uuid iter-term) iter)
    (while (non-zero (uuid iter-term)) (match (uuid iter-term) (

SRC/apply-direct.lm

@@ -1,12 +1,13 @@
 
-apply-direct := λ(: ctx FContext)(: arrow Fragment)(: args FragmentList)(: e-proto Fragment)(: chain U8)(: already-destructured U8). (: (
+apply-direct := λ(: ctx FContext)(: arrow Fragment)(: args FragmentList)(: e-proto Fragment)(: chain U8)(: already-destructured U8)(: blame AST). (: (
+   (let arrow-tt (.type arrow))
    (match (fragment::get( arrow 'fragment_s )) (
       ()
       ( (SCons( (SAtom 'Abs_s) (SCons( lhs rhs )) )) (
          (if (==( already-destructured True_u8 )) () (
-            (set ctx (destructure-lhs( ctx lhs args )))
+            (set ctx (destructure-lhs( ctx (p2(slot( arrow-tt 'Arrow_s ))) lhs args )))
          ))
-         (set e-proto (fragment::render( ctx rhs e-proto )))
+         (set e-proto (fragment::render( ctx rhs e-proto blame )))
       ))
       ( _ (
          (print 'Invalid\sFragment\sApplied:\n_s)

SRC/ascript.lm

@@ -1,8 +1 @@
 
-s-type-list := (: STEOF STypeList);
-ascript := λ(: t S)(: tt Type). (: (
-   (set s-type-list (STSeq(
-      (close s-type-list)
-      t tt
-   )))
-) Nil);

SRC/can-unify.lm

@@ -21,7 +21,7 @@ can-unify := λ(: fpt Type)(: pt Type). (: (
    (match (Tuple( fpt pt )) (
       ()
       ( (Tuple( TAny _ )) (set r 1_u64) )
-      ( (Tuple( (TGround( 'Meta_s _ )) _ )) (set r 1_u64) )
+      ( (Tuple( (TGround( 'Meta_s (LCons( _ _ )) )) _ )) (set r 1_u64) )
       ( (Tuple( (TVar( ltv )) rt )) (set r 1_u64) )
       ( (Tuple( (TAnd( lt1 lt2 )) rt )) (
          (if (can-unify( lt1 rt )) (

SRC/compile-define-tag-constructor.lm

@@ -1,19 +1,18 @@
 
-compile-define-tag-constructor := λ(: ctx FContext)(: tag String)(: arg-types Type)(: base-type Type)(: rtype Type)(: case-number U64). (: (
+compile-define-tag-constructor := λ(: ctx FContext)(: tag String)(: arg-types Type)(: base-type Type)(: rtype Type)(: case-number U64)(: blame AST). (: (
    (let tg (and( (t2( 'Constructor_s (t1 tag) )) (and( (t2( 'Sized_s (t1 '0_s) )) (t2( 'FieldsSized_s (t1 '0_s) )) )) )))
-   (let push-template (fragment-context::lookup( ctx 'template::push_s tg ASTEOF )))
-   (let movl-template (fragment-context::lookup( ctx 'template::mov_s (t3( 'Cons_s tg (t1 'LocalVariable_s) )) ASTEOF )))
-   (let movg-template (fragment-context::lookup( ctx 'template::mov_s (t3( 'Cons_s tg (t1 'GlobalVariable_s) )) ASTEOF )))
+   (let push-template (fragment-context::lookup( ctx 'template::push_s tg blame )))
+   (let movl-template (fragment-context::lookup( ctx 'template::mov_s (t3( 'Cons_s tg (t1 'LocalVariable_s) )) blame )))
+   (let movg-template (fragment-context::lookup( ctx 'template::mov_s (t3( 'Cons_s tg (t1 'GlobalVariable_s) )) blame )))
 
-   (let tag-tctx (TCtxBind( (close TCtxEOF) 'tag_s (t1 tag) ASTEOF )))
+   (let tag-tctx (TCtxBind( (close TCtxEOF) 'tag_s (t1 tag) blame )))
    (let case-tctx (SSLSeq( (close SSLEOF) 'case-number_s (SAtom(to-string case-number)) )))
 
    (let fragment push-template)
    (let arrow-tt (substitute( tag-tctx (.type fragment) )))
    (set fragment (fragment::set-type( fragment arrow-tt )))
    (set fragment (fragment::set( fragment 'fragment-type_s (SAtom 'Fragment_s) )))
    (let spt (substitute( case-tctx (fragment::get( fragment 'fragment_s )) )))
-   (ascript( spt (typeof( (fragment::get( fragment 'fragment_s )) )) ))
    (set fragment (fragment::set( fragment 'fragment_s spt )))
    (set ctx (fragment-context::bind(
       ctx 'push_s arrow-tt fragment
@@ -24,7 +23,6 @@ compile-define-tag-constructor := λ(: ctx FContext)(: tag String)(: arg-types T
    (set fragment (fragment::set-type( fragment arrow-tt )))
    (set fragment (fragment::set( fragment 'fragment-type_s (SAtom 'Fragment_s) )))
    (set spt (substitute( case-tctx (fragment::get( fragment 'fragment_s )) )))
-   (ascript( spt (typeof( (fragment::get( fragment 'fragment_s )) )) ))
    (set fragment (fragment::set( fragment 'fragment_s spt )))
    (set ctx (fragment-context::bind(
       ctx 'mov_s arrow-tt fragment
@@ -35,7 +33,6 @@ compile-define-tag-constructor := λ(: ctx FContext)(: tag String)(: arg-types T
    (set fragment (fragment::set-type( fragment arrow-tt )))
    (set fragment (fragment::set( fragment 'fragment-type_s (SAtom 'Fragment_s) )))
    (set spt (substitute( case-tctx (fragment::get( fragment 'fragment_s )) )))
-   (ascript( spt (typeof( (fragment::get( fragment 'fragment_s )) )) ))
    (set fragment (fragment::set( fragment 'fragment_s spt )))
    (set ctx (fragment-context::bind(
       ctx 'mov_s arrow-tt fragment

SRC/compile-expr-direct.lm

@@ -126,20 +126,6 @@ compile-expr-direct := λ(: ctx FContext)(: term AST)(: stack-offset I64)(: used
          (set e (compile-expr( ctx t stack-offset used )))
          (set e (fragment::set-type( e (typeof term) )))
       ))
-      ( (App( (App( (Var( 'set_s _ )) (Var( k _ )) )) rhs )) (
-         (let kt (typeof rhs))
-
-         (let e1 (compile-expr( ctx rhs stack-offset Used )))
-         (set e1 (fragment::set-type( e1 kt )))
-         (let e2 (fragment-context::lookup( ctx k kt term )))
-         (set e (fragment-apply( ctx stack-offset 'mov_s
-            (FLSeq( (close(FLSeq( (close FLEOF) e1 ))) e2 ))
-            (t3( 'Arrow_s (t3( 'Cons_s (.type e1) (.type e2) )) (t1 'Nil_s) ))
-            term
-         )))
-         (set e (fragment::set-context( e ctx )))
-         (set e (fragment::set-offset( e stack-offset )))
-      ))
       ( (App( (App( (Var( 'while_s _ )) cond )) body )) (
          (let e1 (cc-blob( ctx 'into-branch-conditional_s cond stack-offset )))
          (let e2 (compile-expr( (open(.context e1)) body (.offset e1) Unused )))

SRC/compile-gnu.lm

@@ -19,10 +19,6 @@ compile-gnu := λ. (: (
             (set global-ctx (fragment-context::bind(
                global-ctx k (typeof rhs) fragment
             )))
-            (match preview-program (
-               ()
-               ( (Seq( _ frg )) (ascript( (fragment::get( fragment 'fragment_s )) (typeof frg) )) )
-            ))
          ) ())
          (set preview-program rst)
       ))

SRC/compile-type-case.lm

@@ -4,12 +4,12 @@ compile-type-case := λ(: ctx FContext)(: base-type Type)(: rhs AST)(: case-numb
       ()
       ( (Lit( tag _ )) (
          (let rtype (TAnd( (close base-type) (close(parse-type tag)) )) )
-         (set ctx (compile-define-tag-constructor( ctx tag TAny base-type rtype case-number )))
+         (set ctx (compile-define-tag-constructor( ctx tag TAny base-type rtype case-number rhs )))
       ))
       ( (App( (Lit( tag _ )) args )) (
          (let atype (type-of-s args))
          (let rtype (TAnd( (close base-type) (close(parse-type tag)) )))
-         (set ctx (compile-define-tag-constructor( ctx tag atype base-type rtype case-number )))
+         (set ctx (compile-define-tag-constructor( ctx tag atype base-type rtype case-number rhs )))
       ))
       ( _ () )
    ))

SRC/destructure-lhs.lm

@@ -1,9 +1,9 @@
 
-destructure-lhs := λ(: ctx FContext)(: lhs S)(: args FragmentList). (: (
+destructure-lhs := λ(: ctx FContext)(: tt Type)(: lhs S)(: args FragmentList). (: (
    (match lhs (
       ()
       ( (SCons( (SAtom 'Var_s) (SAtom k) )) (
-         (let a-type (typeof lhs))
+         (let a-type tt)
          (match args (
             ()
             ( (FLSeq( _ f )) (
@@ -13,19 +13,14 @@ destructure-lhs := λ(: ctx FContext)(: lhs S)(: args FragmentList). (: (
                   (print f)
                   (exit 1_u64)
                ))
-               (set ctx (union( ctx (unify( a-type ft )) ))) # destructure tctx
+               (let tctx (unify( a-type ft )))
+               (set ctx (union( ctx tctx ))) # destructure tctx
                (set ctx (FCtxBind( (close ctx) k ft f )))
             ))
          ))
       ))
       ( (SCons( (SAtom 'App_s) (SCons( lhs-rst (SCons( (SAtom 'Var_s) (SAtom k) )) )) )) (
-         (let a-type TAny)
-         (match lhs (
-            ()
-            ( (SCons( (SAtom 'App_s) (SCons( _ binding )) )) (
-               (set a-type (typeof binding))
-            ))
-         ))
+         (let a-type (p1 tt))
          (match args (
             ()
             ( (FLSeq( fl-rst f )) (
@@ -35,12 +30,13 @@ destructure-lhs := λ(: ctx FContext)(: lhs S)(: args FragmentList). (: (
                   (print f)
                   (exit 1_u64)
                ))
-               (set ctx (union( ctx (unify( a-type ft )) )))
+               (let tctx (unify( a-type ft )))
+               (set ctx (union( ctx tctx )))
                (set ctx (FCtxBind( (close ctx) k ft f )))
                (set args fl-rst)
             ))
          ))
-         (set ctx (destructure-lhs( ctx lhs-rst args )))
+         (set ctx (destructure-lhs( ctx (p2 tt) lhs-rst args )))
       ))
       ( SNil () )
       ( _ (

SRC/fragment-apply.lm

@@ -36,7 +36,7 @@ fragment-apply := λ(: ctx FContext)(: offset I64)(: k String)(: args FragmentLi
       ))
    ))
 
-   (let return (apply-direct( ctx arrow args e-proto chain already-destructured )))
+   (let return (apply-direct( ctx arrow args e-proto chain already-destructured sloc )))
 
    # add comments if in GNU mode
    (if (is( config-assemble-mode AssembleGNU )) (

SRC/fragment::let.lm

@@ -1,5 +1,5 @@
 
-fragment::let := λ(: ctx FContext)(: s S). (: (
+fragment::let := λ(: ctx FContext)(: s S)(: blame AST). (: (
    (let return ctx)
    (match s (
       ()
@@ -10,15 +10,15 @@ fragment::let := λ(: ctx FContext)(: s S). (: (
            )) ))
            v
         )) )) (
-         (set v (fragment::render( return v )))
+         (set v (fragment::render( return v blame )))
          (set return (FCtxBind(
             (close return) k TAny (fragment::expression( v ))
          )))
       ))
       ( (SCons( (SAtom 'App_s) (SCons(
           ls rs
         )) )) (
-         (set return (fragment::let( return ls )))
+         (set return (fragment::let( return ls blame )))
       ))
       ( _ () )
    ))