Experimental IntML-Implementation
OCaml
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Examples
Makefile
README
compile.ml
decls.ml
evaluation.ml
intml.ml
lexer.mll
opts.ml
opts.mli
parser.mly
printing.ml
simulate.ml
term.ml
term.mli
top.ml
top.mli
type.ml
type.mli
typing.ml
typing.mli
unify.ml
unify.mli
vargen.ml

README

Basic Usage
===========

 An intml-file consists of definition of the form:
 
   letw f = working_class_term
   letw g = upper_class_terms
 
 See the files in directory Examples/ for syntax and format.
 
 A file containing such definitions can be type-checked using
 
   ./intml.native file.intml
 
 The intml-interpreter is then in interactive mode and can be 
 used to evaluate terms.


Interactive Mode
----------------

Working Class Terms
-------------------

 Working class terms can be evaluated directly.

  # inl(<>)
  : 1 + 'a
 
  = inl(<>)

 They can be defined using letw.

  # letw pi1 = fun x -> let <x1,x2>=x in x1
  pi1 :w 'a * 'b -> 'a
  
  # pi1 <inl(<>),inr(<>)>
  : 1 + 'a
  
  = inl(<>)
  
Upper Class Terms
-----------------

 Upper class terms can be defined using letu.

  # letu d = fun f -> fun x -> let [v]=x in f [v] [v]
  d :u (['a] --> ['a] --> ['b]) --> ['a] --o ['b]

 However, they cannot be evaluated directly, as can working 
 class terms.

 For the evaluation of upper class terms one has the following 
 options:

 * Terms f of type [A] can be evaluated using the working-class 
   construct let [x] = f in x.

    # let [x] = d (fun x -> fun y -> x) [inl(<>)] in x
    : 1 + 'a
 
    = inl(<>)
 
 * The toplevel gives access to the circuit corresponding to any
   working class term. This is available using the #circuit 
   directive.

   The directive 
     #circuit (upper class term)
   displays the type of the circuit for the upper class term.
   
   The directive
     #circuit (upper class term) (working class term)
   feeds the given working class term to the circuit for the
   upper class term and computes the output from the circuit.

   Example:

    # #circuit d
    : 'a * 1 * ('b * 1 + ('c * 1 + 'd)) + (1 * 'a + 1) -> 'a * 1 * ('b
    * 'a + ('c * 'a + 1)) + (1 * 1 + 'd)

    = functional value

   The circuit may thus be sent messages of type 
   'a * 1 * ('b * 1 + ('c * 1 + 'd)) + (1 * 'a + 1)
   and it may answer with messages of type
   'a * 1 * ('b  * 'a + ('c * 'a + 1)) + (1 * 1 + 'd)

   For example, the circuit for d answers the query inr(inr(<>)) 
   with inr(inl(<<>, <>>)).

    # #circuit d inr(inr(<>))
    : 'a * 1 * ('b * 'a + ('c * 'a + 1)) + (1 * 1 + 'd)
 
    = inr(inl(<<>, <>>))
   
   In the #circuit directive it is also possible to use 
   complex upper class terms

    # #circuit (fun x->let <y,z> = x in let [v]=y in [<v,v>])
    : 1 * 1 * ('a + 'b) + 1 -> 1 * 1 * (1 + 'c) + 'a * 'a
 
    = functional value

 * Animations for circuit computation can be generated using
   the #sim directive. This generates a pdf file with an animation
   of circuit computation. It needs graphviz (dot) and pdftk.

   For example 
     
     # #sim d inr(inr(<>)) 

   generates a file circuit.sim.pdf in the current directory, which
   shows the first 10 steps of the computation of cirucit d with input
   inr(inr(<>)). 

   The number of steps can be changed as follows:
    
    # #simlength 20