The agda2dedukti from deducteam

Problems with stdlib translation

When translating this file from the stdlib, I ran into a pattern of the form DefP used for HITs, which then fails as the translator does not support them. However, the file being translated does not use cubical features, and the function which causes a problem is the following, which does not appear to have nothing to do with HITs.

recompute : ∀ {a} {A : Set a} → Dec A → .A → A
recompute (yes x) _ = x
recompute (no ¬p) x = ⊥-elim (¬p x)

When looking at the case tree, we have the fragment (not showing everything, as it's too huge)

funCompiled     =
  case 2 of
    eta Relation.Nullary._because_ ->
      case 2 of
	Agda.Builtin.Bool.Bool.false ->
	  case 2 of
	    Relation.Nullary.Reflects.ofⁿ ->
	      done[{_}, {_}, ¬p, x]
		Data.Empty.Irrelevant.⊥-elim {@3} {@2} (@1 @0)
	    Agda.Primitive.Cubical.primHComp ->
	      done[{_}, {_}, {_}, {_}, {_}, _, _, _]
		Agda.Primitive.Cubical.primComp
		  {λ i -> @8} (λ i -> @7)
		  {Agda.Primitive.Cubical.primIMax @3 Agda.Primitive.Cubical.i0}
		  (λ i ->
		     λ o ->
		       Relation.Nullary.recompute
			 {@9} {@8}
			 (Relation.Nullary._because_
			    Agda.Builtin.Bool.Bool.false (@4 @1 @0))
			 (Agda.Primitive.Cubical.primTransp
			    {λ i -> @10} (λ i -> @9)
			    (Agda.Primitive.Cubical.primIMax
			       (Agda.Primitive.Cubical.primINeg
				  (Agda.Primitive.Cubical.primINeg @1))
			       Agda.Primitive.Cubical.i0)
			    @2))
		  (Relation.Nullary.recompute
		     {@7} {@6}
		     (Relation.Nullary._because_
			Agda.Builtin.Bool.Bool.false @1)
		     (Agda.Primitive.Cubical.primTransp
			{λ i -> @8} (λ i -> @7)
			(Agda.Primitive.Cubical.primIMax
			   (Agda.Primitive.Cubical.primINeg
			      (Agda.Primitive.Cubical.primINeg
				 Agda.Primitive.Cubical.i0))
			   Agda.Primitive.Cubical.i0)
			@0))

which is quite weird, as the branches using cubical primitives do not appear in the original definition. @jespercockx do you have an idea of what might be happening? Are those maybe inserted internally to discharge the branches with impossible indices? If so, does this mean that the cubical part of Agda is also used in the "standard" one?

Which ghc libraries are needed to compile Agda2Dedukti ?

14:47 ~/src/Agda2Dedukti (master) make
cd src/ && ghc Main
[1 of 3] Compiling Agda2Dk.DkSyntax ( Agda2Dk/DkSyntax.hs, Agda2Dk/DkSyntax.o )

Agda2Dk/DkSyntax.hs:5:1: error:
    Could not find module ‘Data.List.Unique’
    Use -v to see a list of the files searched for.
  |
5 | import Data.List.Unique
  | ^^^^^^^^^^^^^^^^^^^^^^^
make: *** [Makefile:14 : compile] Erreur 1

Which ghc libraries need to be installed?

deducteam / agda2dedukti Goto Github PK

agda2dedukti's People

Contributors

Stargazers

Watchers

Forkers

agda2dedukti's Issues

Problems with stdlib translation

Continuous integration missing

Which ghc libraries are needed to compile Agda2Dedukti ?

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent