disambiguation can use a goal as hint for the expected type

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 9effb6ae466b301b5896e783e0f600397cb73f05..248baa195e8cc5c2a958d20d1293cd921ae8cb3c 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -935,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 ->
@@ -957,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 ->
@@ -1025,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)
@@ -1122,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
@@ -1319,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
@@ -1333,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)
@@ -1340,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

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index 78fe417683e33dd6e03cce852851cfa608cf86cd..c94273804e70a1f0bdafc7409bb282dfa9f7d377 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -61,8 +61,11 @@ sig
   val disambiguate_thing:
     dbd:HSql.dbd ->
     context:'context ->
-    metasenv:'metasenv ->
+    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 ->
@@ -95,7 +98,7 @@ sig
     ?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 ->

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index f55b1fed0e646de07d387aacfad9aae8bc60d11f..fe5ee7fe378942f14c08ebe923a7a689698af4b4 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -405,6 +405,39 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
+            let rec count_prods context ty =
+              match CicReduction.whd context ty with
+              | Cic.Prod (n,s,t) -> 
+                 1 + count_prods (Some (n,Cic.Decl s)::context) t
+              | _ -> 0
+            in
+            let exp_prods = count_prods context ty' in
+            let inf_prods = count_prods context inferredty in
+            let te', inferredty, metasenv'', subst'', ugraph2 =
+               let rec aux t m s ug it = function
+                 | 0 -> t,it,m,s,ug
+                 | n ->
+                      match CicReduction.whd context it with
+                      | Cic.Prod (_,src,tgt) -> 
+                          let newmeta, metaty, s, m, ug =
+                            type_of_aux s m context (Cic.Implicit None) ug
+                          in
+                          let s,m,ug = 
+                            fo_unif_subst s context m metaty src ug
+                          in
+(*                           prerr_endline "saturo"; *)
+                          let t =
+                            match t with
+                            | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+                            | _ -> Cic.Appl [t;newmeta]
+                          in
+                          aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+                      | _ -> t,it,m,s,ug     
+               in
+                 aux te' metasenv'' subst'' ugraph2 inferredty
+                   (max 0 (inf_prods - exp_prods))
+            in
+(*             prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
             let (te', ty'), subst''',metasenv''',ugraph3 =
               coerce_to_something true localization_tbl te' inferredty ty'
                 subst'' metasenv'' context ugraph2

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 560e680b46718f9794cb34a3ce4f971c0f97b098..c700c836b456e334f3acd7b862600fc3f2519cec 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -63,6 +63,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Real tactics *)
   | Absurd of loc * 'term
   | Apply of loc * 'term
+  | ApplyRule of loc * 'term
   | ApplyP of loc * 'term (* apply for procedural reconstruction *)
   | ApplyS of loc * 'term * 'term auto_params
   | Assumption of loc

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8e23e56b5357b6e2664e5548e95d5f3660d022d6..9d8d41537fdcbbb198c67a3b031c278a06a82b40 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -114,6 +114,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyRule (_, term) -> "apply rule " ^ term_pp term
   | ApplyP (_, term) -> "applyP " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 2efbc68115c35cc7ba4a74626ffcab92dae938de..d9c4608492dc9e02e6d664265ec2bfbfb9628d79 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -82,6 +82,7 @@ let rec tactic_of_ast status ast =
   (* First order tactics *)
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyRule (_, term) -> Tactics.apply term
   | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 47e7a86276ad3fe2af11f54c35bb14421ac15065..8983fdcb91806243117ca6088b512bdab2ba6fa2 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -46,13 +46,13 @@ 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, _) =
     singleton "first"
       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
-        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
         ~context ~metasenv (text,prefix_len,term))
   in
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
@@ -65,7 +65,7 @@ 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) =
@@ -73,7 +73,7 @@ let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
         (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 ?goal
           (text,prefix_len,term)) in
     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
     lexicon_status_ref := lexicon_status;
@@ -91,7 +91,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 +100,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 +134,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 +210,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)
@@ -463,7 +469,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 +482,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 +499,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 +518,7 @@ 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

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index f482741f34ca4ddc93f28dfb24fb53160e1111ff..1543387ee355af220bd16cef49974519505dfe82 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -37,7 +37,7 @@ type lazy_tactic =
 val disambiguate_tactic:
  LexiconEngine.status ref ->
  Cic.context ->
- Cic.metasenv ->
+ Cic.metasenv -> int option ->
  tactic Disambiguate.disambiguator_input ->
   Cic.metasenv * lazy_tactic
 

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index f83225c35d411203282d1bab13bf35877cfb5aeb..360d56f0285caf875a59defe370be8a8e1ae085c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -207,12 +207,12 @@ let drop_aliases_and_clear_diff (choices, user_asked) =
   (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
   user_asked
 
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?goal ?initial_ugraph
   ~aliases ~universe term
  =
   assert (fresh_instances = None);
   let f =
-    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?goal ?initial_ugraph
   in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff term

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 558eed081fbd845aa235c488b2bb176a4611cdd2..51c7d07b267b8bb33d1b9432612a728ffe7c032d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -183,6 +183,8 @@ EXTEND
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->
         GrafiteAst.Absurd (loc, t)
+    | IDENT "apply"; IDENT "rule"; t = tactic_term ->
+        GrafiteAst.ApplyRule (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
     | IDENT "applyP"; t = tactic_term ->