[Agda] Records with parameters depending on fields?

[Joachim Breitner]

Hi,

on my way from Eugene to Portland, I finished the
correct-according-to-the-typechecker compiler form lambda terms to the
SECD machine. One uglifying change that I had to do was to turn the
record

        record Snapshot Θ t : Set where
          constructor snapshot
          field
            {Δ}         : StackType
            stack       : Stack Δ
            { Γ }       : Cxt
            environment : Env Γ
            control     : Control Γ (Θ ++ Δ) [ t ]

into a data type

data Snapshot Θ t : (All El Θ → El t) → Set where
  snapshot : ∀{Δ sss Γ} {env : Env Γ} {scon : CSem Γ (Θ ++ Δ) t} →
             (stack : Stack Δ sss) → 
             (environment : VEnv Γ env) →
             (control : Control Γ (Θ ++ Δ) t scon) →
             Snapshot Θ t (λ ss' → scon env (joinAll ss' sss))

because I could not see how I can make the last parameter of Snapshot an
index that depends on the actual fields of the constructor. Is there a
way to do that?

Thanks,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140629/d057ebba/attachment.bin