+ | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
+;;
+
+let exp_impl metasenv subst context term =
+ let rec aux metasenv context = function
+ | (Cic.Rel _) as t -> metasenv, t
+ | (Cic.Sort _) as t -> metasenv, t
+ | Cic.Const (uri, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.Const (uri, subst')
+ | Cic.Var (uri, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.Var (uri, subst')
+ | Cic.MutInd (uri, i, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.MutInd (uri, i, subst')
+ | Cic.MutConstruct (uri, i, j, subst) ->
+ let metasenv', subst' = do_subst metasenv context subst in
+ metasenv', Cic.MutConstruct (uri, i, j, subst')
+ | Cic.Meta (n,l) ->
+ let metasenv', l' = do_local_context metasenv context l in
+ metasenv', Cic.Meta (n, l')
+ | Cic.Implicit (Some `Type) ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
+ | Cic.Implicit (Some `Closed) ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+ metasenv', Cic.Meta (idx, [])
+ | Cic.Implicit None ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
+ | Cic.Implicit _ -> assert false
+ | Cic.Cast (te, ty) ->
+ let metasenv', ty' = aux metasenv context ty in
+ let metasenv'', te' = aux metasenv' context te in
+ metasenv'', Cic.Cast (te', ty')
+ | Cic.Prod (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.Prod (name, s', t)
+ | Cic.Lambda (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.Lambda (name, s', t)
+ | Cic.LetIn (name, s, t) ->
+ let metasenv', s' = aux metasenv context s in
+ metasenv', Cic.LetIn (name, s', t)
+ | Cic.Appl l when List.length l > 1 ->
+ let metasenv', l' =
+ List.fold_right
+ (fun term (metasenv, terms) ->
+ let new_metasenv, term = aux metasenv context term in
+ new_metasenv, term :: terms)
+ l (metasenv, [])
+ in
+ metasenv', Cic.Appl l'
+ | Cic.Appl _ -> assert false
+ | Cic.MutCase (uri, i, outtype, term, patterns) ->
+ let metasenv', l' =
+ List.fold_right
+ (fun term (metasenv, terms) ->
+ let new_metasenv, term = aux metasenv context term in
+ new_metasenv, term :: terms)
+ (outtype :: term :: patterns) (metasenv, [])
+ in
+ let outtype', term', patterns' =
+ match l' with
+ | outtype' :: term' :: patterns' -> outtype', term', patterns'
+ | _ -> assert false
+ in
+ metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
+ | Cic.Fix (i, funs) ->
+ let metasenv', types =
+ List.fold_right
+ (fun (name, _, typ, _) (metasenv, types) ->
+ let new_metasenv, new_type = aux metasenv context typ in
+ (new_metasenv, (name, new_type) :: types))
+ funs (metasenv, [])
+ in
+ let rec combine = function
+ | ((name, index, _, body) :: funs_tl),
+ ((_, typ) :: typ_tl) ->
+ (name, index, typ, body) :: combine (funs_tl, typ_tl)
+ | [], [] -> []
+ | _ -> assert false
+ in
+ let funs' = combine (funs, types) in
+ metasenv', Cic.Fix (i, funs')
+ | Cic.CoFix (i, funs) ->
+ let metasenv', types =
+ List.fold_right
+ (fun (name, typ, _) (metasenv, types) ->
+ let new_metasenv, new_type = aux metasenv context typ in
+ (new_metasenv, (name, new_type) :: types))
+ funs (metasenv, [])
+ in
+ let rec combine = function
+ | ((name, _, body) :: funs_tl),
+ ((_, typ) :: typ_tl) ->
+ (name, typ, body) :: combine (funs_tl, typ_tl)
+ | [], [] -> []
+ | _ -> assert false
+ in
+ let funs' = combine (funs, types) in
+ metasenv', Cic.CoFix (i, funs')
+ and do_subst metasenv context subst =
+ List.fold_right
+ (fun (uri, term) (metasenv, substs) ->
+ let metasenv', term' = aux metasenv context term in
+ (metasenv', (uri, term') :: substs))
+ subst (metasenv, [])
+ and do_local_context metasenv context local_context =
+ List.fold_right
+ (fun term (metasenv, local_context) ->
+ let metasenv', term' =
+ match term with
+ | None -> metasenv, None
+ | Some term ->
+ let metasenv', term' = aux metasenv context term in
+ metasenv', Some term'
+ in
+ metasenv', term' :: local_context)
+ local_context (metasenv, [])
+ in
+ aux metasenv context term