we aligned the implementation to the plmms08 paper

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 54b115aa254de92074659c52f97107a72a805bc1..7d95d86775de199f8e83ee7a1798bf6556b9ef4e 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -35,17 +35,6 @@ module D    = Deannotate
 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 =
@@ -61,10 +50,10 @@ let abst s w = Some (s, C.Decl w)
 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
@@ -174,6 +163,19 @@ let mk_fresh_name context = function
 
 (* 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 ->