From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Nov 2002 09:54:54 +0000 (+0000)
Subject: Rendering of InductiveDefinitions, Variables and Axioms implemented.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6ab193f88745acd3def85e47d643a92efb2f9fc5;p=helm.git

Rendering of InductiveDefinitions, Variables and Axioms implemented.
---

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index 57d4fc7e4..d76df870e 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -251,8 +251,6 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-exception NotImplemented;;
-
 let print_object uri ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
@@ -341,7 +339,57 @@ let print_object uri ~ids_to_inner_sorts =
          >]
         in
          xmlty, xmlbo
-     | _ -> raise NotImplemented
+     | C.AVariable (id,n,bo,ty,params) ->
+        let params' = param_attribute_of_params params in
+        let xmlbo =
+         match bo with
+            None -> [< >]
+          | Some bo ->
+             X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+        in
+        let aobj =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
+             X.xml_nempty "Variable"
+              ["name",n ; "params",params' ; "id", id]
+              [< xmlbo ;
+                 X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+              >]
+         >]
+        in
+         aobj, None
+     | C.AInductiveDefinition (id,tys,params,nparams) ->
+        let params' = param_attribute_of_params params in
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+             dtdname ^ "\">\n") ;
+            X.xml_nempty "InductiveDefinition"
+             ["noParams",string_of_int nparams ;
+              "id",id ;
+              "params",params']
+             [< (List.fold_left
+                  (fun i (id,typename,finite,arity,cons) ->
+                    [< i ;
+                       X.xml_nempty "InductiveType"
+                        ["id",id ; "name",typename ;
+                         "inductive",(string_of_bool finite)
+                        ]
+                        [< X.xml_nempty "arity" []
+                            (print_term ids_to_inner_sorts arity) ;
+                           (List.fold_left
+                            (fun i (name,lc) ->
+                              [< i ;
+                                 X.xml_nempty "Constructor"
+                                  ["name",name]
+                                  (print_term ids_to_inner_sorts lc)
+                              >]) [<>] cons
+                           )
+                        >]
+                    >]
+                  ) [< >] tys
+                )
+             >]
+         >], None
  in
   aux
 ;;
diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 8d849634d..932771214 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented;;
-
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
@@ -303,8 +301,19 @@ let acic_object_of_cic_object obj =
        let aty = acic_term_of_cic_term' ty None in
         C.AConstant
          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
-    | C.Constant (id,None,ty,params) -> raise NotImplemented
-    | C.Variable (id,bo,ty,params) -> raise NotImplemented
+    | C.Constant (id,None,ty,params) ->
+       let aty = acic_term_of_cic_term' ty None in
+        C.AConstant
+         ("mettereaposto",None,id,None,aty, params)
+    | C.Variable (id,bo,ty,params) ->
+       let abo =
+        match bo with
+           None -> None
+         | Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
+       in
+       let aty = acic_term_of_cic_term' ty None in
+        C.AVariable
+         ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
        let aconjectures =
         List.map
@@ -357,7 +366,25 @@ let acic_object_of_cic_object obj =
        let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
-    | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
+    | C.InductiveDefinition (tys,params,paramsno) ->
+       let context =
+        List.map
+         (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
+       let idrefs = List.map (function _ -> gen_id seed) tys in
+       let atys =
+        List.map2
+         (fun id (name,inductive,ty,cons) ->
+           let acons =
+            List.map
+             (function (name,ty) ->
+               (name,
+                 acic_term_of_cic_term_context' [] context idrefs ty None)
+             ) cons
+           in
+            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
+         ) (List.rev idrefs) tys
+       in
+        C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
    in
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses
diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index bc174d121..0cd607bb6 100644
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -23,7 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented
 exception NotEnoughElements
 exception NameExpected