(* The code of this module is derived from the code of CicReduction *)
exception Impossible of int;;
-exception ReferenceToDefinition;;
-exception ReferenceToAxiom;;
+exception ReferenceToConstant;;
exception ReferenceToVariable;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception WrongUriToInductiveDefinition;;
exception RelToHiddenHypothesis;;
-(* syntactic_equality up to cookingsno for uris *)
-(* (which is often syntactically irrilevant) *)
-let syntactic_equality ~alpha_equivalence =
+let alpha_equivalence =
let module C = Cic in
let rec aux t t' =
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.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
+ UriManager.eq uri1 uri2 &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
| C.Cast (te,ty), C.Cast (te',ty') ->
aux te te' && aux ty ty'
- | C.Prod (n,s,t), C.Prod (n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
- | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
- | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ aux s s' && aux t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ aux s s' && aux t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ aux s s' && aux t t'
| C.Appl l, C.Appl l' ->
(try
List.fold_left2
(fun b t1 t2 -> b && aux t1 t2) true l l'
with
Invalid_argument _ -> false)
- | 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') ->
+ | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
+ UriManager.eq uri uri' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
+ UriManager.eq uri uri' && i = i' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutConstruct (uri,i,j,exp_named_subst1),
+ C.MutConstruct (uri',i',j',exp_named_subst2) ->
+ UriManager.eq uri uri' && i = i' && j = j' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
UriManager.eq sp sp' && i = i' &&
aux outt outt' && aux t t' &&
(try
i = i' &&
(try
List.fold_left2
- (fun b (name,i,ty,bo) (name',i',ty',bo') ->
- b && (alpha_equivalence || name = name') && i = i' &&
- aux ty ty' && aux bo bo') true fl fl'
+ (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+ b && i = i' && aux ty ty' && aux bo bo'
+ ) true fl fl'
with
Invalid_argument _ -> false)
| C.CoFix (i,fl), C.CoFix (i',fl') ->
i = i' &&
(try
List.fold_left2
- (fun b (name,ty,bo) (name',ty',bo') ->
- b && (alpha_equivalence || name = name') &&
- aux ty ty' && aux bo bo') true fl fl'
+ (fun b (_,ty,bo) (_,ty',bo') ->
+ b && aux ty ty' && aux bo bo'
+ ) true fl fl'
with
Invalid_argument _ -> false)
- | _,_ -> false
- in
- aux
+ | _,_ -> false (* we already know that t != t' *)
+ and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
+ try
+ List.fold_left2
+ (fun b (uri1,t1) (uri2,t2) ->
+ b && UriManager.eq uri1 uri2 && aux t1 t2
+ ) true exp_named_subst1 exp_named_subst2
+ with
+ Invalid_argument _ -> false
+ in
+ aux
;;
(* "textual" replacement of a subterm with another one *)
function
t when (equality t what) -> with_what
| C.Rel _ as t -> t
- | C.Var _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
| C.Meta _ as t -> t
| C.Sort _ as t -> t
| C.Implicit as t -> t
(match List.map aux l with
(C.Appl l')::tl -> C.Appl (l'@tl)
| l' -> C.Appl l')
- | C.Const _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,aux outt, aux t,
- List.map aux pl)
+ | C.Const (uri,exp_named_subst) ->
+ C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutInd (uri,i,exp_named_subst) ->
+ C.MutInd
+ (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ C.MutConstruct
+ (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
| C.Fix (i,fl) ->
let substitutedfl =
List.map
function
t when (equality t what) -> S.lift (k-1) with_what
| C.Rel n as t -> t
- | C.Var _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ 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 ->
let l' =
List.map
| _ as he' -> C.Appl (he'::tl')
end
| C.Appl _ -> assert false
- | C.Const _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t,
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k what outt, substaux k what t,
List.map (substaux k what) pl)
| C.Fix (i,fl) ->
let len = List.length fl in
| 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.Axiom _ -> raise ReferenceToAxiom
+ | 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
+ C.Constant _ -> raise ReferenceToConstant
| 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 context l body
+ | 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,_,_) ->
+ (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 *)
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 context l body
- | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduceaux context l body
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- | 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) ->
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ (reduceaux context l
+ (CicSubstitution.subst_vars exp_named_subst' body))
+ | 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
+ (CicSubstitution.subst_vars exp_named_subst' body))
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ 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 ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
| t -> t
in
(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) =
+ 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
- and num_ingredients =
- List.fold_right
- (fun (k,l) i ->
- if k < cookingsno then i + List.length l else i
- ) ingredients 0
- in
- (arity,r,num_ingredients)
+ C.InductiveDefinition (tl,_,r) ->
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
- let num_to_eat = r + num_ingredients in
- let rec eat_first =
- function
- (0,l) -> l
- | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
- | _ -> raise (Impossible 5)
- in
- eat_first (num_to_eat,tl)
+ let rec eat_first =
+ function
+ (0,l) -> l
+ | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+ | _ -> raise (Impossible 5)
+ in
+ eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
| C.Cast _ | C.Implicit ->
let term' = reduceaux context [] term in
let pl' = List.map (reduceaux context []) pl in
let res =
- C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ C.MutCase (mutind,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
C.CoFix (i, fl')
in
if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+ List.map (function uri,t -> uri,reduceaux context [] t)
in
reduceaux context []
;;
| 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.Axiom _ -> raise ReferenceToAxiom
- | 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 context l body
- )
+ | 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
+ C.Constant _ -> raise ReferenceToConstant
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | 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,_,_) ->
+ 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
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,_,_) ->
- begin
- try
- (**** Step 2 ****)
- let res,constant_args =
- let rec aux rev_constant_args l =
- function
- C.Lambda (name,s,t) as t' ->
- begin
- match l with
- [] -> raise WrongShape
- | he::tl ->
- (* when name is Anonimous the substitution should be *)
- (* superfluous *)
- aux (he::rev_constant_args) tl (S.subst he t)
- 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
- 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
- in
- (**** Step 3 ****)
- let term_to_fold =
- match constant_args with
- [] -> C.Const (uri,cookingsno)
- | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ begin
+ try
+ (**** Step 2 ****)
+ let res,constant_args =
+ let rec aux rev_constant_args l =
+ function
+ C.Lambda (name,s,t) as t' ->
+ begin
+ match l with
+ [] -> raise WrongShape
+ | he::tl ->
+ (* when name is Anonimous the substitution should *)
+ (* be superfluous *)
+ aux (he::rev_constant_args) tl (S.subst he t)
+ 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
+ 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 (CicSubstitution.subst_vars exp_named_subst' body)
in
- 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 context l body
- | AlreadySimplified ->
- (* If we performed delta-reduction, we would find a Fix *)
- (* not applied to a constructor. So, we refuse to perform *)
- (* delta-reduction. *)
- if l = [] then
- t
- else
- C.Appl (t::l)
- end
- | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+ (**** Step 3 ****)
+ let term_to_fold =
+ match constant_args with
+ [] -> C.Const (uri,exp_named_subst')
+ | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
+ in
+ 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 context l
+ (CicSubstitution.subst_vars exp_named_subst' body)
+ | AlreadySimplified ->
+ (* If we performed delta-reduction, we would find a Fix *)
+ (* not applied to a constructor. So, we refuse to perform *)
+ (* delta-reduction. *)
+ let t' = C.Const (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ end
+ | 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,_,_) 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) ->
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ 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) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
| t -> t
in
(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) =
+ 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
- and num_ingredients =
- List.fold_right
- (fun (k,l) i ->
- if k < cookingsno then i + List.length l else i
- ) ingredients 0
- in
- (arity,r,num_ingredients)
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
- let num_to_eat = r + num_ingredients in
- let rec eat_first =
- function
- (0,l) -> l
- | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
- | _ -> raise (Impossible 5)
- in
- eat_first (num_to_eat,tl)
+ let rec eat_first =
+ function
+ (0,l) -> l
+ | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+ | _ -> raise (Impossible 5)
+ in
+ eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
| C.Cast _ | C.Implicit ->
let term' = reduceaux context [] term in
let pl' = List.map (reduceaux context []) pl in
let res =
- C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ C.MutCase (mutind,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
C.CoFix (i, fl')
in
if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+ List.map (function uri,t -> uri,reduceaux context [] t)
in
reduceaux context []
;;
projects / helm.git / blobdiff