From f8edc256de5d8ae2126f01fdaf72ac91151d8ca6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 Aug 2005 09:39:12 +0000
Subject: [PATCH] A parser for aliases implemented (required by the Whelp).

---
 helm/matita/matita.txt                        |  2 ++
 helm/matita/matitaEngine.ml                   |  2 ++
 helm/ocaml/cic_disambiguation/Makefile        |  2 +-
 .../cic_disambiguation/disambiguatePp.ml      | 30 +++++++++++++++++++
 .../cic_disambiguation/disambiguatePp.mli     |  2 +-
 5 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index a8f18ea32..412879c9c 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -70,6 +70,8 @@ TODO
   - riattaccare hbugs (brrr...) -> Zack
 
   GUI LOGICA
+  - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro,
+    ora io (=CSC) ho messo anche un parser!!!)
   - verificare se tutte le query sono ora ottimizzate (usando il comando
     explain) e usano gli indici in maniera ottimale; inoltre migliorare gli
     indici sulle tabelle hits and count
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 24872ffd0..c2db06efa 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -598,6 +598,8 @@ let eval_command opts status cmd =
       eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let aliases =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
          DisambiguateTypes.Environment.add 
diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index dcc99fdec..064a1b2e1 100644
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -7,8 +7,8 @@ REQUIRES = \
 NOTATIONS = number
 INTERFACE_FILES =		\
 	disambiguateTypes.mli	\
-	disambiguatePp.mli	\
 	disambiguateChoices.mli	\
+	disambiguatePp.mli	\
 	disambiguate.mli
 IMPLEMENTATION_FILES = \
 	$(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index decaa5f5c..d6a33cfae 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -25,6 +25,36 @@
 
 open DisambiguateTypes
 
+let parse_environment str =
+ let stream = Stream.of_string str in
+ let environment = ref Environment.empty in
+  try
+    while true do
+     let alias =
+      match GrafiteParser.parse_statement stream with
+         GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
+           -> alias
+       | _ -> assert false in
+     let key,value =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in MatitaEngine *)
+      match alias with
+         GrafiteAst.Ident_alias (id,uri) ->
+          Id id,
+          (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+       | GrafiteAst.Symbol_alias (symb,instance,desc) ->
+          Symbol (symb,instance),
+          DisambiguateChoices.lookup_symbol_by_dsc symb desc
+       | GrafiteAst.Number_alias (instance,desc) ->
+          Num instance,
+          DisambiguateChoices.lookup_num_by_dsc desc
+     in
+      environment := Environment.add key value !environment;
+    done;
+    assert false
+  with End_of_file ->
+   !environment
+
 let pp_environment env =
   let aliases =
     Environment.fold
diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
index 985ba32fc..68cecfaa8 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli
@@ -23,5 +23,5 @@
  * http://helm.cs.unibo.it/
  *)
 
+val parse_environment: string -> DisambiguateTypes.environment
 val pp_environment: DisambiguateTypes.environment -> string
-
-- 
2.39.2