X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=f8782b7aec13db70083d025a44258d1416d0cf21;hb=1bcae23ef41ad2110426eebd97671d27d09213a3;hp=a9b8b55001a47c5ee3390b9556c90f1c4ec642c8;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index a9b8b5500..f8782b7ae 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -127,7 +127,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 +190,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) @@ -288,7 +288,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) @@ -583,8 +583,11 @@ exception AlreadySimplified;; (* Takes a well-typed term and *) (* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) +(* Zeta-reduction is performed if and only if the simplified form of its *) +(* definiendum (applied to the actual arguments) is different from the *) +(* non-simplified form. *) (* 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 *) (* of the recursive simplification. Otherwise, if the Fix can not be *) @@ -598,6 +601,14 @@ exception AlreadySimplified;; (*CSC: It does not perform simplification in a Case *) let simpl context = + let mk_appl t l = + if l = [] then + t + else + match t with + | Cic.Appl l' -> Cic.Appl (l'@l) + | _ -> Cic.Appl (t::l) + in (* reduceaux is equal to the reduceaux locally defined inside *) (* reduce, but for the const case. *) (**** Step 1 ****) @@ -610,7 +621,13 @@ let simpl context = 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) + let lifted_bo = S.lift n bo in + let applied_lifted_bo = mk_appl lifted_bo l in + let simplified = try_delta_expansion context l t lifted_bo in + if simplified = applied_lifted_bo then + if l = [] then t else C.Appl (t::l) + else + simplified | None -> raise RelToHiddenHypothesis with Failure _ -> assert false) @@ -714,7 +731,7 @@ let simpl context = 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) = @@ -876,7 +893,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,10 +902,14 @@ 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") + "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 @@ -933,19 +955,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)) + 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 ;;