[teyjus] r1180 committed - Renaming clash error messages, documentation, and tests...

[tey...@googlecode.com]

Revision: 1180
Author: mitc...@gmail.com
Date: Wed Feb 4 05:50:42 2015 UTC
Log: Renaming clash error messages, documentation, and tests

Modified the error messages when a renaming clash is detected to be more
helpful. Modified the grammar for the wiki to include renaming in signature
and
module renaming. Added a couple of test cases to the renaming tests.


https://code.google.com/p/teyjus/source/detail?r=1180

Added:
/branches/RenamingRedux/source/test/renaming_tests/test2/inclusionstar.mod
/branches/RenamingRedux/source/test/renaming_tests/test2/inclusionstar.sig

/branches/RenamingRedux/source/test/renaming_tests/test2/manualinclusion.mod

/branches/RenamingRedux/source/test/renaming_tests/test2/manualinclusion.sig
/branches/RenamingRedux/source/test/renaming_tests/test6
/branches/RenamingRedux/source/test/renaming_tests/test6/accumulating.mod
/branches/RenamingRedux/source/test/renaming_tests/test6/accumulating.sig
/branches/RenamingRedux/source/test/renaming_tests/test6/base.sig
/branches/RenamingRedux/source/test/renaming_tests/test6/expected.mod
/branches/RenamingRedux/source/test/renaming_tests/test6/expected.sig
/branches/RenamingRedux/source/test/renaming_tests/test6/main.om
/branches/RenamingRedux/source/test/renaming_tests/test7
/branches/RenamingRedux/source/test/renaming_tests/test7/accumulating.mod
/branches/RenamingRedux/source/test/renaming_tests/test7/accumulating.sig
/branches/RenamingRedux/source/test/renaming_tests/test7/base.sig
/branches/RenamingRedux/source/test/renaming_tests/test7/expected.mod
/branches/RenamingRedux/source/test/renaming_tests/test7/expected.sig
/branches/RenamingRedux/source/test/renaming_tests/test7/main.om
/branches/RenamingRedux/source/test/renaming_tests/test8
/branches/RenamingRedux/source/test/renaming_tests/test8/accumulating.mod
/branches/RenamingRedux/source/test/renaming_tests/test8/accumulating.sig
/branches/RenamingRedux/source/test/renaming_tests/test8/base.mod
/branches/RenamingRedux/source/test/renaming_tests/test8/base.sig
/branches/RenamingRedux/source/test/renaming_tests/test8/expected.mod
/branches/RenamingRedux/source/test/renaming_tests/test8/expected.sig
/branches/RenamingRedux/source/test/renaming_tests/test8/main.om
/branches/RenamingRedux/source/test/renaming_tests/test9
/branches/RenamingRedux/source/test/renaming_tests/test9/accumulating.mod
/branches/RenamingRedux/source/test/renaming_tests/test9/accumulating.sig
/branches/RenamingRedux/source/test/renaming_tests/test9/base.mod
/branches/RenamingRedux/source/test/renaming_tests/test9/base.sig
/branches/RenamingRedux/source/test/renaming_tests/test9/expected.mod
/branches/RenamingRedux/source/test/renaming_tests/test9/expected.sig
/branches/RenamingRedux/source/test/renaming_tests/test9/main.om
/branches/RenamingRedux/tmp-docs/mod-grammar.txt
/branches/RenamingRedux/tmp-docs/sig-grammar.txt
/branches/RenamingRedux/tmp-docs/tests.txt
Modified:
/branches/RenamingRedux/source/compiler/translate.ml

/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/base.sig

/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/clash.sig

/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_name_overlap/base.sig
/branches/RenamingRedux/source/test/renaming_tests/OMakefile
/branches/RenamingRedux/source/test/renaming_tests/test2/main.om
/branches/RenamingRedux/source/test/renaming_tests/tests.txt
/branches/RenamingRedux/tmp-docs/wiki-updates.txt

