+type types = {synthesized : Cic.term ; expected : Cic.term option};;
+
+(*CSC: potrebbe creare applicazioni di applicazioni *)
+(*CSC: ora non e' piu' head, ma completa!!! *)
+let rec head_beta_reduce =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ function
+ C.Rel _
+ | C.Var _ as t -> t
+ | C.Meta (n,l) ->
+ C.Meta (n,
+ List.map
+ (function None -> None | Some t -> Some (head_beta_reduce t)) l
+ )
+ | C.Sort _ as t -> t
+ | C.Implicit -> assert false
+ | C.Cast (te,ty) ->
+ C.Cast (head_beta_reduce te, head_beta_reduce ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
+ let he' = S.subst he t in
+ if tl = [] then
+ head_beta_reduce he'
+ else
+ head_beta_reduce (C.Appl (he'::tl))
+ | C.Appl l ->
+ C.Appl (List.map head_beta_reduce l)
+ | C.Const _ as t -> t
+ | C.MutInd _
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cno,i,outt,t,pl) ->
+ C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+ List.map head_beta_reduce pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,i,ty,bo) ->
+ name,i,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.Fix (i,fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,ty,bo) ->
+ name,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.CoFix (i,fl')
+;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant), *)
+(* distinction between fake dependent products *)
+(* and non-dependent products, alfa-conversion *)
+(*CSC: must alfa-conversion be considered or not? *)
+let syntactic_equality t t' =
+ let module C = Cic in
+ let rec syntactic_equality 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') ->
+ syntactic_equality te te' &&
+ syntactic_equality ty ty'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ 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 (_,i,ty,bo) (_,i',ty',bo') ->
+ b && 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 (_,ty,bo) (_,ty',bo') ->
+ b &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | _,_ -> false
+ in
+ try
+ syntactic_equality t t'
+ with
+ _ -> false
+;;