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
|