let simple_expand_match ps =
let rec aux_nob level = function
- | #i_num_var as t -> aux_i_num_var level t
+ | #i_num_var as t -> (aux_i_num_var level t :> nf)
| `Lam(b,t) -> `Lam(b,aux (level+1) t)
| `Pacman as t -> t
and aux level = function
| #nf_nob as t -> aux_nob level t
and aux_i_num_var level = function
| `Match(u,v,bs_lift,bs,args) as torig ->
- let u = aux_i_num_var level u in
+ let (u : i_num_var) = aux_i_num_var level u in
bs := List.map (fun (n, x) -> n, aux 0 x) !bs;
(try
(match u with
| #i_n_var as u ->
- let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *)
- in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in
+ let i = index_of (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
+ let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in
if t <> torig then
- aux level (t :> nf)
- else raise Not_found
+ aux_i_num_var level t
+ else raise Not_found
| _ -> raise Not_found)
with Not_found ->
- mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args))
- | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args))
+ cast_to_i_num_var (mk_appl (`Match(u,v,bs_lift,bs,[])) (List.map (aux_nob level) args)))
+ | `I(v,args) -> cast_to_i_num_var (mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args)))
| `N _ | `Var _ as t -> t
in aux_i_num_var 0
;;
let div = option_map (fun div ->
let divs = super_simplify_ps p.ps ([div] :> i_n_var list) in
List.hd divs) div in
- {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv}
+ {p with div=option_map cast_to_i_var div; ps; conv}
let cast_to_ps_with_match =
function