From b5f6ad3ab6163a257f6491ef6ff922ff8c1239a7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Apr 2002 17:07:57 +0000 Subject: [PATCH] * New implementation of Apply and Elim based on the latest implementation of the unification (not yet commited) --- helm/gTopLevel/proofEngine.ml | 320 ++++++++++++++-------------------- 1 file changed, 130 insertions(+), 190 deletions(-) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 29a23a191..5f64134b5 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -28,55 +28,37 @@ let cic_context_of_named_context = ) ;; +let refine_meta_with_brand_new_metasenv meta term newmetasenv = + let (uri,bo,ty) = + match !proof with + None -> assert false + | Some (uri,_,bo,ty) -> uri,bo,ty + in + let subst_in t = + ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t + in + let bo' = subst_in bo in + let metasenv' = List.remove_assoc meta newmetasenv in + proof := Some (uri,metasenv',bo',ty) +;; + let refine_meta meta term newmetasenv = let (uri,metasenv,bo,ty) = match !proof with None -> assert false | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in - let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in - 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) + let subst_in t = + ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t in - let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in - let bo' = aux bo in - proof := Some (uri,metasenv'',bo',ty) + let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in + let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in + let bo' = subst_in bo in + proof := Some (uri,metasenv'',bo',ty) ;; -(* Returns the first meta whose number is above the number of the higher meta. *) +(* Returns the first meta whose number is above the *) +(* number of the higher meta. *) let new_meta () = let metasenv = match !proof with @@ -230,75 +212,42 @@ let exact bo = raise (Fail "The type of the provided term is not the one expected.") ;; -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 in - let mgul' = - List.map - (function - Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) - | _ as t -> t - ) mgul - in - mgul',uninstantiatedmetas + let newmeta = new_meta () in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let (res,newmetasenv,lastmeta) = aux newmeta ty in + res,newmetasenv,newmeta,lastmeta +;; + +(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) +let classify_metas newmeta in_subst_domain apply_subst = + List.fold_left + (fun (old_uninst,new_uninst) (i,ty) -> + if in_subst_domain i then + old_uninst,new_uninst + else + let ty' = apply_subst ty in + if i < newmeta then + ((i,ty')::old_uninst),new_uninst + else + old_uninst,((i,ty')::new_uninst) + ) ([],[]) ;; (* The term bo must be closed in the current context *) @@ -320,21 +269,33 @@ let apply term = metano,context,ty in let ciccontext = cic_context_of_named_context context in - let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in - let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut 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 + let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in + (* newmeta is the lowest index of the new metas introduced *) + let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in + let newmetasenv = newmetas@metasenv in + let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in + let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in + let apply_subst = CicUnification.apply_subst subst in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + classify_metas newmeta in_subst_domain apply_subst newmetasenv + in + let bo' = + if List.length newmetas = 0 then + term + else + let arguments = + List.map apply_subst + (List.map (function (i,_) -> C.Meta i) newmetas) + in + Cic.Appl (term::arguments) + in + refine_meta_with_brand_new_metasenv metano bo' + (new_uninstantiatedmetas@old_uninstantiatedmetas) ; + match new_uninstantiatedmetas with + [] -> goal := None + | (i,ty)::_ -> goal := Some (i,(context,ty)) ;; - let eta_expand metasenv ciccontext t arg = let module T = CicTypeChecker in let module S = CicSubstitution in @@ -438,43 +399,21 @@ let elim term = let ety = T.type_of_aux' [] [] eliminator_ref in - - let earity = CicUnification.get_arity ety in - let mgu = Array.init earity (fun i -> (C.Meta i)) in - let mgut = Array.make earity C.Implicit in + let (econclusion,newmetas,newmeta,lastmeta) = + new_metasenv_for_apply ety + in (* Here we assume that we have only one inductive hypothesis to *) (* eliminate and that it is the last hypothesis of the theorem. *) (* A better approach would be fingering the hypotheses in some *) (* way. *) - let hypothesis_to_eliminate,econclusion = - (* aux n h t *) - (* traverses the backbone [t] looking for the last hypothesis *) - (* and substituting Pi-abstractions with META declarations. *) - (* [h] is the last hypothesis met up to now. [n] is the next *) - (* unused META. *) - let rec aux n h = - function - C.Prod (_,s,t) -> - mgut.(n) <- s ; - aux (n+1) (Some s) (CicSubstitution.subst (C.Meta n) t) - | C.Cast (te,_) -> aux n h te - | t -> match h with - None -> raise NoHypothesesFound - | Some h' -> h',t - in - aux 0 None ety - in -prerr_endline ("HTOELIM: " ^ CicPp.ppterm hypothesis_to_eliminate) ; + let meta_of_corpse = Cic.Meta (lastmeta - 1) in + let newmetasenv = newmetas @ metasenv in prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ; flush stderr ; - ignore (CicUnification.fo_unif_mgu 0 hypothesis_to_eliminate termty mgu) ; - ignore (CicUnification.fo_unif_mgu 0 term (C.Meta (earity - 1)) mgu) ; - let mgu = CicUnification.unwind mgu in -prerr_endline "Dopo l'unwind dell'mgu"; flush stderr ; - let mark = Array.make earity 1 in - let ueconclusion = - CicUnification.unwind_meta mgu mark econclusion - in + let subst1 = + CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse + in + let ueconclusion = CicUnification.apply_subst subst1 econclusion in prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ; flush stderr ; (* The conclusion of our elimination principle is *) @@ -489,50 +428,51 @@ flush stderr ; C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs | _ -> raise NotTheRightEliminatorShape in + let ty' = CicUnification.apply_subst subst1 ty in let eta_expanded_ty = -(*CSC: metasenv e ?????????????*) - List.fold_left (eta_expand metasenv ciccontext) ty fargs + List.fold_left (eta_expand metasenv ciccontext) ty' fargs in -(*CSC: 0????????*) prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ; - ignore (CicUnification.fo_unif_mgu 0 ueconclusion eta_expanded_ty mgu) ; -prerr_endline "Dopo la seconda unificazione" ; flush stdout ; - let mgu = CicUnification.unwind mgu in - print_endline "unwind"; flush stdout; - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. *) - let mgut = - let mark = Array.make (Array.length mgu) 1 in - Array.map - (CicUnification.unwind_meta_reducing mgu mark (Some emeta)) - mgut ; + let subst2 = +(*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite +da subst1!!!! Dovrei rimuoverle o sono innocue?*) + CicUnification.fo_unif + newmetasenv ciccontext ueconclusion eta_expanded_ty in - print_endline "unwind_array"; flush stdout; - let mgu' = Array.copy mgu in - let mgut' = CicUnification.list_of_array mgut in - print_endline "list"; flush stdout; - Array.iteri - (fun i ty -> -prerr_endline ("META " ^ string_of_int i ^ ": " ^ CicPp.ppterm mgu'.(i) ^ - " == " ^ CicPp.ppterm ty) ; flush stderr ; - let ty' = - CicTypeChecker.type_of_aux' mgut' ciccontext mgu'.(i) +prerr_endline "Dopo la seconda unificazione" ; flush stdout ; +prerr_endline "unwind"; flush stderr; + let in_subst_domain i = + let eq_to_i = function (j,_) -> i=j in + List.exists eq_to_i subst1 || + List.exists eq_to_i subst2 + in + (* When unwinding the META that corresponds to the elimination *) + (* predicate (which is emeta), we must also perform one-step *) + (* beta-reduction. *) + let apply_subst = + function t -> + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + subst2 (Some (emeta,List.length fargs)) t' + in + let newmetasenv' = + List.map (function (i,ty) -> i, apply_subst ty) newmetasenv + in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + classify_metas newmeta in_subst_domain apply_subst newmetasenv in - ignore (CicUnification.fo_unif_mgu 0 ty ty' mgu) - ) mgut ; - let mgu = CicUnification.unwind mgu in - let mgut = CicUnification.unwind_array mgu mgut in -prerr_endline "Dopo le unwind dell'mgut" ; flush stdout ; - let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in -prerr_endline "Dopo il fissaggio" ; flush stdout ; - let bo' = Cic.Appl (eliminator_ref::mgul') in + let arguments = + List.map apply_subst + (List.map (function (i,_) -> C.Meta i) newmetas) + in + let bo' = Cic.Appl (eliminator_ref::arguments) in prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ; - refine_meta metano bo' uninstantiatedmetas ; -prerr_endline "dopo refine meta" ; flush stdout ; - match uninstantiatedmetas with - (n,ty)::tl -> goal := Some (n,(context,ty)) - | [] -> goal := None +List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ; + refine_meta_with_brand_new_metasenv metano bo' + (new_uninstantiatedmetas@old_uninstantiatedmetas) ; + match new_uninstantiatedmetas with + [] -> goal := None + | (i,ty)::_ -> goal := Some (i,(context,ty)) ;; let elim_intros term = -- 2.39.2