todo

Plan and priority list for CoFI tool activities



************************************************
Sonja (Till)
************************************************

Diplom: Encoding for HasCASL in Isabelle/HOL(CF)

Interface Hets <-> ISabelle

in IsaProve.hs
  Hets muss eine Pipe als Inode erzeugen
  und dann auf Beweisterme warten
  und auf "Ende" warten
  und dann Proof_status sen proof_tree entsprechend ausfüllen
    (siehe Logic/Prover.hs)

Isabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
  Beweisterme (siehe Kapitel im RefMan)
  ML "proofs := 1" (am Anfang des .thy file)
  am Ende jedes Theorems: Beweisterm in die Pipe schreiben
    (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
    mit pretty_proof_of und Pretty.string_of
    und Start- und Endmarker
  am Schluss "Ende" ausgeben


Funktion basicInferenceNode in Proofs/Proofs.hs:
  Theorem link nur dann grün, wenn alle Goals bewiesen wurden

Emacs: uni/emacs, George fragen (ger@)

************************************************
Jorina (Till)
************************************************

development graph calculus
- Stack overflow for "show just subtree"
- view-test7.casl should be provable with globDecomp + locDecopm
- fail when doing first globDecomp, then local decomp in RelationsAndOrders
- correct MAYA: glob decomp: some links are not found (Jorina)

************************************************
Martin (Till)
************************************************

type check for CASL

documentation

*** Error encode.casl:8.30, No correct typing for


************************************************
Mingyi (Till)
************************************************

port CCC to Haskell

Funktionen imageOfMorphism und inhabited 
  von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
  mit "cvs add SigFuns.hs" einchecken

New module FreeTypes.hs:

"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
Nothing => don't know

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)
    if not, output "no"
- group the axioms according to their leading operation/predicate symbol,
  i.e. the f resp. the p in
  forall x_1:s_n .... x_n:s_n .                  f(t_1,...,t_m)=t
  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 .                  p(t_1,...,t_m)<=>phi
  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"




check' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)  
check' []                                              = ([([],[])],emptyUniqSet)

-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
check' [EqnInfo n ctx ps (MatchResult CanFail _)] 
   | all_vars ps  = ([(takeList ps (repeat new_wild_pat),[])],  unitUniqSet n)

-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
check' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
   | all_vars ps  = (pats,  addOneToUniqSet indexs n)
  where
    (pats,indexs) = check' rs

-- falls ein Konstruktor dabei ist: split_by_constructor
-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
check' qs@((EqnInfo n ctx ps result):_) 
   | all_vars ps  = ([],  unitUniqSet n)
   | constructors = split_by_constructor qs
   | only_vars    = first_column_only_vars qs
   | otherwise    = panic "Check.check': Not implemented :-("
  where
     -- Note: RecPats will have been simplified to ConPats
     --       at this stage.
    constructors = or (map is_con qs)
    only_vars    = and (map is_var qs) 



************************************************
Heng (Klaus)
************************************************

Write web interface for Hets

see the web interface for Cats:

http://www.informatik.uni-bremen.de/cgi-bin/cats.cgi

/home/till/www/cgi-bin/cats.cgi, adapt for Hets
(replace name of binary: /home/cofi/bin/hets -w ,
 replace string
 put hets.cgi to /home/jiang/www/cgi-bin/hets.cgi
 test with www.tzi.de/cgiwrap/jiang/hets.cgi )


Add option -w to Hets (hetcats/Options.hs)
in hets.hs, look for option, if present, proceed URL input
translate GUI/WebInterface.hs to Haskell

input:
- HetCASL spec
- boxes for
  - output parse tree
  - output pretty printed ASCII
  - output pretty printed LaTeX
  - output development graph (needs GraphBrowser.class, see
    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/medium.html)

output
- errors
- due to boxes



-------------------------------------------------------------------

LaTeX pretty printer

von Christian:
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.


************************************************
Christian
************************************************

assoc attribute does not translate along sig. mors

Haskell modules: hiding, renaming

