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

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 5933f6227124a6f3709d3c90e5d7b0e551747c1e..a1bc1dd9ed2fa0776b9b8d8ad98a25cecfd50345 100644 (file)
--- 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? *)