cicUtil: we moved here pp_term from proceduralHelpers

[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 7d95d86775de199f8e83ee7a1798bf6556b9ef4e..5807e185ae6a4bb2e2313b8a0c36fc9878c9eed3 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -35,102 +35,6 @@ module D    = Deannotate
 module PER  = ProofEngineReduction
 module Ut   = CicUtil
 
-(* 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 =
@@ -192,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