disambiguation can use a goal as hint for the expected type

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index e11927d7d58fe6fb526a80f3347e7d56a5317727..248baa195e8cc5c2a958d20d1293cd921ae8cb3c 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -895,6 +895,8 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
+let domain_of_ast_term = domain_of_term;;
+
 let domain_of_term ~context term = 
  let context = 
    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context 
@@ -933,6 +935,9 @@ sig
     context:'context ->
     metasenv:'metasenv ->
     initial_ugraph:'ugraph ->
+    hint: ('metasenv -> 'raw_thing -> 'raw_thing) * 
+          (('refined_thing,'metasenv) test_result -> 'ugraph ->
+              ('refined_thing,'metasenv) test_result * 'ugraph) ->
     aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
     universe:DisambiguateTypes.codomain_item list
              DisambiguateTypes.Environment.t option ->
@@ -955,11 +960,12 @@ sig
     ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
      list * 'metasenv * 'refined_thing * 'ugraph)
     list * bool
+
   val disambiguate_term :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
     context:Cic.context ->
-    metasenv:Cic.metasenv ->
+    metasenv:Cic.metasenv -> ?goal:int ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
@@ -1023,7 +1029,8 @@ module Make (C: Callbacks) =
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
-      ~initial_ugraph ~aliases ~universe
+      ~initial_ugraph ~hint
+      ~aliases ~universe
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       ~localization_tbl
       (thing_txt,thing_txt_prefix_len,thing)
@@ -1120,10 +1127,12 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
             interpretate_thing ~context ~env:filled_env
              ~uri ~is_path:false thing ~localization_tbl
           in
+          let cic_thing = (fst hint) metasenv cic_thing in
 let foo () =
           let k,ugraph1 =
            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
           in
+          let k, ugraph1 = (snd hint) k ugraph1 in
             (k , ugraph1 )
 in refine_profiler.HExtlib.profile foo ()
         with
@@ -1317,13 +1326,28 @@ in refine_profiler.HExtlib.profile foo ()
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"
 
-    let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+    let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv 
+      ?goal
       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 
       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in
+      let hint = match goal with
+        | None -> (fun _ x -> x), fun k u -> k, u
+        | Some i ->
+            (fun metasenv t ->
+              let _,c,ty = CicUtil.lookup_meta i metasenv in
+              assert(c=context);
+              Cic.Cast(t,ty)),
+            function  
+            | Ok (t,m) -> fun ug ->
+                (match t with
+                | Cic.Cast(t,_) -> Ok (t,m), ug
+                | _ -> assert false) 
+            | k -> fun ug -> k, ug
+      in
       let localization_tbl = Cic.CicHash.create 503 in
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
@@ -1331,6 +1355,7 @@ in refine_profiler.HExtlib.profile foo ()
         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
         ~refine_thing:refine_term (text,prefix_len,term)
         ~localization_tbl
+        ~hint
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)
@@ -1338,12 +1363,18 @@ in refine_profiler.HExtlib.profile foo ()
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
+      let hint = 
+        (fun _ x -> x),
+        fun k u -> k, u
+      in
       let localization_tbl = Cic.CicHash.create 503 in
-      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
+      disambiguate_thing ~dbd ~context:[] ~metasenv:[] 
+        ~aliases ~universe ~uri
         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
         ~initial_ugraph:CicUniv.empty_ugraph
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         ~localization_tbl
+        ~hint
         (text,prefix_len,obj)
 
   end