- let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
- List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
-
- prerr_endline "---------<OPT>----------";
- let sigma = optimize_numerals p_finale in (* optimize numerals *)
- let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
- List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
-
- prerr_endline "---------<PURE>---------";
- let t_of_nf t = ToScott.t_of_nf (t :> nf) in
- let div = option_map t_of_nf p.div in
- let conv = List.map t_of_nf p.conv in
- let ps = List.map t_of_nf p.ps in
-
- let sigma' = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
- let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in
-
- prerr_endline "--------<REDUCE>---------";
- let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *)
- (function Some div ->
- print_endline (Pure.print div);
- let t = Pure.mwhd (e',div,[]) in
- prerr_endline ("*:: " ^ (Pure.print t));
- assert (t = pure_bomb)
- | None -> ()) div;
- List.iter (fun n ->
- verbose ("_::: " ^ (Pure.print n));
- let t = Pure.mwhd (e',n,[]) in
- verbose ("_:: " ^ (Pure.print t));
- assert (t <> pure_bomb)
- ) conv ;
- List.iteri (fun i n ->
- verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));
- let t = Pure.mwhd (e',n,[]) in
- verbose ((string_of_int i) ^ ":: " ^ (Pure.print t));
- assert (t = Scott.mk_n i)
- ) ps ;
- prerr_endline "-------- </DONE> --------";
- `Separable p_finale.sigma
-;;
-
-let zero = `Var(0,0);;
-
-let append_zero =
- function
- | `I _
- | `Var _ as i -> cast_to_i_n_var (mk_app i zero)
- | `N _ -> raise (Parser.ParsingError " numbers in ps")
+ List.iter (fun (x,inst) -> prerr_endline
+ (string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
+
+ prerr_endline "---------<OPT>----------";
+ let sigma = optimize_numerals p_finale in (* optimize numerals *)
+ List.iter (fun (x,inst) -> prerr_endline
+ (string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
+
+ prerr_endline "---------<PURE>---------";
+ ToScott.bomb := !divergent;
+ let scott_of_nf t = ToScott.t_of_nf (t :> nf) in
+ let div = option_map scott_of_nf p.div in
+ let conv = List.map scott_of_nf p.conv in
+ let ps = List.map scott_of_nf p.ps in
+
+ let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in
+ let e' = Pure.env_of_sigma freshno sigma' in
+
+ prerr_endline "--------<REDUCE>---------";
+ (function
+ | Some div ->
+ print_endline (Pure.print div);
+ let t = Pure.mwhd (e',div,[]) in
+ prerr_endline ("*:: " ^ (Pure.print t));
+ assert (Pure.diverged t)
+ | None -> ()) div;
+ List.iter (fun n ->
+ verbose ("_::: " ^ (Pure.print n));
+ let t = Pure.mwhd (e',n,[]) in
+ verbose ("_:: " ^ (Pure.print t));
+ assert (not (Pure.diverged t))
+ ) conv ;
+ List.iteri (fun i n ->
+ verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));
+ let t = Pure.mwhd (e',n,[]) in
+ verbose ((string_of_int i) ^ ":: " ^ (Pure.print t));
+ assert (t = Scott.mk_n i)
+ ) ps ;
+ prerr_endline "-------- </DONE> --------";
+ `Separable p_finale.sigma