max_depth: int option;
depth : int;
defaults : bool;
+ cr : bool;
context : C.context;
case : int list
}
let get_type msg st t = H.get_type msg st.context (H.cic t)
let get_uri_of_head = function
- | C.AConst (_, u, _)
- | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
- | C.AMutInd (_, u, i, _)
- | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
- | C.AMutConstruct (_, u, i, j, _)
- | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
- | _ -> None
+ | C.AConst (_, u, _) ->
+ Some (u, 0, 0, 0)
+ | C.AAppl (_, C.AConst (_, u, _) :: vs) ->
+ Some (u, 0, 0, List.length vs)
+ | C.AMutInd (_, u, i, _) ->
+ Some (u, succ i, 0, 0)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: vs) ->
+ Some (u, succ i, 0, List.length vs)
+ | C.AMutConstruct (_, u, i, j, _) ->
+ Some (u, succ i, j, 0)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: vs) ->
+ Some (u, succ i, j, List.length vs)
+ | _ ->
+ None
let get_uri_of_apply = function
| T.Exact (t, _)
let is_reflexivity st step =
match get_uri_of_apply step with
- | None -> false
- | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n = 0
+
+let is_ho_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j, n) ->
+ st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n > 0
let are_convertible st pred sx dx =
let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in
let mk_preamble st what script = match script with
| step :: script when is_reflexivity st step ->
+ T.Reflexivity (T.note_of_step step) :: script
+ | step :: script when is_ho_reflexivity st step ->
convert st what @ T.Reflexivity (T.note_of_step step) :: script
| T.Exact _ :: _ -> script
| _ -> convert st what @ script
let e = Cn.mk_pattern 1 ity pred in
let script = [T.Branch (qs, "")] in
if Cn.does_not_occur e then script else
- if are_convertible st pred sx dx then
+ if st.cr && are_convertible st pred sx dx then
let dtext = "convertible rewrite" ^ dtext in
let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in
let city, cety = H.cic ity, H.cic ety in
max_depth = List.fold_left depth_map None params;
depth = 0;
defaults = not (List.mem G.IPNoDefaults params);
+ cr = List.mem G.IPCR params;
context = context;
case = []
}