Facilites pour le debogguage des univers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 183 insertions, 28 deletions

diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 1fefb6c444..c26a8039d4 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -181,7 +181,7 @@ let more_general_pat pat1 pat2 =
 
       | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma
 
-      | PSort RType, PSort RType -> sigma
+      | PSort (RType _), PSort (RType _) -> sigma
 
       | PApp (c1,arg1), PApp (c2,arg2) ->
         (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0ce95049ae..63ef38e4f5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1564,7 +1564,7 @@ let rec cvt_varg =
      | _ -> xlate_error "cvt_varg : PROP : Failed match ")
     | Node (_, "CONSTR", ((Node (_, "PROP", [])) :: [])) ->
      Varg_sorttype (CT_sortc "Prop")
-    | Node (_, "CONSTR", ((Node (_, "TYPE", [])) :: [])) ->
+    | Node (_, "CONSTR", ((Node (_, "TYPE", _)) :: [])) ->
      Varg_sorttype (CT_sortc "Type")
     | Node (_, "CONSTR", [c]) -> Varg_constr (xlate_formula c)
     | Node (_, "CONSTRLIST", cs) -> Varg_constrlist (List.map xlate_formula cs)
diff --git a/dev/univdot b/dev/univdot
new file mode 100755
index 0000000000..bb0dd2c89b
--- /dev/null
+++ b/dev/univdot
@@ -0,0 +1,49 @@
+#!/bin/sh
+
+usage() {
+    echo ""
+    echo "usage: univdot [INPUT] [OUTPUT]"
+    echo ""
+    echo "takes the output of Dump Universes \"file\" command"
+    echo "and transforms it to the dot format"
+    echo ""
+    echo "Coq> Dump Universes \"univ.raw\"."
+    echo ""
+    echo "user@host> univdot univ.raw | dot -Tps > univ.ps" 
+    echo ""
+}
+    
+
+# these are dot edge attributes to draw arrows corresponding 
+# to > >= and = edges of the universe graph
+
+GT="[color=red]"
+GE="[color=blue]"
+EQ="[color=black]"
+
+
+# input/output redirection
+case $# in
+  0) ;;
+  1) case $1 in
+       -h|-help|--help) usage
+               exit 0 ;;
+       *) exec < $1 ;;
+     esac ;;
+  2) exec < $1 > $2 ;;
+  *) usage
+     exit 0;;
+esac
+
+
+# dot header
+echo 'digraph G {\
+  size="7.5,10" ;\
+  rankdir = TB ;'
+
+sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
+      -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
+      -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
+| sed -e "s/\./_/g" 
+
+echo "}"
\ No newline at end of file
diff --git a/dev/universes.txt b/dev/universes.txt
new file mode 100644
index 0000000000..65c1e522af
--- /dev/null
+++ b/dev/universes.txt
@@ -0,0 +1,32 @@
+How to debug universes?
+
+1. There is a command Dump Universes in Coq toplevel
+
+   Dump Universes.
+     prints the graph of universes in the form of constraints
+
+   Dump Universes "file".
+     produces the "file" containing universe constraints in the form
+       univ1 # univ2 ;
+     where # can be either > >= or =
+     
+   The file produced by the latter command can be transformed using
+   the script univdot to dot format.
+   For example
+
+   univdot file | dot -Tps > file.ps
+
+   produces a graph of universes in ps format. 
+   > arrows are red, >= blue, and = black.
+
+
+   *) for dot see http://www.research.att.com/sw/tools/graphviz/
+
+
+2. There is a printing option
+  
+   Termast.print_universes : bool ref
+
+   which, when set (in ocaml after Drop), makes all pretty-printed
+   Type's annotated with the name of the universe.
+
diff --git a/kernel/term.ml b/kernel/term.ml
index a1ad328dc3..1f68c1a359 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -42,7 +42,8 @@ let mk_Prop = Prop Null
 let print_sort = function
   | Prop Pos -> [< 'sTR "Set" >]
   | Prop Null -> [< 'sTR "Prop" >]
-  | Type _ -> [< 'sTR "Type" >]
+(*  | Type _ -> [< 'sTR "Type" >] *)
+  | Type u -> [< 'sTR "Type("; pr_uni u; 'sTR ")" >]
 
 (********************************************************************)
 (* type of global reference *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index b3d5a9b0e1..49b2f60728 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -34,9 +34,13 @@ module UniverseOrdered = struct
   let compare = universe_ord
 end
 
+let string_of_univ u = 
+  (Names.string_of_dirpath u.u_mod)^"."^(string_of_int u.u_num)
+
 let pr_uni u =
   [< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
 
+
 let dummy_univ = { u_mod = ["dummy univ"]; u_num = 0 } (* for prover terms *)
 let implicit_univ = { u_mod = ["implicit univ"]; u_num = 0 }
 
@@ -94,7 +98,7 @@ let repr g u =
   let rec repr_rec u =
     let a =
       try UniverseMap.find u g
-      with Not_found -> anomalylabstrm "Impuniv.repr"
+      with Not_found -> anomalylabstrm "Univ.repr"
 	  [< 'sTR"Universe "; pr_uni u; 'sTR" undefined" >] 
     in
     match a with 
@@ -140,21 +144,35 @@ let reprgeq g arcu =
   in 
   searchrec [] arcu.ge
 
+
 (* between : universe -> canonical_arc -> canonical_arc list *)
 (* between u v = {w|u>=w>=v, w canonical}          *)     
 (* between is the most costly operation *)
+
 let between g u arcv = 
-  let rec explore (memo,l) arcu = 
-    try 
-      memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *)
-    with Not_found ->
-      let w = reprgeq g arcu in
-      let (memo',sols) = List.fold_left explore (memo,[]) w in
-      let sols' = if sols=[] then [] else arcu::sols in
-      ((arcu,sols')::memo', list_unionq sols' l) 
+  (* good are all w | u >= w >= v  *)
+  (* bad are all w | u >= w ~>= v *)
+    (* find good and bad nodes in {w | u >= w} *)
+    (* explore b u = (b or "u is good") *)
+  let rec explore ((good, bad, b) as input) arcu =
+    if List.memq arcu good then
+      (good, bad, true) (* b or true *)
+    else if List.memq arcu bad then
+      input    (* (good, bad, b or false) *)
+    else 
+      let childs = reprgeq g arcu in 
+	(* are any children of u good ? *)
+      let good, bad, b_childs = 
+	List.fold_left explore (good, bad, false) childs 
+      in
+	if b_childs then
+	  arcu::good, bad, true (* b or true *)
+	else 
+	  good, arcu::bad, b    (* b or false *)
   in
-  snd (explore ([(arcv,[arcv])],[]) (repr g u))
-
+  let good,_,_ = explore ([arcv],[],false) (repr g u) in
+    good
+      
 (* We assume  compare(u,v) = GE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
    Otherwise, between g u v = [] 
@@ -226,7 +244,7 @@ let merge g u v =
 	let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' w in
 	let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' w' in
 	g'''
-    | [] -> anomaly "between"
+    | [] -> anomaly "Univ.between"
 
 (* merge_disc : universe -> universe -> unit *)
 (* we assume  compare(u,v) = compare(v,u) = NGE *)
@@ -257,7 +275,7 @@ let enforce_univ_geq u v g =
            | GT -> error_inconsistency()
            | GE -> merge g v u
            | NGE -> setgeq g u v
-           | EQ -> anomaly "compare")
+           | EQ -> anomaly "Univ.compare")
     | _ -> g
 
 (* enforceq : universe -> universe -> unit *)
@@ -274,7 +292,7 @@ let enforce_univ_eq u v g =
            | GT -> error_inconsistency()
            | GE -> merge g v u
            | NGE -> merge_disc g u v
-           | EQ -> anomaly "compare")
+           | EQ -> anomaly "Univ.compare")
 
 (* enforcegt u v will force u>v if possible, will fail otherwise *)
 let enforce_univ_gt u v g =
@@ -361,7 +379,9 @@ let sup u v g =
            | _ -> v, Constraint.empty)
     | _ -> u, Constraint.empty
 
+
 (* Pretty-printing *)
+
 let num_universes g =
   UniverseMap.fold (fun _ _ -> succ) g 0
 
@@ -387,4 +407,22 @@ let pr_universes g =
   prlist_with_sep pr_fnl (function (_,a) -> pr_arc a) graph
     
 
+(* Dumping constrains to a file *)
+
+let dump_universes output g = 
+  let dump_arc _ = function
+    | Canonical {univ=u; gt=gt; ge=ge} -> 
+	let u_str = string_of_univ u in
+	  List.iter 
+	    (fun v -> 
+	       Printf.fprintf output "%s > %s ;\n" u_str (string_of_univ v)) 
+	    gt;
+	  List.iter 
+	    (fun v -> 
+	       Printf.fprintf output "%s >= %s ;\n" u_str (string_of_univ v)) 
+	    ge
+    | Equiv (u,v) ->
+	Printf.fprintf output "%s = %s ;\n" (string_of_univ u) (string_of_univ v)
+  in
+    UniverseMap.iter dump_arc g 
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4348a65415..9c717ec31e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -65,3 +65,9 @@ val merge_constraints : constraints -> universes -> universes
 
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
+
+val string_of_univ : universe -> string
+
+(*s Dumping to a file *)
+
+val dump_universes : out_channel -> universes -> unit
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 37725ab7bb..85bd1a3e5f 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -483,7 +483,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 
     | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
     | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
-    | Node(loc,"TYPE", []) -> RSort(loc,RType)
+    | Node(loc,"TYPE", _) -> RSort(loc,RType None)
 	  
     (* This case mainly parses things build in a quotation *)
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
@@ -706,7 +706,7 @@ let interp_type_with_implicits sigma env impls c =
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
-  | Node(loc,"TYPE", []) -> Type Univ.dummy_univ
+  | Node(loc,"TYPE", _) -> Type Univ.dummy_univ
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let judgment_of_rawconstr sigma env c =
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f4edcd5440..f3d066f2f4 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -106,6 +106,12 @@ GEXTEND Gram
       | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg ->
           <:ast< (PrintGrammar $uni $ent) >>
 
+      (* Dump of the universe graph - to file or to stdout *) 
+      | IDENT "Dump"; IDENT "Universes"; f = stringarg ->
+	  <:ast< (DumpUniverses $f) >>
+      | IDENT "Dump"; IDENT "Universes" ->
+	  <:ast< (DumpUniverses) >>
+
       | IDENT "Locate"; IDENT "File"; f = stringarg ->
 	  <:ast< (LocateFile $f) >>
       | IDENT "Locate"; IDENT "Library"; id = identarg ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 18ef4b3ac2..448aa148a6 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -49,6 +49,10 @@ let print_implicits_explicit_args = ref false
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
+(* This forces printing universe names of Type{.} *)
+let print_universes = ref false
+
+
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
@@ -58,6 +62,7 @@ let with_arguments f = with_option print_arguments f
 let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
+let with_universes f = with_option print_universes f
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -261,7 +266,8 @@ let rec ast_of_raw = function
       (match s with
 	 | RProp Null -> ope("PROP",[])
 	 | RProp Pos -> ope("SET",[])
-	 | RType -> ope("TYPE",[]))
+	 | RType (Some u) when !print_universes -> ope("TYPE",[ide(Univ.string_of_univ u)])
+	 | RType _ -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
 	
@@ -389,7 +395,7 @@ let rec ast_of_pattern env = function
       (match s with
 	 | RProp Null -> ope("PROP",[])
 	 | RProp Pos -> ope("SET",[])
-	 | RType -> ope("TYPE",[]))
+	 | RType _ -> ope("TYPE",[]))
 
   | PMeta (Some n) -> ope("META",[num n])
   | PMeta None -> ope("ISEVAR",[])
diff --git a/parsing/termast.mli b/parsing/termast.mli
index df18bc27ee..31dd7d25c4 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -42,8 +42,10 @@ val print_casts : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
+val print_universes : bool ref
 
 val with_casts : ('a -> 'b) -> 'a -> 'b
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
 val with_coercions : ('a -> 'b) -> 'a -> 'b
+val with_universes : ('a -> 'b) -> 'a -> 'b
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 170de079b7..9ce397dd44 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -291,7 +291,7 @@ let rec detype avoid env t =
     | IsMeta n -> RMeta (dummy_loc, n)
     | IsVar id -> RVar (dummy_loc, id)
     | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-    | IsSort (Type _) -> RSort (dummy_loc,RType)
+    | IsSort (Type u) -> RSort (dummy_loc,RType (Some u))
     | IsCast (c1,c2) ->
 	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
     | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 01ccd27fa3..f423777d9b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -171,7 +171,7 @@ let matches_core convert pat c =
 
       | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma
 
-      | PSort RType, IsSort (Type _) -> sigma
+      | PSort (RType _), IsSort (Type _) -> sigma
 
       | PApp (c1,arg1), IsApp (c2,arg2) ->
         (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
@@ -309,7 +309,7 @@ let rec pattern_of_constr t =
     | IsMeta n -> PMeta (Some n)
     | IsVar id -> PVar id
     | IsSort (Prop c) -> PSort (RProp c)
-    | IsSort (Type _) -> PSort RType
+    | IsSort (Type _) -> PSort (RType None)
     | IsCast (c,_)      -> pattern_of_constr c
     | IsLetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | IsProd (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d2855a64ff..9fd30dfc86 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -194,7 +194,7 @@ let pretype_ref _ isevars env lvar ref =
 *)
 let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
-  | RType ->
+  | RType _ ->
       { uj_val = dummy_sort;
 	uj_type = dummy_sort }
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index e7b5bd5efe..053c6c39b7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -26,7 +26,7 @@ type cases_pattern =
   | PatCstr of
       loc * (constructor_path * identifier list) * cases_pattern list * name
 
-type rawsort = RProp of Term.contents | RType
+type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 18e3b1a1f4..0106fc60ab 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -25,7 +25,7 @@ type cases_pattern =
   | PatCstr of
       loc * (constructor_path * identifier list) * cases_pattern list * name
 
-type rawsort = RProp of Term.contents | RType
+type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 8590ee7c18..436b2b8136 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -43,7 +43,7 @@ Syntax constr
     prop [ Prop ] -> ["Prop"]
   | set  [ Set ]  -> ["Set"]
   | type [ Type ] -> ["Type"]
-  | type_sp [ << (TYPE ($PATH $sp) ($NUM $n)) >> ] -> ["Type"]
+  | type_sp [ << (TYPE $id) >> ] -> ["Type" $id]
 (* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
    Printer to know if they must be qualified or not (and previously to
    deal with the duality CCI/FW) *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1010ec1c38..2a840558f2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1755,3 +1755,18 @@ let _ = vinterp_add "PrintMLModules"
 	  (function 
 	     | [] -> (fun () -> Mltop.print_ml_modules ())
 	     | _ -> anomaly "PrintMLModules : does not expect an argument")
+
+let _ = vinterp_add "DumpUniverses"
+	  (function
+	     | [] -> (fun () -> pP (Univ.pr_universes (Global.universes ())))
+	     | [VARG_STRING s] ->
+		 (fun () -> let output = open_out s in
+		    try
+		      Univ.dump_universes output (Global.universes ());
+		      close_out output;
+		      mSG [<'sTR ("Universes written to file \""^s^"\"."); 'fNL >] 
+		    with
+			e -> close_out output; raise e
+		 )
+	     | _ -> 
+		 anomaly "DumpUniverses : expects a filename or nothing as argument")