-
Notifications
You must be signed in to change notification settings - Fork 0
Generator of OCaml construction functions for quotient types
License
fblanqui/moca
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
###################################################################### # # # Moca # # # # Pierre Weis, INRIA Rocquencourt # # Frédéric Blanqui, projet Protheo, INRIA Lorraine # # # # Copyright 2005-2012, # # Institut National de Recherche en Informatique et en Automatique. # # All rights reserved. # # # # This file is distributed under the terms of the Q Public License. # # # ###################################################################### #(* $Id: README,v 1.17 2012-06-04 13:01:21 weis Exp $ *) OVERVIEW: Moca is a fast code generator for Objective Caml ``types with relations''. Types with relations are concrete data types, the values of which must obey to ``invariant rules'', or relations. The constructors of those types are not acessible directly since types with relations are ``private'' types in Objective Caml parlance. Given an annotated definition of a private type, Mocac generates the interface and the implementation of the Caml module that implements the relational type, i.e. the type and the corresponding construction functions to implement the relations and the invariants according to the annotations. The source .mlm file is a specialized version of an Objective Caml module interface file. It should contain the definition of a private type; in addition, the constructors of the type can be annotated with relations that the constructors are supposed to verify. Annotations are enclosed by the keywords begin and end. Let's consider as an example, the regular definition of a simple type for arithmetic expressions, to modelize unary integers with addition and unary minus. We could use two constants One and Zero, a binary constructor Add and a unary constructor Opp, to represent 1, 0, +, and unary -. In regular Objective Caml, we could write: type expr = | One | Zero | Opp of expr | Add of expr * expr;; This is OK, but unfortunately we have no mean to express in the type definition, that in fact Add (One, Zero) is the same as Add (Zero, One) since the addition is commutative. Similarly, we cannot indicate that Add (Zero, One) is in fact One, given that Zero is the neutral element for addition. So that our code will be clobbered with a lot of pattern matchings and calls to ``normalization'' functions to handle this semantics properties that we need for the values of type expr. In fact, we would prefer to express the relations that are verified by the constructors and let the compiler to handle them to built a set of values that verify those constraints. Moca was exactly designed to deal with relations of constructors and to automatically generate the proper construction functions that ensure that the relations always hold for any value of the type expr. Hence, in the .mlm Moca source file for the type expr, we indicate the properties for Add as annotations, stating its algebraic laws type expr = private | One | Zero | Opp of expr | Add of expr * expr begin associative commutative neutral (Zero) inverse (Opp) end;; Now Moca generates the values, one : expr, zero : expr, opp : expr -> expr, and add : expr * expr -> expr, such that the Add constructor will be associative, commutative, will have Zero as neutral element, and Opp as its inverse operation. See the documentation for an exhaustive list of relations that Moca currently supports. In addition, Moca could provide maximal sharing between the values of the type, using dedicated hashing functions and sophisticated weak pointer hashtables. There is nothing to modify in the source code to get maximal sharing: you just have to call the mocac compiler with the special option that triggers the generation of maximally sharing construction functions (that will still implement the specified relations for the constructors). REQUIREMENTS: Moca requires Objective Caml 3.09 or later. INSTALLATION: See file INSTALL. For Windows: see file INSTALL.win. DOCUMENTATION: - The doc/ subdirectory contains the documentation in HTML. EXAMPLES: - The examples/ directory contains a set of examples: look at the various .mlm files. To compile them, do: cd examples make clean make SUPPORT: - Please send bug reports and comments to [email protected] COPYRIGHT: All files marked "Copyright INRIA" in this distribution are copyright 2005-2008 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the conditions stated in file LICENSE.
About
Generator of OCaml construction functions for quotient types
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published