snapshot, notably:

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index c9d5a71612d7e1893c11b033307b518d54759eec..78d30c4cd062a16898dc16eff268fce257940a91 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -60,38 +60,6 @@ let split_obj = function
   | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
   | _ -> assert false
 
-let canonical_context metano metasenv =
-  try
-    let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
-    context
-  with Not_found ->
-    failwith (sprintf "Can't find canonical context for %d" metano)
-
-let get_context_and_metasenv (currentProof:MatitaTypes.currentProof) =
-  if currentProof#onGoing () then
-    let proof = currentProof#proof in
-    let metasenv = proof#metasenv in
-    let goal = proof#goal in
-    (canonical_context goal metasenv, metasenv)
-  else
-    ([], [])
-
-  (** term AST -> Cic.term. Uses disambiguator and change imperatively the
-  * metasenv as needed *)
-let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast =
-  if currentProof#onGoing () then begin
-    let proof = currentProof#proof in
-    let metasenv = proof#metasenv in
-    let goal = proof#goal in
-    let context = canonical_context goal metasenv in
-    let (_, metasenv, term,ugraph) as retval =
-      disambiguator#disambiguateTermAst ~context ~metasenv ast
-    in
-    proof#set_metasenv metasenv;
-    retval
-  end else
-    disambiguator#disambiguateTermAst ast
-
 class virtual interpreterState = 
     (* static values, shared by all states inheriting this class *)
   let loc = ref None in
@@ -167,9 +135,11 @@ class sharedState
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
           let (_, _, term,ugraph) = 
-           disambiguate ~disambiguator ~currentProof term 
+           MatitaCicMisc.disambiguate ~disambiguator ~currentProof term 
          in
-          let (context, metasenv) = get_context_and_metasenv currentProof in
+          let (context, metasenv) =
+            MatitaCicMisc.get_context_and_metasenv currentProof
+          in
 (* this is the Eval Compute
           let term = CicReduction.whd context term in
 *)         
@@ -179,10 +149,9 @@ class sharedState
          in
            (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
-          let sequent = (dummyno, context, expr) in
           (match mathViewer with
-          | None -> ()
-          | Some v -> v#checkTerm sequent metasenv);
+          | Some v -> v#checkTerm (`Cic expr)
+          | _ -> ());
           Quiet
       | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
           let uris =
@@ -557,7 +526,9 @@ class proofState
   ()
 =
   let disambiguate ast =
-    let (_, _, term, _) = disambiguate ~disambiguator ~currentProof ast in
+    let (_, _, term, _) =
+      MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+    in
     term
   in
     (** tactic AST -> ProofEngineTypes.tactic *)
@@ -638,7 +609,6 @@ class proofState
           if not b then failwith "Wrong proof";
           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);
           New_state Command
       | TacticAst.Seq tacticals ->