- | 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