From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 11 Dec 2002 10:48:13 +0000 (+0000)
Subject: * Partial checking of mutual inductive definitions allowed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c9e3f24bf6a98e69f2297da23392069ec298da1;p=helm.git

* Partial checking of mutual inductive definitions allowed.
* New environment variables requested:
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   POSTGRESQL_CONNECTION_STRING
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 89e56bafc..c78c5caff 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -27,7 +27,7 @@
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
 (*                                                                            *)
-(*                Claudio Sacerdoti Coen <natile@cs.unibo.it>               *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
 (*                                 06/01/2002                                 *)
 (*                                                                            *)
 (*                                                                            *)
@@ -60,53 +60,42 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/natile/currentproof";;
-let prooffiletype = "/public/natile/currentprooftype";;
-
-(* SACERDOT
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
-*)
-
-(* NATILE
-let prooffile = "/public/natile/currentproof";;
-let prooffiletype = "/public/natile/currentprooftype";;
-*)
-
-(* TASSI
-let prooffile = "//miohelm/tmp/currentproof";;
-let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
-*)
+let prooffile =
+ try
+  Sys.getenv "GTOPLEVEL_PROOFFILE"
+ with
+  Not_found -> "/public/currentproof"
+;;
 
-(* GALATA
-let prooffile = "/home/galata/miohelm/currentproof";;
-let prooffiletype = "/home/galata/miohelm/currentprooftype";;
-*)
+let prooffiletype =
+ try
+  Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
+ with
+  Not_found -> "/public/currentprooftype"
+;;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
 
-let innertypesfile = "/public/natile/innertypes";;
-let constanttypefile = "/public/natile/constanttype";;
-
-(* SACERDOT
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
-*)
-
-(* NATILE
-let innertypesfile = "/public/natile/innertypes";;
-let constanttypefile = "/public/natile/constanttype";;
-*)
+let innertypesfile =
+ try
+  Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
+ with
+  Not_found -> "/public/innertypes"
+;;
 
-(* TASSI
-let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
-let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
-*)
+let constanttypefile =
+ try
+  Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
+ with
+  Not_found -> "/public/constanttype"
+;;
 
-(* GALATA
-let innertypesfile = "/home/galata/miohelm/innertypes";;
-let constanttypefile = "/home/galata/miohelm/constanttype";;
-*)
+let postgresqlconnectionstring =
+ try
+  Sys.getenv "POSTGRESQL_CONNECTION_STRING"
+ with
+  Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
+;;
 
 let empty_id_to_uris = ([],function _ -> None);;
 
@@ -1630,27 +1619,22 @@ let new_inductive () =
                | _ -> raise AmbiguousInput
            ) names type_widgets
          in
-          (* Let's see if so far the definition is well-typed *)
           let uri = !get_uri () in
-          let params = [] in
-          let paramsno = 0 in
-          let tys =
-           let i = ref 0 in
+          let _ =
+           (* Let's see if so far the definition is well-typed *)
+           let params = [] in
+           let paramsno = 0 in
+           (* To test if the arities of the inductive types are well *)
+           (* typed, we check the inductive block definition where   *)
+           (* no constructor is given to each type.                  *)
+           let tys =
             List.map2
-             (fun name (ty,cons) ->
-               let cons' =
-                List.map
-                 (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in
-               let res = (name, !inductive, ty, cons') in
-                incr i ;
-                res
-             ) names types_and_cons
+             (fun name (ty,cons) -> (name, !inductive, ty, []))
+             names types_and_cons
+           in
+            CicTypeChecker.typecheck_mutual_inductive_defs uri
+             (tys,params,paramsno)
           in
-(*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi
-  anche quando paramsno > 0 ;-((((
-           CicTypeChecker.typecheck_mutual_inductive_defs uri
-            (tys,params,paramsno) ;
-*)
            get_name_context_context_and_subst :=
             (function () ->
               let i = ref 0 in
@@ -3474,9 +3458,7 @@ let _ =
  if !usedb then
   begin
    Mqint.set_database Mqint.postgres_db ;
-   (* Mqint.init "dbname=helm_mowgli" ; *)
-   (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
-   Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm";
+   Mqint.init postgresqlconnectionstring ;
   end ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;