disambiguation even more abstracted

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 219ed6cd850949ed2d72c9f85fcd250693990466..4d7655f6dd65234e0128bbd2884c0813f9c85a54 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -45,19 +45,71 @@ let singleton msg = function
       in
       HLog.debug debug; assert false
 
+
+let lookup_in_library interactive_user_uri_choice input_or_locate_uri item =
+  let dbd = LibraryDb.instance () in
+  let choices_of_id id =
+    let uris = Whelp.locate ~dbd id in
+    let uris =
+     match uris with
+      | [] ->
+         (match 
+           (input_or_locate_uri 
+             ~title:("URI matching \"" ^ id ^ "\" unknown.") 
+             ?id:(Some id) ()) 
+         with
+         | None -> []
+         | Some uri -> [uri])
+      | [uri] -> [uri]
+      | _ ->
+          interactive_user_uri_choice ~selection_mode:`MULTIPLE
+           ?ok:(Some "Try selected.") 
+           ?enable_button_for_non_vars:(Some true)
+           ~title:"Ambiguous input."
+           ~msg: ("Ambiguous input \"" ^ id ^
+              "\". Please, choose one or more interpretations:")
+           ~id
+           uris
+    in
+    List.map
+      (fun uri ->
+        (UriManager.string_of_uri uri,
+         let term =
+           try
+             CicUtil.term_of_uri uri
+           with exn ->
+             assert false
+          in
+         fun _ _ _ -> term))
+      uris
+  in
+  match item with
+  | DisambiguateTypes.Id id -> choices_of_id id
+  | DisambiguateTypes.Symbol (symb, _) ->
+   (try
+     List.map DisambiguateChoices.mk_choice
+      (TermAcicContent.lookup_interpretations symb)
+    with
+     TermAcicContent.Interpretation_not_found -> [])
+  | DisambiguateTypes.Num instance ->
+    DisambiguateChoices.lookup_num_choices ()
+;;
+
   (** @param term not meaningful when context is given *)
-let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
+let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+term =
   let lexicon_status = !lexicon_status_ref in
-  let (diff, metasenv, cic, _) =
+  let (diff, metasenv, subst, cic, _) =
     singleton "first"
-      (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+      (GrafiteDisambiguator.disambiguate_term
         ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-        ~context ~metasenv (text,prefix_len,term))
+        ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~lookup_in_library
+        ~context ~metasenv ~subst:[] (text,prefix_len,term))
   in
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status_ref := lexicon_status;
-  metasenv,cic
+  metasenv,(*subst,*) cic
 ;;
 
   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
@@ -65,15 +117,15 @@ let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
    * each invocation will disambiguate the term and can add aliases. Once all
    * disambiguations have been performed, the first returned function can be
    * used to obtain the resulting aliases *)
-let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
+let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
   (fun context metasenv ugraph ->
     let lexicon_status = !lexicon_status_ref in
-    let (diff, metasenv, cic, ugraph) =
+    let (diff, metasenv, _, cic, ugraph) =
       singleton "second"
-        (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+        (GrafiteDisambiguator.disambiguate_term ~lookup_in_library 
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-          ~context ~metasenv
+          ~context ~metasenv ~subst:[] ?goal
           (text,prefix_len,term)) in
     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
     lexicon_status_ref := lexicon_status;
@@ -91,7 +143,7 @@ let disambiguate_pattern
       None -> None
     | Some wanted ->
        let wanted = 
-         disambiguate_lazy_term text prefix_len lexicon_status_ref wanted 
+         disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted 
        in
        Some wanted
   in
@@ -100,7 +152,8 @@ let disambiguate_pattern
 
 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
   | `Unfold (Some t) ->
-      let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
+      let t = 
+         disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
       `Unfold (Some t)
   | `Normalize
   | `Simpl
@@ -133,18 +186,20 @@ let disambiguate_just disambiguate_term context metasenv =
 ;;
       
 let rec disambiguate_tactic 
-  lexicon_status_ref context metasenv (text,prefix_len,tactic) 
+  lexicon_status_ref context metasenv goal (text,prefix_len,tactic) 
 =
+  let disambiguate_term_hint = 
+    disambiguate_term goal text prefix_len lexicon_status_ref in
   let disambiguate_term = 
-    disambiguate_term text prefix_len lexicon_status_ref in
+    disambiguate_term None text prefix_len lexicon_status_ref in
   let disambiguate_pattern = 
     disambiguate_pattern text prefix_len lexicon_status_ref in
   let disambiguate_reduction_kind = 
     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
   let disambiguate_lazy_term = 
-    disambiguate_lazy_term text prefix_len lexicon_status_ref in
+    disambiguate_lazy_term None text prefix_len lexicon_status_ref in
   let disambiguate_tactic metasenv tac =
-   disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac)
+   disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
   in
   let disambiguate_auto_params m p = 
     disambiguate_auto_params disambiguate_term m context p
@@ -207,6 +262,9 @@ let rec disambiguate_tactic
     | GrafiteAst.Apply (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Apply (loc, cic)
+    | GrafiteAst.ApplyRule (loc, term) ->
+        let metasenv,cic = disambiguate_term_hint context metasenv term in
+        metasenv,GrafiteAst.ApplyRule (loc, cic)
     | GrafiteAst.ApplyP (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.ApplyP (loc, cic)
@@ -449,9 +507,9 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-  let (diff, metasenv, cic, _) =
+  let (diff, metasenv, _, cic, _) =
     singleton "third"
-      (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+      (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
         (text,prefix_len,obj)) in
@@ -463,7 +521,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Index(loc,key,uri) ->
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
-        disambiguate_term text prefix_len lexicon_status_ref [] in
+        disambiguate_term None text prefix_len lexicon_status_ref [] in
        let disambiguate_term_option metasenv =
         function
              None -> metasenv,None
@@ -476,7 +534,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Coercion (loc,t,b,a,s) -> 
        let lexicon_status_ref = ref lexicon_status in 
        let disambiguate_term =
-        disambiguate_term text prefix_len lexicon_status_ref [] in
+        disambiguate_term None text prefix_len lexicon_status_ref [] in
       let metasenv,t = disambiguate_term metasenv t in
       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
    | GrafiteAst.Default _
@@ -493,7 +551,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
       let lexicon_status_ref = ref lexicon_status in 
       let disambiguate_term =
-       disambiguate_term text prefix_len lexicon_status_ref [] in
+       disambiguate_term None text prefix_len lexicon_status_ref [] in
       let disambiguate_term_option metasenv =
        function
           None -> metasenv,None
@@ -512,7 +570,9 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
 let disambiguate_macro 
   lexicon_status_ref metasenv context (text,prefix_len, macro) 
 =
- let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in
+ let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
+  let disambiguate_reduction_kind = 
+    disambiguate_reduction_kind text prefix_len lexicon_status_ref in
   match macro with
    | GrafiteAst.WMatch (loc,term) ->
       let metasenv,term = disambiguate_term context metasenv term in
@@ -529,6 +589,10 @@ let disambiguate_macro
    | GrafiteAst.Check (loc,term) ->
       let metasenv,term = disambiguate_term context metasenv term in
        metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.Eval (loc,kind,term) ->
+      let metasenv, term = disambiguate_term context metasenv term in
+      let kind = disambiguate_reduction_kind kind in
+       metasenv,GrafiteAst.Eval (loc,kind,term)
    | GrafiteAst.AutoInteractive (loc, params) -> 
       let metasenv, params = 
         disambiguate_auto_params disambiguate_term metasenv context params in