type types = {synthesized : Cic.term ; expected : Cic.term option};;
+(* does_not_occur n te *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+let rec does_not_occur n =
+ let module C = Cic in
+ function
+ C.Rel m when m = n -> false
+ | C.Rel _
+ | C.Meta _
+ | C.Sort _
+ | C.Implicit -> true
+ | C.Cast (te,ty) ->
+ does_not_occur n te && does_not_occur n ty
+ | C.Prod (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.Lambda (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.LetIn (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.Appl l ->
+ List.fold_right (fun x i -> i && does_not_occur n x) l true
+ | C.Var (_,exp_named_subst)
+ | C.Const (_,exp_named_subst)
+ | C.MutInd (_,_,exp_named_subst)
+ | C.MutConstruct (_,_,_,exp_named_subst) ->
+ List.fold_right (fun (_,x) i -> i && does_not_occur n x)
+ exp_named_subst true
+ | C.MutCase (_,_,out,te,pl) ->
+ does_not_occur n out && does_not_occur n te &&
+ List.fold_right (fun x i -> i && does_not_occur n x) pl true
+ | C.Fix (_,fl) ->
+ let len = List.length fl in
+ let n_plus_len = n + len in
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ in
+ List.fold_right
+ (fun (_,_,ty,bo) i ->
+ i && does_not_occur n ty &&
+ does_not_occur n_plus_len bo
+ ) fl true
+ | C.CoFix (_,fl) ->
+ let len = List.length fl in
+ let n_plus_len = n + len in
+ let tys =
+ List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ in
+ List.fold_right
+ (fun (_,ty,bo) i ->
+ i && does_not_occur n ty &&
+ does_not_occur n_plus_len bo
+ ) fl true
+;;
+
(*CSC: potrebbe creare applicazioni di applicazioni *)
(*CSC: ora non e' piu' head, ma completa!!! *)
let rec head_beta_reduce =
(*CSC: target of a LetIn? None used. *)
(* Let's visit all the subterms that will not be visited later *)
let _ = type_of_aux context s None in
- (* Checks suppressed *)
- C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
+ let t_typ =
+ (* Checks suppressed *)
+ type_of_aux ((Some (n,(C.Def s)))::context) t None
+ in
+ if does_not_occur 1 t_typ then
+ (* since [Rel 1] does not occur in typ, substituting any term *)
+ (* in place of [Rel 1] is equivalent to delifting once *)
+ CicSubstitution.subst C.Implicit t_typ
+ else
+ C.LetIn (n,s,t_typ)
| C.Appl (he::tl) when List.length tl > 0 ->
let expected_hetype =
(* Inefficient, the head is computed twice. But I know *)