* 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.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
+ ([], [])
+