+
+let flatten_appls =
+ let rec flatten_xns (uri, t) = uri, flatten_term t
+ and flatten_ms = function
+ | None -> None
+ | Some t -> Some (flatten_term t)
+ and flatten_fix (name, i, ty, bo) =
+ name, i, flatten_term ty, flatten_term bo
+ and flatten_cofix (name, ty, bo) =
+ name, flatten_term ty, flatten_term bo
+ and flatten_term = function
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Rel _ as t -> t
+ | C.Const (uri, xnss) -> C.Const (uri, List.map flatten_xns xnss)
+ | C.Var (uri, xnss) -> C.Var (uri, List.map flatten_xns xnss)
+ | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, List.map flatten_xns xnss)
+ | C.MutConstruct (uri, tyno, consno, xnss) -> C.MutConstruct (uri, tyno, consno, List.map flatten_xns xnss)
+ | C.Meta (i, mss) -> C.Meta(i, List.map flatten_ms mss)
+(* begin flattening *)
+ | C.Appl [t] -> flatten_term t
+ | C.Appl (C.Appl ts1 :: ts2) -> flatten_term (C.Appl (ts1 @ ts2))
+ | C.Appl [] -> assert false
+(* end flattening *)
+ | C.Appl ts -> C.Appl (List.map flatten_term ts)
+ | C.Cast (te, ty) -> C.Cast (flatten_term te, flatten_term ty)
+ | C.MutCase (sp, i, outty, t, pl) -> C.MutCase (sp, i, flatten_term outty, flatten_term t, List.map flatten_term pl)
+ | C.Prod (n, s, t) -> C.Prod (n, flatten_term s, flatten_term t)
+ | C.Lambda (n, s, t) -> C.Lambda (n, flatten_term s, flatten_term t)
+ | C.LetIn (n, ty, s, t) -> C.LetIn (n, flatten_term ty, flatten_term s, flatten_term t)
+ | C.Fix (i, fl) -> C.Fix (i, List.map flatten_fix fl)
+ | C.CoFix (i, fl) -> C.CoFix (i, List.map flatten_cofix fl)
+ in
+ flatten_term
+
+let sober ?(flatten=false) c t =
+ if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
+
+let alpha ?flatten c t1 t2 =
+ let t1 = sober ?flatten c t1 in
+ let t2 = sober ?flatten c t2 in
+ Ut.alpha_equivalence t1 t2
+
+let occurs c ~what ~where =
+ let result = ref false in
+ let equality c t1 t2 =
+ let r = alpha ~flatten:true c t1 t2 in
+ result := !result || r; r
+ in
+ let context, what, with_what = c, [what], [C.Rel 0] in
+ let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+ !result
+
+let name_of_uri uri tyno cno =
+ let get_ind_type tys tyno =
+ let s, _, _, cs = List.nth tys tyno in s, cs
+ in
+ match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
+ | C.Variable (s, _, _, _, _), _, _ -> s
+ | C.Constant (s, _, _, _, _), _, _ -> s
+ | C.InductiveDefinition (tys, _, _, _), Some i, None ->
+ let s, _ = get_ind_type tys i in s
+ | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+ let _, cs = get_ind_type tys i in
+ let s, _ = List.nth cs (pred j) in s
+ | _ -> assert false
+
+(* Ensuring Barendregt convenction ******************************************)
+
+let rec add_entries map c = function
+ | [] -> c
+ | hd :: tl ->
+ let sname, w = map hd in
+ let entry = Some (C.Name sname, C.Decl w) in
+ add_entries map (entry :: c) tl
+
+let get_sname c i =
+ try match List.nth c (pred i) with
+ | Some (C.Name sname, _) -> sname
+ | _ -> assert false
+ with
+ | Failure _ -> assert false
+ | Invalid_argument _ -> assert false
+
+let cic_bc c t =
+ let get_fix_decl (sname, i, w, v) = sname, w in
+ let get_cofix_decl (sname, w, v) = sname, w in
+ let rec bc c = function
+ | C.LetIn (name, v, ty, t) ->
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Def (v, ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.LetIn (name, v, ty, t)
+ | C.Lambda (name, w, t) ->
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Decl w) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.Lambda (name, w, t)
+ | C.Prod (name, w, t) ->
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Decl w) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.Prod (name, w, t)
+ | C.Appl vs ->
+ let vs = List.map (bc c) vs in
+ C.Appl vs
+ | C.MutCase (uri, tyno, u, v, ts) ->
+ let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
+ C.MutCase (uri, tyno, u, v, ts)
+ | C.Cast (t, u) ->
+ let t, u = bc c t, bc c u in
+ C.Cast (t, u)
+ | C.Fix (i, fixes) ->
+ let d = add_entries get_fix_decl c fixes in
+ let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
+ let fixes = List.map bc_fix fixes in
+ C.Fix (i, fixes)
+ | C.CoFix (i, cofixes) ->
+ let d = add_entries get_cofix_decl c cofixes in
+ let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
+ let cofixes = List.map bc_cofix cofixes in
+ C.CoFix (i, cofixes)
+ | t -> t
+ in
+ bc c t
+
+let acic_bc c t =
+ let get_fix_decl (id, sname, i, w, v) = sname, cic w in
+ let get_cofix_decl (id, sname, w, v) = sname, cic w in
+ let rec bc c = function
+ | C.ALetIn (id, name, v, ty, t) ->
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Def (cic v, cic ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.ALetIn (id, name, v, ty, t)
+ | C.ALambda (id, name, w, t) ->
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Decl (cic w)) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.ALambda (id, name, w, t)
+ | C.AProd (id, name, w, t) ->
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
+ let entry = Some (name, C.Decl (cic w)) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.AProd (id, name, w, t)
+ | C.AAppl (id, vs) ->
+ let vs = List.map (bc c) vs in
+ C.AAppl (id, vs)
+ | C.AMutCase (id, uri, tyno, u, v, ts) ->
+ let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
+ C.AMutCase (id, uri, tyno, u, v, ts)
+ | C.ACast (id, t, u) ->
+ let t, u = bc c t, bc c u in
+ C.ACast (id, t, u)
+ | C.AFix (id, i, fixes) ->
+ let d = add_entries get_fix_decl c fixes in
+ let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
+ let fixes = List.map bc_fix fixes in
+ C.AFix (id, i, fixes)
+ | C.ACoFix (id, i, cofixes) ->
+ let d = add_entries get_cofix_decl c cofixes in
+ let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
+ let cofixes = List.map bc_cofix cofixes in
+ C.ACoFix (id, i, cofixes)
+ | C.ARel (id1, id2, i, sname) ->
+ let sname = get_sname c i in
+ C.ARel (id1, id2, i, sname)
+ | t -> t
+ in
+ bc c t
+
+let is_acic_proof sorts context v =
+ let id = Ut.id_of_annterm v in
+ try match Hashtbl.find sorts id with
+ | `Prop -> true
+ | _ -> false
+ with Not_found -> is_proof context (cic v)
+