From f9ec0bd466364409050ffccc94e9cb863e2ddf28 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Nov 2006 15:01:04 +0000 Subject: [PATCH] Fixed bug in notation: when a notation is applied to more arguments than expected this is not necessarily a problem: I just create a new application on the fly. --- .../cic_disambiguation/disambiguateChoices.ml | 25 ++++++++++++++----- 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml index bdbc93179..64d2cf8e0 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml @@ -47,16 +47,29 @@ let lookup_num_by_dsc dsc = let mk_choice (dsc, args, appl_pattern) = dsc, (fun env _ cic_args -> - let env' = + let env',rest = let names = List.map (function CicNotationPt.IdentArg (_, name) -> name) args in - try - List.combine names cic_args - with Invalid_argument _ -> - raise (Invalid_choice (lazy "The notation expects a different number of arguments")) + let rec combine_with_rest l1 l2 = + match l1,l2 with + _::_,[] -> raise (Invalid_argument "combine_with_rest") + | [],rest -> [],rest + | he1::tl1,he2::tl2 -> + let l,rest = combine_with_rest tl1 tl2 in + (he1,he2)::l,rest + in + try + combine_with_rest names cic_args + with Invalid_argument _ -> + raise (Invalid_choice (lazy ("The notation " ^ dsc ^ " expects more arguments"))) in - TermAcicContent.instantiate_appl_pattern env' appl_pattern) + let combined = + TermAcicContent.instantiate_appl_pattern env' appl_pattern + in + match rest with + [] -> combined + | _::_ -> Cic.Appl (combined::rest)) let lookup_symbol_by_dsc symbol dsc = try -- 2.39.2