From 430d6307ae5776ed000a78358a2881cb88936c37 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Nov 2008 17:17:02 +0000 Subject: [PATCH] new disambiguator almost attached --- .../acic_content/termAcicContent.ml | 10 +- .../acic_content/termAcicContent.mli | 7 +- .../cic_disambiguation/disambiguateChoices.ml | 18 ++- .../disambiguateChoices.mli | 14 ++- .../grafite_parser/grafiteDisambiguate.ml | 113 +++++++++++++----- .../components/lexicon/lexiconEngine.ml | 4 +- .../components/ng_kernel/oCic2NCic.mli | 2 +- helm/software/matita/matitaExcPp.ml | 4 + 8 files changed, 123 insertions(+), 49 deletions(-) diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 470ab6b3f..61e77c6fe 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -470,7 +470,9 @@ let remove_interpretation id = let _ = load_patterns32 [] -let instantiate_appl_pattern env appl_pattern = +let instantiate_appl_pattern + ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern += let lookup name = try List.assoc name env with Not_found -> @@ -478,10 +480,10 @@ let instantiate_appl_pattern env appl_pattern = assert false in let rec aux = function - | Ast.UriPattern uri -> CicUtil.term_of_uri uri - | Ast.ImplicitPattern -> Cic.Implicit None + | Ast.UriPattern uri -> term_of_uri uri + | Ast.ImplicitPattern -> mk_implicit false | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms) + | Ast.ApplPattern terms -> mk_appl (List.map aux terms) in aux appl_pattern diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli index aec8d598c..91438d248 100644 --- a/helm/software/components/acic_content/termAcicContent.mli +++ b/helm/software/components/acic_content/termAcicContent.mli @@ -65,8 +65,11 @@ val ast_of_acic: (** @param env environment from argument_pattern to cic terms * @param pat cic_appl_pattern *) val instantiate_appl_pattern: - (string * Cic.term) list -> CicNotationPt.cic_appl_pattern -> - Cic.term + mk_appl:('term list -> 'term) -> + mk_implicit:(bool -> 'term) -> + term_of_uri : (UriManager.uri -> 'term) -> + (string * 'term) list -> CicNotationPt.cic_appl_pattern -> + 'term val push: unit -> unit val pop: unit -> unit diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml index bf14623d7..ed3f82fe8 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml @@ -44,7 +44,7 @@ let lookup_num_by_dsc dsc = List.find (has_description dsc) !num_choices with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc))) -let mk_choice (dsc, args, appl_pattern) = +let mk_choice ~mk_appl ~mk_implicit ~term_of_uri (dsc, args, appl_pattern)= dsc, (fun env _ cic_args -> let env',rest = @@ -66,18 +66,26 @@ let mk_choice (dsc, args, appl_pattern) = "The notation " ^ dsc ^ " expects more arguments"))) in let combined = - TermAcicContent.instantiate_appl_pattern env' appl_pattern + TermAcicContent.instantiate_appl_pattern + ~mk_appl ~mk_implicit ~term_of_uri env' appl_pattern in match rest with [] -> combined - | _::_ -> Cic.Appl (combined::rest)) + | _::_ -> mk_appl (combined::rest)) -let lookup_symbol_by_dsc symbol dsc = +let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri symbol dsc = try - mk_choice + mk_choice~mk_appl ~mk_implicit ~term_of_uri (List.find (fun (dsc', _, _) -> dsc = dsc') (TermAcicContent.lookup_interpretations symbol)) with TermAcicContent.Interpretation_not_found | Not_found -> raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc))) +let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc + ~mk_implicit:(function + | true -> Cic.Implicit (Some `Type) + | false -> Cic.Implicit None) + ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l) + ~term_of_uri:CicUtil.term_of_uri +;; diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.mli b/helm/software/components/cic_disambiguation/disambiguateChoices.mli index a229a772f..f40c7aa9f 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.mli +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.mli @@ -44,10 +44,20 @@ val lookup_num_by_dsc: string -> Cic.term codomain_item (** @param symbol symbol as per AST * @param dsc description (1st component of codomain_item) *) -val lookup_symbol_by_dsc: string -> string -> Cic.term codomain_item +val lookup_symbol_by_dsc: + mk_appl: ('term list -> 'term) -> + mk_implicit: (bool -> 'term) -> + term_of_uri: (UriManager.uri -> 'term) -> + string -> string -> 'term codomain_item + +val cic_lookup_symbol_by_dsc: + string -> string -> Cic.term codomain_item val mk_choice: + mk_appl: ('term list -> 'term) -> + mk_implicit: (bool -> 'term) -> + term_of_uri: (UriManager.uri -> 'term) -> string * CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern -> - Cic.term codomain_item + 'term codomain_item diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 33d7273e8..e53272387 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -45,12 +45,58 @@ let singleton msg = function in HLog.debug debug; assert false +let cic_codomain_of_uri uri = + (UriManager.string_of_uri uri, + let term = + try + CicUtil.term_of_uri uri + with exn -> + assert false + in + fun _ _ _ -> term) +;; + +let cic_num_choices = DisambiguateChoices.lookup_num_choices;; + +let cic_mk_choice = + DisambiguateChoices.mk_choice + ~mk_implicit:(function + | true -> Cic.Implicit (Some `Type) + | false -> Cic.Implicit None) + ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l) + ~term_of_uri:CicUtil.term_of_uri +;; + +let ncic_codomain_of_uri uri = + (UriManager.string_of_uri uri, + let term = + try + fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) + with exn -> + assert false + in + fun _ _ _ -> term) +;; + +let ncic_num_choices _ = assert false;; -let lookup_in_library interactive_user_uri_choice input_or_locate_uri item = +let ncic_mk_choice = + DisambiguateChoices.mk_choice + ~mk_implicit:(function + | true -> NCic.Implicit `Closed + | false -> NCic.Implicit `Term) + ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) + ~term_of_uri:(fun uri -> + fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) +;; + +let lookup_in_library + codomain_of_uri mk_choice num_choices + 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 @@ -70,29 +116,17 @@ let lookup_in_library interactive_user_uri_choice input_or_locate_uri item = "\". 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.Id id -> + let uris = choices_of_id id in + List.map codomain_of_uri uris | DisambiguateTypes.Symbol (symb, _) -> (try - List.map DisambiguateChoices.mk_choice - (TermAcicContent.lookup_interpretations symb) + List.map mk_choice (TermAcicContent.lookup_interpretations symb) with TermAcicContent.Interpretation_not_found -> []) - | DisambiguateTypes.Num instance -> - DisambiguateChoices.lookup_num_choices () + | DisambiguateTypes.Num instance -> num_choices () ;; (** @param term not meaningful when context is given *) @@ -104,7 +138,8 @@ term = (CicDisambiguate.disambiguate_term ~aliases:lexicon_status.LexiconEngine.aliases ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~lookup_in_library + ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice + cic_num_choices) ~context ~metasenv ~subst:[] (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in @@ -122,7 +157,9 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, _, cic, ugraph) = singleton "second" - (CicDisambiguate.disambiguate_term ~lookup_in_library + (CicDisambiguate.disambiguate_term + ~lookup_in_library:(lookup_in_library cic_codomain_of_uri + cic_mk_choice cic_num_choices) ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~context ~metasenv ~subst:[] ?goal @@ -495,7 +532,6 @@ let rec disambiguate_tactic | `Proof as t -> metasenv,t in metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) - let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let uri = match obj with @@ -507,28 +543,39 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in - (* +(* (match obj with CicNotationPt.Theorem (_,_,ty,_) -> (try - let [_,_,_,ty],_ = - NMultiPassDisambiguator.disambiguate_term + (match + NCicDisambiguate.disambiguate_term + ~lookup_in_library:(lookup_in_library ncic_codomain_of_uri + ncic_mk_choice ncic_num_choices) ~context:[] ~metasenv:[] ~subst:[] ~aliases:DisambiguateTypes.Environment.empty ~universe:(Some DisambiguateTypes.Environment.empty) ("",0,ty) - in + with + | [_,metasenv,subst,ty],_ -> prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!! " ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty) - with NMultiPassDisambiguator.DisambiguationError _ -> - prerr_endline "ERRORE NUOVA DISAMBIGUAZIONE"; - assert false - | exn -> ()) + NCicPp.ppterm ~metasenv ~subst ~context:[] ty) + | _ -> + prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! ")) + with + | MultiPassDisambiguator.DisambiguationError (_,s) -> + prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE:\n" ^ + String.concat "\n" + (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s))) +(* | exn -> prerr_endline (Printexc.to_string exn) *) + ) | _ -> () - ); *) + ); +*) let (diff, metasenv, _, cic, _) = singleton "third" - (CicDisambiguate.disambiguate_obj ~lookup_in_library + (CicDisambiguate.disambiguate_obj + ~lookup_in_library:(lookup_in_library cic_codomain_of_uri cic_mk_choice + cic_num_choices) ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri (text,prefix_len,obj)) in diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index f48ffe400..cd7b0123d 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -152,7 +152,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] | LexiconAst.Symbol_alias (symb, instance, desc) -> [DisambiguateTypes.Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc] + DisambiguateChoices.cic_lookup_symbol_by_dsc symb desc] | LexiconAst.Number_alias (instance,desc) -> [DisambiguateTypes.Num instance, DisambiguateChoices.lookup_num_by_dsc desc] @@ -163,7 +163,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let diff = try [DisambiguateTypes.Symbol (symbol, 0), - DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] + DisambiguateChoices.cic_lookup_symbol_by_dsc symbol dsc] with DisambiguateChoices.Choice_not_found msg -> prerr_endline (Lazy.force msg); diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index b1351ae28..02ee706ef 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -16,4 +16,4 @@ val nuri_of_ouri: UriManager.uri -> NUri.uri val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list -(* val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list *) +val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 0671037a3..7fa7ea8c5 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -140,6 +140,10 @@ let rec to_string = | CicRefine.RefineFailure msg | CicRefine.AssertFailure msg -> None, "Refiner error: " ^ Lazy.force msg + | NCicRefiner.RefineFailure msg -> + None, "NRefiner failure: " ^ snd (Lazy.force msg) + | NCicRefiner.AssertFailure msg -> + None, "NRefiner assert failure: " ^ Lazy.force msg | CicTypeChecker.TypeCheckerFailure msg -> None, "Type checking error: " ^ Lazy.force msg | CicTypeChecker.AssertFailure msg -> -- 2.39.2