exception Occur;;
-let rec force_does_not_occur k subst to_be_restricted t =
+let rec force_does_not_occur subst to_be_restricted t =
let module C = Cic in
let more_to_be_restricted = ref [] in
let rec aux k = function
in
C.CoFix (i, fl')
in
- let res = aux k t in
+ let res = aux 0 t in
(!more_to_be_restricted, res)
let rec restrict subst to_be_restricted metasenv =
String.concat ", "
(List.map
(fun i ->
- match List.nth context i with
- | None -> assert false
- | Some (n, _) -> CicPp.ppname n)
- indexes)
+ try
+ match List.nth context i with
+ | None -> assert false
+ | Some (n, _) -> CicPp.ppname n
+ with
+ Failure _ -> assert false
+ ) indexes)
in
- let force_does_not_occur_in_context k to_be_restricted = function
+ let force_does_not_occur_in_context to_be_restricted = function
| None -> [], None
| Some (name, Cic.Decl t) ->
let (more_to_be_restricted, t') =
- force_does_not_occur k subst to_be_restricted t
+ force_does_not_occur subst to_be_restricted t
in
more_to_be_restricted, Some (name, Cic.Decl t')
| Some (name, Cic.Def (bo, ty)) ->
let (more_to_be_restricted, bo') =
- force_does_not_occur k subst to_be_restricted bo
+ force_does_not_occur subst to_be_restricted bo
in
let more_to_be_restricted, ty' =
match ty with
| None -> more_to_be_restricted, None
| Some ty ->
let more_to_be_restricted', ty' =
- force_does_not_occur k subst to_be_restricted ty
+ force_does_not_occur subst to_be_restricted ty
in
more_to_be_restricted @ more_to_be_restricted',
Some ty'
else
(try
let more_to_be_restricted', hd' =
- force_does_not_occur_in_context i restricted hd
+ let delifted_restricted =
+ let rec aux =
+ function
+ [] -> []
+ | j::tl when j > i -> (j - i)::aux tl
+ | _::tl -> aux tl
+ in
+ aux restricted
+ in
+ force_does_not_occur_in_context delifted_restricted hd
in
more_to_be_restricted @ more_to_be_restricted',
restricted, hd' :: tl'
in
try
let more_to_be_restricted', t' =
- force_does_not_occur 0 subst restricted t
+ force_does_not_occur subst restricted t
in
let metasenv' = (n, context', t') :: metasenv in
(try
let s = List.assoc n subst in
try
let more_to_be_restricted'', s' =
- force_does_not_occur 0 subst restricted s
+ force_does_not_occur subst restricted s
in
let subst' = (n, s') :: (List.remove_assoc n subst) in
let more =
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
let delift n subst context metasenv l t =
let module S = CicSubstitution in
-(* THIS CODE SHOULD NOT BE USEFUL AT ALL
let l =
let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
List.map2 (fun ct lt ->
| Some _, _ -> lt)
canonical_context l
in
-*)
let to_be_restricted = ref [] in
let rec deliftaux k =
let module C = Cic in
tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ;
res
+
+(** {2 Format-like pretty printers} *)
+
+let fpp_gen ppf s =
+ Format.pp_print_string ppf s;
+ Format.pp_print_newline ppf ();
+ Format.pp_print_flush ppf ()
+
+let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
+let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
+