=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test2/inclusionstar.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+module inclusionstar.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test2/inclusionstar.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+sig inclusionstar.
+
+accum_sig base {*}.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test2/manualinclusion.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+module manualinclusion.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test2/manualinclusion.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+sig manualinclusion.
+
+accum_sig base {kind a, type x}.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test6/accumulating.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+module accumulating.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test6/accumulating.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+sig accumulating.
+
+accum_sig base {}.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test6/base.sig Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig base.
+
+kind a type.
+
+type x int.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test6/expected.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+module expected.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test6/expected.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+sig expected.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test6/main.om Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+MAIN = accumulating
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test7/accumulating.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+module accumulating.
+
+accumulate base {*}.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test7/accumulating.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+sig accumulating.
+
+accum_sig base {kind a}.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test7/base.sig Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig base.
+
+kind a type.
+
+type x int.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test7/expected.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+module expected.
+
+accumulate base.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test7/expected.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+sig expected.
+
+kind a type.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test7/main.om Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+MAIN = accumulating
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test8/accumulating.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+module accumulating.
+
+accumulate base {*}.
+
+y A :- x A.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test8/accumulating.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig accumulating.
+
+accum_sig base {kind a}.
+
+type y int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test8/base.mod Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,3 @@
+module base.
+
+x 1.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test8/base.sig Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig base.
+
+kind a type.
+
+type x int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test8/expected.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+module expected.
+
+accumulate base.
+
+y A :- x A.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test8/expected.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig expected.
+
+kind a type.
+
+type y int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test8/main.om Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+MAIN = accumulating
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test9/accumulating.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+module accumulating.
+
+accumulate base {kind a, type z}.
+
+y A :- z A.
=======================================
--- /dev/null
+++
/branches/RenamingRedux/source/test/renaming_tests/test9/accumulating.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig accumulating.
+
+accum_sig base {kind a}.
+
+type y int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test9/base.mod Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,7 @@
+module base.
+
+type x int -> o.
+
+x 1.
+
+z A :- x A.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test9/base.sig Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig base.
+
+kind a type.
+
+type z int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test9/expected.mod
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+module expected.
+
+accumulate base.
+
+y A :- z A.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test9/expected.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,5 @@
+sig expected.
+
+kind a type.
+
+type y int -> o.
=======================================
--- /dev/null
+++ /branches/RenamingRedux/source/test/renaming_tests/test9/main.om Wed
Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+MAIN = accumulating
=======================================
--- /dev/null
+++ /branches/RenamingRedux/tmp-docs/mod-grammar.txt Wed Feb 4 05:50:42
2015 UTC
@@ -0,0 +1,108 @@
+<Module> ::= <ModHeader> <ModPreamble> <ModBody> <ModEnd>
+
+<ModHeader> ::= 'module' <NameToken> '.'
+
+<ModEnd> ::= '$' % $ stands for eof
+ | 'end'
+
+<ModPreamble> ::= <Empty>
+ | 'import' <QualifiedNames> '.' <ModPreamble>
+ | 'accumulate' <QualifiedNames> '.' <ModPreamble>
+ | 'accum_sig' <QualifiedNames> '.' <ModPreamble>
+ | 'use_sig' <QualifiedNames> '.' <ModPreamble>
+
+<ModBody> ::= <Empty>
+ | <ModSignDecl> <ModBody>
+ | <ModClause> <ModBody>
+
+<ModSignDecl> ::= <Sign-Decl>
+ | 'local' <Ids> '.'
+ | 'local' <Ids> <Type> '.'
+ | 'localkind' <Ids> '.'
+ | 'localkind' <Ids> <Kind> '.'
+
+<ModClause> ::= <Clause> '.'
+
+<Clause> ::= <Atom>
+ | <Clause> ':-' <Goal>
+ | <Goal> '=>' <Clause>
+ | <Clause> ',' <Clause>
+ | <Clause> '&' <Clause>
+ | <PiId> <TypedId> '\' <Clause>
+ | <PiId> <CTerm>
+ | '(' <Clause> ')'
+
+<Goal> ::= '!'
+ | <PiId> <Term>
+ | <PiId> <TypedId> '\' <Goal>
+ | <SigmaId> <Term>
+ | <SigmaId> <TypedId> '\' <Goal>
+ | <Goal> ';' <Goal>
+ | <Goal> ',' <Goal>
+ | <Goal> '&' <Goal>
+ | <Clause> '=>' <Goal>
+ | <Atom>
+ | <FlexAtom>
+ | '(' <Goal> ')'
+
+
+<Atom> ::= <Term> { the type of the term must be boolean
+ and its main functor must be a constant
+ or a variable bound by an enclosing
+ essential universal quantifier }
+
+<FlexAtom> ::= <TypedVar>
+ | <FlexAtom> <AppTerm>
+ | '(' <FlexAtom> ')'
+
+
+<CTerm> ::= <Term> { The main functor of the term must be a
+ constant or a variable bound by an
+ enclosing essential universal
+ quantifier }
+
+<Term> ::= <Term> <TypedCIdent> <Term>
+ | <Term> <TypedCIdent>
+ | <TypedCIdent> <Term>
+ | <Term> <Term>
+ | <TypedId> '\' <Term>
+ | '[' ']' % Prolog list notation
+ | '[' TermList ']' % Prolog list notation
+ | '[' TermList '|' Term ']' % Prolog list notation
+ | <TypedCIdent>
+ | <TypedVar>
+ | <TypedId>
+ | '(' <Term> ')'
+
+<TermList> ::= <Term>
+ | <Term> ',' <TermList>
+
+<PiId> ::= 'pi'
+ | 'pi' ':' <Type>
+ | '(' <PiId> ')'
+
+<SigmaId> ::= 'sigma'
+ | 'sigma' ':' <Type>
+ | '(' <SigmaId> ')'
+
+<TypedId> ::= <AbsToken>
+ | <AbsToken> ':' <Type>
+ | '(' <TypedId> ')'
+
+<TypedVar> ::= <VIdent>
+ | <VIdent> ':' <Type>
+ | '(' <TypedVar> ')'
+
+<TypedCIdent> ::= <SpecialOp>
+ | <Id>
+ | <Id> ':' <Type>
+ | '(' <TypedCIdent> ')'
+
+<SpecialOp> ::= { A pseudo keyword corresponding to one of the
+ overloaded operators }
+
+<AbsToken> ::= { A <NameToken> that does not begin with _ }
+
+<VIdent> ::= { A Teyjus token that begins with an uppercase
+ letter or _ and that is not the variable bound
+ by an enclosing abstraction }
=======================================
--- /dev/null
+++ /branches/RenamingRedux/tmp-docs/sig-grammar.txt Wed Feb 4 05:50:42
2015 UTC
@@ -0,0 +1,87 @@
+== A BNF Specification of Signature Syntax ==
+
+{{{
+<Signature> ::= <SigHeader> <SigPreamble> <Sign-Decls> <SigEnd>
+
+<SigHeader> ::= 'sig' <NameToken> '.'
+
+<SigEnd> ::= 'end' | '$' % $ stands for eof
+
+<SigPreamble> ::= <Empty>
+ | accum_sig <QualifiedSigs> '.' <SigPreamble>
+ | use_sig <QualifiedSigs> '.' <SigPreamble>
+
+<QualifiedNames> ::= <QualifiedName>
+ | <QualifiedName> ',' <QualifiedNames>
+
+<QualifiedName> ::= <NameToken>
+ <NameToken> '{}'
+ | <NameToken> '{' <Renamings> '}'
+
+<Renamings> ::= <Renaming>
+ | <Renaming> ',' <Renamings>
+
+<Renaming> ::= 'kind' <NameToken>
+ | 'kind' <NameToken> '=>' <NameToken>
+ | 'type' <NameToken>
+ | 'type' <NameToken> '=>' <NameToken>
+ | '*'
+
+<Sign-Decls> ::= <Empty>
+ | <Sign-Decl> <Sign-Decls>
+
+<Sign-Decl> ::= 'kind' <Ids> <Kind> '.'
+ | 'typeabbrev' <AbbrForm> <Type> '.'
+ | 'type' <Ids> <Type> '.'
+ | <Fixity> <Ids> <SmallInt> '.'
+ | 'exportdef' <Ids> '.'
+ | 'exportdef' <Ids> <Type> '.'
+ | 'useonly' <Ids> '.'
+ | 'useonly' <Ids> <Type> '.'
+
+<Ids> ::= <Id>
+ | <Id> ',' <Ids>
+
+<Kind> ::= 'type'
+ | 'type' '->' <Kind>
+
+<AbbrForm> ::= <Id>
+ | '(' <Id> <NamedVarList> ')'
+ | '(' <AbbrForm> ')'
+
+<NamedVarList> ::= <NamedVar>
+ | <NamedVar> <NamedVarList>
+
+<Type> ::= <CType> '->' <Type>
+ | <CType>
+
+<CType> ::= <NameToken>
+ | <TyCIdent> <CTypes>
+ | '(' <Type> ')'
+
+<TyCIdent> ::= <Id>
+
+<CTypes> ::= <CType>
+ | <CType> <CTypes>
+
+<Fixity> ::= 'infixl' | 'infixr' | 'infix'
+ | 'prefix' | 'prefixr'
+ | 'postfix' | 'postfixl'
+
+<NameToken> ::= { Any Teyjus token distinct from keywords,
+ pseudo-keywords, integer, string and real
+ literals }
+
+<Id> ::= { Like NameToken, except that the token should
+ also begin with something different from an
+ uppercase letter and _ }
+
+<NamedVar> ::= { Any named token that begins with an
+ uppercase letter }
+
+<SmallInt> ::= { Integer value between 0 and 255; i.e. unsigned
+ one byte number }
+
+<Empty> ::= { empty token sequence }
+}}}
+
=======================================
--- /dev/null
+++ /branches/RenamingRedux/tmp-docs/tests.txt Wed Feb 4 05:50:42 2015 UTC
@@ -0,0 +1,1 @@
+link ../source/test/renaming_tests/tests.txt
=======================================
--- /branches/RenamingRedux/source/compiler/translate.ml Wed Jan 28
07:14:06 2015 UTC
+++ /branches/RenamingRedux/source/compiler/translate.ml Wed Feb 4
05:50:42 2015 UTC
@@ -1167,16 +1167,23 @@
* to new_tbl. If old_sym does not exist raise an error with
* the given message and position. Uses a reverse copy of the
* underlying hash table to check bijectivity *)
- let add old_sym new_sym tbl (new_tbl, rev_tbl) pos errormsg =
- if Table.mem old_sym tbl
- then
- (if (not (Table.mem new_sym rev_tbl)) (* or new_sym matches
type/kind of old sym *)
- then (Table.add old_sym new_sym new_tbl, Table.add new_sym old_sym
rev_tbl)
- else
- let () = Errormsg.error pos "Clash detected!!" in
- (new_tbl, rev_tbl))
- else let () = Errormsg.error pos errormsg in
- (new_tbl, rev_tbl)
+ let add old_sym new_sym tbl (new_tbl, rev_tbl) pos kindortype =
+ match (Table.find old_sym new_tbl) with
+ None ->
+ (match (Table.find new_sym rev_tbl) with
+ None ->
+ (Table.add old_sym new_sym new_tbl,
+ Table.add new_sym old_sym rev_tbl)
+ | Some(previous) ->
+ let msg = (kindortype ^ " " ^ (Symbol.name new_sym) ^ " is " ^
+ "already being renamed from " ^ (Symbol.name previous)
^ ".") in
+ let () = Errormsg.error pos msg in
+ (new_tbl, rev_tbl))
+ | Some(previous) ->
+ let msg = (kindortype ^ " " ^ (Symbol.name old_sym) ^
+ " has already been renamed to " ^ (Symbol.name previous)) in
+ let () = Errormsg.error pos msg in
+ (new_tbl, rev_tbl)
in

