Few OCaml files in contrib/xml

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

4 files changed, 79 insertions, 157 deletions

diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index d0737b311..0c82ae669 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -8,7 +8,7 @@
 (*                                 17/11/1999                                 *)
 (******************************************************************************)
 
-Declare ML Module "xml" "cooking" "xmlcommand" "xmlentries".
+Declare ML Module "xml" "xmlcommand" "xmlentries".
 
 Grammar vernac vernac : Ast :=
   xml_print [ "Print" "XML" identarg($id) "." ] ->
diff --git a/contrib/xml/cooking.ml b/contrib/xml/cooking.ml
deleted file mode 100644
index 10c8d80ef..000000000
--- a/contrib/xml/cooking.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 02/12/1999                                 *)
-(*                                                                            *)
-(* This module compute the list of variables occurring in a term from the     *)
-(* term and the list of variables possibly occuring in it                     *)
-(*                                                                            *)
-(******************************************************************************)
-
-let get_depth_of_var vl v =
- let rec aux n =
-  function
-     [] -> None
-   | (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
- in
-  aux 0 vl
-;;
-
-exception CookingInternalError;;
-
-let string_of_vars_list =
- let add_prefix n s = string_of_int n ^ ": " ^ s in
- let rec aux =
-  function
-     [n,v] -> (n,v)
-   | (n,v)::tl ->
-      let (k,s) = aux tl in
-       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
-   | [] -> raise CookingInternalError
- in
-  function
-     [] -> ""
-   | vl -> let (k,s) = aux vl in add_prefix k s
-;;
-
-(*CSC commento sbagliato ed obsoleto *)
-(* If t is \v1. ... \vn.t' where v1, ..., vn are in the variable list vl then *)
-(* get_params_from_type vl t returns [v1; ...; vn]                            *)
-let get_params_from_type vl t =
- let rec rget t l =
-  let module T = Term in
-  let module N = Names in
-   match T.kind_of_term t with
-      T.IsProd (N.Name id, _, target) ->
-       let id' = N.string_of_id id in
-        (match get_depth_of_var vl id' with
-            None   -> l
-          | Some n -> rget target ((n,id')::l)
-        )
-    | T.IsCast (term, _) -> rget term l
-    | _ -> l
- in
-  let pl = List.rev (rget t []) in
-   string_of_vars_list pl
-;;
-
-(* add_cooking_information csp vl                               *)
-(*  when  csp is the section path of the most cooked object co  *)
-(*  and   vl  is the list of variables possibly occuring in co  *)
-(* returns the list of variables actually occurring in co       *)
-let add_cooking_information sp vl =
- let module D = Declarations in
- let module G = Global in
- let module N = Names in
- let module T = Term in
- let module X = Xml in
-  try
-   let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
-   let typ = T.body_of_type typ in
-    get_params_from_type vl typ
-  with
-   Not_found ->
-    try
-     let {D.mind_packets=packs ; D.mind_nparams=nparams} =
-      G.lookup_mind sp
-     in
-      let {D.mind_nf_arity=arity} = packs.(0) in
-      let arity = T.body_of_type arity in
-       get_params_from_type vl arity
-    with
-     Not_found -> Util.anomaly "Cooking of an uncoockable term required"
-;;
diff --git a/contrib/xml/cooking.mli b/contrib/xml/cooking.mli
deleted file mode 100644
index 6eb5b4330..000000000
--- a/contrib/xml/cooking.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     A tactic to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 17/11/1999                                 *)
-(*                                                                            *)
-(* This module compute the list of variables occurring in a term from the     *)
-(* term and the list of variables possibly occuring in it                     *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* add_cooking_information csp vl                               *)
-(*  when  csp is the section path of the most cooked object co  *)
-(*  and   vl  is the list of variables possibly occuring in co  *)
-(* returns the list of variables actually occurring in co       *)
-val add_cooking_information :
-  Names.section_path -> string list list -> string
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index d0cb0bf88..bb8ab6125 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -17,15 +17,6 @@
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 let verbose = ref false;; (* always set to true during a "Print XML All" *)
 
-
-
-exception ImpossiblePossible;;
-type formal_parameters =
-   Actual of string
- | Possible of string
-;;
-
-
 (* UTILITY FUNCTIONS *)
 
 let print_if_verbose s = if !verbose then print_string s;;
@@ -146,7 +137,23 @@ let string_of_name =
 (* list of variables availables in the actual section *)
 let pvars = ref [];;
 
-let pvars_to_string pvars =
+let string_of_vars_list =
+ let add_prefix n s = string_of_int n ^ ": " ^ s in
+ let rec aux =
+  function
+     [n,v] -> (n,v)
+   | (n,v)::tl ->
+      let (k,s) = aux tl in
+       if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
+   | [] -> assert false
+ in
+  function
+     [] -> ""
+   | vl -> let (k,s) = aux vl in add_prefix k s
+;;
+
+(*
+let string_of_pvars pvars hyps =
  let rec aux =
   function
      [] -> (0, "")
@@ -159,6 +166,20 @@ let pvars_to_string pvars =
  in
   snd (aux (List.rev pvars))
 ;;
+*)
+
+let string_of_pvars pvars hyps =
+ let find_depth pvars v =
+  let rec aux n =
+   function
+      [] -> assert false
+    | l::_ when List.mem v l -> (n,v)
+    | _::tl -> aux (n+1) tl
+  in
+   aux 0 pvars
+ in
+  string_of_vars_list (List.map (find_depth pvars) hyps)
+;;
 
 exception XmlCommandInternalError;;
 
@@ -370,38 +391,36 @@ let print_current_proof c typ id mv =
 (*  and   id          is the identifier (name) of a                        *)
 (*  and   params      is the list of formal params for a                   *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_axiom id typ fv =
+let print_axiom id typ fv hyps =
  let module X = Xml in
  let module N = Names in
   reset_id () ;
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
      X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
      X.xml_nempty "Axiom"
-      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
-       match fv with
-          Possible _ -> raise ImpossiblePossible
-        | Actual fv' -> ["params",fv']
-      ) [< X.xml_nempty "type" [] (print_term [] typ) >]
+      ["name",(N.string_of_id id) ;
+        "id", get_next_id () ;
+        "params",(string_of_pvars fv hyps)]
+      [< X.xml_nempty "type" [] (print_term [] typ) >]
   >]
 ;;
 
-(* print_definition id term type params                                    *)
+(* print_definition id term type params hyps                               *)
 (*  where id          is the identifier (name) of a definition d           *)
 (*  and   term        is the term (body) of d                              *)
 (*  and   type        is the type of d                                     *)
 (*  and   params      is the list of formal params for d                   *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_definition id c typ fv =
+let print_definition id c typ fv hyps =
  let module X = Xml in
  let module N = Names in
   reset_id () ;
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
      X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
      X.xml_nempty "Definition"
-      (["name",(N.string_of_id id) ; "id", get_next_id ()] @
-       match fv with
-          Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
-        | Actual fv' -> ["params",fv'])
+      ["name",(N.string_of_id id) ;
+       "id", get_next_id () ;
+       "params",(string_of_pvars fv hyps)]
       [< X.xml_nempty "body" [] (print_term [] c) ;
          X.xml_nempty "type"  [] (print_term [] typ) >]
   >]
