search

gsdlab / clafer

Clafer is a lightweight modeling language
http://clafer.org
MIT License
45 stars 13 forks source link

Module system #52

Closed mantkiew closed 9 years ago

mantkiew commented 10 years ago

Support for splitting large Clafer models into multiple files. The goal is to have the simplest and minimal support that is just sufficient for our case studies and the Clafer wiki.

Status: in progress, do not merge

Usage

To make all declarations from other files visible in the current model, use import keyword and provide a URL. The protocol part of the URL is mandatory to overcome parser limitations and grammar ambiguities.

import (file://|ftp://|http://)path/to/model.cfr

All imported models are compiled only once and included into a single namespace. Redundant imports are allowed but circular dependencies are not allowed.

Running Example

EAST-ADL Power Window excerpt.

The compiler retrieves the imported models, builds a dependency lattice, and compiles the models in the reverse order of dependencies. When compiling a module, compiler's state (ClaferEnv) contains the list of states of already compiled imported models via cImports :: [ClaferEnv]. The compiler performs all analyses using it's own as well as the imported states.

Parsing

All modules are parsed separately

Desugaring

The import statements are desugared into IModules, whose names are the URLs. The name of the top-level IModule remains empty. Therefore, the imported modules are fully compiled during desugaring and their ClaferEnvs are added to cImports.

Analyses

All analyses work on the combined ClaferEnvs from the top-level and the imported modules. It is important to perform the whole model analysis only once for the combined model. It is necessary for performance reasons; however, it has a drawback that the semantic errors in the imported modules will be caught later as compared to fully compiling the imported modules first.

Generation

The outputs are generated separately for each module and the target language import or cross-reference mechanisms are used to combine them.

The folder test/regression contains correct (intended) outputs for Alloy (.als.reg) and HTML (.html.reg).

Alloy

Alloy provides open command for importing Alloy modules.

Name normalization

The module names in Alloy are restricted in comparison to URLs, which requires normalization: only letters, numbers, underscores, and quote marks are allowed, all other URL characters must be replaced with underscores.

Alloy output requirements

  1. The option --keep-unused must be used, since it is likely that the imported modules will only contain abstract clafers.
  2. For an unused abstract clafer A in an imported module, the constraint [ #A = 0 ] must not be generated.
  3. The option --noalloyruncommand must be used for imported modules, since only the top-level module should have the run command and it only makes sense to perform scope analysis for the top-level module together with all imported modules.

    Running Example

Currently, the HTML generator produces hyperlinks to the declarations of clafers, which contain anchors. For clafers referenced from imported modules, the hyperlinks must additionally include the URL of the HTML output of the imported module. The import statements link to the entire HTML file.

Running Example

wasowski commented 10 years ago

Andrzej: 1. What is the parser problem with the import always requireing the protocol prefix? I think this is a usability obstacle that clatters the models. I would prefer it file:// was default.

Michal: The token for URL is much more general than any other token and because our tokenizer is context insensitive, other parts of the model were parsed as URLs (see grammar). In my original proposal (see first commit), the file:// prefix was optional but I was running into very nasty parsing problems. So, somehow you have to distinguish the URL token from others. It's a tradeoff, either you surround it with special characters or you require some kind of prefix. I chose to require the protocol prefix, as it's quite natural and solves all problems. But yes, I would prefer file:// was assumed by default as well.

Andrzej: 2. I am not enitrely sure if file extensions should always be dropped. This looks good in a Java like import, but is slightly strange if you use a protocol prefix, because this indicates that you refer to a file, not to a logical unit. So you would expect that the same URI would open in a browser for instance (but it won't because the extension is lacking). I think this can cause trouble for novice users who are reading models. I am not entirely sure how to solve it, but my thought was to require a proper file name if you use a protocol prefix (so this becomes a proper URI) and allowing to drop it if you are not using the protocol prefix (using the default file://, as suggested in 1 above).

Michal: agreed. I'll make the extension mandatory, so that it'll be a proper URI.

Andrzej: 3. This module system that you suggest is very simple, essentially the #include solution from C preprocessor. I think this is fine for most purposes, and perhaps the only thing that we need so far. However one can consider doing other things that people do in a module language: hiding, parameterizing and name spaces. We might not want to implement all of these but we could try to pretotype some syntax, so that we are reasonably sure that we can proceed to develop clafer later.

Michal: yes, it's intentionally made into the simplest possible design that is implementable in reasonable time. We can add other features later. The design is also close to Alloy's but even simpler. Finally, it must work equally well on the desktop, on the wiki, and combination of both, which is why support for http:// is needed.

Andrzej: Here are some questions that could have feature interactions with current design

For name spaces it seems to me that it would be nice if modules had names. Is it the file name? Is file name stable and portable enough for that? Do we want to allow more than one module in a file? [names are needed in order to qualify names in name spaces if there are clashes across modules]

Michal: only imported modules have names which are assigned dynamically during compilation. So, you cannot declare it statically in the model but when I import http://abc.com/moduleA.cfr the URL becomes the name of the imported module. It is purely internal and not available to modellers for name qualification etc.

What we could have, is qualified imports like this import http://abc.com/moduleA.cfr as MA, and then we could use x1 : MA::claferx to qualify names. But that's for the next increment, I left it out intentionally as it is not critical.

Andrzej: For parameterization (functors in ML, or templates in C++) import should allow parameters. Do we have the right syntax for that, or will we need to change that later? Alternatively we could allow clafer's (as opposed to modules) to take parameters. This seems appealing, as clafer is really the core concept in the language. On the other hand one needs to apply parameters at module import time (as otherwise some name clashes will be unavoidable).

Michal: yes, we can consider these later given a strongly motivating use case. At the moment, I'd like to implement the simplest yet usable design possible.

Andrzej: So perhaps we should think a bit unconventionally and consider whether modules could be clafers, possible singleton clafers. This would allow using modules the same way as other clafers, and using templates both to parameterize files and to parameterize clafers within a file (for instance to instantiate four different windows with different wiring of references).

Michal: that would be very nice and natural. We can implement that; however, only after we have implemented redefinition and inheritance from nested clafers.

Andrzej: Hiding: how name resolution should work with imports? Do we have any way of hiding module details from polluting the name space of the importer?

Michal: no, currently all modules form a single namespace and naming rules apply globally. That's a tradeoff for now to get something working.