+type ctx =
+ | Ce of NCic.hypothesis * NCic.obj list
+ | Fix of Ref.reference * string * NCic.term
+
+(***** A function to restrict the context of a term getting rid of unsed
+ variables *******)
+
+let restrict octx ctx ot =
+ let odummy = Cic.Implicit None in
+ let dummy = NCic.Meta (~-1,(0,NCic.Irl 0)) in
+ let rec aux m acc ot t =
+ function
+ [],[] -> (ot,t),acc
+ | ohe::otl as octx,he::tl ->
+ if CicTypeChecker.does_not_occur octx 0 1 ot then
+ aux (m+1) acc (CicSubstitution.subst odummy ot)
+ (NCicSubstitution.subst dummy t) (otl,tl)
+ else
+ (match ohe,he with
+ None,_ -> assert false
+ | Some (name,Cic.Decl oty),Ce ((name', NCic.Decl ty),objs) ->
+ aux (m+1) ((m+1,objs,None)::acc) (Cic.Lambda (name,oty,ot))
+ (NCic.Lambda (name',ty,t)) (otl,tl)
+ | Some (name,Cic.Decl oty),Fix (ref,name',ty) ->
+ aux (m+1) ((m+1,[],Some ref)::acc) (Cic.Lambda (name,oty,ot))
+ (NCic.Lambda (name',ty,t)) (otl,tl)
+ | Some (name,Cic.Def (obo,oty)),Ce ((name', NCic.Def (bo,ty)),objs) ->
+ aux (m+1) ((m+1,objs,None)::acc) (Cic.LetIn (name,obo,oty,ot))
+ (NCic.LetIn (name',bo,ty,t)) (otl,tl)
+ | _,_ -> assert false)
+ | _,_ -> assert false in
+ let rec split_lambdas_and_letins octx ctx infos (ote,te) =
+ match infos, ote, te with
+ ([], _, _) -> octx,ctx,ote
+ | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) ->
+ split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
+ (Ce ((name',NCic.Decl so),objs)::ctx) tl (ota,ta)
+ | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
+ split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
+ (Fix (r,name',so)::ctx) tl (ota,ta)
+ | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))->
+ split_lambdas_and_letins ((Some (name,(Cic.Def (obo,oty))))::octx)
+ (Ce ((nam',NCic.Def (bo,ty)),objs)::ctx) tl (ota,ta)
+ | (_, _, _) -> assert false
+ in
+ let long_t,infos = aux 0 [] ot dummy (octx,ctx) in
+ let clean_octx,clean_ctx,clean_ot= split_lambdas_and_letins [] [] infos long_t
+ in
+(*prerr_endline ("RESTRICT PRIMA: " ^ CicPp.pp ot (List.map (function None -> None | Some (name,_) -> Some name) octx));
+prerr_endline ("RESTRICT DOPO: " ^ CicPp.pp clean_ot (List.map (function None -> None | Some (name,_) -> Some name) clean_octx));
+*)
+ clean_octx,clean_ctx,clean_ot, List.map (fun (rel,_,_) -> rel) infos
+;;
+
+
+(**** The translation itself ****)
+