loc * lazy string -> (loc * string) lazy

[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 516c4af20301e1a6946995cbe44c60fd05491448..ad7f70ef1a331e3430228e74f4e88a71b57e689c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -46,18 +46,19 @@ let singleton msg = function
       HLog.debug debug; assert false
 
   (** @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 ())
         ~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)
+        ~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 +66,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 ())
           ~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 +92,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 +101,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
@@ -120,19 +122,33 @@ let disambiguate_auto_params
     metasenv, (terms, params)
 ;;
 
+let disambiguate_just disambiguate_term context metasenv =
+ function
+    `Term t ->
+      let metasenv,t = disambiguate_term context metasenv t in
+       metasenv, `Term t
+  | `Auto params ->
+      let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
+       context params
+      in
+       metasenv, `Auto params
+;;
+      
 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
@@ -195,6 +211,12 @@ 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)
     | GrafiteAst.ApplyS (loc, term, params) ->
         let metasenv, params = disambiguate_auto_params metasenv params in
         let metasenv,cic = disambiguate_term context metasenv term in
@@ -204,9 +226,10 @@ let rec disambiguate_tactic
     | GrafiteAst.AutoBatch (loc,params) ->
         let metasenv, params = disambiguate_auto_params metasenv params in
         metasenv,GrafiteAst.AutoBatch (loc,params)
-    | GrafiteAst.Cases (loc, what, idents) ->
+    | GrafiteAst.Cases (loc, what, pattern, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.Cases (loc, what, idents)
+       let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in
@@ -339,14 +362,11 @@ let rec disambiguate_tactic
                  let metasenv,t = disambiguate_term context metasenv t in
                  metasenv,Some t in
        metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
-    | GrafiteAst.Bydone (loc,term) ->
-        let metasenv,cic = 
-          match term with
-             None -> metasenv,None
-            |Some t ->
-                 let metasenv,t = disambiguate_term context metasenv t in
-                metasenv,Some t in
-                metasenv,GrafiteAst.Bydone (loc, cic)
+    | GrafiteAst.Bydone (loc,just) ->
+        let metasenv,just =
+         disambiguate_just disambiguate_term context metasenv just
+        in
+        metasenv,GrafiteAst.Bydone (loc, just)
     | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
        let metasenv,cic' = 
@@ -356,13 +376,9 @@ let rec disambiguate_tactic
                  let metasenv,t = disambiguate_term context metasenv t in
                  metasenv,Some t in
        metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
-    | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
-        let metasenv,cic =
-          match term with 
-            None -> metasenv,None
-          | Some t ->
-                let metasenv,t = disambiguate_term context metasenv t in
-                metasenv,Some t in
+    | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
+        let metasenv,just =
+         disambiguate_just disambiguate_term context metasenv just in
         let metasenv,cic' = disambiguate_term context metasenv term' in
        let metasenv,cic'' = 
            match term'' with
@@ -370,7 +386,7 @@ let rec disambiguate_tactic
           |  Some t ->  
                    let metasenv,t = disambiguate_term context metasenv t in
                     metasenv,Some t in
-       metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+       metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
     | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
        let metasenv,cic' = disambiguate_term context metasenv term' in
@@ -385,21 +401,18 @@ let rec disambiguate_tactic
    | GrafiteAst.Thesisbecomes (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
        metasenv,GrafiteAst.Thesisbecomes (loc, cic)
-   | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
-       let metasenv,cic =
-           match term with
-             None -> metasenv,None
-           | Some t ->
-                 let metasenv,t = disambiguate_term context metasenv t in
-                 metasenv,Some t in
+   | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
+       let metasenv,just =
+         disambiguate_just disambiguate_term context metasenv just in
         let metasenv,cic' = disambiguate_term context metasenv term1 in
        let cic''= disambiguate_lazy_term term2 in
-       metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
-   | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
-       let metasenv,cic = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
+   | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
+       let metasenv,just =
+         disambiguate_just disambiguate_term context metasenv just in
        let metasenv,cic'= disambiguate_term context metasenv term1 in
        let metasenv,cic''= disambiguate_term context metasenv term2 in
-       metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')   
+       metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')   
    | GrafiteAst.Case (loc, id, params) ->
         let metasenv,params' =
         List.fold_right
@@ -443,7 +456,7 @@ 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 ())
         ~aliases:lexicon_status.LexiconEngine.aliases
@@ -457,7 +470,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
@@ -467,7 +480,12 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
        in
        let metasenv,key = disambiguate_term_option metasenv key in
        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
-   | GrafiteAst.Coercion _
+   | GrafiteAst.Coercion (loc,t,b,a,s) -> 
+       let lexicon_status_ref = ref lexicon_status in 
+       let disambiguate_term =
+        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 _
    | GrafiteAst.Drop _
    | GrafiteAst.Include _
@@ -482,7 +500,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
@@ -501,7 +519,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
@@ -518,6 +538,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