[location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.

3 files changed, 26 insertions, 25 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 48ab3dd57..938fe5237 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1246,15 +1246,16 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_
   in
   List.rev !l
 
-let rec rebuild_return_type (loc, rt) =
-  match rt with
+let rec rebuild_return_type rt =
+  let loc = rt.CAst.loc in
+  match rt.CAst.v with
     | Constrexpr.CProdN(n,t') ->
-        Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
+        CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
-	Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
-				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt],
-			    Loc.tag @@ Constrexpr.CSort(GType []))
+	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit, rt],
+			    CAst.make @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
       evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
@@ -1305,11 +1306,11 @@ let do_build_inductive
 	(fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
-	     Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	     CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
 	  | None ->
-	     Loc.tag @@ Constrexpr.CProdN
+	     CAst.make @@ Constrexpr.CProdN
 	       ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
@@ -1372,11 +1373,11 @@ let do_build_inductive
       (fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
-	   Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	   CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
 	 | None ->
-           Loc.tag @@ Constrexpr.CProdN
+           CAst.make @@ Constrexpr.CProdN
 	   ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dc16626c..f4e9aa372 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -469,7 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   in
   let unbounded_eq =
     let f_app_args =
-      Loc.tag @@ Constrexpr.CAppExpl(
+      CAst.make @@ Constrexpr.CAppExpl(
 	 (None,(Ident (Loc.tag fname)),None) ,
 	 (List.map
 	    (function
@@ -480,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -588,12 +588,12 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
 	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) ->
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } ->
 	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
-	match nal, snd typ with 
+	match nal, typ.CAst.v with 
 	  | [], _ -> rebuild_bl (aux,assoc) bl' typ
 	  | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
 	  | _,CProdN((nal',bk',nal't)::rest,typ') -> 
@@ -606,7 +606,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
-		 else Loc.tag @@ if List.is_empty new_nal'
+		 else CAst.make @@ if List.is_empty new_nal'
 		 then CProdN(rest,typ')
 		 else CProdN(((new_nal',bk',nal't)::rest),typ'))
 	    else 
@@ -614,7 +614,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      let nassoc = make_assoc assoc nal' captured_nal in
 	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
-		bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ'))
+		bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ'))
 	  | _ -> assert false
 
 let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
@@ -725,7 +725,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   in
   ()
 
-let rec add_args id new_args = Loc.map (function
+let rec add_args id new_args = CAst.map (function
   | CRef (r,_) as b ->
       begin match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
@@ -794,7 +794,7 @@ let rec chop_n_arrow n t =
   if n <= 0
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
-    match snd t with
+    match t.CAst.v with
       | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
@@ -813,7 +813,7 @@ let rec chop_n_arrow n t =
 		    then
 		      aux (n - nal_l) nal_ta'
 		    else
-		      let new_t' = Loc.tag @@
+		      let new_t' = CAst.make @@
 			Constrexpr.CProdN(
 					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
@@ -829,7 +829,7 @@ let rec chop_n_arrow n t =
 
 let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
-  match snd b with
+  match b.CAst.v with
     | Constrexpr.CLambdaN ((nal_ta), b') ->
 	begin
 	  let n =
@@ -869,7 +869,7 @@ let make_graph (f_ref:global_reference) =
 	 in
 	 let (nal_tas,b,t)  = get_args extern_body extern_type in
 	 let expr_list =
-	   match snd b with
+	   match b.CAst.v with
 	     | Constrexpr.CFix(l_id,fixexprl) ->
 		 let l =
 		   List.map
@@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) -> Loc.tag ?loc @@ 
+					(fun (loc,n) -> CAst.make ?loc @@ 
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f2654b5de..5b51a213a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -73,7 +73,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in
+    let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when CErrors.noncritical e -> false
@@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let c = RelDecl.get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
-        Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+        CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in