- avoid redefinition of the same uri (checked in add_*_to_worls)

- defined add_inductive_def_to_world
- append owner to baseuri to minimize uri conflicts
- do not clear console!

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index b891f4e9457c2d059d710445dbc61ee03a42e270..8039e48222351b8e845f80ee02f0519fc6dedabd 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -46,9 +46,9 @@ let uri name =
   UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)
 *)
 
-let baseuri = ref "cic:/matita"
+let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner"))
 let qualify name =
-  let baseuri = !baseuri in
+  let baseuri = !(Lazy.force baseuri) in
   if baseuri.[String.length baseuri - 1] = '/' then
     baseuri ^ name
   else
@@ -149,11 +149,12 @@ class sharedState
             (* do nothing, just for compatibility with coq syntax *)
           New_state Command
       | TacticAst.Command (TacticAst.Baseuri (Some uri)) ->
-          baseuri := uri;
+          Lazy.force baseuri := uri;
           console#echo_message (sprintf "base uri set to \"%s\"" uri);
           Quiet
       | TacticAst.Command (TacticAst.Baseuri None) ->
-          console#echo_message (sprintf "base uri is \"%s\"" !baseuri);
+          console#echo_message (sprintf "base uri is \"%s\""
+            !(Lazy.force baseuri));
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
           let (_, _, term,ugraph) = 
@@ -260,13 +261,53 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
     * - save object to disk in xml format
     * - register uri to the getter 
     * - save universe file *)
-let add_constant_to_world ~dbd ~uri ?body ~ty ?(attrs = []) ~ugraph () =
-  let name = UriManager.name_of_uri uri in
-  let obj = Cic.Constant (name, body, ty, [], attrs) in
-  let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_term uri (obj, ugraph);
-  MetadataDb.index_constant ~dbd
-    ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty
+let add_constant_to_world ~(console:MatitaTypes.console)
+  ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph ()
+=
+  let suri = UriManager.string_of_uri uri in
+  if CicEnvironment.in_library uri then
+    error (sprintf "%s constant already defined" suri)
+  else begin
+    let name = UriManager.name_of_uri uri in
+    let obj = Cic.Constant (name, body, ty, params, attrs) in
+    let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+    CicEnvironment.add_type_checked_term uri (obj, ugraph);
+    MetadataDb.index_constant ~dbd
+      ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty;
+    console#echo_message (sprintf "%s constant defined" suri)
+  end
+
+let add_inductive_def_to_world ~(console:MatitaTypes.console)
+  ~dbd ~uri ~indTypes ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph ()
+=
+  let suri = UriManager.string_of_uri uri in
+  if CicEnvironment.in_library uri then
+    error (sprintf "%s inductive type already defined" suri)
+  else begin
+    let name = UriManager.name_of_uri uri in
+    let obj = Cic.InductiveDefinition (indTypes, params, leftno, attrs) in
+    let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+    CicEnvironment.put_inductive_definition uri (obj, ugraph);
+    MetadataDb.index_inductive_def ~dbd
+      ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
+    console#echo_message (sprintf "%s inductive type defined" suri);
+    let elim sort =
+      try
+        let obj = CicElim.elim_of ~sort uri 0 in
+        let (name, body, ty, attrs) = split_obj obj in
+        let suri = qualify name ^ ".con" in
+        let uri = UriManager.uri_of_string suri in
+          (* TODO Zack: make CicElim returns a universe *)
+        let ugraph = CicUniv.empty_ugraph in
+        add_constant_to_world ~console ~dbd ~uri ?body ~ty ~attrs ~ugraph ();
+(*
+        console#echo_message
+          (sprintf "%s eliminator (automatically) defined" suri)
+*)
+      with CicElim.Can_t_eliminate -> ()
+    in
+    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+  end
 
   (** Implements phrases that should be accepted only in Command state *)
 class commandState
@@ -310,9 +351,10 @@ class commandState
           in
           let body = CicMetaSubst.apply_subst subst body_cic in
           let ty = CicMetaSubst.apply_subst subst type_cic in
-          add_constant_to_world ~dbd ~uri ~body ~ty ~ugraph ();
+          add_constant_to_world ~console ~dbd ~uri ~body ~ty ~ugraph ();
           Quiet
       | TacticAst.Command (TacticAst.Inductive (params, indTypes)) ->
+          
           let (uri, (indTypes, params, leftno)) =
             inddef_of_ast params indTypes disambiguator
           in
@@ -320,25 +362,9 @@ class commandState
           let ugraph =
             CicTypeChecker.typecheck_mutual_inductive_defs uri
               (indTypes, params, leftno) CicUniv.empty_ugraph
-         in
-          let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in 
-          CicEnvironment.put_inductive_definition uri (obj, ugraph);
-          MetadataDb.index_inductive_def ~dbd
-            ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
-          let elim sort =
-            try
-              let obj = CicElim.elim_of ~sort uri 0 in
-              let (name, body, ty, attrs) = split_obj obj in
-              let suri = qualify name ^ ".con" in
-              let uri = UriManager.uri_of_string suri in
-                (* TODO Zack: make CicElim returns a universe *)
-              let ugraph = CicUniv.empty_ugraph in
-              add_constant_to_world ~dbd ~uri ?body ~ty ~attrs ~ugraph ();
-              console#echo_message
-                (sprintf "%s eliminator (automatically) defined" suri)
-            with CicElim.Can_t_eliminate -> ()
           in
-          List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+          add_inductive_def_to_world ~console
+            ~dbd ~uri ~indTypes ~params ~leftno ~ugraph ();
           Quiet
       | TacticAst.Command TacticAst.Quit ->
           currentProof#quit ();
@@ -453,7 +479,7 @@ class proofState
            CicReduction.are_convertible [] proved_ty ty ugraph 
          in
           if not b then failwith "Wrong proof";
-          add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph ();
+          add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
           currentProof#abort ();
           (match mathViewer with None -> () | Some v -> v#unload ());
           console#echo_message (sprintf "%s defined" suri);
@@ -496,7 +522,7 @@ class interpreter
       | _ -> ()
 
     method private eval f =
-      let ok () = console#clear (); (true, true) in
+      let ok () = (* console#clear (); *) (true, true) in
       match console#wrap_exn f with
       | Some (New_state Command) -> (state <- commandState); ok ()
       | Some (New_state Proof) -> (state <- proofState); ok ()