src/Tools/Argo/argo_rewr.ML
changeset 63960 3daf02070be5
child 64927 a5a09855e424
     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