snapshot, notably:

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

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index c77ded6be1d2271d3dbf0bfd7738d878f2333620..e6cda30240771ca2c9abc452ee6dc8676dd2ca3e 100644 (file)
--- 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
+    ([], [])
+