- group the axioms according to their leading operation/predicate symbol,
  i.e. the f resp. the p in
  forall x_1:s_n .... x_n:s_n .       phi =>      f(t_1,...,t_m)=t
  forall x_1:s_n .... x_n:s_n .    phi1  =>      p(t_1,...,t_m)<=>phi
  if there are axioms not being of this form, output error


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 
  Sub-/Supertypes
    - for simple types (currently type synonyms)
  symbol representation
  symbol map analysis (hiding sub/supertypes)

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?
Automatic generation of Haskell (for a HasCASL subset)
Proofs in HasCASL
Case study

************************************************
Klaus
************************************************

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
      | exists x . At(x) /\ G
Joost Visser wg. ATerms in Haskell => neues Repository

************************************************
Markus, Lutz
************************************************

Beweise in Isabelle
CASL consistency checker
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
  (Vorbild: Larch-Handbuch)
Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
Parser and static analysis for CSP-CASL 

************************************************
Christoph
************************************************

CASL consistency checker
IsaWin: support CASL-libraries

************************************************
Maciek
************************************************

Static analysis of architectural specs

************************************************
Till
************************************************

update Hets, CASL, daVinci on web page

remove qualifications from output

CASL2PCFOL: x_i -> t_i, t=[inj(x_i)]

packing of binaries: add hets-update, refer to TclTk

CCC interface

test for sublogic before applying comorphism
avoid cyclic comorphisms

Missing points for heterogeneous WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- 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)
   remove datatypes from sort list
   prove local thm link (=> green)

   "prove" menu with choice windows
   incorporate sublogics
   sublogic translation table

   better interaction between Isabelle instance (for one node)
    + selection of single goals that are proved
    => use PGIP interface (Christoph, David)

   correct show theory
   Keep proofs and lemmas in .thy files (kind of merge)
   CASL-like syntax
   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

Generalise CASL2Modal
Mixfix analysis + typecheck for modality axiomatizations
Modal logics: modal logic, temporal logic, mu calculus
+ translations (e.g. modal to FOL)

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

Hets interactive

Remove warnings

Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
Management of change

Integrate provers
  Otter model checker
  FOL-prover by Uli Furhbach
  modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
               Isabelle codings: www.inf.ethz.ch/~vigano
  Renate Schmidt, Manchester: uses FOL prover for description logic
                              (as efficient as DL-specific tools!)
  Look at PROSPER toolkit
  consistency: see IJCAR-workshop on non-provability in Cork
  IJCAR workshop about logical frameworks and meta-languages
Integrate CCC
Encodings


Errors:
Klaus' wayfinding example

ask Detlef: critical pairs, Fossacs paper by Francesco

UniForM workbench:
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)

Integration of MAYA and Isabelle/HOL (global HOL-Coding of
  Grothendieck logic)
  + 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

User interface
--------------
Logic graph window
Input text window
Development graph window
Prover windows


************************************************
FOR STUDENTS
************************************************

Data.Serizable
Emacs mode
Hets Web interface (cf. CATS/web_interface2.sml)
CCC ?
Packaging of installation
integrate QuickCheck
XML interface
GUI (vgl. VSE)
increase performance

++++++++++++++++++++++++++++++++++++++++++++++++
Remaining things
++++++++++++++++++++++++++++++++++++++++++++++++

Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
    Coq, PTT in Maude

Proof general interface (1 day)

Test Maya with basic datatypes

Verbesserung der Fehlermeldungen

Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
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)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)

Basic datatypes CASL-lib/Basic/basic.casl
Repository mit korrekten und fehlerhaften Specs

HetCATS User manual, Doku fuer Environments (2 weeks)

Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
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

Views on CASL specs: CATS/viewer.sml (2 weeks)
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)

Neues Tool-Schaubild auf Web-Seiten veröffentlichen

Library management: CATS/lib_ana.sml (2 weeks)
Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)




{- This does not work due to needed ordering:
instance Functor Set where
  fmap = mapSet
instance Monad Set where
  return = unitSet
  m >>= k          = unionManySets (setToList (fmap k m))
-}




Aufbau von comptable
--------------------
[("normal","normal","normal"),
 ("normal","inclusion","normal"),
 ("inclusion","normal","normal"),
 ("inclusion","inclusion","inclusion")]

Aufbau von ginfo
--------------------
Mit initgraphs erzeugen

Aufbau des Graphen selbst
------------------------
addnode
addlink