From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Dec 2004 13:43:58 +0000 (+0000)
Subject: sync with universes and ~subst (and not ?(subst=[]))
X-Git-Tag: V_0_1_0~173
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bec70852905f57198cd5b659dc72d430c1c5d2c;p=helm.git

sync with universes and ~subst (and not ?(subst=[]))
---

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index bb7f2807d..46341acfd 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -72,8 +72,9 @@ class disambiguator
         | Some env -> (false, env)
         | None -> (true, _env)
       in
-      match disambiguate_term ~dbd context metasenv termAst ~aliases:env with
-      | [ (env, metasenv, term) as x ] ->
+      match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph 
+	~dbd context metasenv termAst ~aliases:env with
+      | [ (env, metasenv, term,ugraph) as x ] ->
           if save_state then self#setEnv env;
           x
       | _ -> assert false
diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 5933f6227..a1bc1dd9e 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -78,7 +78,7 @@ let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
     let metasenv = proof#metasenv in
     let goal = proof#goal in
     let context = canonical_context goal metasenv in
-    let (_, metasenv, term) as retval =
+    let (_, metasenv, term,ugraph) as retval =
       disambiguator#disambiguateTermAst ~context ~metasenv ast
     in
     proof#set_metasenv metasenv;
@@ -155,10 +155,15 @@ class sharedState
           console#echo_message (sprintf "base uri is \"%s\"" !baseuri);
           None
       | TacticAst.Command (TacticAst.Check term) ->
-          let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
+          let (_, _, term,ugraph) = 
+	    disambiguate ~disambiguator ~proof_handler term 
+	  in
           let (context, metasenv) = get_context_and_metasenv proof_handler in
           let dummyno = CicMkImplicit.new_meta metasenv [] in
-          let ty = CicTypeChecker.type_of_aux' metasenv context term in
+          let ty,ugraph1 = 
+	    CicTypeChecker.type_of_aux' metasenv context term ugraph 
+	  in
+	    (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
           let sequent = (dummyno, context, expr) in
           let widget = Lazy.force check_widget in
@@ -185,7 +190,9 @@ class commandState
     method evalTactical = function
       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
       | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
-          let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
+          let (_, metasenv, expr,ugraph) = 
+	    disambiguator#disambiguateTermAst ast 
+	  in
           let uri = UriManager.uri_of_string (qualify name) in
           let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in
           proof_handler.MatitaTypes.new_proof proof;
@@ -211,7 +218,7 @@ let namer_of names =
       incr count;
       name
     end else
-      FreshNamesGenerator.mk_fresh_name metasenv context name ~typ
+      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
   (** Implements phrases that should be accepted only in `Proof state, basically
   * tacticals *)
@@ -223,7 +230,9 @@ class proofState
   ()
 =
   let disambiguate ast =
-    let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
+    let (_, _, term,ugraph) = 
+      disambiguate ~disambiguator ~proof_handler ast 
+    in
     term
   in
     (** tactic AST -> ProofEngineTypes.tactic *)
@@ -292,18 +301,27 @@ class proofState
           let (uri, metasenv, bo, ty) = proof#proof in
           let uri = MatitaTypes.unopt_uri uri in
           if metasenv <> [] then failwith "Proof not completed";
-          let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
-          if not (CicReduction.are_convertible [] proved_ty ty) then
+          let proved_ty,ugraph = 
+	    CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
+	  in
+	  let b,ugraph1 = 
+	    CicReduction.are_convertible [] proved_ty ty ugraph 
+	  in
+          if not b then
             failwith "Wrong proof";
           (* TODO Zack [] probably wrong *)
+	  let ugraph2 = CicUniv.fill_empty_nodes_with_uri ugraph1 uri in
           CicEnvironment.add_type_checked_term uri
-            (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+            ((Cic.Constant ((UriManager.name_of_uri uri),
+			    (Some bo),ty,[])),
+	     ugraph2);
           proof_handler.MatitaTypes.set_proof None;
           (MatitaMathView.proof_viewer_instance ())#unload;
           (* TODO Zack a lot more to be done here:
             * - save object to disk in xml format
             * - collect metadata
-            * - register uri to the getter *)
+            * - register uri to the getter 
+	    * - save universe file *)
           Some `Command
       | TacticAst.Seq tacticals ->
           (* TODO Zack check for proof completed at each step? *)
diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index e9657d191..cd9d34f08 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -74,13 +74,13 @@ class type disambiguator =
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
       (** @param env @see disambiguateTerm above *)
     method disambiguateTermAst:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) 
   end
 
 (*