From 4c9e3f24bf6a98e69f2297da23392069ec298da1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Dec 2002 10:48:13 +0000 Subject: [PATCH] * Partial checking of mutual inductive definitions allowed. * New environment variables requested: GTOPLEVEL_PROOFFILE GTOPLEVEL_PROOFFILETYPE GTOPLEVEL_PROOFFILE GTOPLEVEL_PROOFFILETYPE POSTGRESQL_CONNECTION_STRING --- helm/gTopLevel/gTopLevel.ml | 108 +++++++++++++++--------------------- 1 file changed, 45 insertions(+), 63 deletions(-) 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 *) +(* Claudio Sacerdoti Coen *) (* 06/01/2002 *) (* *) (* *) @@ -60,53 +60,42 @@ let htmlfooter = "" ;; -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 () ; -- 2.39.2