in
1 + aux (None, indexes)
+(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *)
+(* questa o la precedente sembrano essere equivalenti come tempi *)
+let apply_subst_context _ context = context ;;
+
let mk_implicit metasenv subst context =
let newmeta = new_meta metasenv subst in
let newuniv = CicUniv.fresh () in
(* in the following mk_* functions we apply substitution to canonical
* context since we have the invariant that the metasenv has already been
* instantiated with subst *)
- let context = CicMetaSubst.apply_subst_context subst context in
+ let context = apply_subst_context subst context in
([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
(* TASSI: ?? *)
newmeta + 1, context, Cic.Meta (newmeta, []);
let mk_implicit_type metasenv subst context =
let newmeta = new_meta metasenv subst in
let newuniv = CicUniv.fresh () in
- let context = CicMetaSubst.apply_subst_context subst context in
+ let context = apply_subst_context subst context in
([ newmeta, [], Cic.Sort (Cic.Type newuniv);
(* TASSI: ?? *)
newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
if n = 0 then metasenv, []
else
let irl = identity_relocation_list_for_metavariable context in
- let context = CicMetaSubst.apply_subst_context subst context in
+ let context = apply_subst_context subst context in
let newmeta = new_meta metasenv subst in
let newuniv = CicUniv.fresh () in
let rec aux newmeta n =
let fresh_subst metasenv subst context uris =
let irl = identity_relocation_list_for_metavariable context in
- let context = CicMetaSubst.apply_subst_context subst context in
+ let context = apply_subst_context subst context in
let newmeta = new_meta metasenv subst in
let newuniv = CicUniv.fresh () in
let rec aux newmeta = function
(uri,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris
-let expand_implicits 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) = mk_implicit_type metasenv subst context in
- let irl = identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
- | Cic.Implicit (Some `Closed) ->
- let (metasenv', idx) = mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
- | Cic.Implicit None ->
- let (metasenv', idx) = mk_implicit metasenv subst context in
- let irl = identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, 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
-