Allow raw terms to contain references to absolute definitions.

6 files changed, 71 insertions, 44 deletions

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index a149d942c6..30f5399a88 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -32,12 +32,12 @@ GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext;
   tac2pat:
     [ "1" LEFTA
-      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, id, pl)
-      | id = Prim.qualid -> CPatRef (!@loc, id, []) ]
+      [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
+      | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) ]
     | "0"
       [ "_" -> CPatAny (!@loc)
       | "()" -> CPatTup (!@loc, [])
-      | id = Prim.qualid -> CPatRef (!@loc, id, [])
+      | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
       | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (!@loc, pl) ]
     ]
   ;
@@ -54,8 +54,8 @@ GEXTEND Gram
       [ e1 = tac2expr; ";"; e2 = tac2expr -> CTacSeq (!@loc, e1, e2) ]
     | "1" LEFTA
       [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
-      | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, qid)
-      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, qid, r)
+      | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid)
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, RelId qid, r)
       | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (!@loc, e0 :: el) ]
     | "0"
       [ "("; a = tac2expr LEVEL "5"; ")" -> a
@@ -86,7 +86,7 @@ GEXTEND Gram
   tactic_atom:
     [ [ n = Prim.integer -> CTacAtm (!@loc, AtmInt n)
       | s = Prim.string -> CTacAtm (!@loc, AtmStr s)
-      | id = Prim.qualid -> CTacRef id
+      | id = Prim.qualid -> CTacRef (RelId id)
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
       | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
@@ -104,14 +104,14 @@ GEXTEND Gram
     | "2"
       [ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ]
     | "1" LEFTA
-      [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, qid, [t]) ]
+      [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
     | "0"
       [ "("; t = tac2type LEVEL "5"; ")"  -> t
       | id = typ_param -> CTypVar (!@loc, Name id)
       | "_" -> CTypVar (!@loc, Anonymous)
-      | qid = Prim.qualid -> CTypRef (!@loc, qid, [])
+      | qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [])
       | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
-        CTypRef (!@loc, qid, p) ]
+        CTypRef (!@loc, RelId qid, p) ]
     ];
   locident:
     [ [ id = Prim.ident -> (!@loc, id) ] ]
