lambda_mountain 1.12.9

Lambda Mountain
Documentation

preprocess-index-types := ();
	
preprocess := λprogram . (tail(
   (preprocess-index-typedefs program)
   (set program (preprocess-apply-macros program))
   (debug-memory-usage 'preprocess)
   program
));

preprocess-dump := λprogram . (tail(
   (while program (tail(
      (print-s (tail program))(print-s \n)
      (set program (head program))
   )))
));

preprocess-index-typedefs := λprogram . (tail(
   (while program (tail(
      (preprocess-index-typedef (tail program))
      (set program (head program))
   )))
));

preprocess-index-typedef := λterm . (match term (
   ()
   ( (Type( l ds )) (
      (preprocess-index-indices( ds 0 ))
   ))
));

preprocess-index-indices := λdef index . (match def (
   ()
   ( (App( (App( tds (Variable '|) )) body )) (tail(
      (preprocess-index-indices( tds (i2s(inc(s2i index))) ))
      (preprocess-index-index( body index ))
   )))
   ( body (
      (preprocess-index-index( body index ))
   ))
));
	
preprocess-index-index := λbody index . (match body (
   ()
   ( (Literal tag) (tail(
      (set preprocess-index-types (preprocess-index-types (tag index)))
   )))
   ( (App( (Literal tag) args )) (tail(
      (set preprocess-index-types (preprocess-index-types (tag index)))
   )))
));

preprocess-index-of-tag := λtag . (tail(
   (local indices)
   (local index)
   (set indices preprocess-index-types)
   (while indices (tail(
      (if (eq( (head(tail indices)) tag )) (
         (set index (tail(tail indices)))
      ) ())
      (set indices (head indices))
   )))
   index
));

substitute-macro-body := λkvs e . (match e (
   ()
   ((Variable n) (tail(
      (while kvs (match kvs (
         ()
         ( Accept (set kvs ()) )
         ( (ks Accept) (set kvs ks) )
         ( (ks ()) (set kvs ks) )
         ( (ks (KV(k v))) (
            (if (eq(n k)) (tail(
               (set e v)
               (set kvs ())
            )) (
               (set kvs ks)
            ))
         ))
         ( u (fail (UnrecognizedKVMacro kvs)))
      )))
      e
   )))
   ( () () )
   ( (vl vr) (
      (substitute-macro-body( kvs vl ))
      (substitute-macro-body( kvs vr ))
   ))
   ( v v )
));

try-destructure-macro := λlhs e . (match (lhs e) (
   ()
   ( ( Nil Nil ) Accept )
   ( ( (App(pl pr)) (App(el er)) ) (tail(
      (local ll)
      (set ll (try-destructure-macro(pl el)))
      (if ll (tail(
         (local rl)
         (set rl (try-destructure-macro(pr er)))
         (if rl (
            (merge-list( ll rl ))
         ) ())
      )) ())
   )))
   ( ((Literal pl) (Variable el)) (
      (if (eq( pl el )) Accept ())
   ))
   ( ((Literal pl) (Literal el)) (
      (if (eq( pl el )) Accept ())
   ))
   ( ( (App( (Literal :Literal:) (Variable pv) )) (Literal el)) (
      (if (preprocess-index-of-tag el)
         ()
         (Accept (KV( pv e )))
      )
   ))
   ( ( (App( (Literal :Variable:) (Variable pv) )) (Variable el)) (
      (Accept (KV( pv e )))
   ))
   ( ( (App( (App( (Literal :Tag:) (Variable pv) )) (Variable pt) )) (Literal el)) (
      (if (preprocess-index-of-tag el)
         (  Accept
            (KV(
               pv
               (App(
                  (App(
                      (Literal :)
                     (Literal (preprocess-index-of-tag el))
                  ))
                  (preprocess-restructure-type(parse-type( Constant+Literal+U64 )))
               ))
            ))
            (KV(
               pt
               (preprocess-restructure-type(parse-type( el )))
            ))
         )
         ()
      )
   ))
   ( ((Variable pv) e) (
      (Accept (KV( pv e )))
   ))
));

preprocess-destructure-type := λtt . (
   (preprocess-restructure-type( parse-type tt ))
);

preprocess-restructure-type := λtt . (match tt (
   ()
   ( (And( lt rt )) (
      (App(
         (Literal And)
         (App(
            (preprocess-restructure-type lt)
            (preprocess-restructure-type rt)
         ))
      ))
   ))
   ( (Array( lt rt )) (
      (App(
         (Literal Array)
         (App(
            (preprocess-restructure-type lt)
            (preprocess-restructure-type rt)
         ))
      ))
   ))
   ( (tag lts) (
      (if (is-atom tag) (
         (App(
            (Literal tag)
            (preprocess-restructure-type lts)
         ))
      ) (
         (fail (InvalidRestructureType tag lts))
      ))
   ))
   ( () (fail (InvalidRestructureType ())))
   ( tag-or-variable (
      (if (is-variable tag-or-variable) (
         (Variable tag-or-variable)
      ) (
         (Literal tag-or-variable)
      ))
   ))
));

is-macro-head := λname . (match name (
   ()
   ('let True)
   ('match True)
   ('match-pats True)
   ('match-pats-arm True)
));

preprocess-apply-macros := λprogram . (match program (
   ()
   ( (App( (App( (Literal :) mvar )) (Literal mtype) )) (
     (App( (App( (Literal :) (preprocess-apply-macros mvar) )) (preprocess-destructure-type mtype) ))
   ))
   ( (App( (App( (Literal :) mvar )) (Variable mtype) )) (
     (App( (App( (Literal :) (preprocess-apply-macros mvar) )) (preprocess-destructure-type mtype) ))
   ))
   ( (Literal l) (tail(
      (local suffixes)
      (set suffixes parse-suffix)
      (while suffixes (tail(
         (local sfx)
         (set sfx (tail (tail suffixes)) )
         (if (is-suffix( l sfx )) (tail(
            (local literal-type)
            (set literal-type (preprocess-restructure-type(parse-type(clone-rope((Constant+Literal+ (head(tail( suffixes ))) ))))) )
            (set program (
               (App(
                  (App(
                     (Literal ':)
                     (Literal (remove-suffix( l sfx )))
                  ))
                  literal-type
               ))
            ))
         )) ())
         (set suffixes (head suffixes))
      )))
      program
   )))
   ( (Variable l) (tail(
      (local suffixes)
      (set suffixes parse-suffix)
      (while suffixes (tail(
         (local sfx)
         (set sfx (tail (tail suffixes)) )
         (if (is-suffix( l sfx )) (tail(
            (local literal-type)
            (set literal-type (preprocess-restructure-type(parse-type(clone-rope((Constant+Literal+ (head(tail( suffixes ))) ))))) )
            (set program (
               (App(
                  (App(
                     (Literal ':)
                     (Literal (remove-suffix( l sfx )))
                  ))
                  literal-type
               ))
            ))
         )) ())
         (set suffixes (head suffixes))
      )))
      program
   )))
   ( (App( (Variable vn) vt )) (
      if (is-macro-head vn) (preprocess-apply-maybe program)
         (App( (Variable vn) (preprocess-apply-macros vt) ))
   ))
   ( (App( (App( (Variable vn) vt1 )) vt2 )) (
      if (is-macro-head vn) (preprocess-apply-maybe program)
         (App( (App( (Variable vn) (preprocess-apply-macros vt1) ))
                                   (preprocess-apply-macros vt2) ))
   ))
   ( (l r) (
      (preprocess-apply-macros l)
      (preprocess-apply-macros r)
   ))
   ( u u )
));

preprocess-macro-args := λ ctx kvs . (match kvs (
   ()
   ( (KV( k v )) (KV(k (substitute-macro-body( ctx v )) )) )
   ( (k v) (
      (preprocess-macro-args( ctx k ))
      (preprocess-macro-args( ctx v ))
   ))
   ( u u )
));

preprocess-apply-maybe := λ program . (tail(
   (local macros)
   (set macros parse-macros)
   (while macros (match macros (
      ()
      ( (ms (Macro( lhs rhs ))) (tail(
         (local new)
         (set new (try-destructure-macro( lhs program )))
         (if new (tail(
            (set program (substitute-macro-body( new rhs )))
            (set program (parse-macro-substitute-uuids (
               (parse-macro-yield-uuids( () program ))
               program
            )))
            (set program (preprocess-apply-macros program))
            (set macros ())
         )) (
            (set macros ms)
         ))
      )))
      ( u (fail (UnrecognizedMacro u)))
   )))
   (match program (
      ()
      ( (l r) (
         (preprocess-apply-macros l)
         (preprocess-apply-macros r)
      ))
      ( () () )
      (u u)
   ))
))