the intermediate language?

[Robert Watson]

Guys,

I'd like to really play with things under the hood more. I've heard there is an intermediate language between Idris2 proper and the underlying code. Is that the 'type system' or something a bit higher level? Anyway...How can I get to explore all that?

Thanks,

Robert

[G. Allais]

Hi Robert,

Here is a crude roadmap:

* `Idris.Syntax` defines the surface language
* `TTImp.TTImp` defines the (not typechecked) intermediate language
* `Core.Core` defines the core (typechecked) language
* `Core.Value` defines the (weak head) normal forms of `Core`

* `Idris.Desugar` desugars the Idris2 surface language into the TTImp
* `TTImp.Elab.*` typechecks & elaborates TTImp to Core
* `Core.Normalise` defines evaluation & conversion checks
* `Core.Unify` defines pattern unification for holey terms

Cheers,
--
gallais

On 02/04/2021 18:24, Robert Watson wrote:
> CAUTION: This email originated outside the University. Check before clicking links or attachments.

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com<mailto:idris-lang+...@googlegroups.com>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/ee2e1209-6837-499a-b325-301308a99f48n%40googlegroups.com<https://groups.google.com/d/msgid/idris-lang/ee2e1209-6837-499a-b325-301308a99f48n%40googlegroups.com?utm_medium=email&utm_source=footer>.
>

[Nicholas LeCompte]

Hi Robert,

If you weren’t aware, Edwin has a simplified, pedagogical implementation of Idris 2 (“TinyIdris”) which he presented last year at SPLV: 

https://github.com/edwinb/SPLV20 It includes a fairly detailed treatment of the intermediate languages, which are reasonably close to the “real” one used in Idris 2.

You might find it useful to explore the TinyIdris slides / code here first before looking at the proper implementation. I sure did! TinyIdris has similar types and modules to Idris 2, it’s just much smaller, so going through it first gives a really nice birds-eye-view of Idris 2 itself.

Edwin’s lectures from SPLV 2020 are also on YouTube: 

https://youtu.be/2pa3oRFNO8E

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/94f3d678-aef9-e8e9-c1f0-e82afe51196a%40ens-lyon.org.

[Robert Watson]

Awesome. Thanks both.

R

[Robert Watson]

For any other new user who's interested, the TinyIdris of SPLV20 won't work in Idris2 0.3, but seems to work so far using 0.2.1 ... https://github.com/idris-lang/Idris2/releases

R