-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception WrongUriToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant) *)
+let rec syntactic_equality t t' =
+ let module C = Cic in
+ if t = t' then true
+ else
+ match t,t' with
+ C.Rel _, C.Rel _
+ | C.Var _, C.Var _
+ | C.Meta _, C.Meta _
+ | C.Sort _, C.Sort _
+ | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ | C.Cast (te,ty), C.Cast (te',ty') ->
+ syntactic_equality te te' &&
+ syntactic_equality ty ty'
+ | C.Prod (n,s,t), C.Prod (n',s',t') ->
+ n = n' &&
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
+ n = n' &&
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
+ n = n' &&
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Appl l, C.Appl l' ->
+ List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+ | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
+ | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
+ UriManager.eq uri uri' && i = i'
+ | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+ UriManager.eq uri uri' && i = i' && j = j'
+ | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ UriManager.eq sp sp' && i = i' &&
+ syntactic_equality outt outt' &&
+ syntactic_equality t t' &&
+ List.fold_left2
+ (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+ | C.Fix (i,fl), C.Fix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (name,i,ty,bo) (name',i',ty',bo') ->
+ b && name = name' && i = i' &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | C.CoFix (i,fl), C.CoFix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (name,ty,bo) (name',ty',bo') ->
+ b && name = name' &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | _,_ -> false
+;;
(* "textual" replacement of a subterm with another one *)
-let replace ~what ~with_what ~where =
+let replace ~equality ~what ~with_what ~where =
let module C = Cic in
let rec aux =
function
- t when t = what -> with_what
+ t when (equality t what) -> with_what
| C.Rel _ as t -> t
| C.Var _ as t -> t
| C.Meta _ as t -> t
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
| C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
+ | C.Appl l ->
+ (* Invariant enforced: no application of an application *)
+ (match List.map aux l with
+ (C.Appl l')::tl -> C.Appl (l'@tl)
+ | l' -> C.Appl l')
| C.Const _ as t -> t
- | C.Abst _ as t -> t
| C.MutInd _ as t -> t
| C.MutConstruct _ as t -> t
| C.MutCase (sp,cookingsno,i,outt,t,pl) ->
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
-let reduce =
- let rec reduceaux l =
+let reduce context =
+ let rec reduceaux context l =
let module C = Cic in
let module S = CicSubstitution in
function
- C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+ 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)
+ | None -> raise RelToHiddenHypothesis
+ )
| C.Var uri as t ->
(match CicEnvironment.get_cooked_obj uri 0 with
C.Definition _ -> raise ReferenceToDefinition
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
| C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
- | C.Variable (_,Some body,_) -> reduceaux l body
+ | C.Variable (_,Some body,_) -> reduceaux context l 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.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
+ | C.Cast (te,ty) ->
+ C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
assert (l = []) ;
- C.Prod (name, reduceaux [] s, reduceaux [] t)
+ C.Prod (name,
+ reduceaux context [] s,
+ reduceaux ((Some (name,C.Decl s))::context) [] t)
| C.Lambda (name,s,t) ->
(match l with
- [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
- | he::tl -> reduceaux tl (S.subst he t)
+ [] ->
+ C.Lambda (name,
+ reduceaux context [] s,
+ reduceaux ((Some (name,C.Decl s))::context) [] t)
+ | he::tl -> reduceaux context tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
- | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+ | C.LetIn (n,s,t) ->
+ reduceaux context l (S.subst (reduceaux context [] s) t)
| C.Appl (he::tl) ->
- let tl' = List.map (reduceaux []) tl in
- reduceaux (tl'@l) he
+ let tl' = List.map (reduceaux context []) tl in
+ reduceaux context (tl'@l) he
| C.Appl [] -> raise (Impossible 1)
| C.Const (uri,cookingsno) as t ->
(match CicEnvironment.get_cooked_obj uri cookingsno with
- C.Definition (_,body,_,_) -> reduceaux l body
+ C.Definition (_,body,_,_) -> reduceaux context l body
| C.Axiom _ -> if l = [] then t else C.Appl (t::l)
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduceaux l body
+ | C.CurrentProof (_,_,body,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | C.Abst _ as t -> t (*CSC l should be empty ????? *)
| C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
- 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
- reduceaux [] body'
+ 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
+ reduceaux (tys@context) [] body'
| C.Appl (C.CoFix (i,fl) :: tl) ->
- 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 []) tl in
- reduceaux tl body'
+ 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 (tys@context) tl' body'
| t -> t
in
- (match decofix (reduceaux [] term) with
- C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+ (match decofix (reduceaux context [] term) with
+ C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
let (arity, r, num_ingredients) =
match CicEnvironment.get_obj mutind with
in
eat_first (num_to_eat,tl)
in
- reduceaux (ts@l) (List.nth pl (j-1))
- | C.Abst _ | C.Cast _ | C.Implicit ->
+ reduceaux context (ts@l) (List.nth pl (j-1))
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
- let outtype' = reduceaux [] outtype in
- let term' = reduceaux [] term in
- let pl' = List.map (reduceaux []) pl in
+ let outtype' = reduceaux context [] outtype in
+ let term' = reduceaux context [] term in
+ let pl' = List.map (reduceaux context []) pl in
let res =
C.MutCase (mutind,cookingsno,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let t' () =
- let fl' =
- List.map
- (function (n,recindex,ty,bo) ->
- (n,recindex,reduceaux [] ty, reduceaux [] bo)
- ) fl
- in
- C.Fix (i, fl')
+ let tys =
+ List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
in
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- Some (List.nth l recindex)
- with
- _ -> None
+ let t' () =
+ let fl' =
+ List.map
+ (function (n,recindex,ty,bo) ->
+ (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+ ) fl
in
- (match recparam with
- Some recparam ->
- (match reduceaux [] recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
- fl
- body
- in
- (* Possible optimization: substituting whd recparam in l *)
- reduceaux l body'
- | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
- )
- | None -> if l = [] then t' () else C.Appl ((t' ())::l)
- )
- | C.CoFix (i,fl) ->
- let t' =
- let fl' =
- List.map
- (function (n,ty,bo) ->
- (n,reduceaux [] ty, reduceaux [] bo)
- ) fl
+ C.Fix (i, fl')
in
- C.CoFix (i, fl')
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (List.nth l recindex)
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduceaux context [] recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ (* Possible optimization: substituting whd recparam in l*)
+ reduceaux context l body'
+ | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | C.CoFix (i,fl) ->
+ let tys =
+ List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
in
- if l = [] then t' else C.Appl (t'::l)
+ let t' =
+ let fl' =
+ List.map
+ (function (n,ty,bo) ->
+ (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+ ) fl
+ in
+ C.CoFix (i, fl')
+ in
+ if l = [] then t' else C.Appl (t'::l)
in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
- reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
+ reduceaux context []
;;
exception WrongShape;;
exception AlreadySimplified;;
-exception WhatShouldIDo;;
(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
(* change in every iteration, i.e. to the actual arguments for the *)
(* lambda-abstractions that precede the Fix. *)
(*CSC: It does not perform simplification in a Case *)
-let simpl =
+let simpl context =
(* reduceaux is equal to the reduceaux locally defined inside *)
(*reduce, but for the const case. *)
(**** Step 1 ****)
- let rec reduceaux l =
+ let rec reduceaux context l =
let module C = Cic in
let module S = CicSubstitution in
function
- C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+ 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)
+ | None -> raise RelToHiddenHypothesis
+ )
| C.Var uri as t ->
(match CicEnvironment.get_cooked_obj uri 0 with
C.Definition _ -> raise ReferenceToDefinition
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
| C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
- | C.Variable (_,Some body,_) -> reduceaux l body
+ | C.Variable (_,Some body,_) -> reduceaux context l 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.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
+ | C.Cast (te,ty) ->
+ C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
assert (l = []) ;
- C.Prod (name, reduceaux [] s, reduceaux [] t)
+ C.Prod (name,
+ reduceaux context [] s,
+ reduceaux ((Some (name,C.Decl s))::context) [] t)
| C.Lambda (name,s,t) ->
(match l with
- [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
- | he::tl -> reduceaux tl (S.subst he t)
+ [] ->
+ C.Lambda (name,
+ reduceaux context [] s,
+ reduceaux ((Some (name,C.Decl s))::context) [] t)
+ | he::tl -> reduceaux context tl (S.subst he t)
(* when name is Anonimous the substitution should be superfluous *)
)
- | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+ | C.LetIn (n,s,t) ->
+ reduceaux context l (S.subst (reduceaux context [] s) t)
| C.Appl (he::tl) ->
- let tl' = List.map (reduceaux []) tl in
- reduceaux (tl'@l) he
+ let tl' = List.map (reduceaux context []) tl in
+ reduceaux context (tl'@l) he
| C.Appl [] -> raise (Impossible 1)
| C.Const (uri,cookingsno) as t ->
(match CicEnvironment.get_cooked_obj uri cookingsno with
(* superfluous *)
aux (he::rev_constant_args) tl (S.subst he t)
end
- | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
+ | C.LetIn (_,s,t) ->
+ aux rev_constant_args l (S.subst s t)
| C.Fix (i,fl) as t ->
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- List.nth l recindex
- with
- _ -> raise AlreadySimplified
- in
- (match CicReduction.whd recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (function _ ->
- decr counter ; S.subst (C.Fix (!counter,fl))
- ) fl body
- in
- (* Possible optimization: substituting whd *)
- (* recparam in l *)
- reduceaux l body', List.rev rev_constant_args
- | _ -> raise AlreadySimplified
- )
+ let tys =
+ List.map (function (name,_,ty,_) ->
+ Some (C.Name name, C.Decl ty)) fl
+ in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ List.nth l recindex
+ with
+ _ -> raise AlreadySimplified
+ in
+ (match CicReduction.whd context recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (function _ ->
+ decr counter ; S.subst (C.Fix (!counter,fl))
+ ) fl body
+ in
+ (* Possible optimization: substituting whd *)
+ (* recparam in l *)
+ reduceaux (tys@context) l body',
+ List.rev rev_constant_args
+ | _ -> raise AlreadySimplified
+ )
| _ -> raise WrongShape
in
aux [] l body
[] -> C.Const (uri,cookingsno)
| _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
in
- let reduced_term_to_fold = reduce term_to_fold in
-prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
-prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
- replace reduced_term_to_fold term_to_fold res
+ let reduced_term_to_fold = reduce context term_to_fold in
+ replace (=) reduced_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 l body
+ reduceaux context l body
| AlreadySimplified ->
(* If we performed delta-reduction, we would find a Fix *)
(* not applied to a constructor. So, we refuse to perform *)
end
| C.Axiom _ -> if l = [] then t else C.Appl (t::l)
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduceaux l body
+ | C.CurrentProof (_,_,body,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
- | C.Abst _ as t -> t (*CSC l should be empty ????? *)
| C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
| C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
- 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
- reduceaux [] body'
+ 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
+ reduceaux (tys@context) [] body'
| C.Appl (C.CoFix (i,fl) :: tl) ->
- 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 []) tl in
- reduceaux tl body'
+ 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 (tys@context) tl body'
| t -> t
in
- (match decofix (reduceaux [] term) with
- C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+ (match decofix (reduceaux context [] term) with
+ C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
let (arity, r, num_ingredients) =
match CicEnvironment.get_obj mutind with
in
eat_first (num_to_eat,tl)
in
- reduceaux (ts@l) (List.nth pl (j-1))
- | C.Abst _ | C.Cast _ | C.Implicit ->
+ reduceaux context (ts@l) (List.nth pl (j-1))
+ | C.Cast _ | C.Implicit ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
- let outtype' = reduceaux [] outtype in
- let term' = reduceaux [] term in
- let pl' = List.map (reduceaux []) pl in
+ let outtype' = reduceaux context [] outtype in
+ let term' = reduceaux context [] term in
+ let pl' = List.map (reduceaux context []) pl in
let res =
C.MutCase (mutind,cookingsno,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let t' () =
- let fl' =
- List.map
- (function (n,recindex,ty,bo) ->
- (n,recindex,reduceaux [] ty, reduceaux [] bo)
- ) fl
- in
- C.Fix (i, fl')
+ let tys =
+ List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
in
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- Some (List.nth l recindex)
- with
- _ -> None
+ let t' () =
+ let fl' =
+ List.map
+ (function (n,recindex,ty,bo) ->
+ (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+ ) fl
in
- (match recparam with
- Some recparam ->
- (match reduceaux [] recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
- fl
- body
- in
- (* Possible optimization: substituting whd recparam in l *)
- reduceaux l body'
- | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
- )
- | None -> if l = [] then t' () else C.Appl ((t' ())::l)
- )
- | C.CoFix (i,fl) ->
- let t' =
- let fl' =
- List.map
- (function (n,ty,bo) ->
- (n,reduceaux [] ty, reduceaux [] bo)
- ) fl
+ C.Fix (i, fl')
in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (List.nth l recindex)
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduceaux context [] recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ (* Possible optimization: substituting whd recparam in l*)
+ reduceaux context l body'
+ | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | C.CoFix (i,fl) ->
+ let tys =
+ List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ in
+ let t' =
+ let fl' =
+ List.map
+ (function (n,ty,bo) ->
+ (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+ ) fl
+ in
C.CoFix (i, fl')
in
- if l = [] then t' else C.Appl (t'::l)
+ if l = [] then t' else C.Appl (t'::l)
in
- reduceaux []
+ reduceaux context []
;;