(* *)
(******************************************************************************)
+(* $Id$ *)
(* The code of this module is derived from the code of CicReduction *)
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
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
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
(*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 ****)
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
| 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,
| 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 (CicReduction.whd context term) with
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