| Some (metasenv,bo,ty) -> metasenv,bo,ty
in
let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
- let bo' =
- let rec aux =
- let module C = Cic in
- function
- C.Rel _ as t -> t
- | C.Var _ as t -> t
- | C.Meta meta' when meta=meta' -> term
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | 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 _ as t -> t
- | C.MutInd _ as t -> t
- | 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 bo
+ let rec aux =
+ let module C = Cic in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta meta' when meta=meta' -> term
+ | C.Meta _ as t -> t
+ | C.Sort _ as t -> t
+ | 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 _ as t -> t
+ | C.MutInd _ as t -> t
+ | 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
- proof := Some (metasenv',bo',ty)
+ let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in
+ let bo' = aux bo in
+ proof := Some (metasenv'',bo',ty)
;;
+(* Returns the first meta whose number is above the number of the higher meta. *)
let new_meta () =
let metasenv =
match !proof with
(*CSC: deve sparire! *)
let context = cic_context_of_context context in
if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
- refine_meta metano bo []
+ begin
+ refine_meta metano bo [] ;
+ goal := None
+ end
else
raise (Fail "The type of the provided term is not the one expected.")
;;
+
+(* 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
+;;
projects / helm.git / blobdiff