+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst) msg)))
+
+let rec beta_expand test_equality_only metasenv subst context t arg =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ let rec aux metasenv subst n context t' =
+(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*)
+ try
+ let subst,metasenv =
+ fo_unif_subst test_equality_only subst context metasenv arg t'
+ in
+ subst,metasenv,C.Rel (1 + n)
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+ match t' with
+ | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
+ | C.Var (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.Var (uri,exp_named_subst')
+ | C.Meta (i,l) as t->
+ (try
+ let t' = List.assoc i subst in
+ aux metasenv subst n context t'
+ with
+ Not_found -> subst,metasenv,t)
+ | C.Sort _
+ | C.Implicit _ as t -> subst,metasenv,t
+ | C.Cast (te,ty) ->
+ let subst,metasenv,te' = aux metasenv subst n context te in
+ let subst,metasenv,ty' = aux metasenv subst n context ty in
+ subst,metasenv,C.Cast (te', ty')
+ | C.Prod (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ in
+ subst,metasenv,C.Prod (nn, s', t')
+ | C.Lambda (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ in
+ subst,metasenv,C.Lambda (nn, s', t')
+ | C.LetIn (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ in
+ subst,metasenv,C.LetIn (nn, s', t')
+ | C.Appl l ->
+ let subst,metasenv,revl' =
+ List.fold_left
+ (fun (subst,metasenv,appl) t ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,t'::appl
+ ) (subst,metasenv,[]) l
+ in
+ subst,metasenv,C.Appl (List.rev revl')
+ | C.Const (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ let subst,metasenv,outt' = aux metasenv subst n context outt in
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ let subst,metasenv,revpl' =
+ List.fold_left
+ (fun (subst,metasenv,pl) t ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,t'::pl
+ ) (subst,metasenv,[]) pl
+ in
+ subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
+ | C.Fix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+ | C.CoFix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+
+ and aux_exp_named_subst metasenv subst n context ens =
+ List.fold_right
+ (fun (uri,t) (subst,metasenv,l) ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
+ in
+ let argty =
+ type_of_aux' metasenv subst context arg
+ in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ metasenv context (Cic.Name "Heta") ~typ:argty
+ in
+ let subst,metasenv,t' = aux metasenv subst 0 context t in
+ subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+
+and beta_expand_many test_equality_only metasenv subst context t =
+ List.fold_left
+ (fun (subst,metasenv,t) arg ->
+ beta_expand test_equality_only metasenv subst context t arg
+ ) (subst,metasenv,t)