Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1798] branches/mango/Mango
|
From: <fra...@us...> - 2009-08-03 05:39:22
|
Revision: 1798
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1798&view=rev
Author: frankrimlinger
Date: 2009-08-03 05:39:15 +0000 (Mon, 03 Aug 2009)
Log Message:
-----------
Fixed more typing bugs, and arrived at a nominal parametrization of Class_MangoFormal.forName(). Refined logic for the type of a parameter. This type is stored persistently in the rulebase, and it not used by mango. It only has relevance for possible secondary theorem proving. Therefore, to the extent possible, we make this type correspond to ACL2 expectations, which differ in certain ways from those of mango. Chiefly, ACL2 makes no type distinction between a concrete integer and an expression that could evaluate to an integer. But mango does. The type exposed persistently is the "relatvie minimum" type of rev 1793.
Cleaned up the logic for assigned a parameter to a "group". These groups have no logical significance but make it easier to scan the parameter list. The group is now stored persistently in the description field of a parameter, with grandfathered groups just assigned "misc". This should be cleaned up some day.
Expressions which may be bound to context MUST NOT be of type <parameter>. This confuses the parameter harvester because it then gets two versions of the same thing, one with context, the other without. For the same reason, the harvestParameters operator now commutes with the rulekeys for state variable storage and access. It is really only looking for BinderSyms, functions, certain utility rulekeys and predicates. The good news is that all these specialized choices are now rulebased and moderated by the typing system for EZ tweaking.
NEXT BUG: For some reason, translation of hypotheses is picking up context free base expression, which is not what we want.
Revision Links:
--------------
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1793&view=rev
Modified Paths:
--------------
branches/mango/Mango/.settings/org.eclipse.jdt.core.prefs
branches/mango/Mango/Mango/src/mango/core/CoreRule.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java
branches/mango/Mango/Mango/src/mango/module/definition/trap/HarvestParametersTrap.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/Equals.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/OtherEqual.java
branches/mango/Mango/Mango/src/mango/ruleAction/function/engine/StabilizeParameterExp.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/definition/HarvestParameters.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/RenderParameterName.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/SingleQuotes.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateOpVar.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_unknownLocalVar.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_unknownOpVar.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/EnabledParameterReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/UnknownLocalVarReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/UnknownOpVarReq.java
branches/mango/Mango/Mango/src/mango/script/model/MangoScriptModel.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteEvent.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/LAsolver.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/OpVarSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/agent/StabilizeParameterAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/WorkFlowUtil.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/'className' is defined.zip
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/module/definition/agent/HarvestParametersAgent.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_doubleRelax.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_floatRelax.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_intRelax.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_longRelax.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_relaxedNumber.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ImmutableReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/DoubleRelaxReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/FloatRelaxReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/IntRelaxReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/LongRelaxReq.java
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/module/definition/agent/ParameterExpAgent.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/definition/HarvestLocalVariableFunction.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/AmbientLocal.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/Immutable.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
