1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/Argo/argo_rewr.ML Thu Sep 29 20:54:44 2016 +0200
1.3 @@ -0,0 +1,266 @@
1.4 +(* Title: Tools/Argo/argo_rewr.ML
1.5 + Author: Sascha Boehme
1.6 +
1.7 +Bottom-up rewriting of expressions based on rewrite rules and rewrite functions.
1.8 +*)
1.9 +
1.10 +signature ARGO_REWR =
1.11 +sig
1.12 + (* patterns *)
1.13 + datatype pattern =
1.14 + V of int |
1.15 + E of Argo_Expr.expr |
1.16 + A of Argo_Expr.kind |
1.17 + P of Argo_Expr.kind * pattern list |
1.18 + M of pattern |
1.19 + X
1.20 +
1.21 + (* scanning patterns from strings *)
1.22 + val scan: string -> pattern
1.23 +
1.24 + (* pattern matching *)
1.25 + type env
1.26 + val get_all: env -> Argo_Expr.expr list
1.27 + val get: env -> int -> Argo_Expr.expr
1.28 +
1.29 + (* conversions *)
1.30 + type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv
1.31 + val keep: conv
1.32 + val seq: conv list -> conv
1.33 + val args: conv -> conv
1.34 + val rewr: Argo_Proof.rewrite -> Argo_Expr.expr -> conv
1.35 +
1.36 + (* context *)
1.37 + type context
1.38 + val context: context
1.39 + val flat: string ->
1.40 + (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * Argo_Expr.expr) option) ->
1.41 + context -> context
1.42 + val func: string -> (env -> (Argo_Proof.rewrite * pattern) option) -> context -> context
1.43 + val rule: Argo_Proof.rewrite -> string -> string -> context -> context
1.44 +
1.45 + (* rewriting *)
1.46 + val rewrite: context -> conv
1.47 + val rewrite_top: context -> conv
1.48 + val with_proof: conv -> Argo_Expr.expr * Argo_Proof.proof -> Argo_Proof.context ->
1.49 + (Argo_Expr.expr * Argo_Proof.proof) * Argo_Proof.context
1.50 +end
1.51 +
1.52 +structure Argo_Rewr: ARGO_REWR =
1.53 +struct
1.54 +
1.55 +(* patterns *)
1.56 +
1.57 +(*
1.58 + Patterns are used for matching against expressions and as a schema to construct
1.59 + expressions. For matching, only V, E, A and P must be used. For the schema,
1.60 + additionally M and X can be used.
1.61 +*)
1.62 +
1.63 +datatype pattern =
1.64 + V of int | (* indexed placeholder where the index must be greater than 0 *)
1.65 + E of Argo_Expr.expr | (* expression without placeholders *)
1.66 + A of Argo_Expr.kind | (* placeholder for the arguments of an n-ary expression *)
1.67 + P of Argo_Expr.kind * pattern list | (* expression with optional placeholders *)
1.68 + M of pattern | (* mapping operator to iterate over an argument list of an n-ary expression *)
1.69 + X (* closure argument under a mapping operator representing an expression *)
1.70 +
1.71 +fun int_of_pattern (E _) = 0
1.72 + | int_of_pattern (P _) = 1
1.73 + | int_of_pattern (A _) = 2
1.74 + | int_of_pattern (V _) = 3
1.75 + | int_of_pattern _ = raise Fail "bad pattern"
1.76 +
1.77 +(*
1.78 + Specific patterns are ordered before generic patterns, since pattern matching
1.79 + performs a linear search for the most suitable pattern.
1.80 +*)
1.81 +
1.82 +fun pattern_ord (E e1, E e2) = Argo_Expr.expr_ord (e1, e2)
1.83 + | pattern_ord (P (k1, ps1), P (k2, ps2)) =
1.84 + (case Argo_Expr.kind_ord (k1, k2) of EQUAL => list_ord pattern_ord (ps1, ps2) | x => x)
1.85 + | pattern_ord (A k1, A k2) = Argo_Expr.kind_ord (k1, k2)
1.86 + | pattern_ord (V i1, V i2) = int_ord (i1, i2)
1.87 + | pattern_ord (p1, p2) = int_ord (int_of_pattern p1, int_of_pattern p2)
1.88 +
1.89 +
1.90 +(* scanning patterns from strings *)
1.91 +
1.92 +(*
1.93 + The pattern language is cumbersome to use in other structures. Strings are a more
1.94 + lightweight representation. Scanning patterns from strings should be performed at
1.95 + compile time to avoid the parsing overhead at runtime.
1.96 +*)
1.97 +
1.98 +val kind = Scan.many1 Symbol.is_ascii_letter >> (Argo_Expr.kind_of_string o implode)
1.99 +val num = Scan.many1 Symbol.is_ascii_digit >> (the o Int.fromString o implode)
1.100 +val integer = $$ "-" |-- num >> ~ || num
1.101 +val blank = Scan.many1 Symbol.is_ascii_blank >> K ()
1.102 +
1.103 +fun pattern xs = (
1.104 + kind >> (P o rpair []) ||
1.105 + $$ "!" >> K X ||
1.106 + $$ "(" -- $$ "#" -- blank |-- pattern --| $$ ")" >> M ||
1.107 + $$ "(" -- $$ "?" -- blank |-- num --| $$ ")" >> V ||
1.108 + $$ "(" -- Scan.this_string "num" -- blank |-- integer --| $$ ")" >>
1.109 + (E o Argo_Expr.mk_num o Rat.of_int) ||
1.110 + $$ "(" |-- kind --| blank --| $$ "_" --| $$ ")" >> A ||
1.111 + $$ "(" |-- kind -- Scan.repeat1 (blank |-- pattern) --| $$ ")" >> P) xs
1.112 +
1.113 +fun scan s = fst (pattern (map str (String.explode s) @ [""]))
1.114 +
1.115 +
1.116 +(* pattern matching *)
1.117 +
1.118 +exception PATTERN of unit
1.119 +
1.120 +(*
1.121 + The environment stores the matched expressions for the pattern placeholders.
1.122 + The expression for an indexed placeholder (V i) can be retrieved by "get env i".
1.123 + The argument expressions for an n-ary placeholder (A k) can be retrieved by "get_all env".
1.124 +*)
1.125 +
1.126 +type env = Argo_Expr.expr list Inttab.table
1.127 +
1.128 +val empty_env: env = Inttab.empty
1.129 +fun get_all env = Inttab.lookup_list env 0
1.130 +fun get env i = hd (Inttab.lookup_list env i)
1.131 +
1.132 +fun depth_of (V _) = 0
1.133 + | depth_of (E _) = 0
1.134 + | depth_of (A _) = 1
1.135 + | depth_of (P (_, ps)) = 1 + fold (Integer.max o depth_of) ps 0
1.136 + | depth_of (M p) = depth_of p
1.137 + | depth_of X = 0
1.138 +
1.139 +fun match_list f k k' env = if k = k' then f env else raise PATTERN ()
1.140 +
1.141 +fun match (V i) e env = Inttab.update_new (i, [e]) env
1.142 + | match (A k) (Argo_Expr.E (k', es)) env = match_list (Inttab.update_new (0, es)) k k' env
1.143 + | match (P (k, ps)) (Argo_Expr.E (k', es)) env = match_list (fold2 match ps es) k k' env
1.144 + | match _ _ _ = raise Fail "bad pattern"
1.145 +
1.146 +fun unfold_index env (V i) _ = get env i
1.147 + | unfold_index _ (E e) _ = e
1.148 + | unfold_index env (P (k, ps)) e = Argo_Expr.E (k, map (fn p => unfold_index env p e) ps)
1.149 + | unfold_index _ X e = e
1.150 + | unfold_index _ _ _ = raise Fail "bad pattern"
1.151 +
1.152 +fun unfold_pattern env (V i) = get env i
1.153 + | unfold_pattern _ (E e) = e
1.154 + | unfold_pattern env (A k) = Argo_Expr.E (k, get_all env)
1.155 + | unfold_pattern env (P (k, [M p])) = Argo_Expr.E (k, map (unfold_index env p) (get_all env))
1.156 + | unfold_pattern env (P (k, ps)) = Argo_Expr.E (k, map (unfold_pattern env) ps)
1.157 + | unfold_pattern _ _ = raise Fail "bad pattern"
1.158 +
1.159 +
1.160 +(* conversions *)
1.161 +
1.162 +(*
1.163 + Conversions are atomic rewrite steps. For every conversion there is a corresponding
1.164 + inference step.
1.165 +*)
1.166 +
1.167 +type conv = Argo_Expr.expr -> Argo_Expr.expr * Argo_Proof.conv
1.168 +
1.169 +fun keep e = (e, Argo_Proof.keep_conv)
1.170 +
1.171 +fun seq [] e = keep e
1.172 + | seq [cv] e = cv e
1.173 + | seq (cv :: cvs) e =
1.174 + let val ((e, c2), c1) = cv e |>> seq cvs
1.175 + in (e, Argo_Proof.mk_then_conv c1 c2) end
1.176 +
1.177 +fun args cv (Argo_Expr.E (k, es)) =
1.178 + let val (es, cs) = split_list (map cv es)
1.179 + in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv cs) end
1.180 +
1.181 +fun rewr r e _ = (e, Argo_Proof.mk_rewr_conv r)
1.182 +
1.183 +
1.184 +(* context *)
1.185 +
1.186 +(*
1.187 + The context stores functions to flatten expressions and functions to rewrite expressions.
1.188 + Flattening an n-ary expression of kind k produces an expression whose arguments are not
1.189 + of kind k. For instance, flattening (and p (and q r)) produces (and p q r) where p, q and r
1.190 + are not conjunctions.
1.191 +*)
1.192 +
1.193 +structure Pattab = Table(type key = pattern val ord = pattern_ord)
1.194 +
1.195 +type context = {
1.196 + flats:
1.197 + (Argo_Expr.kind * (int -> Argo_Expr.expr list -> (Argo_Proof.rewrite * Argo_Expr.expr) option))
1.198 + list, (* expressions that should be flattened before rewriting *)
1.199 + rewrs: (env -> (Argo_Proof.rewrite * pattern) option) list Pattab.table}
1.200 + (* Looking up matching rules is O(n). This could be optimized. *)
1.201 +
1.202 +fun mk_context flats rewrs: context = {flats=flats, rewrs=rewrs}
1.203 +val context = mk_context [] Pattab.empty
1.204 +
1.205 +fun map_context map_flats map_rewrs ({flats, rewrs}: context) =
1.206 + mk_context (map_flats flats) (map_rewrs rewrs)
1.207 +
1.208 +fun flat lhs f =
1.209 + (case scan lhs of
1.210 + A k => map_context (cons (k, f)) I
1.211 + | _ => raise Fail "bad pattern")
1.212 +
1.213 +fun func lhs f = map_context I (Pattab.map_default (scan lhs, []) (fn fs => fs @ [f]))
1.214 +fun rule r lhs rhs = func lhs (K (SOME (r, scan rhs)))
1.215 +
1.216 +
1.217 +(* rewriting *)
1.218 +
1.219 +(*
1.220 + Rewriting proceeds bottom-up. Whenever a rewrite rule with placeholders is used,
1.221 + the arguments are again rewritten, but only up to depth of the placeholders within the
1.222 + matched pattern.
1.223 +*)
1.224 +
1.225 +fun rewr_rule r env p = rewr r (unfold_pattern env p)
1.226 +
1.227 +fun try_apply p e f =
1.228 + let val env = match p e empty_env
1.229 + in (case f env of NONE => NONE | SOME (r, p) => SOME (r, env, p)) end
1.230 + handle PATTERN () => NONE
1.231 +
1.232 +fun all_args cv k (e as Argo_Expr.E (k', _)) = if k = k' then args (all_args cv k) e else cv e
1.233 +fun all_args_of k (e as Argo_Expr.E (k', es)) = if k = k' then maps (all_args_of k) es else [e]
1.234 +fun kind_depth_of k (Argo_Expr.E (k', es)) =
1.235 + if k = k' then 1 + fold (Integer.max o kind_depth_of k) es 0 else 0
1.236 +
1.237 +fun descend cv flats (e as Argo_Expr.E (k, _)) =
1.238 + if AList.defined Argo_Expr.eq_kind flats k then all_args cv k e
1.239 + else args cv e
1.240 +
1.241 +fun flatten flats (e as Argo_Expr.E (k, _)) =
1.242 + (case AList.lookup Argo_Expr.eq_kind flats k of
1.243 + NONE => keep e
1.244 + | SOME f =>
1.245 + (case f (kind_depth_of k e) (all_args_of k e) of
1.246 + NONE => keep e
1.247 + | SOME (r, e') => rewr r e' e))
1.248 +
1.249 +fun exhaust cv rewrs e =
1.250 + (case Pattab.get_first (fn (p, fs) => get_first (try_apply p e) fs) rewrs of
1.251 + NONE => keep e
1.252 + | SOME (r, env, p) => seq [rewr_rule r env p, cv (depth_of p)] e)
1.253 +
1.254 +fun norm (cx as {flats, rewrs}: context) d e =
1.255 + seq [
1.256 + if d = 0 then keep else descend (norm cx (d - 1)) flats,
1.257 + flatten flats,
1.258 + exhaust (norm cx) rewrs] e
1.259 +
1.260 +fun rewrite cx = norm cx ~1 (* bottom-up rewriting *)
1.261 +fun rewrite_top cx = norm cx 0 (* top-down rewriting *)
1.262 +
1.263 +fun with_proof cv (e, p) prf =
1.264 + let
1.265 + val (e, c) = cv e
1.266 + val (p, prf) = Argo_Proof.mk_rewrite c p prf
1.267 + in ((e, p), prf) end
1.268 +
1.269 +end