Using the same type of binders for interning and externing.

Previously a union type was used for externing.

In particular, moving extended_glob_local_binder to glob_constr.ml.

4 files changed, 66 insertions, 69 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b6aacb5ea5..e723acd13e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -598,6 +598,13 @@ let extern_optimal_prim_token scopes r r' =
   | _ -> raise No_match
 
 (**********************************************************************)
+(* mapping decl                                                       *)
+
+let extended_glob_local_binder_of_decl loc = function
+  | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,t)
+  | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t)
+
+(**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
@@ -756,7 +763,7 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
-                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
+                 let bl = List.map (extended_glob_local_binder_of_decl loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -773,7 +780,7 @@ let rec extern inctx scopes vars r =
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+                 let bl = List.map (extended_glob_local_binder_of_decl loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -817,13 +824,13 @@ and factorize_lambda inctx scopes vars na bk aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
-  | (Inl na,bk,Some bd,ty)::l ->
+  | GLocalDef (_,na,bk,bd,ty)::l ->
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
        CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
-  | (Inl na,bk,None,ty)::l ->
+  | GLocalAssum (_,na,bk,ty)::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
@@ -836,9 +843,7 @@ and extern_local_binder scopes vars = function
             (na::assums,na::ids,
              CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
-  | (Inr p,bk,Some bd,ty)::l -> assert false
-
-  | (Inr p,bk,None,ty)::l ->
+  | GLocalPattern (_,(p,_),_,bk,ty)::l ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
@@ -1052,5 +1057,5 @@ let extern_constr_pattern env sigma pat =
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
-  let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
+  let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5c90ad402e..7799591545 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -455,16 +455,10 @@ let intern_local_pattern intern lvar env p =
        env)
     env (free_vars_of_pat [] p)
 
-type extended_glob_local_binder =
-  | GLocalAssum of (Loc.t * (Name.t * binding_kind * glob_constr))
-  | GLocalDef of Loc.t * (Name.t * binding_kind * glob_constr * glob_constr)
-  | GLocalPattern of
-      Loc.t * (cases_pattern * Id.t list) * Id.t * (Name.t * binding_kind * glob_constr)
-
 let glob_local_binder_of_extended = function
-  | GLocalAssum (loc,(na,bk,t)) -> (na,bk,None,t)
-  | GLocalDef (loc,(na,bk,c,t)) -> (na,bk,Some c,t)
-  | GLocalPattern (loc,_,_,_) ->
+  | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
+  | GLocalDef (loc,na,bk,c,t) -> (na,bk,Some c,t)
+  | GLocalPattern (loc,_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
@@ -472,7 +466,7 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun a -> GLocalAssum a) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def) ->
      let indef = intern env def in
@@ -482,7 +476,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
        | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)
      in
       (push_name_env lvar (impls_term_list indef) env locna,
-       (GLocalDef ((loc,(na,Explicit,term,ty))))::bl)
+       GLocalDef (loc,na,Explicit,term,ty) :: bl)
   | CLocalPattern (loc,p,ty) ->
       let tyc =
         match ty with
@@ -490,18 +484,19 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
         | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
+      let il = List.map snd (free_vars_of_pat [] p) in
       let cp =
         match !intern_cases_pattern_fwd (None,env.scopes) p with
         | (_, [(_, cp)]) -> cp
         | _ -> assert false
       in
-      let il = List.map snd (free_vars_of_pat [] p) in
       let ienv = Id.Set.elements env.ids in
       let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
       let na = (loc, Name id) in
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
-      (env, GLocalPattern(loc,(cp,il),id,snd (List.hd bl')) :: bl)
+      let _,(_,bk,t) = List.hd bl' in
+      (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -587,13 +582,13 @@ let make_letins =
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | GLocalDef (loc,(na,_,b,_))::l ->
+  | GLocalDef (loc,na,_,b,_)::l ->
       subordinate_letins (LPLetIn (loc,(na,b))::letins) l
-  | GLocalAssum (loc,(na,bk,t))::l ->
+  | GLocalAssum (loc,na,bk,t)::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
-  | GLocalPattern (loc,u,id,decl) :: l ->
-      subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,decl)] @ l)
+  | GLocalPattern (loc,u,id,bk,t) :: l ->
+      subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
@@ -607,11 +602,11 @@ let terms_of_binders bl =
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
   let rec extract_variables = function
-    | GLocalAssum (loc,(Name id,_,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l
-    | GLocalDef (loc,(Name id,_,_,_))::l -> extract_variables l
-    | GLocalDef (loc,(Anonymous,_,_,_))::l
-    | GLocalAssum (loc,(Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
-    | GLocalPattern (loc,(u,_),_,_) :: l -> term_of_pat u :: extract_variables l
+    | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l
+    | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
+    | GLocalDef (loc,Anonymous,_,_,_)::l
+    | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
+    | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l
     | [] -> [] in
   extract_variables bl
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7dbd94aa74..8900e2fab6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -783,15 +783,15 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
     let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
     let unify_binder alp b b' =
       match b, b' with
-      | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
+      | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
-      | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
+         alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t')
+      | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
-      | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
+         alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_term alp t t')
+      | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') ->
          let alp, p = unify_pat alp p p' in
-         alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+         alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -820,16 +820,16 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
       else raise No_match in
     let unify_term_binder c b' =
       match c, b' with
-      | GVar (_, id), (Inl na', bk', None, t') (* assum *) ->
-         (Inl (unify_id id na'), bk', None, t')
-      | c, (Inr p', bk', None, t') (* pattern *) ->
+      | GVar (loc, id), GLocalAssum (_, na', bk', t') ->
+         GLocalAssum (loc, unify_id id na', bk', t')
+      | c, GLocalPattern (loc, (p',ids), id, bk', t') ->
          let p = pat_binder_of_term c in
-         (Inr (unify_pat p p'), bk', None, t')
+         GLocalPattern (loc, (unify_pat p p',ids), id, bk', t')
       | _ -> raise No_match in
     let rec unify cl bl' =
     match cl, bl' with
     | [], [] -> []
-    | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl'
+    | c :: cl, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl'
     | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
     | _ -> raise No_match in
     let bl = unify cl bl' in
@@ -882,19 +882,19 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
-  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
       when islambda && Id.equal p e ->
-      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
-  | GLambda (_,na,bk,t,b) when islambda ->
-      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
-  | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
+  | GLambda (loc,na,bk,t,b) when islambda ->
+      match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
+  | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
       when not islambda && Id.equal p e ->
-      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
-  | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
-      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
+      match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
+  | GProd (loc,(Name _ as na),bk,t,b) when not islambda ->
+      match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
   | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
+	(GLocalDef (loc,na,Explicit (*?*), c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -971,29 +971,29 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
-      let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
+  | GLambda (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+      let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders true [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
-  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
+  | GProd (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
@@ -1002,18 +1002,18 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
+  | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
+  | GProd (loc,na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
@@ -1101,7 +1101,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)]
+          bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c8fcbf7410..a61ba172ee 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,12 +47,9 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
 exception No_match
 
-type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
-      glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
-      (glob_decl2 list * subscopes) list
+      (extended_glob_local_binder list * subscopes) list
 
 val match_notation_constr_cases_pattern :
   cases_pattern -> interpretation ->