Haskell parser f�r XHaskell erweitern
Haskell modules: hiding, renaming
************************************************
************************************************
development graph calculus
- Stack overflow for "show just subtree"
- fail when doing first globDecomp, then local decomp in RelationsAndOrders
- correct MAYA: glob decomp: some links are not found (Jorina)
************************************************
************************************************
************************************************
************************************************
Funktionen imageOfMorphism und inhabited
"free datatypes and recursive equations are consistent"
checkFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
Just True => Yes, is consistent
Just False => No, is inconsistent
call the symbols in the image of the signature morphism "new"
- each new sort must be a free type,
i.e. it must occur in a sort generation constraint that is marked as free
(Sort_gen_ax constrs True)
such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
if not, output "don't know"
and there must be one term of that sort (inhabited)
i.e. the f resp. the p in
forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
Implication Application Strong_equation
forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
Implication Predication Equivalence
if there are axioms not being of this form, output "don't know"
************************************************
************************************************
Translation from CASL with subsorts to CASL without subsorts
encode subsorting by injection functions
2. genertion of axioms (injectivity, overloading ...)
details: see paper in Theoretical Computer Science, p. 407
************************************************
************************************************
a) analysierte Formeln und Terme optimal/k�rzer ausgeben:
shorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
In Abh�ngigkeit von Sign werden
z.B. nicht-�berladene Funktionen
unqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
mit dem Ergebnistyp qualifiziert.
((a: Nat) + (b: Nat)): Nat
b) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
und andere Formate besser zu unterst�tzen und einheitlichen PP code
f�r die CASL Datentypen zu bekommen.
HasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
************************************************
************************************************
Missing points for heterogeneous WADT 04 example:
- improve display of HasCASL sigs + mors
Static analysis for HasCASL
checking class constraints of terms
pattern analysis for program equations
- for simple types (currently type synonyms)
Weak amalgamation analysis?
Instantiate Transformation Application system for HasCASL?
Automatic generation of Haskell (for a HasCASL subset)
************************************************
************************************************
visualization of "taxonomy" of CASL signatures
(subsorts = inheritance, unary preds = concepts, binary preds = relations)
Recognize guarded fragment of CASL:
G ::= forall x . At(x) => G where At is a conjunction of atoms
Joost Visser wg. ATerms in Haskell => neues Repository
************************************************
************************************************
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
(Vorbild: Larch-Handbuch)
Parser and static analysis for CSP-CASL
************************************************
************************************************
IsaWin: support CASL-libraries
************************************************
************************************************
Static analysis of architectural specs
************************************************
************************************************
Missing points for heterogeneous WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- correct display of CASL sublogis
- extended globDecomp rule: existing local Thm links
(
e.g. generated by %implied) should lead to fewer new local
links ("local composition" rule)
- Improve adapation to Isabelle's lexis
Isabelle: (ask Christoph)
prove local thm link (=> green)
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
=> use PGIP interface (Christoph, David)
Keep proofs and lemmas in .thy files (kind of merge)
CASL annotation for lemmas that should be used in proof
inherit CASL's mixfix syntax
Signatures versus theories: where to store additional infos?
comp(id,x)=x for comorphism names
Mixfix analysis + typecheck for modality axiomatizations
Modal logics: modal logic, temporal logic, mu calculus
+ translations (
e.g. modal to FOL)
Comorphisms: also map of theories; with default definition
CASL->Haskell with free DTs (mark sortgens) + recursion
Coding of subsorts as unary predicates (for ontologies)
Translation between Achim's ontology data structure and CASL (in Hets)
- List[Dec] wird List[Pos]
- George wg. Schlie�en von Fenstern
- node numbers do not match
- thm links with external target should be provable as well
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
FOL-prover by Uli Furhbach
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Klaus' wayfinding example
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
+ for TAS: reflection of HOL in HOL, to be composed with encodings
(
i.e. signatures, axioms, signature morphisms in HOL,
re-use ML signatures) (Einar)
Display Specs as daVinci subgraphs
************************************************
************************************************
Packaging of installation
++++++++++++++++++++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Proof general interface (1 day)
Test Maya with basic datatypes
Verbesserung der Fehlermeldungen
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
Encoding of structured free (3 days)
Encoding of structured cofree (2 weeks)
Eingabesyntax als Mix zwischen CASL und HOL (3 days)
Adapt Isabelle unions to CASL unions (1 week)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
Comparsion of parsers (ML-yacc parser, SDF-Parser)
Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
PVS anbinden (Kooperation mit Cachan?)
Portations: Intel-Solaris, Mac OS-10 (2 weeks)
(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
{- This does not work due to needed ordering:
instance Functor Set where
m >>= k = unionManySets (setToList (fmap k m))