(* Adds the inclusion to the original and reverse table *)
@@ -1189,18 +1196,12 @@
match renaming with
| Preabsyn.RenameKind (old_psym,new_psym) ->
let (Preabsyn.Symbol (old_sym,_,old_pos)) = old_psym in
- let (Preabsyn.Symbol (new_sym,_,new_pos)) = new_psym in
- let renstring =
- if (Symbol.equal old_sym new_sym) then "include" else "rename" in
- add old_sym new_sym ktable (tbl, rev_tbl) old_pos
- ("Cannot " ^ renstring ^ " unknown kind: '" ^ (Symbol.name
old_sym) ^ "'")
+ let (Preabsyn.Symbol (new_sym,_,_)) = new_psym in
+ add old_sym new_sym ktable (tbl, rev_tbl) old_pos "kind"
| Preabsyn.RenameType (old_psym,new_psym) ->
let (Preabsyn.Symbol (old_sym,_,old_pos)) = old_psym in
- let (Preabsyn.Symbol (new_sym,_,new_pos)) = new_psym in
- let renstring =
- if (Symbol.equal old_sym new_sym) then "include" else "rename" in
- add old_sym new_sym ctable (tbl, rev_tbl) old_pos
- ("Cannot " ^ renstring ^ " unknown type: '" ^ (Symbol.name
old_sym) ^ "'")
+ let (Preabsyn.Symbol (new_sym,_,_)) = new_psym in
+ add old_sym new_sym ctable (tbl, rev_tbl) old_pos "type"
in
(* build lookup tables *)
let (kRenamingTable, revKindRenTable, cRenamingTable, revConstRenTable) =
=======================================
---
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/base.sig
Fri Aug 1 21:01:39 2014 UTC
+++
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/base.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -1,6 +1,7 @@
sig base.

