[Agda] type check cost

[Sergei Meshveliani]

On Wed, 2015-10-07 at 21:54 +0200, Nils Anders Danielsson wrote:
> On 2015-10-07 21:42, Sergei Meshveliani wrote:
> > It reports
> >
> > ------------------------------
> > ...
> > /home/mechvel/doconA/0.04/source/DPrelude.agda:275,46-63
> > Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
> >    _Respects2_ _~_ _≈_
> >    _Respects2_ _~_ _≈_
> > ...
> >
> > Operators used in the grammar:
> >    Respects2 (infix operator, level 20) [_Respects2_
> > (/home/mechvel/doconA/0.04/source/DPrelude.agda:245,1-12)]
> > (the treatment of operators has changed,
> > ...
> > -----------------------------
> 
> Can you give a self-contained example?
> 
> > As I recall, there was a certain recent development version which
> > required fixity decl for each operator.
> > But  agda-2.4.2.4  has rejected this fixity requirement.
> > Right?
> 
> Agda 2.4.2.4 was a maintenance release.
> 
> > Now, what have I to do, to set fixities everywhere in my (large) code?
> 
> We decided not to remove default fixities. However, some things have
> changed. If you provide me with a small, self-contained example, then I
> can perhaps help you.
> 


Please, see the attachment.


I have taken the development Agda by following this:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

-------------------------------
Development version
The development version contains new, unstable features. Installation is
not recommended, except for the initiated.

      * Git repository. README. New features.
      * You can get the development version as follows: 
        
        git clone https://github.com/agda/agda.git
-------------------------------

I applied this

  git clone https://github.com/agda/agda.git

(very probably, I recall this correct), and have installed it.

------
Sergei
-------------- next part --------------
module TT where
open import Level using (_⊔_)
open import Function using (_∘_; _$_; _on_)
open import Relation.Binary using (Rel; _Preserves₂_⟶_⟶_; _Respects_; 
                                        _Respects₂_; _Preserves_⟶_)
open import Data.Product using (_×_; _,_) 


infix 3 _←→_

_←→_ : ∀ {α β} (A : Set α) → (B : Set β) → Set (α ⊔ β) 
_←→_ A B =  (A → B) × (B → A)

_Respects2_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
_Respects2_ _~_ _≈_ =
                      ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ~ y → x' ~ y'

Respects₂gen : ∀ {α α= β β= ℓ} {A : Set α} {B : Set β} → 
                                 (A → B → Set ℓ) → Rel A α= → Rel B β= → Set _
Respects₂gen _~_ _~₁_ _~₂_ = 
                           ∀ {x x' y y'} → x ~₁ x' → y ~₂ y' → x ~ y → x' ~ y'

Respects2←→Respects₂gen : 
           ∀ {a ℓ₁ ℓ₂} {A : Set a} → (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) → 
                                 _~_ Respects2 _≈_ ←→ Respects₂gen _~_ _≈_ _≈_

Respects2←→Respects₂gen {a} {ℓ₁} {ℓ₂} {A} _≈_ _~_ = 
                                                   (to _≈_ _~_ , from _≈_ _~_)
  where    
  to : (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) → _~_ Respects2 _≈_ → 
                                             Respects₂gen _~_ _≈_ _≈_  
  to _≈_ _~_ ~resp≈ x≈x' y≈y' x~y =  ~resp≈ x≈x' y≈y' x~y
 
  from : (_~_ : Rel A ℓ₁) → (_≈_ : Rel A ℓ₂) → Respects₂gen _~_ _≈_ _≈_ → 
                                                            _~_ Respects2 _≈_
  from _~_ _≈_ ~resp'≈≈ x≈x' y≈y' x~y =  ~resp'≈≈ x≈x' y≈y' x~y