+ CicTypeChecker.TypeCheckerFailure msg ->
+ let msg =
+ (sprintf
+ "Kernel Type checking error:
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+ (CicMetaSubst.ppterm subst term)
+ (CicMetaSubst.ppterm [] term)
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst)
+ (CicMetaSubst.ppsubst subst) msg) in
+ raise (AssertFailure msg);;
+
+let exists_a_meta l =
+ List.exists (function Cic.Meta _ -> true | _ -> false) l
+
+let rec deref subst t =
+ let snd (_,a,_) = a in
+ match t with
+ Cic.Meta(n,l) ->
+ (try
+ deref subst
+ (CicSubstitution.subst_meta
+ l (snd (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | Cic.Appl(Cic.Meta(n,l)::args) ->
+ (match deref subst (Cic.Meta(n,l)) with
+ | Cic.Lambda _ as t ->
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+ | r -> Cic.Appl(r::args))
+ | Cic.Appl(((Cic.Lambda _) as t)::args) ->
+ deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
+ | t -> t
+;;
+
+
+let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ let rec aux metasenv subst n context t' ugraph =
+ try
+
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst test_equality_only subst context metasenv
+ (CicSubstitution.lift n arg) t' ugraph
+
+ in
+ subst,metasenv,C.Rel (1 + n),ugraph1
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+ match t' with
+ | C.Rel m -> subst,metasenv,
+ (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
+ | C.Var (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
+ | 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), ugraph
+ | C.Sort _
+ | C.Implicit _ as t -> subst,metasenv,t,ugraph
+ | C.Cast (te,ty) ->
+ let subst,metasenv,te',ugraph1 =
+ aux metasenv subst n context te ugraph in
+ let subst,metasenv,ty',ugraph2 =
+ aux metasenv subst n context ty ugraph1 in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Cast (te', ty')),ugraph2
+ | C.Prod (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Prod (nn, s', t')),ugraph2
+ | C.Lambda (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
+ | C.LetIn (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+ | C.Appl l ->
+ let subst,metasenv,revl',ugraph1 =
+ List.fold_left
+ (fun (subst,metasenv,appl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::appl),ugraph1
+ ) (subst,metasenv,[],ugraph) l
+ in
+ subst,metasenv,(C.Appl (List.rev revl')),ugraph1
+ | C.Const (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
+ | C.MutCase (sp,i,outt,t,pl) ->
+ let subst,metasenv,outt',ugraph1 =
+ aux metasenv subst n context outt ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst n context t ugraph1 in
+ let subst,metasenv,revpl',ugraph3 =
+ List.fold_left
+ (fun (subst,metasenv,pl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::pl),ugraph1
+ ) (subst,metasenv,[],ugraph2) pl
+ in
+ subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
+ (* TASSI: not sure this is serial *)
+ | 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,(CicSubstitution.lift 1 t' ),ugraph
+ | 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,(CicSubstitution.lift 1 t'), ugraph
+
+ and aux_exp_named_subst metasenv subst n context ens ugraph =
+ List.fold_right
+ (fun (uri,t) (subst,metasenv,l,ugraph) ->
+ let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
+ subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
+ in
+ let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name ~subst
+ metasenv context (Cic.Name "Heta") ~typ:argty
+ in
+ let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
+ subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
+
+
+and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+ let subst,metasenv,hd,ugraph =
+ List.fold_right
+ (fun arg (subst,metasenv,t,ugraph) ->
+ let subst,metasenv,t,ugraph1 =
+ beta_expand test_equality_only
+ metasenv subst context t arg ugraph
+ in
+ subst,metasenv,t,ugraph1
+ ) args (subst,metasenv,t,ugraph)
+ in
+ subst,metasenv,hd,ugraph
+