Previous Up Next

Module Absynt

The abstract syntax itself together with some utilities to generate or convert specific terms.
module B = Basic

module Symbol = Mtsymbol.Symbol

type symbol = Symbol.symbol

type vname = symbol × int
type pname = symbol × int

type qindex = int 
type qstarindex = qindex list

type α state = Q of α

type α term = 
     V of vname 
   ∣ P of pname 
   ∣ T of symbol × (α termlist
   ∣ QT of α state × (α term) × (α termlist

type α lhs = α term
type α rhs = α term
type α rule = (α lhs) × (α rhs)

type α qsignature = (α × intlist
type ssignature = (symbol × intlist
type α signature = (α qsignature) × ssignature

type α mtt = symbol × (α signature) × (α statelist × α state list × α rule list

Conversion functions

For convenience, we need a number of functions, mutuallyconverting the various representations of terms, exctracting components etc. Some are trivial, for instance because rules are defined for terms. It might get non-trivial if rule do not simply use terms, but some specialized data-structure.

let vname_of_term (t: α term) =
   match t with
     V(ni) → (n,i)
   ∣ _ → raise (Failure "not convertible (not a variable)")

let pname_of_term (t: α term) =
   match t with
     P(ni) → (n,i)
   ∣ _ → raise (Failure "not convertible (not a parameter)")

let build_vars i : vname list =
   let rec h i start = 
     if i = 0 then [ ] else (Symbol.symbol_of_string("x"), start) :: (h(i−1) (start +1))
   in h i 0

The two functions build_vars_as_terms and build_vars_as_terms_in_context, given a natural number n, yield a list of variables x1,…, xn and a list t[x1], …, t[xn], where t[_] is the context.

let build_vars_as_terms (iint) : α term list =
   let rec h i start = 
     if i = 0 then [ ] else V(Symbol.symbol_of_string("x"), start) :: (h(i−1) (start +1))
   in h i 0

let build_vars_as_terms_in_context (context: α term → α termi : (α termlist =
   let rec h i start = 
     if i = 0 
     then [ ] 
     else context(V(Symbol.symbol_of_string("x"), start)) :: (h(i−1) (start +1))
   in h i 0

We call (informally) a constructor-term a terms of the form f(x1,…,xn) for some f∈ Σ. The functions build_constructorterm, build_constructorterms, build_constructorterms_in_context, and build_qi_terms are straightforward applications, yielding a term f(x1,…,xn), respectively a list of such terms (for a complete signature Σ), respectively a list of terms qα(f(x1…,xn)), respectively constructor terms where the variables can be put in a context.1

let build_constructorterm (ssymbol × int) : qindex term = T(fst sbuild_vars_as_terms (snd s))

let build_constructorterms (sar: ((symbol × intlist)) : (qindex termlist = build_constructorterm sar

let build_constructorterms_in_context 
     (contextqindex term → qindex term
     (sar: ((symbol × intlist)) : (qindex termlist =
   let build_one_term (ssymbol × int) : qindex term = 
     T(fst sbuild_vars_as_terms_in_context context (snd s))
   in build_one_term sar

let build_qi_terms (sar: (symbol × intlist) (iqindex) : (qindex termlist = (fun t → QT(Q(i), t,[ ])) (build_constructorterms sar)

The next function is used to “standardize” the representation of transducers, basically removing doublettes of all kinds. The function merge_rhs joins 2 right-hand sides, removing duplicates merge_rules joins 2 rule lists: it takes identical left-hand sides and merges their right-hand sides. Each rule sets alone is assumed to have unique left-hand sides. The function uniquify_rules takes a rule list and makes the left-hand sides unique, collecting all the right-hand sides belonging to the same left-hand sides. The result is a “proper” association list with no duplicates of left-hand sides.2

let rec uniquify_rules (rl : (α rulelist) : (α rulelist = 
   B.list_remove_doublettes rl

exception My_Parse_error of int × int × (int × intlist
type lexposition = {char_start:intchar_endintline_noint}
type ident = Ident of lexposition × symbol

let line_number p = p.line_no

exception My_Parse_error of int × int × (int × intlist

class linecounter =
     val mutable x = 1 (∗ emacs starts with line-number 1 ∗)
     val mutable m = "Syntax Error"
     method new_line() = xx+1
     method get_line() = x
     method set_message(s) = ms
     method get_message() = m

let lc = new linecounter

let ident_pos i = match i with Ident (p,_) → p

let pos_conc (p1p2) = {char_start = p1.char_start;
                           char_end = p2.char_end;
                           line_no = p1.line_no}

let determine_pos lb = 
   {char_start = (Lexing.lexeme_start lb);
     char_end = (Lexing.lexeme_end lb);
     line_no = (lc#get_line())}

Previous Up Next