RFC: "Text-TT" textual s-expression format for compiled expressions

[evertedsphere]

This has to be cleaned up a bit before it's ready for merging. I'm open to any and all bikeshedding about the "Coredris" name or the actual sexp syntax (like the ^ sigil, or any naming for the ^foo forms or the :tags in them).

I am however convinced that the tag-based format is going to make it parser-friendly for anyone consuming the Coredris format, especially since every tag should correspond to a field of a record/struct in the consumer's AST format.

Questions

1. ~~is the type information I obtained manually actually of any use considering all any backend using this will do is simply pass around some kind of Any type (IdrisVal etc) and cast to expected types at primop application sites?~~ edit: types removed

Output examples

Here's a simple primop wrapper:

(fn
  #:name PrimIO_putStrLn
  #:args [arg_0]
  #:body (app #:fn PrimIO_putStr 
              #:args [(prim-app #:op ++ 
                                #:args [arg_0 
                                         (constant #:type 'string 
                                                   #:val "\u000a")])]))

and here is a slightly more involved example, with linebreaks manually inserted:

(fn
  #:name Prelude___Impl_Num_Integer
  #:args []
  #:body 
  (con #:tag 0 
    #:args 
    ['erased 
     (lam #:var arg_1928 
       #:body 
       (lam #:var arg_1929 
         #:body 
         (app 
           #:fn (app #:fn (call Prelude_-zpl_Num__Integer) #:args [arg_1928])
           #:args [arg_1929]))) 
     (lam #:var arg_1930 
       #:body 
       (lam #:var arg_1931 
         #:body 
         (app 
           #:fn (app #:fn (call Prelude_-zst_Num__Integer) #:args [arg_1930])
           #:args [arg_1931]))) 
     (lam #:var arg_1932 
          #:body (app 
                   #:fn (call Prelude_fromInteger_Num__Integer) 
                   #:args [arg_1932]))]))

[evertedsphere]

cc @edwinb

[jfdm]

This looks very interesting, thanks!

I was wondering if the named should refer to TT more than idris, especially as you are going from TT rather than Idris.

[evertedsphere]

Oh, I see what you're saying, that is probably the better way to go! If you have an alternative name that references TT instead of Idris, feel free to suggest it and I'll change it in the source. (I was thinking of it as "Idris Core" by analogy to GHC Core.)

[jfdm]

was thinking of it as "Idris Core" by analogy to GHC Core.

Funnily enough that is the correct analogy you are going for, and fortunately for Idris the core already has a name: TT.

I am not one for catchy names, so I would tend to go for informative ones to denote that it is TT but expressed using s-expression. Some examples: Textual-TT and TT-SExpr. These would be sufficient IMHO. TT-sExpressed if you want something interesting.

[evertedsphere]

Thanks for the suggestions, I'll keep them in mind! (Text-TT sounds funnily similar to \texttt{..})