search

namme-anetten / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

runElab True/False calls does not (seem to) respect the not toplevel/toplevel distinction #51

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
If I understand correctly the True/False convention, runElab is called with 
True iif it is not at the top-level.

So, I wrote the following code instead: 

> isTopLevel = do
>   ls <- getLayers
>   case ls of 
>     B0 -> return True
>     _ -> return False

> runElab _ (ty :>: elab) = do
>     atTopLevel <- isTopLevel
>     case atTopLevel of
>       False -> runElab' True (ty :>: elab)
>       True -> do
>                ty' <- bquoteHere ty
>                x <- pickName "h" ""
>                make (x :<: ty')
>                goIn
>                (tm :=>: tmv, okay) <- runElab' True (ty :>: elab)
>                if okay
>                  then  return . (, True)  =<< neutralise =<< giveOutBelow tm
>                  else  return . (, False) =<< neutralise =<< 
getCurrentDefinition <* goOut

Renaming the current runElab to runElab'. That is, I ignore the Boolean flag 
and dynamically check whether we are at the toplevel or not. However, in 
Solution.pig, the result diverges:

@@ -35,6 +37,8 @@
     ] ;
   hope := HOPE? : :- M.D == ((: Set) Set) ;
   G := coe M.D Set hope M.d : Set ;
-  hope := hope^1 : :- M.D == ((: Set) Set) ;
+  h7
+    [ hope := hope^1 : :- M.D == ((: Set) Set) ;
+    ] coe M.D Set hope M.d : Set ;
 ]
 Loaded.

Which means that the "hope" goal is created thinking that we are at the 
toplevel while we actually aren't.

I don't know if this is a bug or not. But the specification of this boolean 
flag should match its actual semantics. Also, although the code above is 
drafty, it might be worth removing the flags (if possible) and doing a dynamic 
check instead. It doesn't cost much and removes some burden on the programmer.

Original issue reported on code.google.com by pedag...@gmail.com on 25 Aug 2010 at 9:06

GoogleCodeExporter commented 9 years ago 
> Which means that the "hope" goal is created thinking that we are at the 
toplevel while we actually aren't.

That's the other way around: the "hope" goal is created as if we weren't at the 
toplevel, while we actually are...

Original comment by pedag...@gmail.com on 25 Aug 2010 at 10:15

GoogleCodeExporter commented 9 years ago 
After having looked at the way the flag is (ab)used, I understand why this 
didn't worked. The semantics of the flag is clearly *not the one* we currently 
give, although it's not clear what its semantics *actually is* (for me at 
least).

Original comment by pedag...@gmail.com on 26 Aug 2010 at 4:52

GoogleCodeExporter commented 9 years ago 
Sorry, you have been led astray by my poor name choice and lack of 
documentation. The top-level flag does not refer to depth in the proof state: 
rather, it means that the current goal should be solved by the elaborator. When 
not at the top level, the elaborator has to create a subgoal for anything that 
involves manipulating the proof state (e.g. introducing a lambda). I will work 
on RunElab to explain this in more detail.

Original comment by adamgundry on 30 Aug 2010 at 8:27

GoogleCodeExporter commented 9 years ago 
I've rewritten RunElab and related files to explain things more clearly 
(hopefully). Next step, editing Wire.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100830100124-e29d1-e9638070ec
64505b00fc6fd6e9891780ee715c06.gz

Original comment by adamgundry on 30 Aug 2010 at 12:10

GoogleCodeExporter commented 9 years ago 
Wire now has PropagateStatus instead of AtToplevel; the names aren't the best, 
but hopefully between them and the improved documentation things should be 
clearer. This all serves me right for using boolean flags in the first place.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100830155557-e29d1-8fff017929
4bdee1e045f83192b6afef759f926a.gz

Original comment by adamgundry on 31 Aug 2010 at 8:16