path: root/pretyping/astterm.ml

(* $Id$ *)

open Std
open Pp
open Names
open CoqAst
open Ast
open Vectops
open Generic
open Term
open Environ
open Termenv
open Impuniv
open Himsg
open Multcase_astterm 
open Evd
open More_util
open Rawterm

(**  Multcases ... **)

let prpattern k p = Printer.gencompr CCI (Termast.ast_of_pat p)

(* when an head ident is not a constructor in pattern *)
let mssg_hd_is_not_constructor s =
  [< 'sTR ("The symbol "^s^" should be a constructor") >]


(* checking linearity of a list of ids in patterns *)
let non_linearl_mssg id =
  [<'sTR "The variable " ; 'sTR(string_of_id id);
    'sTR " is bound several times in pattern" >] 

let rec has_duplicate = function 
  | [] -> None
  | x::l -> if List.mem x l then (Some x) else has_duplicate l

let check_linearity loc ids =
  match has_duplicate ids with
    | Some id -> user_err_loc (loc,"dbize_eqn",non_linearl_mssg id)
    | None -> ()

let mal_formed_mssg () =
  [<'sTR "malformed macro of multiple case" >]

(* determines if some pattern variable starts with uppercase *)
let warning_uppercase loc uplid = (* Comment afficher loc ?? *)
  let vars =
    prlist_with_sep pr_spc (fun v -> [< 'sTR (string_of_id v) >]) uplid in
  let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
  wARN [<'sTR ("Warning: the variable"^s1); vars;
	 'sTR (" start"^s2^" with upper case in pattern"); 'cUT >]

let is_uppercase_var v =
  match (string_of_id v).[0] with
    | 'A'..'Z' -> true
    | _  -> false

let check_uppercase loc ids =
  let uplid = filter is_uppercase_var ids in
  if uplid <> [] then warning_uppercase loc uplid

(* check that the number of pattern matches the number of matched args *)
let mssg_number_of_patterns n pl =
  [< 'sTR"Expecting ";'iNT n ; 'sTR" pattern(s) but found ";
    'iNT (List.length pl); 'sTR" in " >]

let check_number_of_pattern loc n l =
  if n<>(List.length l) then
    user_err_loc (loc,"check_number_of_pattern",mssg_number_of_patterns n l)

(* absolutize_eqn replaces pattern variables that are global. This
 * means that we are going to remove the pattern abstractions that
 * correspond to constructors.
 * Warning: Names that are global but do not correspond to
 * constructors are considered non-known_global. E.g. if nat appears
 * in a pattern is considered as a variable name.  known_global should
 * be refined in order to consider known_global names only those that
 * correspond to constructors of inductive types.
 *)
(*
let is_constructor =  function
    DOPN(MutConstruct((sp,tyi),i),cl)-> true | _ ->false

let is_known_constructor k env id =
  let srch =
    match k with
	CCI -> Machops.search_reference
      | FW -> Machops.search_freference
      | _ -> anomaly "known_global" in
    try is_constructor (srch env id) 
    with (Not_found | UserError _) -> 
      (try  is_constructor (Environ.search_synconst k id) 
       with Not_found -> false)


let rec abs_eqn k env avoid = function
    (v::ids, Slam(_,ona,t)) ->
      let id = id_of_string (Ast.id_of_ast v) in
      if is_known_constructor k env id
      then abs_eqn k env avoid (ids, subst1 (VAR id) t)
      else
	let id' = if is_underscore id then id else next_ident_away id avoid in
	let (nids,nt) = abs_eqn k env (id'::avoid) (ids,t) in
	(id'::nids, DLAM(na,nt))
  | ([],t) -> ([],t)
  | _ -> assert false


let rec absolutize_eqn absrec k env = function
    DOP1(XTRA("LAMEQN",ids),lam_eqn) ->
      let gids = ids_of_sign (get_globals env) in
      let (nids,neqn) =	abs_eqn k env gids (ids, lam_eqn) in
      let uplid = filter is_uppercase_var nids in
      let _ = if uplid <> [] then warning_uppercase uplid in
      DOP1(XTRA("LAMEQN",nids), absrec neqn)
  | _ -> anomalylabstrm "absolutize_eqn" (mal_formed_mssg())

*)
(****************************************************************)
(* Arguments normally implicit in the "Implicit Arguments mode" *)
(* but explicitely given                                        *)
(*
let dest_explicit_arg = function
    (DOP1(XTRA ("!", [Num(_,j)]), t)) -> (j,t)
  | _ -> raise Not_found

let is_explicit_arg = function
    (DOP1(XTRA ("!", [Num(_,j)]), t)) -> true
  | _ -> false

let explicitize_appl l args = 
 let rec aux n l args acc =
 match (l,args) with 
  (i::l',a::args') -> 
   if i=n 
   then try let j,a' = dest_explicit_arg a in
            if j > i
            then aux (n+1) l' args (mkExistential::acc)
            else if j = i
                 then aux (n+1) l' args' (a'::acc)
                 else error "Bad explicitation number"
        with Not_found -> aux (n+1) l' args (mkExistential::acc)
   else if is_explicit_arg a then error "Bad explicitation number"
   else aux (n+1) l args' (a::acc)
 | ([],_) -> (List.rev acc)@args
 | (_,[]) -> (List.rev acc)
in aux 1 l args []


let absolutize k sigma env constr = 
 let rec absrec env constr = match constr with
    VAR id -> fst (absolutize_var_with_impl k sigma env id)
  | Rel _ as t -> t
  | DOP1(XTRA ("!", [Num _]), _) -> error "Bad explicitation number"
  | DOPN(AppL,cl) -> (* Detect implicit args occurrences *)
     let cl1 = Array.to_list cl in
     let f = List.hd cl1 in
     let args = List.tl cl1 in
       begin match f with 
           VAR id ->
             let (c, impargs) = absolutize_var_with_impl k sigma env id in
             let newargs = explicitize_appl impargs args in
               mkAppList c (List.map (absrec env) newargs)
         | DOPN((Const _ | MutInd _ | MutConstruct _) as op, _) ->
	     let id = id_of_global op in
             let (c, impargs) = search_ref_with_impl k env id in
             let newargs = explicitize_appl impargs args in
               mkAppList c (List.map (absrec env) newargs)
         | (DOP1(XTRA ("!",[]), t)) ->
             mkAppList (absrec env t) (List.map (absrec env) args)
         | _ -> mkAppL (Array.map (absrec env) cl)
       end

  (* Pattern branches have a special absolutization *)
  | DOP1(XTRA("LAMEQN",_),_) as eqn  -> absolutize_eqn (absrec env) k env eqn

  | DOP0 _ as t -> t
  | DOP1(oper,c) -> DOP1(oper,absrec env c)
  | DOP2(oper,c1,c2) -> DOP2(oper,absrec env c1,absrec env c2)
  | DOPN(oper,cl) -> DOPN(oper,Array.map (absrec env) cl)
  | DOPL(oper,cl) -> DOPL(oper,List.map (absrec env) cl)
  | DLAM(na,c)    -> DLAM(na,absrec (add_rel (na,()) env) c)
  | DLAMV(na,cl)  -> DLAMV(na,Array.map (absrec (add_rel (na,()) env)) cl)

 in absrec env constr


(* Fonctions exportées *)
let absolutize_cci sigma env constr = absolutize CCI sigma env constr
let absolutize_fw  sigma env constr = absolutize FW  sigma env constr
*)

let dbize_sp = function
    Path(loc,sl,s) ->
      (try section_path sl s
       with Invalid_argument _ | Failure _ ->
         anomaly_loc(loc,"Astterm.dbize_sp",
                     [< 'sTR"malformed section-path" >]))
  | ast -> anomaly_loc(Ast.loc ast,"Astterm.dbize_sp",
                     [< 'sTR"not a section-path" >])
(*
let dbize_op loc opn pl cl =
    match (opn,pl,cl) with
        ("META",[Num(_,n)], []) -> DOP0(Meta n)
      | ("XTRA",(Str(_,s))::tlpl,_) when (multcase_kw s) ->
          DOPN(XTRA(s,tlpl),Array.of_list cl)
      | ("XTRA",(Str(_,s))::tlpl,[]) -> DOP0(XTRA(s,tlpl))
      | ("XTRA",(Str(_,s))::tlpl,[c]) -> DOP1(XTRA(s,tlpl),c)
      | ("XTRA",(Str(_,s))::tlpl,[c1;c2]) -> DOP2(XTRA(s,tlpl),c1,c2)
      | ("XTRA",(Str(_,s))::tlpl,_) -> DOPN(XTRA(s,tlpl), Array.of_list cl)

      | ("PROP", [Id(_,s)], []) ->
          (try RSort(Prop (contents_of_str s))
           with Invalid_argument s -> anomaly_loc (loc,"Astterm.dbize_op",
                                                   [< 'sTR s >]))
      | ("TYPE", [], []) -> RSort(Type(dummy_univ))

      | ("IMPLICIT", [], []) -> DOP0(Implicit)
      | ("CAST", [], [c1;c2]) -> DOP2(Cast,c1,c2)

      | ("CONST", [sp], _) -> DOPN(Const (dbize_sp sp),Array.of_list cl)
      | ("ABST", [sp], _) ->
          (try global_abst (dbize_sp sp) (Array.of_list cl)
           with
               Failure _ | Invalid_argument _ ->
                 anomaly_loc(loc,"Astterm.dbize_op",
                             [< 'sTR"malformed abstraction" >])
             | Not_found -> user_err_loc(loc,"Astterm.dbize_op",
                                         [< 'sTR"Unbound abstraction" >]))
      | ("MUTIND", [sp;Num(_,tyi)], _) ->
          DOPN(MutInd (dbize_sp sp, tyi),Array.of_list cl)
            
      | ("MUTCASE", [], p::c::l) -> mkMutCase None p c l

      | ("MUTCONSTRUCT", [sp;Num(_,tyi);Num(_,n)], _) ->
          DOPN(MutConstruct ((dbize_sp sp, tyi),n),Array.of_list cl)

      | ("SQUASH",[],[_]) -> user_err_loc
            (loc,"Astterm.dbize_op",
             [< 'sTR "Unrecognizable braces expression." >])

      | (op,_,_) -> anomaly_loc
            (loc,"Astterm.dbize_op",
             [< 'sTR "Unrecognizable constr operator: "; 'sTR op >])


let split_params =
 let rec sprec acc = function
     (Id _ as p)::l -> sprec (p::acc) l
   | (Str _ as p)::l -> sprec (p::acc) l
   | (Num _ as p)::l -> sprec (p::acc) l
   | (Path _ as p)::l -> sprec (p::acc) l
   | l -> (List.rev acc,l)
 in sprec []

*)

let is_underscore id = (id = "_")

let name_of_nvar s =
  if is_underscore s then Anonymous else Name (id_of_string s)

let ident_of_nvar loc s =
  if is_underscore s then
    user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
  else (id_of_string s)

let ids_of_ctxt cl =
  List.map(function (VAR id) -> id |_->anomaly"ids_of_ctxt") (Array.to_list cl)

let maybe_constructor env s =
  try match Machops.search_reference env (id_of_string s) with 
      DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
    | _ -> None
  with Not_found -> None

let dbize_ctxt = 
  List.map 
    (function
       | Nvar (loc,s) -> ident_of_nvar loc s
       | _ -> anomaly "Bad ast for local ctxt of a global reference")

let dbize_global loc = function
  | ("CONST", sp::ctxt)  -> RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
  | ("EVAR", sp::ctxt)   -> RRef (loc,EVar (dbize_sp sp,dbize_ctxt ctxt))
  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> RRef (loc,Ind (dbize_sp sp, tyi,dbize_ctxt ctxt))
  | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) ->
      RRef (loc,Construct (((dbize_sp sp,ti),n),dbize_ctxt ctxt))
  | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp)
(* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *)
  | _ -> anomaly_loc (loc,"dbize_global",
		      [< 'sTR "Bad ast for this global a reference">])

let ref_from_constr = function
  | DOPN (Const sp,ctxt) -> 
   if is_existential_id (basename sp) 
   then EVar (sp,ids_of_ctxt ctxt) 
   else RConst (sp,ids_of_ctxt ctxt)
  | DOPN (MutConstruct (spi,j),ctxt) -> Construct ((spi,j),ids_of_ctxt ctxt)
  | DOPN (MutInd (sp,i),ctxt) -> Ind (sp,i,ids_of_ctxt ctxt)
  | _ -> anomaly "Not a reference"

let dbize_ref k sigma env loc s =
  let id = ident_of_nvar loc s in
  if (is_existential_id id) then
    match k with
 	CCI -> 
	  RRef (loc,ref_from_constr (
		  Machops.lookup_exist sigma env (evar_of_id k id))),[]
      | FW  -> error "existentials in fterms not implemented"
      | OBJ -> anomaly "absolutize_var"
  else
  try match lookup_id id env with
      RELNAME(n,_) -> RRef (loc,RRel n),[]
    | _ -> RRef(loc,Var id), (try Vartab.implicits_of_var k id with _ -> [])
  with Not_found ->
  try let c,il = match k with
      CCI -> Machops.search_reference1 env id
    | FW  -> Machops.search_freference1 env id
    | OBJ -> anomaly "search_ref_cci_fw" in
    RRef (loc,ref_from_constr c), il
  with UserError _ ->
  try (search_synconst k id,[])
  with Not_found -> error_var_not_found "dbize_ref" loc s


let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)])
let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
let destruct_binder = function
    Node(_,"BINDER",c::idl) ->
      List.map (fun id -> (id_of_string (nvar_of_ast id),c)) idl
  | _ -> anomaly "BINDER is expected"

let rec dbize_pattern env = function
  | Node(_,"AS",[Nvar (loc,s); p]) ->
      (match name_of_nvar s with
	  Anonymous -> dbize_pattern env p
	| Name id   -> 
	    let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
  | Node(_,"APPLIST", Nvar(loc,s)::pl) ->
      (match (maybe_constructor env s, pl) with
	 | Some c, _ ->
	     let (idsl,pl') = List.split (List.map (dbize_pattern env) pl) in
	     (List.flatten idsl,PatCstr (loc,c,pl'))
	 | None, [] ->
	     (match name_of_nvar s with
		 Anonymous -> ([], PatVar (loc,Anonymous))
	       | Name id as name -> ([id], PatVar (loc,name)))
	 | None, _ ->
	     user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s))
  | _ -> anomaly "dbize: badly-formed ast for Cases pattern"

let rec dbize_fix = function
  | [] -> ([],[],[],[])
  | Node(_,"NUMFDECL", [Nvar(_,fi); Num(_,ni); astA; astT])::rest ->
      let (lf,ln,lA,lt) = dbize_fix rest in
	((id_of_string fi)::lf, (ni-1)::ln, astA::lA, astT::lt)
  | Node(_,"FDECL", [Nvar(_,fi); Node(_,"BINDERS",bl); astA; astT])::rest ->
      let binders = List.flatten (List.map destruct_binder bl) in
      let ni = List.length binders - 1 in
      let (lf,ln,lA,lt) = dbize_fix rest in
        ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA,
	 (mkLambdaCit binders astT)::lt)
  | _ -> anomaly "FDECL or NUMFDECL is expected"

let rec dbize_cofix = function
  | [] -> ([],[],[])
  | Node(_,"CFDECL", [Nvar(_,fi); astA; astT])::rest -> 
      let (lf,lA,lt) = dbize_cofix rest in
	((id_of_string fi)::lf, astA::lA, astT::lt)
  | _ -> anomaly "CFDECL is expected"

let dbize k sigma =
  let rec dbrec env = function
    Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)

(*
   | Slam(_,ona,Node(_,"V$",l)) ->
       let na =
         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
       in DLAMV(na,Array.of_list (List.map (dbrec (add_rel (na,()) env)) l))

   | Slam(_,ona,t) ->
       let na =
         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
       in DLAM(na, dbrec (add_rel (na,()) env) t)
*)
   | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
       let (lf,ln,lA,lt) = dbize_fix ldecl in
       let n =
	 try (index (ident_of_nvar locid iddef) lf) -1
         with Failure _ ->
	   error_fixname_unbound "dbize (FIX)" false locid iddef in
       let ext_env =
	 List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
       let defl = Array.of_list (List.map (dbrec ext_env) lt) in
       let arityl = Array.of_list (List.map (dbrec env) lA) in
	 RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)

   | Node(loc,"COFIX", (Nvar(locid,iddef))::ldecl) ->
       let (lf,lA,lt) = dbize_cofix ldecl in
       let n =
         try (index (ident_of_nvar locid iddef) lf) -1
         with Failure _ ->
	   error_fixname_unbound "dbize (COFIX)" true locid iddef in
       let ext_env =
	 List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
       let defl = Array.of_list (List.map (dbrec ext_env) lt) in
       let arityl = Array.of_list (List.map (dbrec env) lA) in
	 RRec (loc,RCofix n, Array.of_list lf, arityl, defl)

   | Node(loc,("PROD"|"LAMBDA" as k), [c1;Slam(_,ona,c2)]) ->
       let na = match ona with
	   Some s -> Name (id_of_string s)
	 | _ -> Anonymous in
       let kind = if k="PROD" then BProd else BLambda in
       RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2)
   | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> iterated_binder BProd c1 env c2
   | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> iterated_binder BLambda c1 env c2

   | Node(loc,"APPLISTEXPL", f::args) ->
       RApp (loc,dbrec env f,List.map (dbrec env) args)
   | Node(loc,"APPLIST", Nvar(locs,s)::args) ->
       let (c, impargs) = dbize_ref k sigma env locs s in
       RApp (loc, c, dbize_args env impargs args)
   | Node(loc,"APPLIST", f::args) ->	   
       RApp (loc,dbrec env f,List.map (dbrec env) args)

   | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) ->
       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
       RCases (loc,po,
	       List.map (dbrec env) tms,
	       List.map (dbize_eqn (List.length tms) env) eqns)

   | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) ->
       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
       let isrec = match isrectag with
	 | "REC" -> true | "NOREC" -> false 
	 | _ -> anomaly "dbize: wrong REC tag in CASE" in
	 ROldCase (loc,isrec,po,dbrec env c,Array.of_list (List.map (dbrec env) cl))

   | Node(loc,"ISEVAR",[]) -> RHole (Some loc)
   | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n)

   | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
   | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
   | Node(loc,"TYPE", []) -> RSort(loc,RType)

   (* This case mainly parses things build from   in a quotation *)
   | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
       dbize_global loc (key,l)

   | Node(loc,opn,tl) -> anomaly "dbize tmp"

 | _ -> anomaly "dbize: unexpected ast"

  and dbize_eqn n env = function
  | Node(loc,"EQN",rhs::lhs) ->
      let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
      let ids = List.flatten idsl in
      check_linearity loc ids;
      check_uppercase loc ids;
      check_number_of_pattern loc n pl;
      let env' =
	List.fold_left (fun env id -> add_rel (Name id,()) env) env ids in
	(ids,pl,dbrec env' rhs)
  | _ -> anomaly "dbize: badly-formed ast for Cases equation"

  and iterated_binder oper ty env = function
    Slam(loc,ona,body) ->
      let na =
        (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
      in RBinder(loc, oper, na, 
		 dbrec (add_rel (Anonymous,()) env) ty, (* To avoid capture *)
		 (iterated_binder oper ty (add_rel (na,()) env) body))
  | body -> dbrec env body

  and dbize_args env l args =
  let rec aux n l args = match (l,args) with 
    | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
	if i=n & j>=i then
	  if j=i
	  then (dbrec env a)::(aux (n+1) l' args')
	  else (RHole None)::(aux (n+1) l' args)
	else error "Bad explicitation number"
    | (i::l',a::args') -> 
	if i=n
	then (RHole None)::(aux (n+1) l' args)
	else (dbrec env a)::(aux (n+1) l' args')
    | ([],args) -> List.map (dbrec env) args
    | (_,[]) -> []
  in aux 1 l args

  in dbrec


(*
let dbize_kind ... =
  let c =
    try dbize k sigma env com
    with e ->
      wrap_error
 	(Ast.loc com, "dbize_kind",
         [< 'sTR"During conversion from explicit-names to" ; 'sPC ;
           'sTR"debruijn-indices" >], e,
         [< 'sTR"Perhaps the input is malformed" >]) in

  let c =
    try absolutize k sigma env c
    with e -> 
      wrap_error
 	(Ast.loc com, "Astterm.dbize_kind",
         [< 'sTR"During the relocation of global references," >], e,
         [< 'sTR"Perhaps the input is malformed" >])
  in c

*)

let dbize_cci sigma env com = dbize CCI sigma env com
let dbize_fw  sigma env com = dbize FW sigma env com

(* constr_of_com takes an environment of typing assumptions,
 * and translates a command to a constr.

let raw_constr_of_com sigma env com =
  let c = dbize_cci sigma (unitize_env env) com in
    try Sosub.soexecute c
    with Failure _|UserError _ -> error_sosub_execute CCI com

let raw_fconstr_of_com sigma env com =
  let c = dbize_fw sigma (unitize_env env) com in
    try Sosub.soexecute c
    with Failure _|UserError _ -> error_sosub_execute FW com

let raw_constr_of_compattern sigma env com =
  let c = dbize_cci sigma (unitize_env env) com in
    try Sosub.try_soexecute c
    with Failure _|UserError _ -> error_sosub_execute CCI com
 *)

let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env env) com
let raw_constr_of_compattern sigma env com = 
  dbize_cci sigma (unitize_env env) com


(* Globalization of AST quotations (mainly used in command quotations
   to get statically bound idents in grammar or pretty-printing rules) *)

let ast_adjust_consts sigma = (* locations are kept *)
 let rec dbrec env = function
    Nvar(loc,s) as ast ->
      (let id = id_of_string s in
      if (Ast.isMeta s) or (is_existential_id id) then ast
      else if List.mem id (ids_of_env env) then ast
      else 
      try match Machops.search_reference env id with
	| DOPN (Const sp,_) -> 
	    if is_existential_id (basename sp) 
	    then Node(loc,"EVAR",[path_section loc sp])
	    else Node(loc,"CONST",[path_section loc sp])
	| DOPN (MutConstruct ((sp,i),j),_) ->
	    Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j])
	| DOPN (MutInd (sp,i),_) ->
	    Node (loc,"MUTIND",[path_section loc sp;num i])
	| _ -> anomaly "Not a reference"
      with UserError _ | Not_found ->
      try let _ = search_synconst CCI id in Node(loc,"SYNCONST",[Nvar(loc,s)])
      with Not_found -> warning ("Could not globalize "^s); ast)

   | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t)

   | Slam(loc,Some na,t) ->
       let env' = add_rel (Name (id_of_string na),()) env in
         Slam(loc,Some na,dbrec env' t)
   | Node(loc,opn,tl) -> Node(loc,opn,List.map (dbrec env) tl)
   | x -> x
 in dbrec



let globalize_command ast =
  let (sigma,sign) = Termenv.initial_sigma_sign() in
    ast_adjust_consts sigma (gLOB sign) ast



(* Avoid globalizing in non command ast for tactics *)
let rec glob_ast sigma env = function 
  | Node(loc,"COMMAND",[c]) ->
      Node(loc,"COMMAND",[ast_adjust_consts sigma env c])
  | Node(loc,"COMMANDLIST",l) -> 
      Node(loc,"COMMANDLIST", List.map (ast_adjust_consts sigma env) l)
  | Slam(loc,None,t) ->
      Slam(loc,None,glob_ast sigma (add_rel (Anonymous,()) env) t)
  | Slam(loc,Some na,t) ->
      let env' = add_rel (Name (id_of_string na),()) env in
        Slam(loc,Some na, glob_ast sigma env' t)
  | Node(loc,opn,tl) -> Node(loc,opn,List.map (glob_ast sigma env) tl)
  | x -> x


let globalize_ast ast =
  let (sigma,sign) = Termenv.initial_sigma_sign() in
    glob_ast sigma (gLOB sign) ast


(* Installation of the AST quotations. "command" is used by default. *)

open Pcoq

let _ = 
  define_quotation true "command" 
    (map_entry globalize_command Command.command);
  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic);
  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)