Simple syntax extension

The formulae used in a TWB file are defined according to the CONNECTIVES definition given at the top of the file.

DImp, "_<->_", Two;
And, "_&_", One;
Or, "_v_", One;
Imp, "_->_", One;
Not, "~_", Zero;
Falsum, Const;
Verum, Const

However, since data type are currently hardwired in the TWB library, writing more complex formulae is at the moment fairly complicated. To fix this shortcoming I worked to a camlp4 extension to extend the TWB syntax on the fly using an initial grammar definition.

For example if I want to define a simple PDL like syntax for my formulae, I can just write my grammar definition at the be beginning of a TWB file and then use the formuale defined accordingly to this definition in the rest of the file.

This is a small example I've been working on...

CONNECTIVES [&;v;<;>;U;*]
l :=
* l
| l U l
| Var ;

expr :=
expr & expr
| expr v expr
| < l > expr
| Var ;

let a = term ( B v A ) ;;
let b = term ( a v D ) ;;
let c = term ( b & ( a v b ) ) ;;
let d = term ( < B > c ) ;;
let e = term ( < * A U B > c & ( c v d ) ) ;;

This extension is particularly complicated to write as it uses undocumented libraries of the ocaml pre-processor to extend the ocaml grammar on the fly. I'll work to integrate this code in the TWB in the next few weeks.

AttachmentSize bytes KB