@@ -464,7 +483,7 @@ let print_mutual_inductive_packet names p =
 (*  and   nparams     is the number of "parameters" in the arity of the    *)
 (*                    mutual inductive types                               *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_mutual_inductive packs fv nparams =
+let print_mutual_inductive packs fv hyps nparams =
  let module D = Declarations in
  let module X = Xml in
  let module N = Names in
@@ -478,10 +497,9 @@ let print_mutual_inductive packs fv nparams =
       X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
        dtdname ^ "\">\n\n") ;
       X.xml_nempty "InductiveDefinition"
-       (["noParams",string_of_int nparams ; "id",get_next_id ()] @
-        (match fv with
-            Possible fv' -> ["params",fv' ; "paramMode","POSSIBLE"]
-          | Actual fv' -> ["params",fv']))
+       ["noParams",string_of_int nparams ;
+        "id",get_next_id () ;
+        "params",(string_of_pvars fv hyps)]
        [< (Array.fold_right
             (fun x i -> [< print_mutual_inductive_packet names x ; i >])
             packs
@@ -491,6 +509,14 @@ let print_mutual_inductive packs fv nparams =
    >]
 ;;
 
+let string_list_of_named_context_list =
+ List.map
+  (function
+      (n,None,_) -> Names.string_of_id n
+    | _          -> assert false
+  )
+;;
+
 (* print id dest                                                          *)
 (*  where id   is the identifier (name) of a definition/theorem or of an  *)
 (*             inductive definition                                       *)
@@ -510,14 +536,16 @@ let print id fn =
   let pp_cmds =
    begin
     try
-     let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
+     let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+      G.lookup_constant sp in
+     let hyps = string_list_of_named_context_list hyps in
      let typ = T.body_of_type typ in
       begin
        match val0 with
-          None -> print_axiom id typ (Actual "")
+          None -> print_axiom id typ [] hyps
         | Some lcvr ->
            match !lcvr with
-              D.Cooked c -> print_definition id c typ (Actual "")
+              D.Cooked c -> print_definition id c typ [] hyps
             | D.Recipe _ ->
                print_string " COOKING THE RECIPE\n" ;
                ignore (D.cook_constant lcvr) ;
@@ -527,17 +555,18 @@ let print id fn =
                 begin
                  match val0 with
                    Some {contents= D.Cooked c} ->
-                    print_definition id c typ (Actual "")
+                    print_definition id c typ [] hyps
                  | _ -> Util.error "COOKING FAILED"
                 end
           end
     with
      Not_found ->
       try
-       let {D.mind_packets=packs ; D.mind_nparams=nparams} =
+       let {D.mind_packets=packs ; D.mind_nparams=nparams ; D.mind_hyps=hyps} =
         G.lookup_mind sp
        in
-        print_mutual_inductive packs (Actual "") nparams
+        let hyps = string_list_of_named_context_list hyps in
+         print_mutual_inductive packs [] hyps nparams
       with
        Not_found ->
         try
@@ -619,28 +648,29 @@ let print_object o id sp dn fv =
    match tag with
       "CONSTANT"  (* = Definition, Theorem *)
     | "PARAMETER" (* = Axiom *) ->
-         (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE const_hyps *)
-(*
-         let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
-*)
-let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = G.lookup_constant sp in
-if (Names.string_of_id id) = "SN" then
- List.iter (fun (id,_,_) -> print_string ("*** " ^ N.string_of_id id ^ "\n")) hyps ;
+        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
+         G.lookup_constant sp
+        in
+         let hyps = string_list_of_named_context_list hyps in
          let typ = T.body_of_type typ in
           begin
            match val0 with
-              None -> print_axiom id typ fv
+              None -> print_axiom id typ fv hyps
             | Some lcvr ->
                match !lcvr with
-                  D.Cooked c -> print_definition id c typ fv
+                  D.Cooked c -> print_definition id c typ fv hyps
                 | D.Recipe _ -> Util.anomaly "trying to print a recipe"
           end
     | "INDUCTIVE" ->
          (*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *)
-         let {D.mind_packets=packs ; D.mind_nparams=nparams} =
-          G.lookup_mind sp
+         let
+          {D.mind_packets=packs ;
+           D.mind_nparams=nparams ;
+           D.mind_hyps = hyps
+          } = G.lookup_mind sp
          in
-           print_mutual_inductive packs fv nparams
+          let hyps = string_list_of_named_context_list hyps in
+           print_mutual_inductive packs fv hyps nparams
     | "VARIABLE" ->
 (*V7 DON'T KNOW HOW TO DO IT
         let (_,typ) = G.lookup_named id in
@@ -698,7 +728,7 @@ and print_node n id sp bprintleaf dn =
             toprint := (id,sp,sp,o,!pvars,dn)::!toprint
            else
             (* this is a local term *)
-            print_object o id sp dn (Possible (pvars_to_string !pvars)) ;
+            print_object o id sp dn !pvars ;
             print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n")
           end
          else
@@ -738,7 +768,6 @@ and print_node n id sp bprintleaf dn =
 (* print_library_segment on all its sons                                     *)
 let print_closed_section s ls dn =
  let module L = Lib in
- let module C = Cooking in
   toprint := [] ;
   (*CSC: this should always be empty yet! But just to be sure... :-) *)
   pvars := [] ;
@@ -750,10 +779,10 @@ let print_closed_section s ls dn =
       (id,usp,csp,uo,pv,dn) ->
        print_if_verbose ("\nCooked=" ^ (Names.string_of_path csp) ^
         "\tUncooked=" ^ (Names.string_of_path usp)) ;
-       let formal_vars = C.add_cooking_information csp pv in
+       let formal_vars = pv in
         pvars := pv ;
         (*CSC Actual was Some *)
-        print_object uo id usp dn (Actual formal_vars)
+        print_object uo id usp dn formal_vars
    ) !toprint ;
   print_if_verbose "\n/Module\n" ;
 ;;