kind a type.
+kind b type -> type.

type q a -> o.
type r a -> a -> o.
=======================================
---
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/clash.sig
Fri Aug 1 21:01:39 2014 UTC
+++
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_directive_clash/clash.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -1,3 +1,3 @@
sig clash.

-accum_sig base {kind a, type q => b, type r => b}.
+accum_sig base {kind a => c, kind b => c, type q => s, type r => s}.
=======================================
---
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_name_overlap/base.sig
Fri Aug 1 21:01:39 2014 UTC
+++
/branches/RenamingRedux/source/test/compiler_negative_tests/renaming_name_overlap/base.sig
Wed Feb 4 05:50:42 2015 UTC
@@ -1,5 +1,6 @@
sig base.

kind a type.
+kind b type.

type q a -> o.
=======================================
--- /branches/RenamingRedux/source/test/renaming_tests/OMakefile Tue Jan 27
07:15:08 2015 UTC
+++ /branches/RenamingRedux/source/test/renaming_tests/OMakefile Wed Feb 4
05:50:42 2015 UTC
@@ -16,6 +16,10 @@

FILES = $(rootname $(glob *.mod))

+ # Redirect warning messages to /dev/null
+ if $(file-exists /dev/null)
+ stderr = /dev/null
+
%.dis: %.lpo $(TJDIS)
$(TJDIS) $< >$@

