(* syntactic_equality up to cookingsno for uris *)
(* (which is often syntactically irrilevant) *)
-let rec syntactic_equality t t' =
+let syntactic_equality ~alpha_equivalence =
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' &&
+ 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.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.Appl l, C.Appl l' ->
+ (try
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
+ (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') ->
+ UriManager.eq sp sp' && i = i' &&
+ aux outt outt' && aux t t' &&
+ (try
+ List.fold_left2
+ (fun b t1 t2 -> b && aux t1 t2) true pl pl'
+ with
+ Invalid_argument _ -> false)
+ | C.Fix (i,fl), C.Fix (i',fl') ->
+ 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'
+ 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'
+ with
+ Invalid_argument _ -> false)
+ | _,_ -> false
+ in
+ aux
;;
(* "textual" replacement of a subterm with another one *)
(* replaces in a term a term with another one. *)
(* Lifting are performed as usual. *)
let replace_lifting ~equality ~what ~with_what ~where =
- let rec substaux k =
+ let rec substaux k what =
let module C = Cic in
+ let module S = CicSubstitution in
function
- t when (equality t what) -> CicSubstitution.lift (k-1) with_what
- | C.Rel n as t -> t (*CSC: ??? BUG ? *)
+ t when (equality t what) -> S.lift (k-1) with_what
+ | C.Rel n as t -> t
| C.Var _ as t -> t
| C.Meta (i, l) as t ->
let l' =
List.map
(function
None -> None
- | Some t -> Some (substaux k t)
+ | Some t -> Some (substaux k what t)
) l
in
C.Meta(i,l')
| C.Sort _ 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)
- | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
| C.Appl (he::tl) ->
(* Invariant: no Appl applied to another Appl *)
- let tl' = List.map (substaux k) tl in
+ let tl' = List.map (substaux k what) tl in
begin
- match substaux k he with
+ match substaux k what he with
C.Appl l -> C.Appl (l@tl')
| _ as he' -> C.Appl (he'::tl')
end
| 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 outt, substaux k t,
- List.map (substaux k) pl)
+ C.MutCase (sp,cookingsno,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
let substitutedfl =
List.map
- (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
+ (fun (name,i,ty,bo) ->
+ (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
fl
in
C.Fix (i, substitutedfl)
let len = List.length fl in
let substitutedfl =
List.map
- (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
+ (fun (name,ty,bo) ->
+ (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
fl
in
C.CoFix (i, substitutedfl)
in
- substaux 1 where
+ substaux 1 what where
;;
(* Takes a well-typed term and fully reduces it. *)
projects / helm.git / blobdiff