`COMPILE to` definitions from `Haskell.*` modules

Open
  • Is something wrong?
#472 0 comments 1 reaction 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
48/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Domain
compilers

Research direction

Start by reproducing the example in the issue, comparing the working Vec mapping to List with the failing Fin mapping to Nat. Then trace how COMPILE AGDA2HS handles datatype targets from Haskell.* modules and identify what blocks Nat; done means the example compiles with the intended mapping. The issue does not name source files or tests.

Written by the indexing model from the issue text.

Description

enhancement

While COMPILE ... to List is supported, it seems that agda2hs doesn't support COMPILE ... to Nat and other datatypes from Haskell.* modules.

{-# OPTIONS --erasure #-}

module Issue where

open import Haskell.Prelude

private variable
  @0 n : Nat

-- Works

data Vec (a : Type) : @0 Nat → Type where
  []  : Vec a zero
  _∷_ : a → Vec a n → Vec a (suc n)
{-# COMPILE AGDA2HS Vec to List #-}

emptyVec : Vec a 0
emptyVec = []
{-# COMPILE AGDA2HS emptyVec #-}

-- Doesn't work

data Fin : @0 Nat → Type where
  zero : Fin (suc n)
  suc  : Fin n → Fin (suc n)
{-# COMPILE AGDA2HS Fin to Nat #-}

fzero : Fin 1
fzero = zero
{-# COMPILE AGDA2HS fzero #-}
Dominant language
Agda
Stars
211
Forks
51
Avg merge
1d 11h
Merged PRs (30d)
9

Getting set up

This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from agda/agda2hs

All issues in agda/agda2hs

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.