todo revision 2d6b942b2d10709143b699783f38957d8856e67f
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringPlan and priority list for CoFI tool activities
ebcd5d3acd4c470668bbcd945a5aa42f0af5ccf0Kay Sievers************************************************
ebcd5d3acd4c470668bbcd945a5aa42f0af5ccf0Kay Sievers************************************************
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay SieversHaskell parser f�r XHaskell erweitern
c904f64d84db8c4eebedf210ba10893f19ba05edLennart PoetteringDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
05677bb78079c3fa0283101aac2c07581f4873f1Lennart PoetteringHaskell modules: hiding, renaming
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversdevelopment graph calculus
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers- Stack overflow for "show just subtree"
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering************************************************
f7f21d33db5dfe88dc8175c61dada44013347729Lennart Poettering************************************************
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poetteringtype check for CASL
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering*** Error encode.casl:8.30, No correct typing for
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering************************************************
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering************************************************
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poetteringport CCC to Haskell
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart PoetteringFunktionen imageOfMorphism und inhabited
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering mit "cvs add SigFuns.hs" einchecken
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poettering"free datatypes and recursive equations are consistent"
07f74a7ebde5acf098ab72dc49a3371731ffb476Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
07f74a7ebde5acf098ab72dc49a3371731ffb476Lennart PoetteringJust True => Yes, is consistent
07f74a7ebde5acf098ab72dc49a3371731ffb476Lennart PoetteringJust False => No, is inconsistent
a26336da875a6657d404d1e44b86ae067c34b110Kay SieversNothing => don't know
e85647f73e235c2a6ea412cb8d841e092c373501Lennart Poetteringcall the symbols in the image of the signature morphism "new"
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering- each new sort must be a free type,
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poettering (Sort_gen_ax constrs True)
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering if not, output "don't know"
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering and there must be one term of that sort (inhabited)
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering if not, output "no"
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering- group the axioms according to their leading operation/predicate symbol,
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering i.e. the f resp. the p in
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
d889a2069a87e4617b32ddbdeace5a53a12c699dLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering Implication Application Strong_equation
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering Implication Predication Equivalence
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering if there are axioms not being of this form, output "don't know"
7e2668c6fd5720ae4d2d55eb8a062739687516afLennart Poettering************************************************
e85647f73e235c2a6ea412cb8d841e092c373501Lennart Poettering************************************************
a888b352eb53b07daa24fa859ceeb254336b293dLennart PoetteringTranslation from CASL with subsorts to CASL without subsorts
3b2d5b02ae231f1d3eb0d96eb980155d7797304eLennart Poetteringsee CATS/basic_encode.sml, encode SubCFOL into CFOL
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poetteringencode subsorting by injection functions
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering1. translation of signatures (see HetCATS/CASL/Sign.hs)
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering2. genertion of axioms (injectivity, overloading ...)
88f642c00b1708c5e0203c1753a9ef91d1de5442Kay Sieversdetails: see paper in Theoretical Computer Science, p. 407
9efaf380a7c7fa16f44b1aa15b967e99f331203aLennart Poettering************************************************
9efaf380a7c7fa16f44b1aa15b967e99f331203aLennart Poettering************************************************
4ee717820208a4c8e92383d0dbefa401827fab38Kay SieversDarstellung des Logik-Graphen
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sieversdazu importieren:
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sievers-- f�r Graph-Darstellung
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sieversimport DaVinciGraph
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sieversimport GraphDisp
b8217b7bd5fd171916a095b150fad4c3a37f5a41Kay Sieversimport GraphConfigure
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers-- f�r Erzeugen von Fenstern
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sieversimport TextDisplay
b8217b7bd5fd171916a095b150fad4c3a37f5a41Kay Sieversimport Configuration
08f23fd29c9df9c8b4e874933eb39711f069754bLennart Poetteringimport qualified HTk
3cc588803dba3530cd39000d299353a31e4c068bLennart Poetteringplus unten genannte Module
18b754d345ecb0b15e369978aaffa72e9814b86aKay SieversAufgabe: den Logik-Graph aus folgendem Modul:
068665b6fd9839f27bcace7e8f56c0baa6935272Lennart Poettering logicGraph aus Comorphisms/LogicGraph.hs, Typ in Logic/Grothendieck.hs
b070e7f3c9ed680c821bd89d42506695f2438506Lennart Poetteringaufbereiten f�r Anzeige, Vorbild ist in uni/graphs/test/GraphDispTest.hs
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart PoetteringAufbau von nodeTypeParams
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering-------------------------
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart PoetteringKnoten (bzw. Kanten) habe Werte, in diesem Fall: AnyLogic (bzw. AnyComorphism)
6ba383fa49e01302dfeae1f5083bb942b055628bLennart Poetteringnur 1 Knotentyp, rund, gr�n
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart PoetteringMen�funktionen AnyLogic -> IO ()
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart PoetteringValueTitle AnyLogic -> String (= language_name aus Logic/Logic.hs)
71100051c5d351daac20610f3a4b8c14901088d8Lennart Poettering$$$ ist Funktion zum Zusammenf�gen von Knotentyp-Parametern
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poetteringunter Men�eintrag "Info" anzeigen: Werte aus Logic/Logic.hs
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poetteringerstmal AnyLogic-Wert auspacken, z.B. mit
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringLogik-Namen ausgbene (mit language_name lid)
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringTest auf Just _, dann String ausgeben
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poetteringparse_basic_spec lid "Parser for basic specifications"
6b80b9b8ee6d372e00ece51e6a11c6d31899aaecLennart Poetteringparse_symb_items lid "Parser for symbol lists"
6b80b9b8ee6d372e00ece51e6a11c6d31899aaecLennart Poetteringparse_symb_map_items lid "Parser for symbol maps"
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poetteringparse_sentence lid "Parser for sentences"
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poetteringbasic_analysis lid "Analysis of basic specifications"
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poetteringdata_logic lid "is a process logic"
7d900eb6f58ca76a0f742c6e1823aa7317d4471fLennart Poetteringmap (sublogic_names lid) (all_sublogics lid)
101f077676e9fbe1a66c8b2dc4864a8d7a94c372Lennart Poettering -- sp�ter besser als eigener Men�punkt ==> eigener Graph
101f077676e9fbe1a66c8b2dc4864a8d7a94c372Lennart Poetteringmap prover_name (provers lid) -- aus Logic/Provers.hs
f7f964eb3625e4cca7f16377fa12aa7a760243e7Lennart Poetteringmap cons_checker_name (cons_checkers lid)
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringAnzeigen dieser Ausgabe mit:
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering createTextDisplay title str [size(100,50)]
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poetteringstr ist der anzuzeigende Inhalt
d0e5a33374cee92962af33dfc03873e470b014f6Lennart PoetteringAufbau von arcTypeParams
6edd7ca1624f89c9a36067b721a0280e748acb17Kay Sievers-------------------------
15e9fbd851c15ecaad4888932584f37dcd26111aLennart Poettering- einen "normal" f�r "normale" Comorphismen, schwarz
15e9fbd851c15ecaad4888932584f37dcd26111aLennart Poettering- einen "inclusion" f�r Inclusions, blau
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart PoetteringKantenmen�: Anzeige von sourceSublogic und targetSublogic (siehe Logic/Comorphisms.hs)
353e12c2f4a9e96a47eb80b80d2ffb7bc1d44a1bLennart Poetteringmittels language_name
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart PoetteringAufbau des Graphen selbst
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poettering------------------------
7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart PoetteringGraphDisp.newGraph daVinciSort -- aus uni/graphs/GraphDisp.hs
7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poettering -- mit leerem globalen Men�
36e43bddd0a4526e77cdae2c922bb29f67bd74adLennart PoetteringAnzeige des Graphen
b61c90514e134dc781617d172961f25e7352f53bLennart Poettering-------------------
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering-------------------------------------------------------------------
a558d00381291afd6a81f7df07269fe76eeae556Lennart PoetteringLaTeX pretty printer
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringa) analysierte Formeln und Terme optimal/k�rzer ausgeben:
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringshorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
a558d00381291afd6a81f7df07269fe76eeae556Lennart PoetteringIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringmit dem Ergebnistyp qualifiziert.
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart Poettering((a: Nat) + (b: Nat)): Nat
31ed59c51126fce7d958c188772a397e2a1ed010Lennart Poetteringb) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
31ed59c51126fce7d958c188772a397e2a1ed010Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
62f21ec91ad8e7e24079962f4df066b0094fe68dLennart Poetteringf�r die CASL Datentypen zu bekommen.
62f21ec91ad8e7e24079962f4df066b0094fe68dLennart PoetteringHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
62f21ec91ad8e7e24079962f4df066b0094fe68dLennart Poettering************************************************
62f21ec91ad8e7e24079962f4df066b0094fe68dLennart Poettering************************************************
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering- group the axioms according to their leading operation/predicate symbol,
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering i.e. the f resp. the p in
0716c60e37d2083325cd5316caf4310f0acc9a89Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poettering if there are axioms not being of this form, output error
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart PoetteringMissing points for heterogeneous WADT 04 example:
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering- improve display of HasCASL sigs + mors
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart PoetteringStatic analysis for HasCASL
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poettering checking class constraints of terms
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering pattern analysis for program equations
25d6283acfeb87730c2c0c4c2ef76a66fa397e87Lennart Poettering - for simple types (currently type synonyms)
25d6283acfeb87730c2c0c4c2ef76a66fa397e87Lennart Poettering symbol representation
a6eb9147a820d1c08b315867373a21bd0ece2f05Lennart Poettering symbol map analysis (hiding sub/supertypes)
b011116d1829bde044a638cbabfb070a7e0e8fa7Kay SieversWeak amalgamation analysis?
7d441ddb5ca090b5a97f58ac4b4d97b3e84fa81eLennart PoetteringInstantiate Transformation Application system for HasCASL?
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart PoetteringProofs in HasCASL
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
a2f5666d06fe8233025738047115bb9e3959df3eLennart Poetteringvisualization of "taxonomy" of CASL signatures
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering (subsorts = inheritance, unary preds = concepts, binary preds = relations)
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart PoetteringRecognize guarded fragment of CASL:
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poettering G ::= forall x . At(x) => G where At is a conjunction of atoms
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poettering | exists x . At(x) /\ G
de6c78f8795743894431a099d26ec562a8acf3dfLennart PoetteringJoost Visser wg. ATerms in Haskell => neues Repository
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poettering************************************************
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering************************************************
d3c7d7dd77b2b72315164b672462825cef6c0f9aKay SieversBeweise in Isabelle
72b9ed828bd22f3ddd74b6853c183eebf006d6d8Lennart PoetteringCASL consistency checker
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart PoetteringWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering (Vorbild: Larch-Handbuch)
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringParser and static analysis for CSP-CASL
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering************************************************
97f73ffb04947acf0a5854e3a7bdbb7a0105f6faLennart Poettering************************************************
85f248b26653f5322c26735661d63d4e8460c30eLennart PoetteringCASL consistency checker
85f248b26653f5322c26735661d63d4e8460c30eLennart PoetteringIsaWin: support CASL-libraries
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering************************************************
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering************************************************
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart PoetteringStatic analysis of architectural specs
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering************************************************
7c697168102cb64c5cb65a542959684014da99c7Lennart Poettering************************************************
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart PoetteringMissing points for heterogeneous WADT 04 example:
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering- coding to Isabelle: translate sort gen constraints
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering- correct display of CASL sublogis
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering- extended globDecomp rule: existing local Thm links
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering (e.g. generated by %implied) should lead to fewer new local
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart Poettering links ("local composition" rule)
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poettering- Improve adapation to Isabelle's lexis
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringIsabelle: (ask Christoph)
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poettering free datatypes
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering prove local thm link (=> green)
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering better interaction between Isabelle instance (for one node)
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering + selection of single goals that are proved
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering => use PGIP interface (Christoph, David)
c798c40ec957a35cd4b7d04a196a9e58880c6ff3Lennart Poettering correct show theory
c798c40ec957a35cd4b7d04a196a9e58880c6ff3Lennart Poettering Keep proofs and lemmas in .thy files (kind of merge)
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering CASL-like syntax
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering CASL annotation for lemmas that should be used in proof
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering inherit CASL's mixfix syntax
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart PoetteringSignatures versus theories: where to store additional infos?
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart Poetteringcomp(id,x)=x for comorphism names
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart PoetteringGeneralie CASL2Modal
44143309dd0b37d61d7d842ca58f01a65646ec71Kay SieversMixfix analysis + typecheck for modality axiomatizations
3d57c6ab801f4437f12948e29589e3d00c3ad9dbLennart PoetteringModal logics: modal logic, temporal logic, mu calculus
b9a2a36b519ccd79c4198e7dda4e657d597a14adLennart Poettering+ translations (e.g. modal to FOL)
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart PoetteringComorphisms: also map of theories; with default definition
9408a2d295a312a5472345090e28e0502570494bLennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay SieversCoding of subsorts as unary predicates (for ontologies)
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering- List[Dec] wird List[Pos]
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering- George wg. Schlie�en von Fenstern
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering- node numbers do not match
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poettering- thm links with external target should be provable as well
a8f11321c209830a35edd0357e8def5d4437d854Lennart PoetteringRemove warnings