X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaCicMisc.ml;h=dbb80c791ab9833f3b675cc8bae22c65e5aa85e5;hb=e1cb0f658f9b16009fe536fd315b621df1157a65;hp=523e33ea2458d86cf249251c22eded2aa5d97992;hpb=687d1d3676afa3f936c22855f9510b78d702ec4c;p=helm.git

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index 523e33ea2..dbb80c791 100644
--- a/helm/matita/matitaCicMisc.ml
+++ b/helm/matita/matitaCicMisc.ml
@@ -23,15 +23,49 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
   (** create a Cic.CurrentProof from a given proof *)
 let cicCurrentProof (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [], [])
 
   (** create a Cic.Constant from a given proof *)
 let cicConstant (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [])
+  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], [])
+
+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)
+
+  (** 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
+
+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
+    ([], [])