@@ -165,7 +165,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   tac2rec_fieldexpr:
-    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> qid, e ] ]
+    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> RelId qid, e ] ]
   ;
   tac2typ_prm:
     [ [ -> []
diff --git a/tac2entries.ml b/tac2entries.ml
index c776ad13d4..374a367188 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -243,7 +243,7 @@ let register_ltac ?(local = false) isrec tactics =
     | Anonymous -> None
     | Name id ->
       let qid = Libnames.qualid_of_ident id in
-      let e = CTacLet (Loc.ghost, true, bindings, CTacRef (loc, qid)) in
+      let e = CTacLet (Loc.ghost, true, bindings, CTacRef (RelId (loc, qid))) in
       let (e, t) = intern e in
       let e = match e with
       | GTacLet (true, _, e) -> assert false
diff --git a/tac2env.ml b/tac2env.ml
index 0fcdba1ca7..a36d022e4d 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -13,11 +13,6 @@ open Names
 open Libnames
 open Tac2expr
 
-type ltac_constant = KerName.t
-type ltac_constructor = KerName.t
-type ltac_projection = KerName.t
-type type_constant = KerName.t
-
 type constructor_data = {
   cdata_prms : int;
   cdata_type : type_constant;
@@ -121,7 +116,7 @@ struct
     id, (DirPath.repr dir)
 end
 
-type tacref =
+type tacref = Tac2expr.tacref =
 | TacConstant of ltac_constant
 | TacConstructor of ltac_constructor
 
diff --git a/tac2env.mli b/tac2env.mli
index 477f4ebec7..c4b8c1e0ca 100644
--- a/tac2env.mli
+++ b/tac2env.mli
@@ -63,10 +63,6 @@ val interp_projection : ltac_projection -> projection_data
 
 (** {5 Name management} *)
 
-type tacref =
-| TacConstant of ltac_constant
-| TacConstructor of ltac_constructor
-
 val push_ltac : visibility -> full_path -> tacref -> unit
 val locate_ltac : qualid -> tacref
 val locate_extended_all_ltac : qualid -> tacref list
diff --git a/tac2expr.mli b/tac2expr.mli
index 1840b567b4..63207ac78f 100644
--- a/tac2expr.mli
+++ b/tac2expr.mli
@@ -22,6 +22,10 @@ type ltac_constructor = KerName.t
 type ltac_projection = KerName.t
 type type_constant = KerName.t
 
+type 'a or_relid =
+| RelId of qualid located
+| AbsKn of 'a
+
 (** {5 Misc} *)
 
 type ml_tactic_name = {
@@ -35,7 +39,7 @@ type raw_typexpr =
 | CTypVar of Name.t located
 | CTypArrow of Loc.t * raw_typexpr * raw_typexpr
 | CTypTuple of Loc.t * raw_typexpr list
-| CTypRef of Loc.t * qualid located * raw_typexpr list
+| CTypRef of Loc.t * type_constant or_relid * raw_typexpr list
 
 type raw_typedef =
 | CTydDef of raw_typexpr option
@@ -66,15 +70,19 @@ type atom =
 | AtmInt of int
 | AtmStr of string
 
+type tacref =
+| TacConstant of ltac_constant
+| TacConstructor of ltac_constructor
+
 (** Tactic expressions *)
 type raw_patexpr =
 | CPatAny of Loc.t
-| CPatRef of Loc.t * qualid located * raw_patexpr list
+| CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list
 | CPatTup of raw_patexpr list located
 
 type raw_tacexpr =
 | CTacAtm of atom located
-| CTacRef of qualid located
+| CTacRef of tacref or_relid
 | CTacFun of Loc.t * (Name.t located * raw_typexpr option) list * raw_tacexpr
 | CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list
 | CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr
@@ -85,13 +93,13 @@ type raw_tacexpr =
 | CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr
 | CTacCse of Loc.t * raw_tacexpr * raw_taccase list
 | CTacRec of Loc.t * raw_recexpr
-| CTacPrj of Loc.t * raw_tacexpr * qualid located
-| CTacSet of Loc.t * raw_tacexpr * qualid located * raw_tacexpr
+| CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid
+| CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr
 | CTacExt of Loc.t * raw_generic_argument
 
 and raw_taccase = raw_patexpr * raw_tacexpr
 
-and raw_recexpr = (qualid located * raw_tacexpr) list
+and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
 
 type case_info =
 | GCaseTuple of int
diff --git a/tac2intern.ml b/tac2intern.ml
index 32d1e07c17..c7e02a7b06 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -190,7 +190,8 @@ let push_name id t env = match id with
 
 let loc_of_tacexpr = function
 | CTacAtm (loc, _) -> loc
-| CTacRef (loc, _) -> loc
+| CTacRef (RelId (loc, _)) -> loc
+| CTacRef (AbsKn _) -> Loc.ghost
 | CTacFun (loc, _, _) -> loc
 | CTacApp (loc, _, _) -> loc
 | CTacLet (loc, _, _, _) -> loc
@@ -230,9 +231,10 @@ let rec subst_type subst (t : 'a glb_typexpr) = match t with
 let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
 | CTypVar (loc, Name id) -> GTypVar (get_alias (loc, id) env)
 | CTypVar (_, Anonymous) -> GTypVar (fresh_id env)
-| CTypRef (_, (loc, qid), args) ->
-  let (dp, id) = repr_qualid qid in
-  let (kn, nparams) =
+| CTypRef (loc, rel, args) ->
+  let (kn, nparams) = match rel with
+  | RelId (loc, qid) ->
+    let (dp, id) = repr_qualid qid in
     if DirPath.is_empty dp && Id.Map.mem id env.env_rec then
       Id.Map.find id env.env_rec
     else
@@ -243,10 +245,17 @@ let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
       in
       let (nparams, _) = Tac2env.interp_type kn in
       (kn, nparams)
+  | AbsKn kn ->
+    let (nparams, _) = Tac2env.interp_type kn in
+    (kn, nparams)
   in
   let nargs = List.length args in
   let () =
     if not (Int.equal nparams nargs) then
+      let loc, qid = match rel with
+      | RelId lid -> lid
+      | AbsKn kn -> loc, shortest_qualid_of_type kn
+      in
       user_err ~loc (strbrk "The type constructor " ++ pr_qualid qid ++
         strbrk " expects " ++ int nparams ++ strbrk " argument(s), but is here \
         applied to " ++ int nargs ++ strbrk "argument(s)")
@@ -467,7 +476,8 @@ let check_redundant_clause = function
 | [] -> ()
 | (p, _) :: _ -> warn_redundant_clause ~loc:(loc_of_patexpr p) ()
 
-let get_variable env (loc, qid) =
+let get_variable env var = match var with
+| RelId (loc, qid) ->
   let (dp, id) = repr_qualid qid in
   if DirPath.is_empty dp && Id.Map.mem id env.env_var then ArgVar (loc, id)
   else
@@ -477,10 +487,12 @@ let get_variable env (loc, qid) =
         CErrors.user_err ~loc (str "Unbound value " ++ pr_qualid qid)
     in
     ArgArg kn
+| AbsKn kn -> ArgArg kn
 
-let get_constructor env (loc, qid) =
+let get_constructor env var = match var with
+| RelId (loc, qid) ->
   let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in
-  match c with
+  begin match c with
   | Some (TacConstructor knc) ->
     let kn = Tac2env.interp_constructor knc in
     ArgArg (kn, knc)
@@ -491,12 +503,19 @@ let get_constructor env (loc, qid) =
     let (dp, id) = repr_qualid qid in
     if DirPath.is_empty dp then ArgVar (loc, id)
     else CErrors.user_err ~loc (str "Unbound constructor " ++ pr_qualid qid)
+  end
+| AbsKn knc ->
+  let kn = Tac2env.interp_constructor knc in
+  ArgArg (kn, knc)
 
-let get_projection (loc, qid) =
+let get_projection var = match var with
+| RelId (loc, qid) ->
   let kn = try Tac2env.locate_projection qid with Not_found ->
     user_err ~loc (pr_qualid qid ++ str " is not a projection")
   in
   Tac2env.interp_projection kn
+| AbsKn kn ->
+  Tac2env.interp_projection kn
 
 let intern_atm env = function
 | AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, []))
@@ -526,8 +545,8 @@ let rec intern_patexpr env = function
   end
 | CPatRef (_, qid, pl) ->
   begin match get_constructor env qid with
-  | ArgVar (loc, _) ->
-    user_err ~loc (str "Unbound constructor " ++ pr_qualid (snd qid))
+  | ArgVar (loc, id) ->
+    user_err ~loc (str "Unbound constructor " ++ Nameops.pr_id id)
   | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
   end
 | CPatTup (_, pl) ->
@@ -565,7 +584,7 @@ let is_constructor env qid = match get_variable env qid with
 
 let rec intern_rec env = function
 | CTacAtm (_, atm) -> intern_atm env atm
-| CTacRef qid ->
+| CTacRef qid as e ->
   begin match get_variable env qid with
   | ArgVar (_, id) ->
     let sch = Id.Map.find id env.env_var in
@@ -574,7 +593,8 @@ let rec intern_rec env = function
     let (_, _, sch) = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
   | ArgArg (TacConstructor kn) ->
-    intern_constructor env (fst qid) kn []
+    let loc = loc_of_tacexpr e in
+    intern_constructor env loc kn []
   end
 | CTacFun (loc, bnd, e) ->
   let fold (env, bnd, tl) ((_, na), t) =
@@ -590,12 +610,13 @@ let rec intern_rec env = function
   let (e, t) = intern_rec env e in
   let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in
   (GTacFun (bnd, e), t)
-| CTacApp (loc, CTacRef qid, args) when is_constructor env qid ->
+| CTacApp (loc, CTacRef qid, args) as e when is_constructor env qid ->
   let kn = match get_variable env qid with
   | ArgArg (TacConstructor kn) -> kn
   | _ -> assert false
   in
-  intern_constructor env (fst qid) kn args
+  let loc = loc_of_tacexpr e in
+  intern_constructor env loc kn args
 | CTacApp (loc, f, args) ->
   let (f, ft) = intern_rec env f in
   let fold arg (args, t) =
@@ -687,7 +708,10 @@ let rec intern_rec env = function
   let pinfo = get_projection proj in
   let () =
     if not pinfo.pdata_mutb then
-      let (loc, _) = proj in
+      let loc = match proj with
+      | RelId (loc, _) -> loc
+      | AbsKn _ -> Loc.ghost
+      in
       user_err ~loc (str "Field is not mutable")
   in
   let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
@@ -974,8 +998,12 @@ and intern_constructor env loc kn args =
     error_nargs_mismatch loc nargs (List.length args)
 
 and intern_record env loc fs =
-  let map ((loc, qid), e) =
-    let proj = get_projection (loc, qid) in
+  let map (proj, e) =
+    let loc = match proj with
+    | RelId (loc, _) -> loc
+    | AbsKn _ -> Loc.ghost
+    in
+    let proj = get_projection proj in
     (loc, proj, e)
   in
   let fs = List.map map fs in