1) The NG kernel now accepts only usage of declared universes

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 27590ed3eed7ff1179eb9ec81006961b09b13eb0..258e83c949da272dd1b412faa010fe5d7b558b4f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -18,26 +18,29 @@ module F = Format
 let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);;
 let set_head_beta_reduce = (:=) head_beta_reduce;;
 
+let get_obj = ref (fun _ -> assert false);;
+let set_get_obj f = get_obj := f;;
+
 let r2s pp_fix_name r = 
   try
     match r with
     | R.Ref (u,R.Ind (_,i,_)) -> 
-        (match NCicLibrary.get_obj u with
+        (match !get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,name,_,_ = List.nth itl i in name
         | _ -> assert false)
     | R.Ref (u,R.Con (i,j,_)) -> 
-        (match NCicLibrary.get_obj u with
+        (match !get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,_,_,cl = List.nth itl i in
             let _,name,_ = List.nth cl (j-1) in name
         | _ -> assert false)
     | R.Ref (u,(R.Decl | R.Def _)) -> 
-        (match NCicLibrary.get_obj u with
+        (match !get_obj u with
         | _,_,_,_, C.Constant (_,name,_,_,_) -> name
         | _ -> assert false)
     | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
-        (match NCicLibrary.get_obj u with
+        (match !get_obj u with
         | _,_,_,_, C.Fixpoint (_,fl,_) -> 
             if pp_fix_name then
               let _,name,_,_,_ = List.nth fl i in name
@@ -45,7 +48,7 @@ let r2s pp_fix_name r =
               NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
         | _ -> assert false)
   with 
-  | NCicLibrary.ObjectNotFound _ 
+  | NCicEnvironment.ObjectNotFound _ 
   | Failure "nth" 
   | Invalid_argument "List.nth" -> R.string_of_reference r
 
@@ -210,11 +213,12 @@ let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
 let rec ppmetasenv ~formatter ~subst metasenv = function
   | [] -> ()
   | (i,(name, ctx, ty)) :: tl ->
+      F.fprintf formatter "@[<hov 2>";
       let name = match name with Some n -> "("^n^")" | _ -> "" in
       ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx;
-      F.fprintf formatter " ⊢ ?%d%s : " i name;
+      F.fprintf formatter "@;⊢@;?%d%s :@;" i name;
       ppterm ~formatter ~metasenv ~subst ~context:ctx ty;
-      F.fprintf formatter "\n";
+      F.fprintf formatter "@]@\n";
       ppmetasenv ~formatter ~subst metasenv tl
 ;;
 
@@ -244,43 +248,49 @@ let ppobj ~formatter (u,_,metasenv, subst, o) =
   ppmetasenv ~formatter ~subst metasenv;
   F.fprintf formatter "\n";
   F.fprintf formatter "subst:\n";
-  (*ppsubst subst ~formatter ~metasenv;*)
+  (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "...";
   F.fprintf formatter "\n";
   match o with 
   | NCic.Fixpoint (b, fl, _) -> 
-      F.fprintf formatter "{%s}\n" (NUri.string_of_uri u);
-      F.fprintf formatter "%s" (if b then "let rec " else "let corec ");
-      HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ")
+      F.fprintf formatter "{%s}@\n@[<hov 0>" (NUri.string_of_uri u);
+      F.fprintf formatter "@[<hov 2>%s"(if b then "let rec " else "let corec ");
+      HExtlib.list_iter_sep
+       ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
        (fun (_,name,n,ty,bo) ->
-        F.fprintf formatter "%s on %d : " name n;
+        F.fprintf formatter "%s on %d :@;" name n;
         ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-        F.fprintf formatter " :=\n";
-        ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl
+        F.fprintf formatter "@]@;@[<hov 2>:=@;";
+        ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo;
+        F.fprintf formatter "@]") fl;
+        F.fprintf formatter "@]"
   | NCic.Inductive (b, leftno,tyl, _) -> 
-      F.fprintf formatter "{%s} with %d fixed params\n%s"
+      F.fprintf formatter "{%s} with %d fixed params@\n@[<hov 0>@[<hov 2>%s"
        (NUri.string_of_uri u) leftno
        (if b then "inductive " else "coinductive ");
-      HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ")
+      HExtlib.list_iter_sep
+        ~sep:(fun () -> F.fprintf formatter "@\n@[<hov 2>and ")
        (fun (_,name,ty,cl) ->
-          F.fprintf formatter "%s: " name;
+          F.fprintf formatter "%s:@;" name;
           ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-          F.fprintf formatter " :=\n";
-          HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "\n")
+          F.fprintf formatter "@]@;@[<hov 3>:=@;";
+          HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "@;")
            (fun (_,name,ty) ->
-             F.fprintf formatter "  | %s: " name;
-             ppterm ~formatter ~metasenv ~subst ~context:[] ty)
-           cl
-        ) tyl
+             F.fprintf formatter "| %s: " name;
+             ppterm ~formatter ~metasenv ~subst ~context:[] ty;)
+           cl;
+          F.fprintf formatter "@]"
+        ) tyl ;
+        F.fprintf formatter "@]"
   | NCic.Constant (_,name,None,ty, _) -> 
-     F.fprintf formatter "{%s}\naxiom %s : " (NUri.string_of_uri u) name;
+     F.fprintf formatter "{%s}@\n@[<hov 2>axiom %s :@;" (NUri.string_of_uri u) name;
      ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-     F.fprintf formatter "\n"
+     F.fprintf formatter "@]@\n"
   | NCic.Constant (_,name,Some bo,ty, _) ->
-     F.fprintf formatter "{%s}\ndefinition %s : " (NUri.string_of_uri u) name;
+     F.fprintf formatter "{%s}@\n@[<hov 0>@[<hov 2>definition %s :@;" (NUri.string_of_uri u) name;
      ppterm ~formatter ~metasenv ~subst ~context:[] ty;
-     F.fprintf formatter " := \n";
+     F.fprintf formatter "@]@;@[<hov 2>:=@;";
      ppterm ~formatter ~metasenv ~subst ~context:[] bo;
-     F.fprintf formatter "\n"
+     F.fprintf formatter "@]@\n@]"
 ;;
 
 let ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =