From 83e22b5abc05902d1468d1cf033251dae46b69bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 17 Mar 2020 10:37:30 +0100 Subject: Renaming "ident" into "name" in grammar entries, to prevent confusions. We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle --- interp/constrintern.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8bd77abc4a..0645636255 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -976,6 +976,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_id {loc;v=id} = + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) @@ -991,16 +994,20 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> + let a,terms = match terms with a::terms -> a,terms | _ -> assert false in + let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr AsName -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> - let onlyident = (x = NtnParsedAsIdent) in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> + let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> -- cgit v1.2.3