(* *)
(******************************************************************************)
+(* $Id$ *)
(* The code of this module is derived from the code of CicReduction *)
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)
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)
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
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)
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
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (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))
)
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.Constant (_,Some body,_,_) ->
+ 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
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
| 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
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
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
match o with
- C.InductiveDefinition (tl,_,r) ->
+ C.InductiveDefinition (tl,_,r,_) ->
let (_,_,arity,_) = List.nth tl i in
(arity,r)
| _ -> raise WrongUriToInductiveDefinition
(* 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 =
(* reduceaux is equal to the reduceaux locally defined inside *)
(* reduce, but for the const case. *)
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
- )
+ (* 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
in
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (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.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,
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.Constant (_,Some body,_,_) ->
- try_delta_expansion l
+ 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) ->
| 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
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) =
- let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
match o with
- C.InductiveDefinition (tl,ingredients,r) ->
+ C.InductiveDefinition (tl,ingredients,r,_) ->
let (_,_,arity,_) = List.nth tl i in
(arity,r)
| _ -> raise WrongUriToInductiveDefinition
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
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
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
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
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 *)
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
+;;
projects / helm.git / blobdiff