modelexpansion in a procedure interpretation goes wrong
Issue #797
new
the main is not executed in this case
vocabulary V2 {}
theory T2 : V2 {}
structure S2 : V2 {}
vocabulary V {
type t //extern vocabulary types
P(t)
}
theory T : V {}
procedure isP(a){
modelexpand(T2,S2)
return false
}
structure S : V {
t = {1}
P = procedure isP
}
----------- Main
include <mx>
procedure main() {
print("hi")
}
Comments (5)
-
-
reporter bij mij geen segfault maar gewoon stoppen van executie. Ik blame bootstrapping (splitdefs), want met deze procedure werkt het wel:
procedure isP(a){ stdoptions.postprocessdefs = false stdoptions.splitdefs = false stdoptions.guaranteenorecursionnegation = true modelexpand(T2,S2) return false }
-
Inderdaad, splitdefs geeft hier de fout.
Maar in het algemeen, werkt dit niet. Als je je code bijvoorbeeld vervangt door
vocabulary V { type t //extern vocabulary types P(t) } theory T : V {} procedure isP(a){ stdoptions.verbosity.transformations=2 stdoptions.splitdefs = false print(modelexpand(T2,S2)[1]) return false } structure S : V { t = {1} P = procedure isP } ----------- Main include <mx> procedure main() { stdoptions.postprocessdefs = false print("hi") } vocabulary V2 {} theory T2 : V2 {} structure S2 : V2 {}
gaat het ook mis (zelfs zonder splitdefs).
Het probleem is dat er al een mx call wordt uitgevoerd vooraleer IDP in een consistente state is gebracht
-
reporter de "fout" in deze versie zit hier denk ik in de parsing waardoor T2 niet beschikbaar is aan isP
-
Inderdaad. Dus je moet nog geen calls uitvoeren voor de parser klaar is met de state op te bouwen.
- Log in to comment
This segfaults.