jirkamarsik / acgtk Goto Github PK
View Code? Open in Web Editor NEWA publicly open Git mirror for the ACG toolkit hosted at
Home Page: http://www.loria.fr/equipes/calligramme/acg/
License: Other
A publicly open Git mirror for the ACG toolkit hosted at
Home Page: http://www.loria.fr/equipes/calligramme/acg/
License: Other
************************************************************************** * * * ACG development toolkit * * * * Copyright 2008 INRIA * * * * More information on "http://acg.gforge.inria.fr/" * * License: CeCILL, see the LICENSE file or "http://www.cecill.info" * * Authors: see the AUTHORS file * * * * * * * * * * $Rev:: $: Revision of last commit * * $Author:: $: Author of last commit * * $Date:: $: Date of last commit * * * ************************************************************************** This distribution provides two executables (possibly with the .opt extension, see the INSTALL file): acgc and acg ************ *** acgc *** ************ acgc is a "compiler" of ACG source code, i.e. files containing definitions of signarures and lexicons. It basically checks whether they are correctly written (syntactically and wrt types and constant typing) and outputs a .acgo object file. An interactive mode is available to parse terms according to signatures. Run ./acgc -help to get help *********** *** acg *** *********** acg is an interpreter of command meant to be useful when using ACGs. To get a list of command, run ./acg then on the prompt type help; Example files are given in the ./examples directory. Read the ./examples/README file *************** * Basic usage * *************** Let's assume you defined a file my_acg.acg in directory my_dir. A basic usage of the acgc and acg commands could be: $ acgc -o my_acg.acgo my_acg.acg This will produce a my_acg.acgo file (note that this is the default name and location if the -o option is not provided). Then, running : $ acg will open a prompt in which you can type: # load o my_acg.acgo; to load the data contained in the my_acg.acg file. Assuming you have defined the signature Sig and the lexicon Lex, you can then run the following commands: # Sig check lambda x.some_cst x: NP ->S; to check whether "lambda x.cst x" is a term of type "NP ->S" according to Sig. You can type: # Lex realize lambda x.cst x: NP ->S; to compute the image of "lambda x.cst x" is a term of type "NP ->S" by Lex (assuming this term and this type are correct according to the abstract signature of Lex). You can type: # Lex parse John+loves+Mary: S; to check whether the term "John+loves+Mary" has an antecend of type "S" by Lex, assuming that "John+loves+Mary" is a term of type "Lex (S)" in the object signature of Lex. Type CTRL-D to exit from the program. ******************** ** ACG emacs mode ** ******************** There is an ACG emacs mode (acg.el) in the emacs directory. Look at the INSTALL file to see how to install it and where you can find the acg.el file if automatically installed (in particular using opam). It's main feature is to be loaded when editing an acg data file (with signatures and lexicons). It is automatically loaded for files with a .acg extension It basically contains compilation directives and next-error searching. 1. First load an acg file 2. then run "M-x compile" (or C-cC-c) to call the compiler (acgc or acgc.opt) 3. then run "M-x next-error" (or C-x`) to search for the next error (if any) and highlights it ************************************ * Syntax of signature and lexicons * ************************************ (see the examples/tag.acg file for an example) Signatures are defined by: signature my_sig_name= sig_entries end Sig_entries always ends with a ; and can be: + type declaration as in NP,S : type; + type definition as in o :type; string = o -> o; Note that type constructors are -> and => for the linear and intuitionnistic arrow respectively. + constant declarations as in foo:NP; bar,dummy:NP -> S; infix + : string -> string -> string; prefix - : bool -> bool; binder All : (e =>t) -> t; infix > : bool -> bool -> bool; (*This means implication*) Note that infix and prefix are keywords to introduce symbols (of length 1. This probably will change). Also notes that comments are surrounded by (* and *) + constant definitions as in n = lambda n. bar n : NP -> S; infix + = lambda x y z.x(y z): string -> string -> string; prefix - = lambda p.not p:bool -> bool; everyone = lambda P. All x. (human x) > (P x) ; Note the syntax for binders (All in the last example). Available construction for terms are: lambda x y z.t for linear abstraction Lambda x y z.t for non-linear abstraction t u v for application (eauql to (t u) v) t SYM u if SYM is a infix symbol (lowest priority) SYM t if SYM is a prefic symbol (highest priority) BINDER x y z.t if BINDER is a binder Lexicons are defined by: lexicon my_lex_name(abstract_sig_name) : object_sig_name = lex_entries end or by lexicon composition as in: lexicon my_new_lex = lex_2 << lex_1 Lex_entries always ends with a ; and have the following form: abstract_atomic_type1, abstract_atomic_type2 := object_type; abstract_const1, abstract_const2 := object_term;
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.