X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaCicMisc.ml;h=dbb80c791ab9833f3b675cc8bae22c65e5aa85e5;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=c77ded6be1d2271d3dbf0bfd7738d878f2333620;hpb=e3c0cc9893402419e363ad6616a599f194438273;p=helm.git

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index c77ded6be..dbb80c791 100644
--- a/helm/matita/matitaCicMisc.ml
+++ b/helm/matita/matitaCicMisc.ml
@@ -23,6 +23,8 @@
  * 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
@@ -35,3 +37,35 @@ let cicConstant (uri, metasenv, bo, ty) =
     (* TODO CSC: Wrong: [] is just plainly wrong *)
   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
+    ([], [])
+