76 | _ => t) |
76 | _ => t) |
77 | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u) |
77 | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u) |
78 | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t) |
78 | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t) |
79 | unfold_let t = t; |
79 | unfold_let t = t; |
80 |
80 |
81 val dummy_var_name = "?f" |
|
82 |
|
83 fun mk_map_pattern ctxt s = |
81 fun mk_map_pattern ctxt s = |
84 let |
82 let |
85 val bnf = the (bnf_of ctxt s); |
83 val bnf = the (bnf_of ctxt s); |
86 val mapx = map_of_bnf bnf; |
84 val mapx = map_of_bnf bnf; |
87 val live = live_of_bnf bnf; |
85 val live = live_of_bnf bnf; |
88 val (f_Ts, _) = strip_typeN live (fastype_of mapx); |
86 val (f_Ts, _) = strip_typeN live (fastype_of mapx); |
89 val fs = map_index (fn (i, T) => Var ((dummy_var_name, i), T)) f_Ts; |
87 val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts; |
90 in |
88 in |
91 (mapx, betapplys (mapx, fs)) |
89 (mapx, betapplys (mapx, fs)) |
92 end; |
90 end; |
93 |
91 |
94 fun dest_map ctxt s call = |
92 fun dest_map ctxt s call = |