let s' = aux ctx s in
C.LetIn (n, s, aux ((def n s')::ctx) t)
| C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
+ | C.Appl [] -> assert false
| C.Const (uri,exp_named_subst) ->
C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
| C.MutInd (uri,typeno,exp_named_subst) ->
| C.CoFix _ -> t
let normalize ?delta ?subst ctx term =
- prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term);
+(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
let t = normalize ?delta ?subst ctx term in
- prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t);
+(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
t
+(* performs an head beta/cast reduction *)
+let rec head_beta_reduce =
+ function
+ (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ let he''' =
+ match he'' with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | _ -> Cic.Appl (he''::tl')
+ in
+ head_beta_reduce he'''
+ | Cic.Cast (te,_) -> head_beta_reduce te
+ | t -> t