+let plain_acic_term_of_cic_term =
+ let module C = Cic in
+ let mk_fresh_id =
+ let id = ref 0 in
+ function () -> incr id; "i" ^ string_of_int !id in
+ let rec aux context t =
+ let fresh_id = mk_fresh_id () in
+ match t with
+ C.Rel n ->
+ let idref,id =
+ match get_nth context n with
+ idref,(Some (C.Name s,_)) -> idref,s
+ | idref,_ -> idref,"__" ^ string_of_int n
+ in
+ C.ARel (fresh_id, idref, n, id)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AVar (fresh_id,uri,exp_named_subst')
+ | C.Implicit _
+ | C.Meta _ -> assert false
+ | C.Sort s -> C.ASort (fresh_id, s)
+ | C.Cast (v,t) ->
+ C.ACast (fresh_id, aux context v, aux context t)
+ | C.Prod (n,s,t) ->
+ C.AProd
+ (fresh_id, n, aux context s,
+ aux ((fresh_id, Some (n, C.Decl s))::context) t)
+ | C.Lambda (n,s,t) ->
+ C.ALambda
+ (fresh_id,n, aux context s,
+ aux ((fresh_id, Some (n, C.Decl s))::context) t)
+ | C.LetIn (n,s,t) ->
+ C.ALetIn
+ (fresh_id, n, aux context s,
+ aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+ | C.Appl l ->
+ C.AAppl (fresh_id, List.map (aux context) l)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AConst (fresh_id, uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri, tyno, outty, term, patterns) ->
+ C.AMutCase (fresh_id, uri, tyno, aux context outty,
+ aux context term, List.map (aux context) patterns)
+ | C.Fix (funno, funs) ->
+ let tys =
+ List.map
+ (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+ in
+ C.AFix (fresh_id, funno,
+ List.map2
+ (fun (id,_) (name, indidx, ty, bo) ->
+ (id, name, indidx, aux context ty, aux (tys@context) bo)
+ ) tys funs
+ )
+ | C.CoFix (funno, funs) ->
+ let tys =
+ List.map (fun (name,ty,_) ->
+ mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+ in
+ C.ACoFix (fresh_id, funno,
+ List.map2
+ (fun (id,_) (name, ty, bo) ->
+ (id, name, aux context ty, aux (tys@context) bo)
+ ) tys funs
+ )
+ in
+ aux
+;;