-(* helpers ******************************************************************)
-
-let split2_last l1 l2 =
-try
- let n = pred (List.length l1) in
- let before1, after1 = HEL.split_nth n l1 in
- let before2, after2 = HEL.split_nth n l2 in
- before1, before2, List.hd after1, List.hd after2
-with Invalid_argument _ -> failwith "A2P.split2_last"
-
-let string_of_head = function
- | C.ASort _ -> "sort"
- | C.AConst _ -> "const"
- | C.AMutInd _ -> "mutind"
- | C.AMutConstruct _ -> "mutconstruct"
- | C.AVar _ -> "var"
- | C.ARel _ -> "rel"
- | C.AProd _ -> "prod"
- | C.ALambda _ -> "lambda"
- | C.ALetIn _ -> "letin"
- | C.AFix _ -> "fix"
- | C.ACoFix _ -> "cofix"
- | C.AAppl _ -> "appl"
- | C.ACast _ -> "cast"
- | C.AMutCase _ -> "mutcase"
- | C.AMeta _ -> "meta"
- | C.AImplicit _ -> "implict"
-
-let clear st = {st with intros = []}
-
-let next st = {(clear st) with depth = succ st.depth}
-
-let add st entry intro =
- {st with context = entry :: st.context; intros = intro :: st.intros}
-
-let push st = {st with case = 1 :: st.case}
-
-let inc st =
- {st with case = match st.case with
- | [] -> assert false
- | hd :: tl -> succ hd :: tl
- }
-
-let case st str =
- let case = String.concat "." (List.rev_map string_of_int st.case) in
- Printf.sprintf "case %s: %s" case str
-
-let test_depth st =
-try
- let msg = Printf.sprintf "Depth %u: " st.depth in
- match st.max_depth with
- | None -> true, ""
- | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
-with Invalid_argument _ -> failwith "A2P.test_depth"
-
-let is_rewrite_right = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
- | _ -> false
-
-let is_rewrite_left = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
- | _ -> false
-
-let is_fwd_rewrite_right hd tl =
- if is_rewrite_right hd then match List.nth tl 3 with
- | C.ARel _ -> true
- | _ -> false
- else false
-
-let is_fwd_rewrite_left hd tl =
- if is_rewrite_left hd then match List.nth tl 3 with
- | C.ARel _ -> true
- | _ -> false
- else false
-
-let get_inner_types st v =
-try
- let id = Ut.id_of_annterm v in
- try match Hashtbl.find st.types id with
- | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
- | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st)
- with Not_found -> None
-with Invalid_argument _ -> failwith "A2P.get_inner_types"
-(*
-let get_inner_sort st v =
-try
- let id = Ut.id_of_annterm v in
- try Hashtbl.find st.sorts id
- with Not_found -> `Type (CicUniv.fresh())
-with Invalid_argument _ -> failwith "A2P.get_sort"
-*)
-let get_type msg st bo =
-try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
- ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
-let get_entry st id =
- let rec aux = function
- | [] -> assert false
- | Some (C.Name name, e) :: _ when name = id -> e
- | _ :: tl -> aux tl
- in
- aux st.context
-
-let get_ind_names uri tno =
-try
- let ts = match E.get_obj Un.oblivion_ugraph uri with
- | C.InductiveDefinition (ts, _, _, _), _ -> ts
- | _ -> assert false
- in
- match List.nth ts tno with
- | (_, _, _, cs) -> List.map fst cs
-with Invalid_argument _ -> failwith "A2P.get_ind_names"