snapshot, notably:

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index bb43d67e0ae950159bb249a45d09262cb46bbaff..b891f4e9457c2d059d710445dbc61ee03a42e270 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -54,8 +54,8 @@ let qualify name =
   else
     String.concat "/" [baseuri; name]
 let split_obj = function
-  | Cic.Constant (name, body, ty, _)
-  | Cic.Variable (name, body, ty, _) -> (name, body, ty)
+  | Cic.Constant (name, body, ty, _, attrs)
+  | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
   | _ -> assert false
 
 let canonical_context metano metasenv =
@@ -260,9 +260,9 @@ 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 ~ugraph () =
+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, []) 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
@@ -316,7 +316,7 @@ class commandState
           let (uri, (indTypes, params, leftno)) =
             inddef_of_ast params indTypes disambiguator
           in
-          let obj = Cic.InductiveDefinition (indTypes, params, leftno) in
+          let obj = Cic.InductiveDefinition (indTypes, params, leftno, []) in
           let ugraph =
             CicTypeChecker.typecheck_mutual_inductive_defs uri
               (indTypes, params, leftno) CicUniv.empty_ugraph
@@ -325,20 +325,21 @@ class commandState
           CicEnvironment.put_inductive_definition uri (obj, ugraph);
           MetadataDb.index_inductive_def ~dbd
             ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
-          let msgs = ref [] in
           let elim sort =
             try
               let obj = CicElim.elim_of ~sort uri 0 in
-              let (name, body, ty) = split_obj obj in
-              let uri = UriManager.uri_of_string (qualify name ^ ".con") 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 ~ugraph ();
-              msgs := (sprintf "%s defined" name) :: !msgs;
+              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 ())) ];
-          Echo (String.concat "\n" (List.rev !msgs))
+          Quiet
       | TacticAst.Command TacticAst.Quit ->
           currentProof#quit ();
           New_state Command (* dummy answer, useless *)
@@ -441,6 +442,7 @@ class proofState
           let proof = currentProof#proof in
           let (uri, metasenv, bo, ty) = proof#proof in
           let uri = MatitaTypes.unopt_uri uri in
+          let suri = UriManager.string_of_uri uri in
             (* TODO Zack this function probably should not simply fail with
             * Failure, but rather raise some more meaningful exception *)
           if metasenv <> [] then failwith "Proof not completed";
@@ -454,6 +456,7 @@ class proofState
           add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph ();
           currentProof#abort ();
           (match mathViewer with None -> () | Some v -> v#unload ());
+          console#echo_message (sprintf "%s defined" suri);
           New_state Command
       | TacticAst.Seq tacticals ->
           (* TODO Zack check for proof completed at each step? *)