diff options
author | 2006-07-03 16:40:20 +0000 | |
---|---|---|
committer | 2006-07-03 16:40:20 +0000 | |
commit | 1e69c6a499757b05180205e84ed2bf6f1cbf7b2f (patch) | |
tree | 0b6c57991e1bd849593f846ae8b91ce18d9f9194 | |
parent | b7c3f0f2f57bcd0cc768c869d707b70f78c5bbfd (diff) |
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/interface/xlate.ml | 4 | ||||
-rw-r--r-- | interp/constrextern.ml | 4 | ||||
-rw-r--r-- | interp/constrintern.ml | 29 | ||||
-rw-r--r-- | interp/topconstr.ml | 2 | ||||
-rw-r--r-- | interp/topconstr.mli | 2 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 3 | ||||
-rw-r--r-- | parsing/ppconstr.ml | 4 |
7 files changed, 31 insertions, 17 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index e8fd52dba..2a11f55c9 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -336,8 +336,8 @@ and | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, List.map xlate_match_pattern l) and translate_one_equation = function - (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp, - xlate_formula a) + (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a) + | _ -> xlate_error "TODO: disjunctive multiple patterns" and xlate_binder_ne_list = function [] -> assert false diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a81ca599c..44f4baee6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -186,7 +186,7 @@ let rec check_same_type ty1 ty2 = | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> - List.iter2 check_same_pattern pl1 pl2; + List.iter2 (List.iter2 check_same_pattern) pl1 pl2; check_same_type r1 r2) brl1 brl2 | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () @@ -797,7 +797,7 @@ and extern_local_binder scopes vars = function LocalRawAssum([(dummy_loc,na)],ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = - (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, + (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_symbol (tmp_scope,scopes as allscopes) vars t = function diff --git a/interp/constrintern.ml b/interp/constrintern.ml index deb7abbde..aa9a379db 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -81,9 +81,8 @@ let explain_non_linear_pattern id = str "The variable " ++ pr_id id ++ str " is bound several times in pattern" let explain_bad_patterns_number n1 n2 = - let s = if n1 > 1 then "s" else "" in - str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found " - ++ int n2 + str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++ + str " but found " ++ int n2 let explain_bad_explicitation_number n po = match n with @@ -357,7 +356,8 @@ let rec has_duplicate = function | x::l -> if List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = - join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs)) + join_loc (cases_pattern_loc (List.hd (List.hd lhs))) + (cases_pattern_loc (list_last (list_last lhs))) let check_linearity lhs ids = match has_duplicate ids with @@ -929,11 +929,24 @@ let internalise sigma globalenv env allow_soapp lvar c = ((name_fold Idset.add na ids,ts,sc), (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) - and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) = + (* Expands a multiple pattern into a disjunction of multiple patterns *) + and intern_multiple_pattern scopes pl = let idsl_pll = - List.map (intern_cases_pattern globalenv scopes ([],[]) None) lhs in - - let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in + List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in + product_of_cases_patterns [] idsl_pll + + (* Expands a disjunction of multiple pattern *) + and intern_disjunctive_multiple_pattern scopes loc mpl = + assert (mpl <> []); + let mpl' = List.map (intern_multiple_pattern scopes) mpl in + let (idsl,mpl') = List.split mpl' in + let ids = List.hd idsl in + check_or_pat_variables loc ids (List.tl idsl); + (ids,List.flatten mpl') + + (* Expands a pattern-matching clause [lhs => rhs] *) + and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) = + let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; check_number_of_pattern loc n (snd (List.hd pll)); diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 6e7ea0f9c..855fcb329 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -515,7 +515,7 @@ type constr_expr = (constr_expr * explicitation located option) list | CCases of loc * constr_expr option * (constr_expr * (name option * constr_expr option)) list * - (loc * cases_pattern_expr list * constr_expr) list + (loc * cases_pattern_expr list list * constr_expr) list | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 57a2c976c..e06a48215 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -98,7 +98,7 @@ type constr_expr = (constr_expr * explicitation located option) list | CCases of loc * constr_expr option * (constr_expr * (name option * constr_expr option)) list * - (loc * cases_pattern_expr list * constr_expr) list + (loc * cases_pattern_expr list list * constr_expr) list | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 2a975a964..443a10511 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -274,7 +274,8 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; eqn: - [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] + [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; + "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] ; pattern: [ "200" RIGHTA [ ] diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 613fbfe78..92b07e08b 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -186,12 +186,12 @@ let rec pr_patt sep inh p = let pr_patt = pr_patt mt - let pr_eqn pr (loc,pl,rhs) = spc() ++ hov 4 (pr_with_comments loc (str "| " ++ - hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++ + hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function |