First committed version that (may) use the MathML editor to enter formulas.

[helm.git] / helm / gTopLevel / disambiguate.ml

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index c0e1818e1d18532c6fe480c6f00d05e81112b463..afa47790ac3254173e4b2f708e8a2d570ba0d9f9 100644 (file)
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -51,6 +51,12 @@ let get_last_query =
 
 module type Callbacks =
   sig
+    (* The following two functions are used to save/restore the metasenv *)
+    (* before/after the parsing.                                         *)
+    (*CSC: This should be made functional sooner or later! *)
+    val get_metasenv : unit -> Cic.metasenv
+    val set_metasenv : Cic.metasenv -> unit
+
     val output_html : string -> unit
     val interactive_user_uri_choice :
       selection_mode:[`SINGLE | `EXTENDED] ->
@@ -64,7 +70,8 @@ module type Callbacks =
 ;;
 
 type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+  CicTextualParser0.interpretation
 ;;
 
 module Make(C:Callbacks) =
@@ -110,6 +117,10 @@ module Make(C:Callbacks) =
     | Ko
     | Uncertain
 
+   type ambiguous_choices =
+      Uris of CicTextualParser0.uri list
+    | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
+
    let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
     let known_ids,resolve_id = id_to_uris in
     let dom' =
@@ -122,13 +133,29 @@ module Make(C:Callbacks) =
       filter dom
     in
      (* for each id in dom' we get the list of uris associated to it *)
-     let list_of_uris = List.map locate_one_id dom' in
+     let list_of_uris =
+      List.map
+       (function
+           CicTextualParser0.Id id -> Uris (locate_one_id id)
+         | CicTextualParser0.Symbol (descr,choices) ->
+            (* CSC: Implementare la funzione di filtraggio manuale *)
+            (* CSC: corrispondente alla locate_one_id              *)
+            Symbols (List.map snd choices)
+       ) dom' in
      let tests_no =
-      List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+      List.fold_left
+       (fun i uris ->
+         let len =
+          match uris with
+             Uris l -> List.length l
+           | Symbols l -> List.length l
+         in
+          i * len
+       ) 1 list_of_uris
      in
       if tests_no > 1 then
        C.output_html
-        ("<h1>Disambiguation phase started: " ^
+        ("<h1>Disambiguation phase started: up to " ^
           string_of_int tests_no ^ " cases will be tried.") ;
      (* and now we compute the list of all possible assignments from *)
      (* id to uris that generate well-typed terms                    *)
@@ -137,25 +164,19 @@ module Make(C:Callbacks) =
       let test resolve_id residual_dom =
        (* We put implicits in place of every identifier that is not *)
        (* resolved by resolve_id                                    *)
-       let resolve_id'' =
-        let resolve_id' =
-         function id ->
-          match resolve_id id with
-             None -> None
-           | Some uri -> Some (CicTextualParser0.Uri uri)
-        in
-         List.fold_left
-          (fun f id ->
-            function id' ->
-             if id = id' then Some (CicTextualParser0.Implicit) else f id'
-          ) resolve_id' residual_dom
+       let resolve_id' =
+        List.fold_left
+         (fun f id ->
+           function id' ->
+            if id = id' then Some (CicTextualParser0.Implicit) else f id'
+         ) resolve_id residual_dom
        in
         (* and we try to refine the term *)
-        let saved_status = !CicTextualParser0.metasenv in
-        let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
+        let saved_status = C.get_metasenv () in
+        let metasenv',expr = mk_metasenv_and_expr resolve_id' in
 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
         (* The parser is imperative ==> we must restore the old status ;-(( *)
-        CicTextualParser0.metasenv := saved_status ;
+        C.set_metasenv saved_status ;
          try
           let term,_,_,metasenv'' =
            CicRefine.type_of_aux' metasenv' context expr
@@ -185,7 +206,7 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
            let rec filter =
             function
                [] -> []
-             | uri::uritl ->
+             | (uri : CicTextualParser0.interpretation_codomain_item)::uritl ->
                 let resolve_id' =
                  function id' -> if id = id' then Some uri else resolve_id id'
                 in
@@ -207,7 +228,14 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
                       filter uritl
                  )
            in
-            filter uris
+            (match uris with
+                Uris uris ->
+                 filter
+                  (List.map (function uri -> CicTextualParser0.Uri uri) uris)
+              | Symbols symbols ->
+                 filter
+                  (List.map
+                    (function sym -> CicTextualParser0.Term sym) symbols))
         | _,_ -> assert false
       in
        aux resolve_id dom' list_of_uris
@@ -236,20 +264,27 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
             (function (resolve,_,_) ->
               List.map
                (function id ->
-                 id,
+                 (match id with
+                     CicTextualParser0.Id id -> id
+                   | CicTextualParser0.Symbol (descr,_) -> descr
+                 ),
                   match resolve id with
                      None -> assert false
-                   | Some uri ->
-                      match uri with
-                         CicTextualParser0.ConUri uri
-                       | CicTextualParser0.VarUri uri ->
-                          UriManager.string_of_uri uri
-                       | CicTextualParser0.IndTyUri (uri,tyno) ->
-                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
-                           string_of_int (tyno+1) ^ ")"
-                       | CicTextualParser0.IndConUri (uri,tyno,consno) ->
-                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
-                           string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
+                   | Some (CicTextualParser0.Uri uri) ->
+                      (match uri with
+                          CicTextualParser0.ConUri uri
+                        | CicTextualParser0.VarUri uri ->
+                           UriManager.string_of_uri uri
+                        | CicTextualParser0.IndTyUri (uri,tyno) ->
+                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+                            string_of_int (tyno+1) ^ ")"
+                        | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+                            string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")")
+                   | Some (CicTextualParser0.Term term) ->
+                      (* CSC: Implementare resa delle scelte *)
+                      "To be implemented XXX01"
+                   | Some CicTextualParser0.Implicit -> assert false
                ) dom
             ) resolve_ids
           in