1structure PrecAnalysis :> PrecAnalysis =
2struct
3
4open HOLgrammars term_grammar_dtype
5
6type lspec = listspec
7type rel = HOLgrammars.rule_element
8type mlsp = HOLgrammars.mini_lspec
9
10infix |>
11fun (x |> f) = f x
12
13fun listfld_tok ppels =
14  case ppels of
15      [] => raise Fail "No TOK in list field pp-element list"
16    | RE (TOK s) :: _ => s
17    | RE TM :: _ => raise Fail "TM in list field pp-element list"
18    | ListForm _ :: _ => raise Fail "ListForm in list field pp-element list"
19    | _ :: rest => listfld_tok rest
20
21fun listform_left ({leftdelim,...} : lspec) = listfld_tok leftdelim
22fun listform_right ({rightdelim,...} : lspec) = listfld_tok rightdelim
23
24fun rel_equalities rels =
25  let
26    fun recurse rels (A as (lastopt, acc)) =
27      case (lastopt, rels) of
28          (_, []) => acc
29        | (SOME(_, true), TM :: _) => raise Fail "Two TM elements in a row"
30        | (SOME(tk1,false), TM :: rest) => recurse rest (SOME(tk1,true), acc)
31        | (SOME(tk1, tmp), TOK tk2::rest) =>
32            recurse rest (SOME(tk2,false), (tk1,tmp,tk2)::acc)
33        | (SOME(tk1, true), ListTM _ :: rest) =>
34            raise Fail "rel_equalities: TM before ListTM"
35        | (SOME(tk1, false), ListTM{sep,...} :: TOK tk2 :: rest) =>
36            recurse rest (SOME (tk2,false),
37                          (tk1,true,sep) :: (sep,true,sep) ::
38                          (sep,false,tk2) :: (sep,true,tk2) ::
39                          (tk1,true,tk2) :: (tk1,false,tk2) :: acc)
40        | (_, ListTM _ :: ListTM _ :: _) =>
41            raise Fail "rel_equalities: two ListTMs in a row"
42        | (_, ListTM _ :: TM :: _) =>
43            raise Fail "rel_equalities: ListTM followed by TM"
44        | (_, [ListTM _]) => raise Fail "rel_equalities: last ListTM"
45        | (NONE, TM :: _) => raise Fail "rel_equalities: initial TM"
46        | (NONE, TOK tk :: rest) => recurse rest (SOME(tk,false), acc)
47        | (NONE, ListTM _ :: _) => raise Fail "rel_equalities: initial ListTM"
48  in
49    recurse rels (NONE, [])
50  end
51
52fun ppel_equalities ppels = rel_equalities (term_grammar.rule_elements ppels)
53fun rule_equalities (rr : rule_record) = ppel_equalities (#elements rr)
54
55type rell_transform = rule_element list -> rule_element list
56
57fun mkrels_infix rels = TM :: (rels @ [TM])
58fun mkrels_suffix rels = TM :: rels
59fun mkrels_prefix rels = rels @ [TM]
60fun mkrels_closefix rels = rels
61
62fun check_for_listreductions check rels =
63  let
64    val rev = List.rev
65    fun recurse A left_opt sep_opt p rels =
66      (* left_opt is candidate left-delimiter, sep_opt candidate separator
67         Invariant:
68           left_opt = SOME l ==> TOK l was seen earlier as candidate leftdelim
69           sep_opt = SOME s ==>
70             ?l. left_opt = SOME l /\ TOK s followed a TM after the l was
71                 seen and there have been no other TOKs seen since, and
72                 check(l,s) = NONE
73           (p <=> last thing seen was TM)
74       *)
75      case rels of
76          [] => rev A
77        | [TM] => rev A
78        | [TOK tk1] => (* tk1 may end a list *)
79          let
80          in
81            case sep_opt of
82                SOME s =>
83                   (case check(s, tk1) of
84                        NONE =>
85                        (case check(valOf left_opt, tk1) of
86                             NONE => rev A
87                           | SOME lp =>
88                               rev ((valOf left_opt, tk1, lp) :: A))
89                      | SOME lp => rev ((s,tk1,lp)::A))
90              | NONE =>
91                   (case left_opt of
92                        NONE => rev A
93                      | SOME l => (case check(l,tk1) of
94                                       NONE => rev A
95                                     | SOME lp => rev ((l,tk1,lp) :: A)))
96          end
97        | TOK tk1 :: TM :: rest =>
98          let
99          in
100            case sep_opt of
101                SOME s =>
102                   (if s = tk1 andalso p then
103                      recurse A left_opt sep_opt true rest
104                    else
105                      case check (valOf left_opt, tk1) of
106                          NONE =>
107                          (case check (s, tk1) of
108                               NONE =>
109                                 if p then
110                                   recurse A (SOME s) (SOME tk1) true rest
111                                 else
112                                   recurse A (SOME tk1) NONE true rest
113                             | SOME lp =>
114                                 recurse ((s,tk1,lp)::A) (SOME tk1) NONE
115                                         true rest)
116                        | SOME lp => recurse ((valOf left_opt, tk1, lp)::A)
117                                             (SOME tk1) NONE true rest)
118              | NONE =>
119                  (case left_opt of
120                       NONE => recurse A (SOME tk1) NONE true rest
121                     | SOME l =>
122                         (case check (l, tk1) of
123                              NONE => if p then
124                                        recurse A left_opt (SOME tk1) true rest
125                                      else
126                                        recurse A (SOME tk1) NONE true rest
127                            | SOME lp =>
128                                recurse ((l,tk1,lp)::A) (SOME tk1) NONE
129                                        true rest))
130          end
131        | TOK tk1 :: TOK tk2 :: rest =>
132            (case sep_opt of
133                 SOME s =>
134                   if s = tk1 andalso p then
135                     case check (valOf left_opt, tk2) of
136                         NONE =>
137                         (case check(tk1,tk2) of
138                              NONE => recurse A (SOME tk2) NONE false rest
139                            | SOME lp =>
140                                recurse ((tk1,tk2,lp)::A) (SOME tk2) NONE
141                                        false rest)
142                       | SOME lp =>
143                          recurse ((valOf left_opt, tk2, lp)::A)
144                                  (SOME tk2) NONE false rest
145                   else
146                     (case check(s,tk1) of
147                         NONE =>
148                         if p then
149                           case check(s,tk2) of
150                               NONE =>
151                               (case check (tk1,tk2) of
152                                    NONE => recurse A (SOME tk2) NONE false rest
153                                  | SOME lp =>
154                                    recurse ((tk1,tk2,lp)::A) (SOME tk2)
155                                            NONE false rest)
156                             | SOME lp =>
157                               (* s is the left, tk1 is the sep, tk2 right *)
158                               recurse ((s,tk2,lp)::A) (SOME tk2) NONE false
159                                       rest
160                         else
161                           (case check (tk1,tk2) of
162                                    NONE => recurse A (SOME tk2) NONE false rest
163                                  | SOME lp =>
164                                    recurse ((tk1,tk2,lp)::A) (SOME tk2)
165                                            NONE false rest)
166                       | SOME lp =>
167                            recurse ((s,tk1,lp)::A) (SOME tk1) NONE
168                                    false (TOK tk2 :: rest))
169               | NONE => (* no sep *)
170                 let
171                   val f = case check(tk1,tk2) of
172                                NONE => (fn A => A)
173                              | SOME lp => (fn A => (tk1,tk2,lp) :: A)
174                 in
175                   case left_opt of
176                      NONE => recurse (f A) (SOME tk2) NONE false rest
177                    | SOME l =>
178                      (case check(l,tk1) of
179                           NONE =>
180                           if p then (* tk1 might be sep and tk2 rdelim *)
181                             case check(l,tk2) of
182                                 NONE =>
183                                   recurse (f A) (SOME tk2) NONE false rest
184                               | SOME lp =>
185                                   recurse ((l,tk2,lp)::A) (SOME tk2) NONE false
186                                           rest
187                           else
188                             recurse (f A) (SOME tk2) NONE false rest
189                         | SOME lp =>
190                             recurse (f ((l,tk1,lp)::A)) (SOME tk2) NONE false
191                                     rest)
192                 end)
193        | TM :: rest => (* p must be false as two TMs in a row is impossible *)
194            recurse A left_opt sep_opt true rest
195        | _ => raise Fail "check_for_listreductions: impossible rhs"
196  in
197    recurse [] NONE NONE false rels
198  end
199
200fun rev2 (l1, l2, c) = (List.rev l1, List.rev l2, c)
201fun c1 x (l1, l2, c) = (x::l1, l2, c)
202fun c2 x (l1, l2, c) = (l1, x::l2, c)
203fun inc (l1, l2, c) = (l1, l2, c + 1)
204fun ap1 f (x,y,z) = (f x, y, z)
205
206fun remove_listrels lsps rels =
207  let
208    fun recurse (A as (outrels, listbits, tmc)) lsps rels =
209      case lsps of
210          [] => ap1 (fn l => l @ rels) (rev2 A)
211        | (ld,rd,lsp:mini_lspec)::more_lsps =>
212          (case rels of
213               [] => rev2 A
214             | TM :: rrest => recurse (A |> inc |> c1 TM) lsps rrest
215             | (rel as TOK tk) :: more_rels =>
216                 if tk <> ld then recurse (c1 rel A) lsps more_rels
217                 else (* tk = ld *)
218                   let
219                     val {sep,...} = lsp
220                   in
221                     case more_rels of
222                         TOK tk' :: later_rels =>
223                           if tk' = rd then
224                             recurse
225                               (A |> c1 rel |> c1 TM |> c2 (lsp,[]))
226                               more_lsps
227                               more_rels
228                           else
229                             (* probably an error; can't be sep as no TM first*)
230                             recurse (c1 rel A) more_lsps more_rels
231                       | TM :: (inter_rels as (TOK sep' :: later_rels)) =>
232                           if sep = sep' then
233                             consume_list
234                               (A |> c1 rel |> c1 TM |> inc) (lsp, [#3 A]) rd
235                               more_lsps later_rels
236                           else if sep' = rd then
237                             recurse
238                               (A |> c1 rel |> c1 TM |> inc |> c2 (lsp, [#3 A]))
239                               more_lsps inter_rels
240                           else (* probably an error *)
241                             recurse (A |> c1 rel |> c1 TM |> inc)
242                                     lsps
243                                     inter_rels
244                       | _ => raise Fail "remove_listrels: malformed RHS"
245                   end
246             | _ => raise Fail "remove_listrels: malformed RHS(2)")
247    and consume_list A (curr as (lsp, idxs)) rdelim lsps rels =
248        case rels of
249            [] => (* probably an error *) rev2 (A |> c2 (lsp, List.rev idxs))
250          | TM :: rest => consume_list (A |> inc) (lsp, #3 A :: idxs)
251                                       rdelim lsps rest
252          | TOK t :: rest =>
253            if t = rdelim then
254              recurse (A |> c2 (lsp, List.rev idxs)) lsps rels
255            else (* it's assumed to be the sep *)
256              consume_list A curr rdelim lsps rest
257          | _ => raise Fail "consume_list: malformed RHS"
258    val (x, y, _) = recurse ([], [], 0) lsps rels
259  in
260    (x,y)
261  end
262
263end
264