+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
+
+let rec deref subst =
+ function
+ Cic.Meta(n,l) as t ->
+ (try
+ deref subst
+ (CicSubstitution.lift_meta
+ l (snd (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | t -> t
+;;
+
+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' =
+ try
+ let subst,metasenv =
+ fo_unif_subst test_equality_only subst context metasenv
+ (CicSubstitution.lift n 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) ->
+ (* andrea: in general, beta_expand can create badly typed
+ terms. This happens quite seldom in practice, UNLESS we
+ iterate on the local context. For this reason, we renounce
+ to iterate and just lift *)
+ let l =
+ List.map
+ (function
+ Some t -> Some (CicSubstitution.lift 1 t)
+ | None -> None) l in
+ subst, metasenv, C.Meta (i,l)
+ (*
+ let (subst, metasenv, context, local_context) =
+ List.fold_right
+ (fun t (subst, metasenv, context, local_context) ->
+ match t with
+ | None -> (subst, metasenv, context, None :: local_context)
+ | Some t ->
+ let (subst, metasenv, t) =
+ aux metasenv subst n context t
+ in
+ (subst, metasenv, context, Some t :: local_context))
+ l (subst, metasenv, context, [])
+ in
+ prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
+ (subst, metasenv, C.Meta (i, local_context)) *)
+ | 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' *)
+ subst,metasenv,CicSubstitution.lift 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' *)
+ subst,metasenv,CicSubstitution.lift 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
+ (* prova *)
+ (* old
+ subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+ *)
+ subst, metasenv, C.Lambda (fresh_name,argty,t')
+
+and beta_expand_many test_equality_only metasenv subst context t args =
+ let subst,metasenv,hd =
+ List.fold_right
+ (fun arg (subst,metasenv,t) ->
+ let subst,metasenv,t =
+ beta_expand test_equality_only metasenv subst context t arg in
+ subst,metasenv,t
+ ) args (subst,metasenv,t) in
+ subst,metasenv,hd