23174

1 
(* Title: Tools/Compute_Oracle/am_util.ML


2 
ID: $Id$


3 
Author: Steven Obua


4 
*)


5 


6 
signature AM_UTIL = sig


7 


8 
type naming (* = string > int *)


9 


10 
exception Parse of string


11 
exception Tokenize


12 


13 
(* takes a naming for the constants *)


14 
val read_rule : naming > string > AbstractMachine.pattern * AbstractMachine.term


15 


16 
(* takes a naming for the constants and one for the free variables *)


17 
val read_term : naming > naming > string > AbstractMachine.term


18 


19 
val term_ord : AbstractMachine.term * AbstractMachine.term > order


20 


21 
end


22 


23 
structure AM_Util : AM_UTIL =


24 
struct


25 


26 
fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)


27 
 term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)


28 
 term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =


29 
prod_ord term_ord term_ord (a1, a2)


30 
 term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)


31 
 term_ord (AbstractMachine.Const _, _) = LESS


32 
 term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER


33 
 term_ord (AbstractMachine.Var _, _) = LESS


34 
 term_ord (AbstractMachine.App _, AbstractMachine.Abs _) = LESS


35 
 term_ord (AbstractMachine.App _, _) = GREATER


36 
 term_ord (AbstractMachine.Abs _, _) = LESS


37 


38 
type naming = string > int


39 


40 
datatype token =


41 
TokenConst of string  TokenLeft  TokenRight  TokenVar of string 


42 
TokenLambda  TokenDot  TokenNone  TokenEq


43 


44 
exception Tokenize;


45 


46 
fun tokenize s =


47 
let


48 
fun is_lower c = "a" <= c andalso c <= "z";


49 
val is_alphanum = Symbol.is_ascii_letter orf Symbol.is_ascii_digit;


50 
fun tz TokenNone [] = []


51 
 tz x [] = [x]


52 
 tz TokenNone (c::cs) =


53 
if Symbol.is_ascii_blank c then tz TokenNone cs


54 
else if is_lower c then (tz (TokenVar c) cs)


55 
else if is_alphanum c then (tz (TokenConst c) cs)


56 
else if c = "%" then (TokenLambda :: (tz TokenNone cs))


57 
else if c = "." then (TokenDot :: (tz TokenNone cs))


58 
else if c = "(" then (TokenLeft :: (tz TokenNone cs))


59 
else if c = ")" then (TokenRight :: (tz TokenNone cs))


60 
else if c = "=" then (TokenEq :: (tz TokenNone cs))


61 
else raise Tokenize


62 
 tz (TokenConst s) (c::cs) =


63 
if is_alphanum c then (tz (TokenConst (s ^ c)) cs)


64 
else (TokenConst s)::(tz TokenNone (c::cs))


65 
 tz (TokenVar s) (c::cs) =


66 
if is_alphanum c then (tz (TokenVar (s ^ c)) cs)


67 
else (TokenVar s)::(tz TokenNone (c::cs))


68 
 tz _ _ = raise Tokenize


69 
in tz TokenNone (explode s) end


70 


71 
exception Parse of string;


72 


73 
fun cons x xs =


74 
if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))


75 
else (x::xs)


76 


77 
fun parse_pattern f pvars ((TokenConst c)::ts) =


78 
let


79 
val (pvars, ts, plist) = parse_pattern_list f pvars ts


80 
in


81 
(pvars, ts, AbstractMachine.PConst (f c, plist))


82 
end


83 
 parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")


84 
and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)


85 
 parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))


86 
 parse_pattern_single f pvars (TokenLeft::ts) =


87 
let


88 
val (pvars, ts, p) = parse_pattern f pvars ts


89 
in


90 
case ts of


91 
TokenRight::ts => (pvars, ts, p)


92 
 _ => raise (Parse "parse_pattern_single: closing bracket expected")


93 
end


94 
 parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")


95 
and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])


96 
 parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])


97 
 parse_pattern_list f pvars ts =


98 
let


99 
val (pvars, ts, p) = parse_pattern_single f pvars ts


100 
val (pvars, ts, ps) = parse_pattern_list f pvars ts


101 
in


102 
(pvars, ts, p::ps)


103 
end


104 


105 
fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts


106 
 app_terms x [] = x


107 


108 
fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))


109 
 parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))


110 
 parse_term_single f vars (TokenLeft::ts) =


111 
let


112 
val (ts, term) = parse_term f vars ts


113 
in


114 
case ts of


115 
TokenRight::ts => (ts, term)


116 
 _ => raise Parse ("parse_term_single: closing bracket expected")


117 
end


118 
 parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =


119 
let


120 
val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts


121 
in


122 
(ts, AbstractMachine.Abs term)


123 
end


124 
 parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")


125 
and parse_term_list f vars [] = ([], [])


126 
 parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])


127 
 parse_term_list f vars ts =


128 
let


129 
val (ts, term) = parse_term_single f vars ts


130 
val (ts, terms) = parse_term_list f vars ts


131 
in


132 
(ts, term::terms)


133 
end


134 
and parse_term f vars ts =


135 
let


136 
val (ts, terms) = parse_term_list f vars ts


137 
in


138 
case terms of


139 
[] => raise (Parse "parse_term: no term found")


140 
 (t::terms) => (ts, app_terms t terms)


141 
end


142 


143 
fun read_rule f s =


144 
let


145 
val t = tokenize s


146 
val (v, ts, pattern) = parse_pattern f [] t


147 
fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")


148 
 vars (v::vs) x = if v = x then 0 else (vars vs x)+1


149 
in


150 
case ts of


151 
TokenEq::ts =>


152 
let


153 
val (ts, term) = parse_term f (vars v) ts


154 
in


155 
case ts of


156 
[] => (pattern, term)


157 
 _ => raise (Parse "read_rule: still tokens left, end expected")


158 
end


159 
 _ => raise (Parse ("read_rule: = expected"))


160 
end


161 


162 
fun read_term f g s =


163 
let


164 
val t = tokenize s


165 
val (ts, term) = parse_term f g t


166 
in


167 
case ts of


168 
[] => term


169 
 _ => raise (Parse ("read_term: still tokens left, end expected"))


170 
end


171 


172 
end
