-(* The term bo must be closed in the current context *)
-let apply term =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let metasenv =
- match !proof with
- None -> assert false
- | Some (metasenv,_,_) -> metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- (*CSC: deve sparire! *)
- let ciccontext = cic_context_of_context context in
- let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
- 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 ->
- 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 []
- in
- let mgul' =
- List.map
- (function
- Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i))
- | _ as t -> t
- ) mgul in
- let bo' =
- if List.length mgul' = 0 then
- term
- else
- Cic.Appl (term::mgul')
- in
- refine_meta metano bo' uninstantiatedmetas ;
- match uninstantiatedmetas with
- (n,ty)::tl -> goal := Some (n,(context,ty))
- | [] -> goal := None
-;;