Export to DK does not handle opaque symbols

[thomastraversie]

When trying to export the Lambdapi code

symbol Prop : TYPE;
symbol Prf : Prop → TYPE;

opaque symbol theorem1 : Π P : Prop, Prf P → Prf P ≔
λ P : Prop, λ pP : Prf P, pP;

opaque symbol theorem2 : Π P : Prop, Prf P → Prf P ≔
begin 
    assume P pP;
    refine pP 
end;

to Dedukti, the theorems are just translated as definitions:

def Prop : Type.
def Prf : (Prop -> Type).
def theorem1 : (P : Prop -> ((Prf P) -> (Prf P))).
def theorem2 : (P : Prop -> ((Prf P) -> (Prf P))).

[fblanqui]

I see. Currently, the export to dk is done after compilation but compilation does not record the definition of opaque symbols to save memory. To avoid this problem, we should modify the export to dk so that it is done just after parsing, like we do for the coq export. This would be much more efficient.

[fblanqui]

Hi Thomas. One solution is make a copy of your files, remove the opaque modifiers with sed, and export files.

I'm working on having a dk output which does not require elaboration. But it won't be able to handle proofs. Proofs can only be translated after compilation.

[thomastraversie]

I see, thanks for the solution.

[fblanqui]

See #1060