X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=62c2adab57e2e9f34e04c7ca1fff6c50fa9d828b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c70be1fb736b61b4da38d15c491f2e5d77579f18;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index c70be1fb7..62c2adab5 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) @@ -142,7 +142,7 @@ let replace ~equality ~what ~with_what ~where = C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) | C.Meta _ -> t | C.Sort _ -> t - | C.Implicit 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) @@ -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) @@ -216,7 +216,7 @@ let replace_lifting ~equality ~what ~with_what ~where = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) | C.Prod (n,s,t) -> C.Prod @@ -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) @@ -315,7 +315,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) @@ -382,27 +382,28 @@ let reduce context = C.Rel n as t -> (match List.nth context (n-1) with Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) + | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo) | None -> raise RelToHiddenHypothesis ) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (match CicEnvironment.get_obj uri with + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> + | C.Variable (_,None,_,_,_) -> let t' = C.Var (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,Some body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (reduceaux context l te, reduceaux context l ty) | C.Prod (name,s,t) -> @@ -429,15 +430,16 @@ let reduce context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.Constant (_,Some body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) - | C.Constant (_,None,_,_) -> + | C.Constant (_,None,_,_,_) -> let t' = C.Const (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> + | C.CurrentProof (_,_,body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition @@ -490,11 +492,12 @@ let reduce context = C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,_,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in + match o with + C.InductiveDefinition (tl,_,r,_) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) + | _ -> raise WrongUriToInductiveDefinition in let ts = let rec eat_first = @@ -506,7 +509,7 @@ let reduce context = eat_first (r,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in @@ -581,19 +584,30 @@ 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 reduced, 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 = + 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 ****) @@ -602,30 +616,33 @@ let simpl context = let module S = CicSubstitution in function C.Rel n as t -> - (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 l t (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) + (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) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (match CicEnvironment.get_obj uri with + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> + | C.Variable (_,None,_,_,_) -> let t' = C.Var (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,Some body,_,_,_) -> reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body) ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (reduceaux context l te, reduceaux context l ty) | C.Prod (name,s,t) -> @@ -652,16 +669,17 @@ let simpl context = let exp_named_subst' = reduceaux_exp_named_subst context l exp_named_subst in - (match CicEnvironment.get_obj uri with - C.Constant (_,Some body,_,_) -> - try_delta_expansion l + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.Constant (_,Some body,_,_,_) -> + try_delta_expansion context l (C.Const (uri,exp_named_subst')) (CicSubstitution.subst_vars exp_named_subst' body) - | C.Constant (_,None,_,_) -> + | C.Constant (_,None,_,_,_) -> let t' = C.Const (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body + | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) | C.MutInd (uri,i,exp_named_subst) -> @@ -706,15 +724,16 @@ 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) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,ingredients,r) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in + match o with + C.InductiveDefinition (tl,ingredients,r,_) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) + | _ -> raise WrongUriToInductiveDefinition in let ts = let rec eat_first = @@ -726,7 +745,7 @@ let simpl context = eat_first (r,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in @@ -792,7 +811,7 @@ let simpl context = and reduceaux_exp_named_subst context l = List.map (function uri,t -> uri,reduceaux context [] t) (**** Step 2 ****) - and try_delta_expansion l term body = + and try_delta_expansion context l term body = let module C = Cic in let module S = CicSubstitution in try @@ -842,7 +861,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 @@ -854,9 +873,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 *) @@ -865,3 +903,90 @@ let simpl context = in reduceaux context [] ;; + +let unfold ?what context where = + 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',_) + | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_) + | 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 + (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 + (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in + let rec hd_delta_beta context tl = + function + Cic.Rel n as t -> + (try + match List.nth context (n-1) with + Some (_,Cic.Decl _) -> cannot_delta_expand t + | Some (_,Cic.Def (bo,_)) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.lift n bo) tl) + | None -> raise RelToHiddenHypothesis + with + Failure _ -> assert false) + | Cic.Const (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | Cic.Var (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant _ -> raise ReferenceToConstant + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | Cic.Variable (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t + ) + | Cic.Appl [] -> assert false + | Cic.Appl (he::tl) -> hd_delta_beta context tl he + | t -> cannot_delta_expand t + in + let context_and_matched_term_list = + match what with + None -> [context, where] + | Some what -> + let res = + ProofEngineHelpers.locate_in_term + ~equality:first_is_the_expandable_head_of_second + what ~where context + in + if res = [] then + raise + (ProofEngineTypes.Fail + (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))) + else + res + in + 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 +;;