From 61c55501b5ef3f3362b65d8172c1b5085594a4c2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Apr 2007 13:18:15 +0000 Subject: [PATCH] pattern with match fixed --- .../components/cic_disambiguation/disambiguate.ml | 11 ++++++++--- .../components/cic_disambiguation/disambiguate.mli | 3 +-- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 1a3183625..64a469cab 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -172,9 +172,10 @@ let find_in_context name context = in aux 1 context -let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast +let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast ~localization_tbl = + (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); let rec aux ~localize loc (context: Cic.name list) = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> @@ -217,6 +218,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast do_branch' context args in let (indtype_uri, indtype_no) = + if create_dummy_ids then + (UriManager.uri_of_string "cic:/fake_indty.con", 0) + else match indty_ident with | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with @@ -459,7 +463,8 @@ let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in (* here we are throwing away useful localization informations!!! *) fst ( - interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true + interpretate_term ~create_dummy_ids:true + ~context ~env:Environment.empty ~uri:None ~is_path:true path ~localization_tbl, localization_tbl) let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = @@ -1184,7 +1189,7 @@ in refine_profiler.HExtlib.profile foo () disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term - ~interpretate_thing:interpretate_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index 123fcf969..c1a50aceb 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -41,8 +41,7 @@ exception NoWellTypedInterpretation of exception PathNotWellFormed val interpretate_path : - context:Cic.name list -> CicNotationPt.term -> - Cic.term + context:Cic.name list -> CicNotationPt.term -> Cic.term type 'a disambiguator_input = string * int * 'a -- 2.39.2