From: Claudio Sacerdoti Coen Date: Mon, 29 Apr 2002 10:53:51 +0000 (+0000) Subject: * Bug fixed: Elim did not work for principles whose conclusion was just X-Git-Tag: V_0_3_0_debian_8~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ca6aaf6c6b4c5fc37ef61c56ed6fc9d81c76b626 * Bug fixed: Elim did not work for principles whose conclusion was just a META and not an application. * The old implementation of ElimIntros was misleading: It applied Intros only to the first goal. Removed. * A new implementation of ElimIntros (and of ApplyIntros) is partially provided, but unused. It requires the forthcoming new META definition and unification algorithm. --- diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index ac828a959..7781be6ae 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -162,6 +162,35 @@ let perforate context term ty = exception Fail of string;; +(* lambda_abstract newmeta ty *) +(* returns a triple [bo],[context],[ty'] where *) +(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) +(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) +(* So, lambda_abstract is the core of the implementation of *) +(* the Intros tactic. *) +let lambda_abstract newmeta ty = + let module C = Cic in + let rec collect_context = + function + C.Cast (te,_) -> collect_context te + | C.Prod (n,s,t) -> + let (ctx,ty,bo) = collect_context t in + let n' = + match n with + C.Name _ -> n +(*CSC: generatore di nomi? Chiedere il nome? *) + | C.Anonimous -> C.Name "fresh_name" + in + ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo)) + | C.LetIn (n,s,t) -> + let (ctx,ty,bo) = collect_context t in + ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo)) + | _ as t -> [], t, (C.Meta newmeta) + in + let revcontext,ty',bo = collect_context ty in + bo,(List.rev revcontext),ty' +;; + let intros () = let module C = Cic in let module R = CicReduction in @@ -176,25 +205,8 @@ let intros () = | Some (metano,(context,ty)) -> metano,context,ty in let newmeta = new_meta () in - let rec collect_context = - function - C.Cast (te,_) -> collect_context te - | C.Prod (n,s,t) -> - let (ctx,ty,bo) = collect_context t in - let n' = - match n with - C.Name _ -> n -(*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonimous -> C.Name "fresh_name" - in - ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> - let (ctx,ty,bo) = collect_context t in - ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo)) - | _ as t -> [], t, (C.Meta newmeta) - in - let revcontext',ty',bo' = collect_context ty in - let context'' = (List.rev revcontext') @ context in + let (bo',newcontext,ty') = lambda_abstract newmeta ty in + let context'' = newcontext @ context in refine_meta metano bo' [newmeta,ty'] ; goal := Some (newmeta,(context'',ty')) ;; @@ -226,9 +238,40 @@ let exact bo = raise (Fail "The type of the provided term is not the one expected.") ;; +(*CSC: The call to the Intros tactic is embedded inside the code of the *) +(*CSC: Elim tactic. Do we already need tacticals? *) (* 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. *) +(* head, a META environment in which there is new a META for each hypothesis,*) +(* a list of arguments for the new applications and the indexes of the first *) +(* and last new METAs introduced. The nth argument in the list of arguments *) +(* is the nth new META lambda-abstracted as much as possible. Hence, this *) +(* functions already provides the behaviour of Intros on the new goals. *) +let new_metasenv_for_apply_intros 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 newargument,newcontext,ty' = lambda_abstract newmeta s in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + res,(newmeta,ty')::newmetasenv,newargument::arguments,lastmeta + | t -> t,[],[],newmeta + in + 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,arguments,lastmeta) = aux newmeta ty in + res,newmetasenv,arguments,newmeta,lastmeta +;; + +(* Auxiliary function for apply: given a type (a backbone), it returns its *) +(* head, a META environment in which there is new a META for each hypothesis,*) +(* a list of arguments for the new applications and the indexes of the first *) +(* and last new METAs introduced. The nth argument in the list of arguments *) +(* is just the nth new META. *) let new_metasenv_for_apply ty = let module C = Cic in let module S = CicSubstitution in @@ -236,19 +279,21 @@ let new_metasenv_for_apply ty = 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 + let newargument = C.Meta newmeta in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + res,(newmeta,s)::newmetasenv,newargument::arguments,lastmeta + | t -> t,[],[],newmeta in 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 + let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in + res,newmetasenv,arguments,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 metasenv = List.fold_right @@ -285,7 +330,9 @@ let apply term = let ciccontext = cic_context_of_named_context context in 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 (consthead,newmetas,arguments,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 @@ -305,24 +352,14 @@ let apply term = 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) + let arguments' = List.map apply_subst arguments in + Cic.Appl (term::arguments') in refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing (new_uninstantiatedmetas@old_uninstantiatedmetas) ; -prerr_endline "QUI4" ; flush stderr ; ( match new_uninstantiatedmetas with [] -> goal := None | (i,ty)::_ -> goal := Some (i,(context,ty)) -) ; -List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas) -; prerr_endline "FATTO" ; flush stderr ; -List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ; -prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b)) -; prerr_endline "FATTO2" ; flush stderr ;; let eta_expand metasenv ciccontext t arg = @@ -376,7 +413,7 @@ exception NotAnInductiveTypeToEliminate;; exception NotTheRightEliminatorShape;; exception NoHypothesesFound;; -let elim term = +let elim_intros term = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in @@ -428,7 +465,7 @@ let elim term = let ety = T.type_of_aux' [] [] eliminator_ref in - let (econclusion,newmetas,newmeta,lastmeta) = + let (econclusion,newmetas,arguments,newmeta,lastmeta) = new_metasenv_for_apply ety in (* Here we assume that we have only one inductive hypothesis to *) @@ -454,7 +491,20 @@ flush stderr ; (* to refine the term. *) let emeta, fargs = match ueconclusion with +(*CSC: Code to be used for Apply *) C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs + | C.Meta emeta -> emeta,[] +(*CSC: Code to be used for ApplyIntros + C.Appl (he::fargs) -> + let rec find_head = + function + C.Meta emeta -> emeta + | C.Lambda (_,_,t) -> find_head t + | C.LetIn (_,_,t) -> find_head t + | _ ->raise NotTheRightEliminatorShape + in + find_head he,fargs +*) | _ -> raise NotTheRightEliminatorShape in let ty' = CicUnification.apply_subst subst1 ty in @@ -504,11 +554,8 @@ prerr_endline "unwind"; flush stderr; let old_uninstantiatedmetas,new_uninstantiatedmetas = classify_metas newmeta in_subst_domain apply_subst newmetasenv in - let arguments = - List.map apply_subst - (List.map (function (i,_) -> C.Meta i) newmetas) - in - let bo' = Cic.Appl (eliminator_ref::arguments) in + let arguments' = List.map apply_subst arguments in + let bo' = Cic.Appl (eliminator_ref::arguments') in prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ; 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' @@ -519,11 +566,6 @@ List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp | (i,ty)::_ -> goal := Some (i,(context,ty)) ;; -let elim_intros term = - elim term ; - intros () -;; - let reduction_tactic reduction_function term = let curi,metasenv,pbo,pty = match !proof with