X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=a9fa6473f280ac7e12fc50422181b99cf0a248cf;hb=ef05c795559108c1d33cfa048531849807867a81;hp=54b115aa254de92074659c52f97107a72a805bc1;hpb=2ea5357bace160aaf57750d9dcfb3077fe5a1b38;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 54b115aa2..a9fa6473f 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -35,113 +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 =
-   let rec aux = function
-      | hd :: tl when tl <> [] -> map hd; out ss; aux tl
-      | hd :: tl               -> map hd; aux tl
-      | []                     -> ()
-   in
-   out so; aux l; out sc
-
-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"
-
-let pp_name out = function
-   | C.Name s    -> out s
-   | C.Anonymous -> out "_"
-
-let pp_rel out c i =
-   try match List.nth c (pred i) with
-      | None           -> out (Printf.sprintf "%u[?]" i)
-      | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
-   with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
-
-let pp_implict out = function
-   | None         -> out "?"
-   | Some `Closed -> out "?[Closed]" 
-   | Some `Type   -> out "?[Type]"
-   | Some `Hole   -> out "?[Hole]"
-
-let pp_uri out a =
-   out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
-
-let rec pp_term out e c = function
-   | C.Sort h                      -> pp_sort out h
-   | C.Rel i                       -> pp_rel out c i
-   | C.Implicit x                  -> pp_implict out x
-   | C.Meta (i, iss)               ->
-      let map = function None   -> out "_" | Some v -> pp_term out e c v in
-      out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
-   | C.Var (a, xss)              ->
-      pp_uri out a; pp_xss out e c xss
-   | C.Const (a, xss)              ->
-      pp_uri out a; pp_xss out e c xss
-   | C.MutInd (a, m, xss)          ->
-      pp_uri out a; out (Printf.sprintf "/%u" m);
-      pp_xss out e c xss
-   | C.MutConstruct (a, m, n, xss) ->
-      pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
-      pp_xss out e c xss
-   | C.Cast (v, w)                 ->
-      out "type "; pp_term out e c w; out " contains "; pp_term out e c v
-   | C.Appl vs                     ->
-      xiter out "(" " @ " ")" (pp_term out e c) vs
-   | C.MutCase (a, m, w, v, vs)    ->
-      out "match "; pp_term out e c v;
-      out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
-      out " to "; pp_term out e c w;
-      xiter out " cases " " | " "" (pp_term out e c) vs
-   | C.Prod (s, w, t)             ->
-      out "forall "; pp_name out s; out " of "; pp_term out e c w;
-      out " in "; pp_term out e (abst s w :: c) t
-   | C.Lambda (s, w, t)            ->
-      out "fun "; pp_name out s; out " of "; pp_term out e c w;
-      out " in "; pp_term out e (abst s w :: c) t
-   | C.LetIn (s, v, w, t)          ->
-      out "let "; pp_name out s; 
-      out " def "; pp_term out e c v; out " of "; pp_term out e c w;
-      out " in "; pp_term out e (abbr s v w :: c) t
-   | C.Fix (i, fs)                 ->
-      let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
-      let c' = List.fold_left map c fs in
-      let map (s, i, w, v) =
-         out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v; 
-	 out " of "; pp_term out e c w;
-      in
-      xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
-   | C.CoFix (i, fs)                 ->
-      let map c (s, w, v) = abbr (C.Name s) v w :: c in
-      let c' = List.fold_left map c fs in
-      let map (s, w, v) =
-         out s; pp_term out e c' v; 
-	 out " of "; pp_term out e c w;
-      in
-      xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
-
-and pp_xss out e c xss = 
-   let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
-   xiter out "[" "; " "]" map xss 
-
 (* fresh name generator *****************************************************)
 
 let split name =
@@ -174,6 +67,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 -> 
@@ -190,18 +96,24 @@ let compose f g x = f (g x)
 let fst3 (x, _, _) = x
 
 let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
-   with e -> 
-      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+   let error e = 
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
       raise e
+   in
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with 
+      | Rf.RefineFailure s as e -> 
+         Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
+	 error e
+      | e                       ->
+         Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
+	 error e
 
 let get_type msg c t =
    let log s =
       prerr_endline ("TC: " ^ s); 
       prerr_endline ("TC: context: " ^ Pp.ppcontext c);
-      prerr_string "TC: term   : "; pp_term prerr_string [] c t;
+      prerr_string "TC: term   : "; Ut.pp_term prerr_string [] c t;
       prerr_newline (); prerr_endline ("TC: location: " ^ msg)
    in   
    try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
@@ -215,12 +127,15 @@ let get_tail c t =
       | (_, hd) :: _, _ -> hd
       | _               -> assert false
 
-let is_proof c t =
-   match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
+let is_prop c t =
+   match get_tail c (get_type "is_prop" c t) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
 
+let is_proof c t =
+   is_prop c (get_type "is_prop" c t)
+
 let is_sort = function
    | C.Sort _ -> true
    | _        -> false