module PER = ProofEngineReduction
module Ut = CicUtil
-(* time stamping ************************************************************)
-
-let print_times =
- let old = ref 0.0 in
- fun msg ->
- let times = Unix.times () in
- let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in
- let lap = stamp -. !old in
- Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout;
- old := stamp
-
(* raw cic prettyprinter ****************************************************)
let xiter out so ss sc map l =
let abbr s v w = Some (s, C.Def (v, w))
let pp_sort out = function
- | C.Type _ -> out "\Type"
- | C.Prop -> out "\Prop"
- | C.CProp _ -> out "\CProp"
- | C.Set -> out "\Set"
+ | C.Type _ -> out "*Type"
+ | C.Prop -> out "*Prop"
+ | C.CProp _ -> out "*CProp"
+ | C.Set -> out "*Set"
let pp_name out = function
| C.Name s -> out s
(* helper functions *********************************************************)
+let rec list_fold_right_cps g map l a =
+ match l with
+ | [] -> g a
+ | hd :: tl ->
+ let h a = map g hd a in
+ list_fold_right_cps h map tl a
+
+let rec list_fold_left_cps g map a = function
+ | [] -> g a
+ | hd :: tl ->
+ let h a = list_fold_left_cps g map a tl in
+ map h a hd
+
let rec list_map_cps g map = function
| [] -> g []
| hd :: tl ->