-let fix_andreas_meta mgu mgut =
- let mgul = Array.to_list mgu in
- let mgutl = Array.to_list mgut in
- let applymetas_to_metas =
- let newmeta = new_meta () in
- (* WARNING: here we are using the invariant that above the most *)
- (* recente new_meta() there are no used metas. *)
- Array.init (List.length mgul) (function i -> newmeta + i) in
- (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
- (* Here we assume that either a META has been instantiated with *)
- (* a close term or with itself. *)
- let uninstantiatedmetas =
- List.fold_right2
- (fun bo ty newmetas ->
- let module C = Cic in
- match bo with
- Cic.Meta i ->
- let newmeta = applymetas_to_metas.(i) in
- (*CSC: se ty contiene metas, queste hanno il numero errato!!! *)
- let ty_with_newmetas =
- (* Substitues (META n) with (META (applymetas_to_metas.(n))) *)
- let rec aux =
- function
- C.Rel _
- | C.Var _ as t -> t
- | C.Meta n -> C.Meta (applymetas_to_metas.(n))
- | C.Sort _
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
- | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
- | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.Const _ as t -> t
- | C.Abst _ -> assert false
- | C.MutInd _
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,aux outt, aux t,
- List.map aux pl)
- | C.Fix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, aux ty, aux bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- in
- aux ty
- in
- (newmeta,ty_with_newmetas)::newmetas
- | _ -> newmetas
- ) mgul mgutl []
+(* Auxiliary function for apply: given a type (a backbone), it returns its *)
+(* head, a META environment in which there is a META for each hypothesis and *)
+(* the indexes of the first and last new METAs introduced. *)
+let new_metasenv_for_apply ty =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let rec aux newmeta =
+ function
+ C.Cast (he,_) -> aux newmeta he
+ | C.Prod (_,s,t) ->
+ let (res,newmetasenv,lastmeta) =
+ aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
+ in
+ res,(newmeta,s)::newmetasenv,lastmeta
+ | t -> t,[],newmeta