X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=0dc4ce4ee3e617a1b1cb6a98efa6dc68db8e922b;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=a9b8b55001a47c5ee3390b9556c90f1c4ec642c8;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index a9b8b5500..0dc4ce4ee 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -33,6 +33,7 @@ (* *) (******************************************************************************) +(* $Id$ *) (* The code of this module is derived from the code of CicReduction *) @@ -127,7 +128,7 @@ let replace ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) + if equality what t then with_what else find_image_aux (tl1,tl2) | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength in find_image_aux (what,with_what) @@ -190,7 +191,7 @@ let replace_lifting ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) + if equality what t then with_what else find_image_aux (tl1,tl2) | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength in find_image_aux (what,with_what) @@ -206,7 +207,7 @@ let replace_lifting ~equality ~what ~with_what ~where = List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> + | C.Meta (i, l) -> let l' = List.map (function @@ -288,7 +289,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = function [],[] -> raise Not_found | what::tl1,with_what::tl2 -> - if equality t what then with_what else find_image_aux (tl1,tl2) + if equality what t then with_what else find_image_aux (tl1,tl2) | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength in find_image_aux (what,with_what) @@ -298,14 +299,14 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = S.lift (k-1) (find_image t) with Not_found -> match t with - C.Rel n as t -> + C.Rel n -> if n < k then C.Rel n else C.Rel (n + nnn) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> uri,substaux k t) exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> + | C.Meta (i, l) -> let l' = List.map (function @@ -450,7 +451,7 @@ let reduce context = in let t' = C.MutInd (uri,i,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) as t -> + | C.MutConstruct (uri,i,j,exp_named_subst) -> let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in @@ -459,10 +460,7 @@ let reduce context = | C.MutCase (mutind,i,outtype,term,pl) -> let decofix = function - C.CoFix (i,fl) as t -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in + C.CoFix (i,fl) -> let (_,_,body) = List.nth fl i in let body' = let counter = ref (List.length fl) in @@ -473,9 +471,6 @@ let reduce context = in reduceaux context [] body' | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl - in let (_,_,body) = List.nth fl i in let body' = let counter = ref (List.length fl) in @@ -584,17 +579,19 @@ exception AlreadySimplified;; (* Takes a well-typed term and *) (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) (* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *) -(* w.r.t. zero or more variables and if the Fix can be reductaed, than it *) +(* w.r.t. zero or more variables and if the Fix can be reductaed, than it*) (* is reduced, the delta-reduction is succesfull and the whole algorithm *) -(* is applied again to the new redex; Step 3) is applied to the result *) +(* is applied again to the new redex; Step 3.1) is applied to the result *) (* of the recursive simplification. Otherwise, if the Fix can not be *) (* reduced, than the delta-reductions fails and the delta-redex is *) (* not reduced. Otherwise, if the delta-residual is not the *) -(* lambda-abstraction of a Fix, then it is reduced and the result is *) -(* directly returned, without performing step 3). *) -(* 3) Folds the application of the constant to the arguments that did not *) +(* lambda-abstraction of a Fix, then it performs step 3.2). *) +(* 3.1) Folds the application of the constant to the arguments that did not *) (* change in every iteration, i.e. to the actual arguments for the *) (* lambda-abstractions that precede the Fix. *) +(* 3.2) Computes the head beta-zeta normal form of the term. Then it tries *) +(* reductions. If the reduction cannot be performed, it returns the *) +(* original term (not the head beta-zeta normal form of the definiendum) *) (*CSC: It does not perform simplification in a Case *) let simpl context = @@ -606,14 +603,8 @@ let simpl context = let module S = CicSubstitution in function C.Rel n as t -> - (try - match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def (bo,_)) -> - try_delta_expansion context l t (S.lift n bo) - | None -> raise RelToHiddenHypothesis - with - Failure _ -> assert false) + (* we never perform delta expansion automatically *) + if l = [] then t else C.Appl (t::l) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst @@ -634,7 +625,7 @@ let simpl context = | C.Sort _ as t -> t (* l should be empty *) | C.Implicit _ as t -> t | C.Cast (te,ty) -> - C.Cast (reduceaux context l te, reduceaux context l ty) + C.Cast (reduceaux context l te, reduceaux context [] ty) | C.Prod (name,s,t) -> assert (l = []) ; C.Prod (name, @@ -687,9 +678,7 @@ let simpl context = | C.MutCase (mutind,i,outtype,term,pl) -> let decofix = function - C.CoFix (i,fl) as t -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in + C.CoFix (i,fl) -> let (_,_,body) = List.nth fl i in let body' = let counter = ref (List.length fl) in @@ -700,21 +689,19 @@ let simpl context = in reduceaux context [] body' | C.Appl (C.CoFix (i,fl) :: tl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - let tl' = List.map (reduceaux context []) tl in - reduceaux context tl body' + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux context tl' body' | t -> t in - (match decofix (reduceaux context [] term) with + (match decofix (CicReduction.whd context term) with C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = @@ -808,7 +795,7 @@ let simpl context = let res,constant_args = let rec aux rev_constant_args l = function - C.Lambda (name,s,t) as t' -> + C.Lambda (name,s,t) -> begin match l with [] -> raise WrongShape @@ -819,11 +806,7 @@ let simpl context = end | C.LetIn (_,s,t) -> aux rev_constant_args l (S.subst s t) - | C.Fix (i,fl) as t -> - let tys = - List.map (function (name,_,ty,_) -> - Some (C.Name name, C.Decl ty)) fl - in + | C.Fix (i,fl) -> let (_,recindex,_,body) = List.nth fl i in let recparam = try @@ -851,7 +834,7 @@ let simpl context = in aux [] l body in - (**** Step 3 ****) + (**** Step 3.1 ****) let term_to_fold, delta_expanded_term_to_fold = match constant_args with [] -> term,body @@ -863,9 +846,28 @@ let simpl context = replace (=) [simplified_term_to_fold] [term_to_fold] res with WrongShape -> - (* The constant does not unfold to a Fix lambda-abstracted *) - (* w.r.t. zero or more variables. We just perform reduction.*) - reduceaux context l body + (**** Step 3.2 ****) + let rec aux l = + function + C.Lambda (name,s,t) -> + (match l with + [] -> raise AlreadySimplified + | he::tl -> + (* when name is Anonimous the substitution should *) + (* be superfluous *) + aux tl (S.subst he t)) + | C.LetIn (_,s,t) -> aux l (S.subst s t) + | t -> + let simplified = reduceaux context l t in + if t = simplified then + raise AlreadySimplified + else + simplified + in + (try aux l body + with + AlreadySimplified -> + if l = [] then term else C.Appl (term::l)) | AlreadySimplified -> (* If we performed delta-reduction, we would find a Fix *) (* not applied to a constructor. So, we refuse to perform *) @@ -876,7 +878,8 @@ let simpl context = ;; let unfold ?what context where = - let first_is_the_expandable_head_of_second t1 t2 = + let contextlen = List.length context in + let first_is_the_expandable_head_of_second context' t1 t2 = match t1,t2 with Cic.Const (uri,_), Cic.Const (uri',_) | Cic.Var (uri,_), Cic.Var (uri',_) @@ -884,17 +887,21 @@ let unfold ?what context where = | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri' | Cic.Const _, _ | Cic.Var _, _ -> false + | Cic.Rel n, Cic.Rel m + | Cic.Rel n, Cic.Appl (Cic.Rel m::_) -> + n + (List.length context' - contextlen) = m + | Cic.Rel _, _ -> false | _,_ -> raise (ProofEngineTypes.Fail - "The term to unfold is neither a constant nor a variable") + (lazy "The term to unfold is not a constant, a variable or a bound variable ")) in let appl he tl = if tl = [] then he else Cic.Appl (he::tl) in let cannot_delta_expand t = raise (ProofEngineTypes.Fail - ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in + (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in let rec hd_delta_beta context tl = function Cic.Rel n as t -> @@ -933,19 +940,26 @@ let unfold ?what context where = | Cic.Appl (he::tl) -> hd_delta_beta context tl he | t -> cannot_delta_expand t in - let context, where = + let context_and_matched_term_list = match what with - None -> context, where + None -> [context, where] | Some what -> - try + let res = ProofEngineHelpers.locate_in_term ~equality:first_is_the_expandable_head_of_second what ~where context - with - ProofEngineHelpers.TermNotFound -> + in + if res = [] then raise (ProofEngineTypes.Fail - ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)) + (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))) + else + res in - hd_delta_beta context [] where + let reduced_terms = + List.map + (function (context,where) -> hd_delta_beta context [] where) + context_and_matched_term_list in + let whats = List.map snd context_and_matched_term_list in + replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where ;;