+exception Uncertain of string
+exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
+
+let debug_print = fun _ -> ()
+
+type substitution = (int * (Cic.context * Cic.term)) list
+
+(*
+let rec deref subst =
+ let third _,_,a = a in
+ function
+ Cic.Meta(n,l) as t ->
+ (try
+ deref subst
+ (CicSubstitution.subst_meta
+ l (third (CicUtil.lookup_subst n subst)))
+ with
+ CicUtil.Subst_not_found _ -> t)
+ | t -> t
+;;
+*)
+
+let lookup_subst = CicUtil.lookup_subst
+;;
+
+
+(* clean_up_meta take a metasenv and a term and make every local context
+of each occurrence of a metavariable consistent with its canonical context,
+with respect to the hidden hipothesis *)
+
+(*
+let clean_up_meta subst metasenv t =
+ let module C = Cic in
+ let rec aux t =
+ match t with
+ C.Rel _
+ | C.Sort _ -> t
+ | C.Implicit _ -> assert false
+ | C.Meta (n,l) as t ->
+ let cc =
+ (try
+ let (cc,_) = lookup_subst n subst in cc
+ with CicUtil.Subst_not_found _ ->
+ try
+ let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
+ with CicUtil.Meta_not_found _ -> assert false) in
+ let l' =
+ (try
+ List.map2
+ (fun t1 t2 ->
+ match t1,t2 with
+ None , _ -> None
+ | _ , t -> t) cc l
+ with
+ Invalid_argument _ -> assert false) in
+ C.Meta (n, l')
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest)
+ | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest)
+ | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Const (uri, exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutInd (uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+ in
+ C.MutConstruct (uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ C.MutCase (uri, tyno, aux out, aux te, List.map aux pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ aux t *)
+
+(*** Functions to apply a substitution ***)
+
+let apply_subst_gen ~appl_fun subst term =
+ let rec um_aux =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.Var (uri, exp_named_subst')
+ | C.Meta (i, l) ->
+ (try
+ let (_, t,_) = lookup_subst i subst in
+ um_aux (S.subst_meta l t)
+ with CicUtil.Subst_not_found _ ->
+ (* unconstrained variable, i.e. free in subst*)
+ let l' =
+ List.map (function None -> None | Some t -> Some (um_aux t)) l
+ in
+ C.Meta (i,l'))
+ | C.Sort _ as t -> t
+ | C.Implicit _ -> assert false
+ | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
+ | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+ | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.Const (uri, exp_named_subst')
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.MutInd (uri,typeno,exp_named_subst')
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
+ in
+ C.MutConstruct (uri,typeno,consno,exp_named_subst')
+ | C.MutCase (sp,i,outty,t,pl) ->
+ let pl' = List.map um_aux pl in
+ C.MutCase (sp, i, um_aux outty, um_aux t, pl')
+ | C.Fix (i, fl) ->
+ let fl' =
+ List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
+ in
+ C.Fix (i, fl')
+ | C.CoFix (i, fl) ->
+ let fl' =
+ List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
+ in
+ C.CoFix (i, fl')
+ in
+ um_aux term
+;;
+
+let apply_subst =
+ let appl_fun um_aux he tl =
+ let tl' = List.map um_aux tl in
+ let t' =
+ match um_aux he with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | he' -> Cic.Appl (he'::tl')
+ in
+ begin
+ match he with
+ Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
+ | _ -> t'
+ end
+ in
+ fun s t ->
+(* incr apply_subst_counter; *)
+ apply_subst_gen ~appl_fun s t
+;;
+
+let rec apply_subst_context subst context =
+(*
+ incr apply_subst_context_counter;
+ context_length := !context_length + List.length context;
+*)
+ List.fold_right
+ (fun item context ->
+ match item with
+ | Some (n, Cic.Decl t) ->
+ let t' = apply_subst subst t in
+ Some (n, Cic.Decl t') :: context
+ | Some (n, Cic.Def (t, ty)) ->
+ let ty' =
+ match ty with
+ | None -> None
+ | Some ty -> Some (apply_subst subst ty)
+ in
+ let t' = apply_subst subst t in
+ Some (n, Cic.Def (t', ty')) :: context
+ | None -> None :: context)
+ context []
+
+let apply_subst_metasenv subst metasenv =
+(*
+ incr apply_subst_metasenv_counter;
+ metasenv_length := !metasenv_length + List.length metasenv;
+*)
+ List.map
+ (fun (n, context, ty) ->
+ (n, apply_subst_context subst context, apply_subst subst ty))
+ (List.filter
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
+ metasenv)