ggreif / omega

Automatically exported from code.google.com/p/omega
Other
7 stars 0 forks source link

rules appear duplicated #53

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
What steps will reproduce the problem?
1. enter the check> prompt in a non-trivial case
i.e. <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue46-
SetEmulation.omg>
2. type :rules
3. observe
check> :rules
rules
Axiom S(Nat'): [] => Nat' (1+'j)t --> [Nat' 'j]
  Axiom Z(Nat'): [] => Nat' 0t --> []
  Axiom S(Nat'): [] => Nat' (1+'j)t --> [Nat' 'j]
  Axiom Z(Nat'): [] => Nat' 0t --> []

What is the expected output? What do you see instead?

I see duplicated axioms, and these definitely do not help with performance.
I would expect that each rule only appears once.
Please note, that this testcase only loads with a custom Omega, 
(branches/potentially-unsound).
I did not test on 1.4.2

Original issue reported on code.google.com by ggr...@gmail.com on 22 Dec 2007 at 6:31

GoogleCodeExporter commented 9 years ago
I have this reproduced.

---------------------
import "LangPrelude.prg"
import "somefile.prg"

three = check 42
---------------------

You will see that rules appear three times. While working on issue 67 I have 
observed this. My interpretation is 
that for the current file and all imports the predefined definitions get 
applied. Or at least their rules. It should 
only be applied for the current file.

Raising prio, because (in issue 67's context) this can lead to ambiguities:

  Axiom (DiffLabel): ['a != 'b] => DiffLabel 'a 'b --> []
  Axiom (DiffLabel): ['a != 'b] => DiffLabel 'a 'b --> []

Original comment by ggr...@gmail.com on 3 Nov 2009 at 6:41

GoogleCodeExporter commented 9 years ago
Something like this fixes the symptoms. Not sure that this is the real solution:

ggreif$ svn diff Toplevel.hs
Index: Toplevel.hs
===================================================================
--- Toplevel.hs (Revision 277)
+++ Toplevel.hs (Arbeitskopie)
@@ -21,7 +21,7 @@
              ,var_env,type_env,rules,runtime_env,syntaxExt)
 import RankN(pprint,Z,failD,disp0,dispRef)
 import System(getArgs)
-import Data.Map(Map,toList)
+import Data.Map(Map,toList,empty)
 import Directory
 import Char(isAlpha,isDigit)
 import System.IO(hClose)
@@ -221,7 +221,7 @@
 importFile (Import name vs) tenv =
   case lookup name (imports tenv) of
      Just previous -> return tenv
-     Nothing -> do { new <- elabFile name initTcEnv
+     Nothing -> do { new <- elabFile name (initTcEnv{rules = empty})
                    ; unknownExt vs (syntaxExt new)
                    ; return(importNames name vs new tenv) }

Original comment by ggr...@gmail.com on 3 Nov 2009 at 9:24

GoogleCodeExporter commented 9 years ago
Suggested fix checked in as r328.

Original comment by ggr...@gmail.com on 10 Mar 2010 at 9:02

GoogleCodeExporter commented 9 years ago

Original comment by ggr...@gmail.com on 10 Mar 2010 at 9:03