=======================================
--- /branches/RenamingRedux/source/test/renaming_tests/test2/main.om Tue
Jan 27 07:15:08 2015 UTC
+++ /branches/RenamingRedux/source/test/renaming_tests/test2/main.om Wed
Feb 4 05:50:42 2015 UTC
@@ -1,1 +1,1 @@
-MAIN = accumulating
+MAIN = inclusionstar manualinclusion
=======================================
--- /branches/RenamingRedux/source/test/renaming_tests/tests.txt Wed Jan 28
07:00:33 2015 UTC
+++ /branches/RenamingRedux/source/test/renaming_tests/tests.txt Wed Feb 4
05:50:42 2015 UTC
@@ -5,20 +5,26 @@
it'se well-formed.

Secondly, that an inclusion statement, i.e. {type x} is just a special
case of
-a renaming statement {type x => x}. Either we'll cover this with a test
case
-or do some reasoning about the code.
+a renaming statement {type x => x}. The code has been changed so that an
+inclusion statement really is just a special case of a renaming statement.
+We also have a test case to enforce this specification (test 1).

Then, we test that multiple redundant renaming statements are allowed by
the
-compiler.
+compiler (test 4).

We also specify that an empty renaming directive, i.e. in
accum_sig m1 {}.
-corresponds to not accumulating the module at all. We'll then have a test
case
-that checks this.
+corresponds to not accumulating the module at all. (test 5)

