diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 01:04:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:05 +0100 |
| commit | 00bfd6fa443232bc908cfa13553e2fa1cf783ffa (patch) | |
| tree | 6790ecc2f7b4e6882d049d751f63fc3bc761f0ef /interp | |
| parent | 6480c7e1d89558252f2e8a8f1b7d3b03f7ef6a74 (diff) | |
Preliminary work before extending support for binders in notations
(binders shall be substitutable by arbitrary cases patterns).
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8e2e3bd23..5c9a12c29 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -442,6 +442,22 @@ let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) = (push_name_env ntnvars (impls_term_list term) env locna, (na,Explicit,term,ty)) +let intern_cases_pattern_as_binder ?loc ntnvars env p = + let il,cp = + match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with + | (il, [(subst,cp)]) -> + if not (Id.Map.equal Id.equal subst Id.Map.empty) then + user_err ?loc (str "Unsupported nested \"as\" clause."); + il,cp + | _ -> assert false + in + let env = {env with ids = List.fold_right Id.Set.add il env.ids} in + let na = alias_of_pat cp in + let ienv = Name.fold_right Id.Set.remove na env.ids in + let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in + let na = (loc, Name id) in + env,((cp,il),id),na + let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern ntnvars env nal bk ty in @@ -456,19 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func | Some ty -> ty | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) in - let il,cp = - match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with - | (il, [(subst,cp)]) -> - if not (Id.Map.equal Id.equal subst Id.Map.empty) then - user_err ?loc (str "Unsupported nested \"as\" clause."); - il,cp - | _ -> assert false - in - let env = {env with ids = List.fold_right Id.Set.add il env.ids} in - let na = alias_of_pat cp in - let ienv = Name.fold_right Id.Set.remove na env.ids in - let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in - let na = (loc, Name id) in + let env, ((cp,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in |