From 154cbc049da8d8c3dd090a919a40c90eb23cc24e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 12:53:35 +0000 Subject: [PATCH] disambiguation can use a goal as hint for the expected type --- .../cic_disambiguation/disambiguate.ml | 37 +++++++++++++++++-- .../cic_disambiguation/disambiguate.mli | 7 +++- .../components/cic_unification/cicRefine.ml | 33 +++++++++++++++++ .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 1 + .../grafite_engine/grafiteEngine.ml | 1 + .../grafite_parser/grafiteDisambiguate.ml | 34 ++++++++++------- .../grafite_parser/grafiteDisambiguate.mli | 2 +- .../grafite_parser/grafiteDisambiguator.ml | 4 +- .../grafite_parser/grafiteParser.ml | 2 + 10 files changed, 99 insertions(+), 23 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 9effb6ae4..248baa195 100644 --- 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 78fe41768..c94273804 100644 --- 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 f55b1fed0..fe5ee7fe3 100644 --- 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 560e680b4..c700c836b 100644 --- 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 8e23e56b5..9d8d41537 100644 --- 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 2efbc6811..d9c460849 100644 --- 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 47e7a8627..8983fdcb9 100644 --- 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 f482741f3..1543387ee 100644 --- 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 f83225c35..360d56f02 100644 --- 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 558eed081..51c7d07b2 100644 --- 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 -> -- 2.39.2