Inclusion: with * symbol
- - Equivalence to manual inclusion of all elements
- - Name clashes output appropriate error messages
+ - Equivalence to manual inclusion of all elements (test 3).
+ - Name clashes result in failed compilation (renaming_directive_clash,
+ in compiler_negative_tests)

Selective: no * symbol
- - Check that omitted elements behave as expected
+ - Check that omitted elements behave as expected:
+ * Check that omitted constants are invisible to the top-level (test 8)
+ - Check that including an undefined type results in an error
+ (renaming_missing_source, in compiler_negative_tests)
+ - Check that the renaming function contains no clashes; i.e. is bijective,
+ and each case is disallowed by the compiler
=======================================
--- /branches/RenamingRedux/tmp-docs/wiki-updates.txt Tue Jan 6 18:35:18
2015 UTC
+++ /branches/RenamingRedux/tmp-docs/wiki-updates.txt Wed Feb 4 05:50:42
2015 UTC
@@ -1,11 +1,43 @@
Running list of what needs to be updated and/or added to the wiki.
---
+ * We define 'renaming' to be the act of moving a reference (represented
by
+ its name) in some module to to a (possibly different) name an
accumulating
+ context. For example, if some module m1 contains a statement of the
form:
+ type a int -> o.
+ Some module could accumulate m1 with a statement like:
+ accumulate m1 {type a => b}.
+ So that if 'b' is visible in the modules signature, a query like:
+ [m2] ?- b X.
+ Would be equivalent to a query from m1:
+ [m1] ?- a X.

+ * Refer to the updated grammar in SigSyntax and ModSyntax for the exact
+ grammatical changes renaming brings in

* We extended the renaming syntax with the '*' token that includes
everything
- not mentioned. Any renamings superceed the inclusion of the renamed
- type/kind.
+ not mentioned. Any renamings superceed the implied inclusion of the
renamed
+ type/kind. For example,
+ accum_sig m1 {*, kind a => b}.
+ will accumulate all kinds/constants in m1 with their original names,
but
+ will rename the kind 'a' to 'b'. The '*' is a sytactic convenience for
the
+ manual inclusion of all elements, and the statements:
+ accum_sig m1 {*}.
+ accum_sig m1.
+ Are defined to be equivalent by our specification.

- * An empty renaming should be ignored and print a warning message
+ * An empty renaming directive following an accumulation statement
+ effectively nullifies the accumulation. Given the statement:
+ accum_sig m1 {}.
+ There is no content that needs to be accumulated, and thus the
statement
+ is ignored, and a warning is issued by the compiler.

- * We should document how clashes are being handled
+ * The renaming function must be bijective in each of its namespaces: that
+ is, a given kind/constant can't be renamed to two different names, and
two
+ different kinds/constants can't be renamed to the same name. I.e,
+ accum_sig m1 {kind a => c, kind a => b}.
+ accum_sig m1 {kind a => c, kind b => c}.
+ Are both disallowed according to our specification.
+
+ * Renaming will permit two duplicate statements, however. So a statement
like
+ accum_sig m1 {kind a, kind a}.
+ will be allowed, but will give a warning.