-let mk_implicit' metasenv context =
- let (metasenv, index) = mk_implicit metasenv context in
- (metasenv, index - 1, index)
-
-let mk_implicit_type metasenv context =
- let newmeta = new_meta metasenv in
- let irl = identity_relocation_list_for_metavariable context in
- ([ newmeta, context, Cic.Sort Cic.Type ;
- newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
- newmeta + 1)
-
-let expand_implicits metasenv 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 ->
- let (metasenv', type_index, _) = mk_implicit' metasenv context in
- let irl = identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (type_index, irl)
- | 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
- let metasenv'', t' =
- aux metasenv' (Some (name, Cic.Decl s') :: context) t
- in
- metasenv'', Cic.Prod (name, s', t')
- | Cic.Lambda (name, s, t) ->
- let metasenv', s' = aux metasenv context s in
- let metasenv'', t' =
- aux metasenv' (Some (name, Cic.Decl s') :: context) t
- in
- metasenv'', Cic.Lambda (name, s', t')
- | Cic.LetIn (name, s, t) ->
- let metasenv', s' = aux metasenv context s in
- let metasenv'', t' =
- aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
- 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 context' =
- (List.rev_map
- (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
- types)
- @ context
- in
- let metasenv'', bodies =
- List.fold_right
- (fun (_, _, _, body) (metasenv, bodies) ->
- let new_metasenv, new_body = aux metasenv context' body in
- (new_metasenv, new_body :: bodies))
- funs (metasenv', [])
- in
- let rec combine = function
- | ((name, index, _, _) :: funs_tl),
- ((_, typ) :: typ_tl),
- (body :: body_tl) ->
- (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
- | [], [], [] -> []
- | _ -> assert false
- in
- let funs' = combine (funs, types, bodies) 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 context' =
- (List.rev_map
- (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
- types)
- @ context
- in
- let metasenv'', bodies =
- List.fold_right
- (fun (_, _, body) (metasenv, bodies) ->
- let new_metasenv, new_body = aux metasenv context' body in
- (new_metasenv, new_body :: bodies))
- funs (metasenv', [])
- in
- let rec combine = function
- | ((name, _, _) :: funs_tl),
- ((_, typ) :: typ_tl),
- (body :: body_tl) ->
- (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
- | [], [], [] -> []
- | _ -> assert false
- in
- let funs' = combine (funs, types, bodies) 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
-