aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorherbelin2001-08-10 14:42:22 +0000
committerherbelin2001-08-10 14:42:22 +0000
commit8e92ee787e7d1fd48cae1eccf67a9b05e739743e (patch)
treeb33191fbaba0cad4b14a96cf5d7786dd2c07c3d7 /parsing
parentc0a3b41ad2f2afba3f060e0d4001bd7aceea0831 (diff)
Parsing
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rwxr-xr-xparsing/ast.ml145
-rwxr-xr-xparsing/ast.mli28
-rw-r--r--parsing/astterm.ml138
-rw-r--r--parsing/coqast.ml45
-rw-r--r--parsing/coqast.mli20
-rw-r--r--parsing/coqlib.ml21
-rw-r--r--parsing/coqlib.mli4
-rw-r--r--parsing/esyntax.ml18
-rw-r--r--parsing/extend.ml423
-rw-r--r--parsing/g_basevernac.ml436
-rw-r--r--parsing/g_cases.ml42
-rw-r--r--parsing/g_constr.ml462
-rw-r--r--parsing/g_ltac.ml410
-rw-r--r--parsing/g_prim.ml458
-rw-r--r--parsing/g_rsyntax.ml6
-rw-r--r--parsing/g_tactic.ml426
-rw-r--r--parsing/g_vernac.ml436
-rw-r--r--parsing/g_zsyntax.ml11
-rw-r--r--parsing/lexer.ml43
-rw-r--r--parsing/pcoq.ml49
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/pretty.ml597
-rw-r--r--parsing/prettyp.ml20
-rw-r--r--parsing/printer.ml30
-rw-r--r--parsing/q_coqast.ml462
-rw-r--r--parsing/search.ml8
-rw-r--r--parsing/termast.ml31
27 files changed, 1055 insertions, 396 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml
index b870371274..dc751186f7 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -21,11 +21,13 @@ let dummy_loc = (0,0)
let loc = function
| Node (loc,_,_) -> loc
| Nvar (loc,_) -> loc
+ | Nmeta (loc,_) -> loc
| Slam (loc,_,_) -> loc
+ | Smetalam (loc,_,_) -> loc
| Num (loc,_) -> loc
| Id (loc,_) -> loc
| Str (loc,_) -> loc
- | Path (loc,_,_) -> loc
+ | Path (loc,_) -> loc
| Dynamic (loc,_) -> loc
(* building a node with dummy location *)
@@ -36,27 +38,24 @@ let ide s = Id(dummy_loc,s)
let nvar s = Nvar(dummy_loc,s)
let num n = Num(dummy_loc,n)
let str s = Str(dummy_loc,s)
-let path sl s = Path(dummy_loc,sl,s)
+let path sl = Path(dummy_loc,sl)
let dynamic d = Dynamic(dummy_loc,d)
let rec set_loc loc = function
| Node(_,op,al) -> Node(loc, op, List.map (set_loc loc) al)
| Slam(_,idl,b) -> Slam(loc,idl, set_loc loc b)
+ | Smetalam(_,idl,b) -> Smetalam(loc,idl, set_loc loc b)
| Nvar(_,s) -> Nvar(loc,s)
+ | Nmeta(_,s) -> Nmeta(loc,s)
| Id(_,s) -> Id(loc,s)
| Str(_,s) -> Str(loc,s)
| Num(_,s) -> Num(loc,s)
- | Path(_,sl,s) -> Path(loc,sl,s)
+ | Path(_,sl) -> Path(loc,sl)
| Dynamic(_,d) -> Dynamic(loc,d)
-let path_section loc sp =
- let (sl,bn,pk) = repr_path sp in
- Coqast.Path(loc, sl @ [string_of_id bn], string_of_kind pk)
+let path_section loc sp = Coqast.Path(loc, sp)
-let section_path sl k =
- match List.rev sl with
- | s::pa -> make_path (List.rev pa) (id_of_string s) (kind_of_string k)
- | [] -> invalid_arg "section_path"
+let section_path sp = sp
(* ast destructors *)
let num_of_ast = function
@@ -76,7 +75,7 @@ type pat =
| Pquote of t
| Pmeta of string * tok_kind
| Pnode of string * patlist
- | Pslam of string option * pat
+ | Pslam of identifier option * pat
| Pmeta_slam of string * pat
and patlist =
@@ -105,15 +104,16 @@ let rec print_ast ast =
match ast with
| Num(_,n) -> [< 'iNT n >]
| Str(_,s) -> [< 'qS s >]
- | Path(_,sl,u) ->
- [< prlist (fun s -> [< 'sTR"#"; 'sTR s >]) sl; 'sTR"."; 'sTR u >]
+ | Path(_,sl) -> [< pr_sp sl >]
| Id (_,s) -> [< 'sTR"{" ; 'sTR s ; 'sTR"}" >]
- | Nvar(_,s) -> [< 'sTR s >]
+ | Nvar(_,s) -> [< pr_id s >]
+ | Nmeta(_,s) -> [< 'sTR s >]
| Node(_,op,l) ->
hOV 3 [< 'sTR"(" ; 'sTR op ; 'sPC ; print_astl l; 'sTR")" >]
| Slam(_,None,ast) -> hOV 1 [< 'sTR"[<>]"; print_ast ast >]
| Slam(_,Some x,ast) ->
- hOV 1 [< 'sTR"["; 'sTR x; 'sTR"]"; 'cUT; print_ast ast >]
+ hOV 1 [< 'sTR"["; pr_id x; 'sTR"]"; 'cUT; print_ast ast >]
+ | Smetalam(_,id,ast) -> hOV 1 [< 'sTR id; print_ast ast >]
| Dynamic(_,d) ->
hOV 0 [< 'sTR"<dynamic: "; 'sTR(Dyn.tag d); 'sTR">" >]
@@ -137,8 +137,8 @@ let rec print_astpat = function
| Pnode(op,al) ->
hOV 2 [< 'sTR"(" ; 'sTR op; 'sPC; print_astlpat al; 'sTR")" >]
| Pslam(None,b) -> hOV 1 [< 'sTR"[<>]"; 'cUT; print_astpat b >]
- | Pslam(Some s,b) ->
- hOV 1 [< 'sTR"["; 'sTR s; 'sTR"]"; 'cUT; print_astpat b >]
+ | Pslam(Some id,b) ->
+ hOV 1 [< 'sTR"["; pr_id id; 'sTR"]"; 'cUT; print_astpat b >]
and print_astlpat = function
| Pnil -> [< >]
@@ -172,14 +172,20 @@ let check_cast loc a k =
| _ -> user_err_loc (loc,"Ast.cast_val",
[< 'sTR"cast _"; print_ast_cast k; 'sTR"failed" >])
-let rec coerce_to_var v = function
- | Nvar(_,id) -> id
- | Node(_,"QUALID",[Nvar(_,id)]) -> id
- | Node(_,"QUALIDARG",[Nvar(_,id)]) -> id
+let rec coerce_to_var = function
+ | Nvar(_,id) as var -> var
+ | Nmeta(_,id) as var -> var
+ | Node(_,"QUALID",[Nvar(_,id) as var]) -> var
+ | Node(_,"QUALIDARG",[Nvar(_,id) as var]) -> var
| ast -> user_err_loc
(loc ast,"Ast.coerce_to_var",
[< 'sTR"This expression should be a simple identifier" >])
+let coerce_to_id a = match coerce_to_var a with
+ | Nvar (_,id) -> id
+(* | Nmeta(_,id) -> id_of_string id*)
+ | ast -> invalid_arg "coerce_to_id"
+
let env_assoc_value loc v env =
try
List.assoc v env
@@ -200,8 +206,8 @@ let env_assoc sigma k (loc,v) =
let env_assoc_nvars sigma (dloc,v) =
match env_assoc_value dloc v sigma with
- | Vastlist al -> List.map (coerce_to_var v) al
- | Vast ast -> [coerce_to_var v ast]
+ | Vastlist al -> List.map coerce_to_id al
+ | Vast ast -> [coerce_to_id ast]
let build_lams dloc idl ast =
List.fold_right (fun id lam -> Slam(dloc,Some id,lam)) idl ast
@@ -253,14 +259,16 @@ let check_ast_meta env loc pv =
let rec val_of_ast env ast =
match ast with
- | Nvar(loc,pv) when isMeta pv ->
+ | Nmeta(loc,pv) ->
check_ast_meta env loc pv;
Pmeta(pv,Tany)
+(*
| Id(loc,pv) when isMeta pv ->
check_ast_meta env loc pv;
Pmeta(pv,Tid)
+*)
| Node(_,"$QUOTE",[qast]) -> Pquote (set_loc dummy_loc qast)
- | Slam(loc,Some s,a) when isMeta s ->
+ | Smetalam(loc,s,a) ->
let _ = type_of_meta env loc s in (* ids are coerced to id lists *)
Pmeta_slam(s, val_of_ast env a)
| (Path _|Num _|Id _|Str _|Nvar _) -> Pquote (set_loc dummy_loc ast)
@@ -274,7 +282,7 @@ let rec val_of_ast env ast =
and vall_of_astl env astl =
match astl with
- | (Node(loc,"$LIST",[Nvar(locv,pv)]))::asttl when isMeta pv ->
+ | (Node(loc,"$LIST",[Nmeta(locv,pv)]))::asttl ->
if type_of_meta env locv pv = ETastl then
if asttl = [] then
Plmeta pv
@@ -309,7 +317,9 @@ let rec alpha alp a1 a2 =
| (Id(_,s1),Id(_,s2)) -> s1=s2
| (Str(_,s1),Str(_,s2)) -> s1=s2
| (Num(_,n1),Num(_,n2)) -> n1=n2
- | (Path(_,sl1,s1),Path(_,sl2,s2)) -> sl1=sl2 & s1=s2
+ | (Path(_,sl1),Path(_,sl2)) -> sl1=sl2
+ | ((Smetalam _ | Nmeta _ | Dynamic _), _) -> false
+ | (_, (Smetalam _ | Nmeta _ | Dynamic _)) -> false
| _ -> false
let alpha_eq (a1,a2)= alpha [] a1 a2
@@ -324,6 +334,7 @@ let alpha_eq_val = function
let rec occur_var_ast s = function
| Node(loc,op,args) -> List.exists (occur_var_ast s) args
| Nvar(_,s2) -> s = s2
+ | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here"
| Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
| Id _ | Str _ | Num _ | Path _ -> false
| Dynamic _ -> (* Hum... what to do here *) false
@@ -331,6 +342,7 @@ let rec occur_var_ast s = function
let rec replace_vars_ast l = function
| Node(loc,op,args) -> Node (loc,op, List.map (replace_vars_ast l) args)
| Nvar(loc,s) as a -> (try Nvar (loc, List.assoc s l) with Not_found -> a)
+ | Smetalam _ | Nmeta _ -> anomaly "replace_var: metas should not occur here"
| Slam(loc,None,body) -> Slam(loc,None,replace_vars_ast l body)
| Slam(loc,Some s,body) as a ->
if List.mem_assoc s l then a else
@@ -342,7 +354,7 @@ exception No_match of string
let no_match_loc (loc,s) = Stdpp.raise_with_loc loc (No_match s)
-(* Binds value v to variable var. If var is already bound, checks if the
+(* Binds value v to variable var. If var is already bound, checks if
its value is alpha convertible with v. This allows non-linear patterns.
Important note: The Metavariable $_ is a special case; it cannot be
@@ -390,6 +402,8 @@ let rec amatch alp sigma spat ast =
| (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
| (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
+ | (Pmeta_slam(pv,pb), Smetalam(loc, s, b)) ->
+ anomaly "amatch: match a pattern with an open ast"
| (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op ->
(try amatchl alp sigma argp args
with e -> Stdpp.raise_with_loc loc e)
@@ -443,26 +457,35 @@ let make_astvar env loc v cast =
(Pmeta(v,cast), env')
(* Note: no metavar in operator position. necessary ? *)
-(* TODO: $SLAM pour recuperer tous les Slam d'un coup dans une liste *)
let rec pat_of_ast env ast =
match ast with
- | Nvar(loc,pv) when isMeta pv -> make_astvar env loc pv Tany
+ | Nmeta(loc,pv) -> make_astvar env loc pv Tany
+(* Obsolète
| Id(loc,pv) when isMeta pv -> make_astvar env loc pv Tid
- | Slam(loc,Some s,a) when isMeta s ->
+*)
+ | Smetalam(loc,s,a) ->
let senv = bind_patvar env loc s ETast in
let (pa,env') = pat_of_ast senv a in
(Pmeta_slam(s, pa), env')
- | Node(_,"$VAR",[Nvar(loc,pv)]) when isMeta pv ->
+ | Node(_,"$VAR",[Nmeta(loc,pv)]) ->
make_astvar env loc pv Tvar
- | Node(_,"$ID",[Nvar(loc,pv)]) when isMeta pv ->
+ | Node(_,"$ID",[Nmeta(loc,pv)]) ->
make_astvar env loc pv Tid
- | Node(_,"$NUM",[Nvar(loc,pv)]) when isMeta pv ->
+ | Node(_,"$NUM",[Nmeta(loc,pv)]) ->
make_astvar env loc pv Tnum
- | Node(_,"$STR",[Nvar(loc,pv)]) when isMeta pv ->
+ | Node(_,"$STR",[Nmeta(loc,pv)]) ->
make_astvar env loc pv Tstr
- | Node(_,"$PATH",[Nvar(loc,pv)]) when isMeta pv ->
+ | Node(_,"$PATH",[Nmeta(loc,pv)]) ->
make_astvar env loc pv Tpath
| Node(_,"$QUOTE",[qast]) -> (Pquote (set_loc dummy_loc qast), env)
+
+ (* This may occur when the meta is not textual but bound by coerce_to_id*)
+ | Slam(loc,Some id,b) when isMeta (string_of_id id) ->
+ let s = string_of_id id in
+ let senv = bind_patvar env loc s ETast in
+ let (pb,env') = pat_of_ast senv b in
+ (Pmeta_slam(s, pb), env')
+
| Slam(_,os,b) ->
let (pb,env') = pat_of_ast env b in
(Pslam(os,pb), env')
@@ -478,7 +501,7 @@ let rec pat_of_ast env ast =
and patl_of_astl env astl =
match astl with
- | [Node(_,"$LIST",[Nvar(loc,pv)])] when isMeta pv ->
+ | [Node(_,"$LIST",[Nmeta(loc,pv)])] ->
let penv = bind_patvar env loc pv ETastl in
(Plmeta pv, penv)
| [] -> (Pnil,env)
@@ -583,51 +606,3 @@ let to_act_check_vars env etyp ast =
match ast with
| Node(_,"ASTACT",[a]) -> act_of_ast env etyp a
| _ -> invalid_arg_loc (loc ast,"Ast.to_act_env")
-
-
-(* Hash-consing *)
-module Hloc = Hashcons.Make(
- struct
- type t = Coqast.loc
- type u = unit
- let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
- let hash_sub () x = x
- let hash = Hashtbl.hash
- end)
-
-module Hast = Hashcons.Make(
- struct
- type t = Coqast.t
- type u = (Coqast.t -> Coqast.t) * ((loc -> loc) * (string -> string))
- let hash_sub (hast,(hloc,hstr)) = function
- | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
- | Nvar(l,s) -> Nvar(hloc l, hstr s)
- | Slam(l,None,t) -> Slam(hloc l, None, hast t)
- | Slam(l,Some s,t) -> Slam(hloc l, Some (hstr s), hast t)
- | Num(l,n) -> Num(hloc l, n)
- | Id(l,s) -> Id(hloc l, hstr s)
- | Str(l,s) -> Str(hloc l, hstr s)
- | Path(l,d,k) -> Path(hloc l, List.map hstr d, hstr k)
- | Dynamic(l,d) -> Dynamic(hloc l, d)
- let equal a1 a2 =
- match (a1,a2) with
- | (Node(l1,s1,al1), Node(l2,s2,al2)) ->
- (l1==l2 & s1==s2 & List.length al1 = List.length al2)
- & List.for_all2 (==) al1 al2
- | (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
- | (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
- | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) -> l1==l2 & t1==t2
- | (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
- | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
- | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
- | (Path(l1,d1,k1), Path(l2,d2,k2)) ->
- (l1==l2 & k1==k2 & List.length d1 = List.length d2)
- & List.for_all2 (==) d1 d2
- | _ -> false
- let hash = Hashtbl.hash
- end)
-
-let hcons_ast hstr =
- let hloc = Hashcons.simple_hcons Hloc.f () in
- let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr) in
- (hast,hloc)
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 0379ba305f..d3e0ee4ab2 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -21,24 +21,23 @@ val loc : Coqast.t -> Coqast.loc
(* ast constructors with dummy location *)
val ope : string * Coqast.t list -> Coqast.t
-val slam : string option * Coqast.t -> Coqast.t
-val nvar : string -> Coqast.t
+val slam : identifier option * Coqast.t -> Coqast.t
+val nvar : identifier -> Coqast.t
val ide : string -> Coqast.t
val num : int -> Coqast.t
val str : string -> Coqast.t
-val path : string list -> string -> Coqast.t
+val path : section_path -> Coqast.t
val dynamic : Dyn.t -> Coqast.t
val set_loc : Coqast.loc -> Coqast.t -> Coqast.t
val path_section : Coqast.loc -> section_path -> Coqast.t
-val section_path : string list -> string -> section_path
-
+val section_path : section_path -> section_path
(* ast destructors *)
val num_of_ast : Coqast.t -> int
val id_of_ast : Coqast.t -> string
-val nvar_of_ast : Coqast.t -> string
+val nvar_of_ast : Coqast.t -> identifier
(* ast processing datatypes *)
@@ -47,7 +46,7 @@ type pat =
| Pquote of Coqast.t
| Pmeta of string * tok_kind
| Pnode of string * patlist
- | Pslam of string option * pat
+ | Pslam of identifier option * pat
| Pmeta_slam of string * pat
and patlist =
@@ -71,7 +70,11 @@ type v =
type env = (string * v) list
-val coerce_to_var : string -> Coqast.t -> string
+val coerce_to_var : Coqast.t -> Coqast.t
+
+(*
+val coerce_to_id : Coqast.t -> identifier
+*)
exception No_match of string
@@ -96,8 +99,8 @@ val vall_of_astl : entry_env -> Coqast.t list -> patlist
val alpha_eq : Coqast.t * Coqast.t -> bool
val alpha_eq_val : v * v -> bool
-val occur_var_ast : string -> Coqast.t -> bool
-val replace_vars_ast : (string * string) list -> Coqast.t -> Coqast.t
+val occur_var_ast : identifier -> Coqast.t -> bool
+val replace_vars_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
val bind_env : env -> string -> v -> env
val ast_match : env -> pat -> Coqast.t -> env
@@ -111,8 +114,3 @@ val to_pat : entry_env -> Coqast.t -> (pat * entry_env)
val eval_act : Coqast.loc -> env -> act -> v
val to_act_check_vars : entry_env -> entry_type -> Coqast.t -> act
-
-(* Hash-consing *)
-val hcons_ast: (string -> string) ->
- (Coqast.t -> Coqast.t) * (Coqast.loc -> Coqast.loc)
-
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 30ec93b79e..194ce335ee 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -27,10 +27,6 @@ open Ast
open Coqast
open Nametab
-type extended_global_reference =
- | TrueGlobal of global_reference
- | SyntacticDef of section_path
-
(*Takes a list of variables which must not be globalized*)
let from_list l = List.fold_right Idset.add l Idset.empty
@@ -40,7 +36,7 @@ let rec adjust_implicits n = function
(* 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") >]
+ [< 'sTR "The symbol "; pr_id s; 'sTR " should be a constructor" >]
(* checking linearity of a list of ids in patterns *)
let non_linearl_mssg id =
@@ -50,7 +46,7 @@ let non_linearl_mssg id =
let error_capture_loc loc s =
user_err_loc
(loc,"ast_to_rawconstr",
- [< 'sTR ("The variable "^s^" occurs in its type") >])
+ [< 'sTR "The variable "; pr_id s; 'sTR " occurs in its type" >])
let error_expl_impl_loc loc =
user_err_loc
@@ -116,34 +112,34 @@ let check_number_of_pattern loc n l =
(* Translation of references *)
let ast_to_sp = function
- | Path(loc,sl,s) ->
+ | Path(loc,sp) ->
(try
- section_path sl s
+ section_path sp
with Invalid_argument _ | Failure _ ->
anomaly_loc(loc,"Astterm.ast_to_sp",
- [< 'sTR"malformed section-path" >]))
+ [< 'sTR"ill-formed section-path" >]))
| ast -> anomaly_loc(Ast.loc ast,"Astterm.ast_to_sp",
[< 'sTR"not a section-path" >])
-let is_underscore id = (id = "_")
+let is_underscore id = (id = wildcard)
let name_of_nvar s =
- if is_underscore s then Anonymous else Name (id_of_string s)
+ if is_underscore s then Anonymous else Name 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)
+ else s
let interp_qualid p =
let outnvar = function
| Nvar (loc,s) -> s
- | _ -> anomaly "interp_qualid: bad-formed qualified identifier" in
+ | _ -> anomaly "interp_qualid: ill-formed qualified identifier" in
match p with
| [] -> anomaly "interp_qualid: empty qualified identifier"
| l ->
let p, r = list_chop (List.length l -1) (List.map outnvar l) in
- make_qualid p (id_of_string (List.hd r))
+ make_qualid p (List.hd r)
let maybe_variable = function
| [Nvar (_,s)] -> Some s
@@ -161,7 +157,7 @@ let ids_of_ctxt ctxt =
type pattern_qualid_kind =
| IsConstrPat of loc * (constructor_path * identifier list)
- | IsVarPat of loc * string
+ | IsVarPat of loc * identifier
let maybe_constructor env = function
| Node(loc,"QUALID",l) ->
@@ -188,7 +184,13 @@ let maybe_constructor env = function
| Node(loc,"MUTCONSTRUCT",[sp;Num(_,ti);Num(_,n)]) ->
(* Buggy: needs to compute the context *)
IsConstrPat (loc,(((ast_to_sp sp,ti),n),[]))
-
+
+ | Path(loc,sp) ->
+ (match absolute_reference sp with
+ | ConstructRef (spi,j) ->
+ IsConstrPat (loc,((spi,j),[]))
+ | _ -> error ("Unknown absolute constructor name: "^(string_of_path sp)))
+
| Node(loc,("CONST"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) ->
user_err_loc (loc,"ast_to_pattern",
[< 'sTR "Found a pattern involving global references which are not constructors"
@@ -237,10 +239,9 @@ let ref_from_constr c = match kind_of_term c with
[vars2] is the set of global variables, env is the set of variables
abstracted until this point *)
-let ast_to_var (env,impls) (vars1,vars2) loc s =
- let id = id_of_string s in
+let ast_to_var (env,impls) (vars1,vars2) loc id =
let imps =
- if Idset.mem id env or List.mem s vars1
+ if Idset.mem id env or List.mem id vars1
then
try List.assoc id impls
with Not_found -> []
@@ -248,7 +249,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc s =
let _ = lookup_id id vars2 in
(* Car Fixpoint met les fns définies tmporairement comme vars de sect *)
try
- let ref = Nametab.locate (make_qualid [] (id_of_string s)) in
+ let ref = Nametab.locate (make_qualid [] id) in
implicits_of_global ref
with _ -> []
in RVar (loc, id), [], imps
@@ -262,6 +263,10 @@ type 'a globalization_action = {
fail : qualid -> 'a * int list;
}
+let implicits_of_extended_reference = function
+ | TrueGlobal ref -> implicits_of_global ref
+ | SyntacticDef _ -> []
+
let translate_qualid act qid =
(* Is it a bound variable? *)
try
@@ -269,56 +274,47 @@ let translate_qualid act qid =
| [],id -> act.parse_var id, []
| _ -> raise Not_found
with Not_found ->
- (* Is it a global reference? *)
- try
- let ref = Nametab.locate qid in
- act.parse_ref (TrueGlobal ref), implicits_of_global ref
- with Not_found ->
- (* Is it a reference to a syntactic definition? *)
+ (* Is it a global reference or a syntactic definition? *)
try
- let sp = Syntax_def.locate_syntactic_definition qid in
- act.parse_ref (SyntacticDef sp), []
+ let ref = Nametab.extended_locate qid in
+ act.parse_ref ref, implicits_of_extended_reference ref
with Not_found ->
act.fail qid
(**********************************************************************)
-let rawconstr_of_var env vars loc s =
+let rawconstr_of_var env vars loc id =
try
- ast_to_var env vars loc s
+ ast_to_var env vars loc id
with Not_found ->
- Pretype_errors.error_var_not_found_loc loc (id_of_string s)
+ Pretype_errors.error_var_not_found_loc loc id
let rawconstr_of_qualid env vars loc qid =
(* Is it a bound variable? *)
try
match repr_qualid qid with
- | [],s -> ast_to_var env vars loc (string_of_id s)
+ | [],s -> ast_to_var env vars loc s
| _ -> raise Not_found
with Not_found ->
- (* Is it a global reference? *)
- try
- let ref = Nametab.locate qid in
+ (* Is it a global reference or a syntactic definition? *)
+ try match Nametab.extended_locate qid with
+ | TrueGlobal ref ->
let hyps = implicit_section_args ref in
let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
let imps = implicits_of_global ref in
RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
- with Not_found ->
- (* Is it a reference to a syntactic definition? *)
- try
- let sp = Syntax_def.locate_syntactic_definition qid in
+ | SyntacticDef sp ->
set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp),[],[]
with Not_found ->
error_global_not_found_loc loc qid
-let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
+let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some 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 mkProdC (x,a,b) = ope("PROD",[a;slam(Some 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
+ | Node(_,"BINDER",c::idl) -> List.map (fun id -> (nvar_of_ast id,c)) idl
| _ -> anomaly "BINDER is expected"
(* [merge_aliases] returns the sets of all aliases encountered at this
@@ -328,14 +324,15 @@ let merge_aliases (ids,subst as aliases) = function
| Name id ->
ids@[id],
if ids=[] then subst
- else (string_of_id id,string_of_id (List.hd ids))::subst
+ else (id, List.hd ids)::subst
let alias_of = function
| ([],_) -> Anonymous
| (id::_,_) -> Name id
-let message_redondant_alias (s1,s2) =
- warning ("Alias variable "^s1^" is merged with "^s2)
+let message_redundant_alias (s1,s2) =
+ warning ("Alias variable "^(string_of_id s1)
+ ^" is merged with "^(string_of_id s2))
let rec ast_to_pattern env aliases = function
| Node(_,"PATTAS",[Nvar (loc,s); p]) ->
@@ -363,12 +360,12 @@ let rec ast_to_fix = function
| [] -> ([],[],[],[])
| Node(_,"NUMFDECL", [Nvar(_,fi); Num(_,ni); astA; astT])::rest ->
let (lf,ln,lA,lt) = ast_to_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 ->
+ (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) = ast_to_fix rest in
- ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA,
+ (fi::lf, ni::ln, (mkProdCit binders astA)::lA,
(mkLambdaCit binders astT)::lt)
| _ -> anomaly "FDECL or NUMFDECL is expected"
@@ -376,13 +373,13 @@ let rec ast_to_cofix = function
| [] -> ([],[],[])
| Node(_,"CFDECL", [Nvar(_,fi); astA; astT])::rest ->
let (lf,lA,lt) = ast_to_cofix rest in
- ((id_of_string fi)::lf, astA::lA, astT::lt)
+ (fi::lf, astA::lA, astT::lt)
| _ -> anomaly "CFDECL is expected"
let error_fixname_unbound str is_cofix loc name =
user_err_loc
(loc,"ast_to (COFIX)",
- [< 'sTR "The name"; 'sPC ; 'sTR name ;
+ [< 'sTR "The name"; 'sPC ; pr_id name ;
'sPC ; 'sTR "is not bound in the corresponding"; 'sPC ;
'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >])
(*
@@ -431,7 +428,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
| Node(loc,("PROD"|"LAMBDA"|"LETIN" as k), [c1;Slam(_,ona,c2)]) ->
let na,ids' = match ona with
- | Some s -> let id = id_of_string s in Name id, Idset.add id ids
+ | Some id -> Name id, Idset.add id ids
| _ -> Anonymous, ids in
let c1' = dbrec env c1 and c2' = dbrec (ids',impls) c2 in
(match k with
@@ -522,17 +519,17 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
check_uppercase loc eqn_ids;
check_number_of_pattern loc n pl;
let rhs = replace_vars_ast subst rhs in
- List.iter message_redondant_alias subst;
+ List.iter message_redundant_alias subst;
let env_ids = List.fold_right Idset.add eqn_ids ids in
(loc, eqn_ids,pl,dbrec (env_ids,impls) rhs)
- | _ -> anomaly "ast_to_rawconstr: badly-formed ast for Cases equation"
+ | _ -> anomaly "ast_to_rawconstr: ill-formed ast for Cases equation"
and iterated_binder oper n ty (ids,impls as env) = function
| Slam(loc,ona,body) ->
let na,ids' = match ona with
- | Some s ->
- if n>0 then check_capture loc s ty body;
- let id = id_of_string s in Name id, Idset.add id ids
+ | Some id ->
+ if n>0 then check_capture loc id ty body;
+ Name id, Idset.add id ids
| _ -> Anonymous, ids
in
let r = iterated_binder oper (n+1) ty (ids',impls) body in
@@ -614,16 +611,15 @@ let ast_adjust_consts sigma =
| Node(loc, ("APPLIST" as key), (Node(locs,"QUALID",p) as ast)::args) ->
let f = adjust_qualid env loc ast (interp_qualid p) in
Node(loc, key, f :: List.map (dbrec env) args)
- | Nvar (loc, s) as ast ->
- let id = id_of_string s in
- if isMeta s then ast
- else if Idset.mem id env then ast
- else adjust_qualid env loc ast (make_qualid [] (id_of_string s))
+ | Nmeta (loc, s) as ast -> ast
+ | Nvar (loc, id) as ast ->
+ if Idset.mem id env then ast
+ else adjust_qualid env loc ast (make_qualid [] id)
| Node (loc, "QUALID", p) as ast ->
adjust_qualid env loc ast (interp_qualid p)
| Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
| Slam (loc, Some na, t) ->
- let env' = Idset.add (id_of_string na) env in
+ let env' = Idset.add na env in
Slam (loc, Some na, dbrec env' t)
| Node (loc, opn, tl) -> Node (loc, opn, List.map (dbrec env) tl)
| x -> x
@@ -653,7 +649,7 @@ let rec glob_ast sigma env =
Node (loc, "CONSTRLIST", List.map (ast_adjust_consts sigma env) l)
| Slam (loc, None, t) -> Slam (loc, None, glob_ast sigma env t)
| Slam (loc, Some na, t) ->
- let env' = Idset.add (id_of_string na) env in
+ let env' = Idset.add 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
@@ -727,20 +723,14 @@ let retype_list sigma env lst =
(* of instantiations (variables and metas) *)
(* Note: typ is retyped *)
let interp_constr_gen sigma env lvar lmeta com exptyp =
- let c =
- interp_rawconstr_gen sigma env [] false
- (List.map (fun x -> string_of_id (fst x)) lvar)
- com
+ let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) com
and rtype lst = retype_list sigma env lst in
understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
(*Interprets a casted constr according to two lists of instantiations
(variables and metas)*)
let interp_openconstr_gen sigma env lvar lmeta com exptyp =
- let c =
- interp_rawconstr_gen sigma env [] false
- (List.map (fun x -> string_of_id (fst x)) lvar)
- com
+ let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) com
and rtype lst = retype_list sigma env lst in
understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
@@ -807,9 +797,7 @@ let interp_constrpattern_gen sigma env lvar com =
let c =
ast_to_rawconstr sigma
(from_list (ids_of_rel_context (rel_context env)), [])
- true (List.map
- (fun x ->
- string_of_id (fst x)) lvar,named_context env) com
+ true (List.map fst lvar,named_context env) com
and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
try
pattern_of_rawconstr nlvar c
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index 81df802bc0..7604818f25 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -8,16 +8,22 @@
(* $Id$ *)
+(*i*)
+open Names
+(*i*)
+
type loc = int * int
type t =
| Node of loc * string * t list
- | Nvar of loc * string
- | Slam of loc * string option * t
+ | Nmeta of loc * string
+ | Nvar of loc * identifier
+ | Slam of loc * identifier option * t
+ | Smetalam of loc * string * t
| Num of loc * int
- | Id of loc * string
| Str of loc * string
- | Path of loc * string list* string
+ | Id of loc * string
+ | Path of loc * section_path
| Dynamic of loc * Dyn.t
type the_coq_ast = t
@@ -28,6 +34,7 @@ let subst_meta bl ast =
| Node(loc, node_name, args) ->
Node(loc, node_name, List.map aux args)
| Slam(loc, var, arg) -> Slam(loc, var, aux arg)
+ | Smetalam(loc, var, arg) -> Smetalam(loc, var, aux arg)
| other -> other
in
aux ast
@@ -36,6 +43,7 @@ let rec collect_metas = function
| Node (_,"META", [Num(_, n)]) -> [n]
| Node(_, _, args) -> List.concat (List.map collect_metas args)
| Slam(loc, var, arg) -> collect_metas arg
+ | Smetalam(loc, var, arg) -> collect_metas arg
| _ -> []
(* Hash-consing *)
@@ -51,38 +59,41 @@ module Hloc = Hashcons.Make(
module Hast = Hashcons.Make(
struct
type t = the_coq_ast
- type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string))
- let hash_sub (hast,(hloc,hstr)) = function
+ type u =
+ (the_coq_ast -> the_coq_ast) *
+ ((loc -> loc) * (string -> string)
+ * (identifier -> identifier) * (section_path -> section_path))
+ let hash_sub (hast,(hloc,hstr,hid,hsp)) = function
| Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
- | Nvar(l,s) -> Nvar(hloc l, hstr s)
+ | Nmeta(l,s) -> Nmeta(hloc l, hstr s)
+ | Nvar(l,s) -> Nvar(hloc l, hid s)
| Slam(l,None,t) -> Slam(hloc l, None, hast t)
- | Slam(l,Some s,t) -> Slam(hloc l, Some (hstr s), hast t)
+ | Slam(l,Some s,t) -> Slam(hloc l, Some (hid s), hast t)
+ | Smetalam(l,s,t) -> Smetalam(hloc l, hstr s, hast t)
| Num(l,n) -> Num(hloc l, n)
| Id(l,s) -> Id(hloc l, hstr s)
| Str(l,s) -> Str(hloc l, hstr s)
- | Path(l,d,k) -> Path(hloc l, List.map hstr d, hstr k)
+ | Path(l,d) -> Path(hloc l, hsp d)
| Dynamic(l,d) -> Dynamic(hloc l, d)
let equal a1 a2 =
match (a1,a2) with
| (Node(l1,s1,al1), Node(l2,s2,al2)) ->
(l1==l2 & s1==s2 & List.length al1 = List.length al2)
& List.for_all2 (==) al1 al2
+ | (Nmeta(l1,s1), Nmeta(l2,s2)) -> l1==l2 & s1==s2
| (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
| (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
- | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) -> l1==l2 & t1==t2
+ | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) ->l1==l2 & s1==s2 & t1==t2
+ | (Smetalam(l1,s1,t1), Smetalam(l2,s2,t2)) -> l1==l2 & s1==s2 & t1==t2
| (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
| (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
| (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
- | (Path(l1,d1,k1), Path(l2,d2,k2)) ->
- (l1==l2 & k1==k2 & List.length d1 = List.length d2)
- & List.for_all2 (==) d1 d2
+ | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2)
| _ -> false
let hash = Hashtbl.hash
end)
-let hcons_ast hstr =
+let hcons_ast (hstr,hid,hpath) =
let hloc = Hashcons.simple_hcons Hloc.f () in
- let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr) in
+ let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in
(hast,hloc)
-
-
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 255611c463..f741574e82 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -8,18 +8,24 @@
(*i $Id$ i*)
+(*i*)
+open Names
+(*i*)
+
(* Abstract syntax trees. *)
type loc = int * int
type t =
| Node of loc * string * t list
- | Nvar of loc * string
- | Slam of loc * string option * t
+ | Nmeta of loc * string
+ | Nvar of loc * identifier
+ | Slam of loc * identifier option * t
+ | Smetalam of loc * string * t
| Num of loc * int
- | Id of loc * string
| Str of loc * string
- | Path of loc * string list* string
+ | Id of loc * string
+ | Path of loc * section_path
| Dynamic of loc * Dyn.t
(* returns the list of metas occuring in the ast *)
@@ -30,5 +36,7 @@ val collect_metas : t -> int list
val subst_meta : (int * t) list -> t -> t
(* hash-consing function *)
-val hcons_ast: (string -> string) -> (t -> t) * (loc -> loc)
-
+val hcons_ast:
+ (string -> string) * (Names.identifier -> Names.identifier)
+ * (section_path -> section_path)
+ -> (t -> t) * (loc -> loc)
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 88548def38..dca396ea21 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -15,9 +15,20 @@ open Declare
open Pattern
open Nametab
-let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
+let make_dir l = make_dirpath (List.map id_of_string l)
+let coq_id = id_of_string "Coq"
+let init_id = id_of_string "Init"
+let arith_id = id_of_string "Arith"
+let datatypes_id = id_of_string "Datatypes"
+
+let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
+let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
+let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+let nat_path = make_path datatypes_module (id_of_string "nat") CCI
let myvar_path =
- make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
+ make_path arith_module (id_of_string "My_special_variable") CCI
let glob_nat = IndRef (nat_path,0)
@@ -26,14 +37,14 @@ let glob_S = ConstructRef ((nat_path,0),2)
let glob_My_special_variable_nat = ConstRef myvar_path
-let eq_path = make_path ["Coq";"Init";"Logic"] (id_of_string "eq") CCI
-let eqT_path = make_path ["Coq";"Init";"Logic_Type"] (id_of_string "eqT") CCI
+let eq_path = make_path logic_module (id_of_string "eq") CCI
+let eqT_path = make_path logic_type_module (id_of_string "eqT") CCI
let glob_eq = IndRef (eq_path,0)
let glob_eqT = IndRef (eqT_path,0)
let reference dir s =
- let dir = "Coq"::"Init"::[dir] in
+ let dir = make_dir ("Coq"::"Init"::[dir]) in
let id = id_of_string s in
try
Nametab.locate_in_absolute_module dir id
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
index b4e66f9f27..92292161af 100644
--- a/parsing/coqlib.mli
+++ b/parsing/coqlib.mli
@@ -18,6 +18,10 @@ open Pattern
(*s Global references *)
+(* Modules *)
+val logic_module : Names.dir_path
+val logic_type_module : Names.dir_path
+
(* Natural numbers *)
val glob_nat : global_reference
val glob_O : global_reference
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 64f7d877e6..28be507232 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -23,9 +23,9 @@ open Extend
* according to the key of the pattern. *)
type key =
- | Cst of string list (* keys for global constants rules *)
- | Ind of string list * int
- | Cstr of (string list * int) * int
+ | Cst of Names.section_path (* keys for global constants rules *)
+ | Ind of Names.section_path * int
+ | Cstr of (Names.section_path * int) * int
| Nod of string (* keys for other constructed asts rules *)
| Oth (* key for other syntax rules *)
| All (* key for catch-all rules (i.e. with a pattern such as $x .. *)
@@ -33,12 +33,12 @@ type key =
let warning_verbose = ref true
let ast_keys = function
- | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl,_)]) ::_) ->
+ | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) ->
[Cst sl; Nod "APPLIST"; All]
- | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl,_); Num (_,tyi)]) ::_) ->
+ | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl); Num (_,tyi)]) ::_) ->
[Ind (sl,tyi); Nod "APPLIST"; All]
| Node(_,"APPLIST", Node(_,"MUTCONSTRUCT",
- [Path (_,sl,_); Num (_,tyi); Num (_,i)]) ::_) ->
+ [Path (_,sl); Num (_,tyi); Num (_,i)]) ::_) ->
[Cstr ((sl,tyi),i); Nod "APPLIST"; All]
| Node(_,s,_) -> [Nod s; All]
| _ -> [Oth; All]
@@ -47,16 +47,16 @@ let spat_key astp =
match astp with
| Pnode("APPLIST",
Pcons(Pnode("CONST",
- Pcons(Pquote(Path (_,sl,s)),_)), _))
+ Pcons(Pquote(Path (_,sl)),_)), _))
-> Cst sl
| Pnode("APPLIST",
Pcons(Pnode("MUTIND",
- Pcons(Pquote(Path (_,sl,s)),
+ Pcons(Pquote(Path (_,sl)),
Pcons(Pquote(Num (_,tyi)),_))), _))
-> Ind (sl,tyi)
| Pnode("APPLIST",
Pcons(Pnode("MUTCONSTRUCT",
- Pcons(Pquote(Path (_,sl,s)),
+ Pcons(Pquote(Path (_,sl)),
Pcons(Pquote(Num (_,tyi)),
Pcons(Pquote(Num (_,i)),_)))), _))
-> Cstr ((sl,tyi),i)
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index d3c0eecba7..2c74daa860 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -114,14 +114,9 @@ let nterm univ ast =
let prod_item univ env ast =
match ast with
| Str (_, s) -> env, Term (terminal s)
- | Node (_, "NT", [nt; Nvar (locp, p)]) ->
+ | Node (_, "NT", [nt; Nmeta (locp, p)]) ->
let (nont, etyp) = nterm univ nt in
- if isMeta p then
- ((p, etyp) :: env, NonTerm (nont, etyp, Some p))
- else
- user_err_loc
- (locp,"Extend.prod_item",
- [< 'sTR"This ident is not a metavariable." >])
+ ((p, etyp) :: env, NonTerm (nont, etyp, Some p))
| Node (_, "NT", [nt]) ->
let (nont, etyp) = nterm univ nt in
env, NonTerm (nont, etyp, None)
@@ -150,10 +145,10 @@ let gram_entry univ (nt, etyp, ass, rl) =
gl_rules = List.map (gram_rule univ etyp) rl }
let gram_assoc = function
- | Id (_, "LEFTA") -> Some LeftA
- | Id (_, "RIGHTA") -> Some RightA
- | Id (_, "NONA") -> Some NonA
- | Id (_, "NONE") -> None
+ | Node (_, "LEFTA", []) -> Some LeftA
+ | Node (_, "RIGHTA", []) -> Some RightA
+ | Node (_, "NONA", []) -> Some NonA
+ | Node (_, "NONE", []) -> None
| ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.assoc")
let gram_define_entry univ = function
@@ -168,10 +163,10 @@ let gram_define_entry univ = function
try
create_entry univ nt etyp
with Failure s ->
- user_err_loc (ntl,"Extend.gram_define_entry",[< 'sTR s >])
+ user_err_loc (ntl,"gram_define_entry",[< 'sTR s >])
in
(nt, etyp, assoc, rl)
- | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.gram_define_entry")
+ | ast -> invalid_arg_loc (Ast.loc ast, "gram_define_entry")
let interp_grammar_command univ astl =
@@ -252,7 +247,7 @@ let rec unparsing_hunk_of_ast vars = function
| Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) ->
let (ppex, rel) = extern_of_ast loc ext_args in
PH (Ast.val_of_ast vars e, Some ppex, rel)
- | Node(loc, "PH", [e; Id(_,pr)]) ->
+ | Node(loc, "PH", [e; Node(_,pr, [])]) ->
let reln =
(match pr with
| "L" -> L
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f3d066f2f4..7e48d545ae 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -28,14 +28,14 @@ GEXTEND Gram
[ [ l = LIST1 identarg -> l ] ]
;
qualidarg:
- [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ]
+ [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST $l)) >> ] ]
;
ne_qualidarg_list:
[ [ q = qualidarg; l = ne_qualidarg_list -> q::l
| q = qualidarg -> [q] ] ]
;
qualidconstarg:
- [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST l)) >> ] ]
+ [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST $l)) >> ] ]
;
numarg:
[ [ n = Prim.number -> n
@@ -81,7 +81,7 @@ GEXTEND Gram
command:
[ [ IDENT "Comments"; args = commentarg_list ->
- <:ast< (Comments ($LIST args)) >>
+ <:ast< (Comments ($LIST $args)) >>
| IDENT "Pwd" -> <:ast< (PWD) >>
| IDENT "Cd" -> <:ast< (CD) >>
| IDENT "Cd"; dir = stringarg -> <:ast< (CD $dir) >>
@@ -114,7 +114,7 @@ GEXTEND Gram
| IDENT "Locate"; IDENT "File"; f = stringarg ->
<:ast< (LocateFile $f) >>
- | IDENT "Locate"; IDENT "Library"; id = identarg ->
+ | IDENT "Locate"; IDENT "Library"; id = qualidarg ->
<:ast< (LocateLibrary $id) >>
| IDENT "Locate"; id = qualidarg ->
<:ast< (Locate $id) >>
@@ -199,17 +199,17 @@ GEXTEND Gram
(* Set printing of coercions *)
| "Set"; IDENT "Printing"; IDENT "Coercion";
qidl = ne_qualidarg_list ->
- <:ast< (PRINTING_COERCIONS_ON ($LIST qidl)) >>
+ <:ast< (PRINTING_COERCIONS_ON ($LIST $qidl)) >>
| "Set"; IDENT "Printing"; IDENT "Coercions" ->
<:ast< (PRINTING_COERCIONS_ON) >>
| IDENT "Unset"; IDENT "Printing"; IDENT "Coercion";
qidl = ne_qualidarg_list ->
- <:ast< (PRINTING_COERCIONS_OFF ($LIST qidl)) >>
+ <:ast< (PRINTING_COERCIONS_OFF ($LIST $qidl)) >>
| IDENT "Unset"; IDENT "Printing"; IDENT "Coercions" ->
<:ast< (PRINTING_COERCIONS_OFF) >>
| IDENT "Test"; IDENT "Printing"; IDENT "Coercion";
qidl = ne_qualidarg_list ->
- <:ast< (TEST_PRINTING_COERCIONS ($LIST qidl)) >>
+ <:ast< (TEST_PRINTING_COERCIONS ($LIST $qidl)) >>
| IDENT "Test"; IDENT "Printing"; IDENT "Coercions" ->
<:ast< (TEST_PRINTING_COERCIONS) >>
@@ -289,10 +289,10 @@ GEXTEND Gram
| "Grammar"; univ = univ;
tl = LIST1 Prim.grammar_entry SEP "with" ->
- <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
+ <:ast< (GRAMMAR { $univ } (ASTLIST ($LIST $tl))) >>
| "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";" ->
- <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >>
+ <:ast< (SYNTAX { $univ } (ASTLIST ($LIST $el))) >>
(* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
| IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
@@ -308,18 +308,18 @@ GEXTEND Gram
Prim.grammar_entry:
[[ nont = Prim.ident; etyp = Prim.entry_type; ":=";
ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
- <:ast< (GRAMMARENTRY $nont $etyp $ep ($LIST rl)) >> ]]
+ <:ast< (GRAMMARENTRY $nont $etyp $ep ($LIST $rl)) >> ]]
;
entry_prec:
- [[ IDENT "LEFTA" -> <:ast< {LEFTA} >>
- | IDENT "RIGHTA" -> <:ast< {RIGHTA} >>
- | IDENT "NONA" -> <:ast< {NONA} >>
- | -> <:ast< {NONE} >> ] ]
+ [[ IDENT "LEFTA" -> <:ast< (LEFTA) >>
+ | IDENT "RIGHTA" -> <:ast< (RIGHTA) >>
+ | IDENT "NONA" -> <:ast< (NONA) >>
+ | -> <:ast< (NONE) >> ] ]
;
grammar_rule:
[[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
a = Prim.astact ->
- <:ast< (GRAMMARRULE ($ID name) $a ($LIST pil)) >> ]]
+ <:ast< (GRAMMARRULE ($ID $name) $a ($LIST $pil)) >> ]]
;
rule_name:
[[ name = IDENT -> name ]]
@@ -369,7 +369,7 @@ GEXTEND Gram
| e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] ->
match oprec with
| Some pr -> <:ast< (PH $e $pr) >>
- | None -> <:ast< (PH $e {Any}) >> ]]
+ | None -> <:ast< (PH $e (Any)) >> ]]
;
box:
[ [ "<"; bk = box_kind; ">" -> bk ] ]
@@ -382,8 +382,8 @@ GEXTEND Gram
| IDENT "t" -> <:ast< (PpTB) >> ] ]
;
paren_reln_or_extern:
- [ [ IDENT "L" -> <:ast< {L} >>
- | IDENT "E" -> <:ast< {E} >>
+ [ [ IDENT "L" -> <:ast< (L) >>
+ | IDENT "E" -> <:ast< (E) >>
| pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
match precrec with
| Some p -> <:ast< (EXTERN ($STR $pprim) $p) >>
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 52c35ce043..3ce0e7b4a8 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -26,7 +26,7 @@ GEXTEND Gram
| p = pattern; "as"; id = ident ->
<:ast< (PATTAS $id $p)>>
| p1 = pattern; ","; p2 = pattern ->
- <:ast< (PATTCONSTRUCT (QUALID Datatypes pair) $p1 $p2) >>
+ <:ast< (PATTCONSTRUCT Coq.Init.Datatypes.pair $p1 $p2) >>
| p = pattern -> p ] ]
;
ne_pattern_list:
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e0a7e61ae7..92e2262f34 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -19,18 +19,29 @@ GEXTEND Gram
ne_ident_comma_list ne_constr_list sort ne_binders_list qualid
global;
ident:
- [ [ id = IDENT -> <:ast< ($VAR $id) >>
+ [ [ id = Prim.var -> id
(* This is used in quotations *)
- | id = METAIDENT -> <:ast< ($VAR $id) >> ] ]
+ | id = Prim.metaident -> id ] ]
;
global:
- [ [ l = qualid -> <:ast< (QUALID ($LIST l)) >>
+ [ [ l = qualid -> <:ast< (QUALID ($LIST $l)) >>
(* This is used in quotations *)
- | id = METAIDENT -> <:ast< ($VAR $id) >> ] ]
+ | id = Prim.metaident -> id ] ]
;
qualid:
+ [ [ id = Prim.var; l = fields -> id :: l
+ | id = Prim.var -> [ id ]
+ ] ]
+ ;
+ fields:
+ [ [ id = FIELD; l = fields -> <:ast< ($VAR $id) >> :: l
+ | id = FIELD -> [ <:ast< ($VAR $id) >> ]
+ ] ]
+ ;
+(*
+ qualid:
[ [ id = IDENT; l = fields -> <:ast< ($VAR $id) >> :: l ] ]
;
fields:
@@ -38,6 +49,7 @@ GEXTEND Gram
| -> []
] ]
;
+*)
raw_constr:
[ [ c = Prim.ast -> c ] ]
;
@@ -65,18 +77,19 @@ GEXTEND Gram
| "?"; n = Prim.number -> <:ast< (META $n) >>
| bl = binders; c = constr -> <:ast< ($ABSTRACT "LAMBDALIST" $bl $c) >>
| "("; lc1 = lconstr; ":"; c = constr; body = product_tail ->
- let id = Ast.coerce_to_var "lc1" lc1 in
+ let id = Ast.coerce_to_var lc1 in
<:ast< (PROD $c [$id]$body) >>
| "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
body = product_tail ->
- let id1 = Ast.coerce_to_var "lc1" lc1 in
- let id2 = Ast.coerce_to_var "lc2" lc2 in
- <:ast< (PRODLIST $c [$id1][$id2]$body) >>
+ let id1 = Ast.coerce_to_var lc1 in
+ let id2 = Ast.coerce_to_var lc2 in
+ <:ast< (PRODLIST $c [$id1][$id2]$body) >>
| "("; lc1 = lconstr; ","; lc2 = lconstr; ",";
idl = ne_ident_comma_list; ":"; c = constr; body = product_tail ->
- let id1 = Ast.coerce_to_var "lc1" lc1 in
- let id2 = Ast.coerce_to_var "lc2" lc2 in
- <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
+ let id1 = Ast.coerce_to_var lc1 in
+ let id2 = Ast.coerce_to_var lc2 in
+(* <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>*)
+ <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER $c $id1 $id2 ($LIST $idl))) $body) >>
| "("; lc1 = lconstr; ")" -> lc1
| "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
<:ast< (SOAPP $lc1 ($LIST $cl)) >>
@@ -109,9 +122,15 @@ GEXTEND Gram
<:ast< (MATCH "SYNTH" $c ($LIST $cl)) >>
| IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = constr; "in"; c1 = constr ->
- <:ast< (LET "SYNTH" $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
+ <:ast< (LET "SYNTH" $c ($ABSTRACT "LAMBDALIST"
+ (BINDERS (BINDER (ISEVAR) ($LIST $b))) $c1)) >>
+ | IDENT "let"; id1 = ident ; "="; c = constr; "in"; c1 = constr ->
+ <:ast< (LETIN $c [$id1]$c1) >>
+(*
| IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr ->
+ let id1 = Names.id_of_string id1 in
<:ast< (LETIN $c [$id1]$c1) >>
+*)
| IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
IDENT "else"; c3 = constr ->
<:ast< ( IF "SYNTH" $c1 $c2 $c3) >>
@@ -119,7 +138,9 @@ GEXTEND Gram
| "<"; l1 = lconstr; ">";
IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = constr; "in"; c1 = constr ->
- <:ast< (LET $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
+(* <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>*)
+ <:ast< (LET $l1 $c ($ABSTRACT "LAMBDALIST" (BINDERS
+ (BINDER (ISEVAR) ($LIST $b))) $c1)) >>
| "<"; l1 = lconstr; ">";
IDENT "if"; c1 = constr; IDENT "then";
c2 = constr; IDENT "else"; c3 = constr ->
@@ -180,11 +201,14 @@ GEXTEND Gram
| id = vardecls -> [id] ] ]
;
binders:
+ [ [ "["; bl = ne_vardecls_list; "]" -> <:ast< (BINDERS ($LIST $bl)) >> ] ]
+ ;
+ rawbinders:
[ [ "["; bl = ne_vardecls_list; "]" -> bl ] ]
;
ne_binders_list:
- [ [ bl = binders; bll = ne_binders_list -> bl @ bll
- | bl = binders -> bl ] ]
+ [ [ bl = rawbinders; bll = ne_binders_list -> bl @ bll
+ | bl = rawbinders -> bl ] ]
;
type_option:
[ [ ":"; c = constr -> c
@@ -206,9 +230,9 @@ GEXTEND Gram
fixbinder:
[ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = constr;
":="; def = constr -> <:ast< (NUMFDECL $id $recarg $type_ $def) >>
- | id = ident; idl = ne_binders_list; ":"; type_ = constr;
+ | id = ident; bl = ne_binders_list; ":"; type_ = constr;
":="; def = constr ->
- <:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ]
+ <:ast< (FDECL $id (BINDERS ($LIST $bl)) $type_ $def) >> ] ]
;
fixbinders:
[ [ fb = fixbinder; "with"; fbs = fixbinders -> fb::fbs
@@ -225,9 +249,9 @@ GEXTEND Gram
product_tail:
[ [ ";"; idl = ne_ident_comma_list;
":"; c = constr; c2 = product_tail ->
- <:ast< (PRODLIST $c ($SLAM $idl $c2)) >>
+ <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER $c ($LIST $idl))) $c2) >>
| ";"; idl = ne_ident_comma_list; c2 = product_tail ->
- <:ast< (PRODLIST (ISEVAR) ($SLAM $idl $c2)) >>
+ <:ast< ($ABSTRACT "PRODLIST" (BINDERS (BINDER (ISEVAR) ($LIST $idl))) $c2) >>
| ")"; c = constr -> c ] ]
;
END;;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b027f8f4de..dc69dca1ad 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -48,8 +48,8 @@ GEXTEND Gram
[ [ id = constrarg; "["; pc = constrarg; "]" ->
(match id with
| Coqast.Node(_,"COMMAND",
- [Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)])]) ->
- <:ast< (SUBTERM ($VAR $s) $pc) >>
+ [Coqast.Node(_,"QUALID",[Coqast.Nvar(_,_) as s])]) ->
+ <:ast< (SUBTERM $s $pc) >>
| _ ->
errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
| "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >>
@@ -124,7 +124,7 @@ GEXTEND Gram
<:ast< (MATCH $com ($LIST $mrl)) >>
| "("; te = tactic_expr; ")" -> te
| "("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
- <:ast< (APP $te ($LIST tel)) >>
+ <:ast< (APP $te ($LIST $tel)) >>
| IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
<:ast<(FIRST ($LIST $l))>>
| IDENT "Info"; tc = tactic_expr -> <:ast< (INFO $tc) >>
@@ -152,8 +152,8 @@ GEXTEND Gram
| l = Constr.qualid ->
(match l with
| [id] -> id
- | _ -> <:ast< (QUALIDARG ($LIST l)) >>)
- | id = METAIDENT -> <:ast< ($VAR $id) >>
+ | _ -> <:ast< (QUALIDARG ($LIST $l)) >>)
+ | id = Prim.metaident -> id
| "?" -> <:ast< (COMMAND (ISEVAR)) >>
| "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
| IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 9c50e1fcfe..7955660650 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -10,17 +10,18 @@
open Coqast
open Pcoq
-
+open Names
open Prim
GEXTEND Gram
- GLOBAL: var ident metaident number string path ast astpat astact entry_type;
+ GLOBAL: var ident metaident number string (*path*) ast astpat
+ astact entry_type;
- var:
- [ [ s = IDENT -> Nvar(loc,s) ] ]
- ;
metaident:
- [ [ s = METAIDENT -> Nvar(loc,s) ] ]
+ [ [ s = METAIDENT -> Nmeta(loc,s) ] ]
+ ;
+ var:
+ [ [ s = IDENT -> Nvar(loc, id_of_string s) ] ]
;
ident:
[ [ s = IDENT -> Id(loc,s) ] ]
@@ -32,31 +33,54 @@ GEXTEND Gram
[ [ s = STRING -> Str(loc,s) ] ]
;
astpath:
- [ [ (l,pk) = astqualid -> Path(loc,l,pk) ] ]
+ [ [ id = IDENT; (l,a) = astfields ->
+ Path(loc, make_path (make_dirpath (id_of_string id :: l)) a CCI)
+ | id = IDENT ->
+ Path(loc, make_path (make_dirpath []) (id_of_string id) Names.CCI)
+ ] ]
;
- astqualid:
- [ [ "#"; l = LIST1 IDENT SEP "#"; "."; pk = IDENT -> (l, pk) ] ]
+ astfields:
+ [ [ id = FIELD; (l,a) = astfields -> id_of_string id :: l, a
+ | id = FIELD -> [], id_of_string id
+ ] ]
;
astident:
- [ [ s = IDENT -> s
- | s = METAIDENT -> s ] ]
+ [ [ s = IDENT -> s ] ]
;
(* ast *)
ast:
- [ [ id = astident -> Nvar(loc,id)
- | s = INT -> Num(loc, int_of_string s)
- | s = STRING -> Str(loc,s)
+ [ [ id = metaident -> id
| p = astpath -> p
- | "{"; s = IDENT; "}" -> Id(loc,s)
+ | s = INT -> Num(loc, int_of_string s)
+ | s = STRING -> Str(loc, s)
+ | "{"; s = METAIDENT; "}" -> Id(loc,s)
| "("; nname = astident; l = LIST0 ast; ")" -> Node(loc,nname,l)
+ | "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id])
+ | "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id])
+ | "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id])
+ | "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id])
+ | "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l)
+ | "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id])
+ | "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id])
+ | "["; "<>"; "]"; b = ast -> Slam(loc,None,b)
+ | "["; a = ast; "]"; b = ast ->
+ (match a with
+ | Nvar (_,id) -> Slam(loc,Some id,b)
+ | Nmeta (_,s) -> Smetalam(loc,s,b)
+ | _ -> failwith "Slam expects a var or a metavar")
+
+(*
| "["; ido = astidoption; "]"; b = ast -> Slam(loc,ido,b)
+ | "["; id = METAIDENT; "]"; b = ast -> Smetalam(loc,id,b)
+*)
| "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
;
+(*
astidoption:
[ [ "<>" -> None
- | id = astident -> Some id ] ]
+ | id = IDENT -> Some (id_of_string id) ] ]
;
-
+*)
(* meta-syntax entries *)
astpat:
[ [ "<<" ; a = ast; ">>" -> Node loc "ASTPAT" [a]
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 1cce6719d5..ff42bc01d0 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -16,8 +16,10 @@ exception Non_closed_number
let get_r_sign loc =
let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
- ((ast_of_id "R0", ast_of_id "R1", ast_of_id "Rplus",
- ast_of_id "NRplus"))
+ ((ast_of_id (id_of_string "R0"),
+ ast_of_id (id_of_string "R1"),
+ ast_of_id (id_of_string "Rplus"),
+ ast_of_id (id_of_string "NRplus")))
let r_of_int n dloc =
let (ast0,ast1,astp,_) = get_r_sign dloc in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c93f807025..b1f68d0701 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -58,11 +58,11 @@ GEXTEND Gram
[ [ id = idmeta_arg -> <:ast< (INHYP $id) >> ] ]
;
qualidarg:
- [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
+ [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST $l)) >>
| "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ]
;
qualidconstarg:
- [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST l)) >> ] ]
+ [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST $l)) >> ] ]
;
pure_numarg:
[ [ n = Prim.number -> n
@@ -94,8 +94,8 @@ GEXTEND Gram
ident_or_constrarg:
[ [ c = Constr.constr ->
match c with
- | Coqast.Nvar(_,s) -> <:ast<($VAR $s)>>
- | Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>>
+ | Coqast.Nvar(_,s) -> c
+ | Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s) as c]) -> c
| _ -> <:ast< (COMMAND $c) >> ] ]
;
ne_identarg_list:
@@ -167,9 +167,9 @@ GEXTEND Gram
binding_list:
[ [ c1 = constrarg; ":="; c2 = constrarg; bl = simple_binding_list ->
let id = match c1 with
- | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
+ | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
| _ -> assert false
- in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>>
+ in <:ast<(BINDINGS (BINDING $id $c2) ($LIST $bl))>>
| n = pure_numarg; ":="; c = constrarg; bl = simple_binding_list ->
<:ast<(BINDINGS (BINDING $n $c) ($LIST $bl))>>
| c1 = constrarg; bl = com_binding_list ->
@@ -203,20 +203,20 @@ GEXTEND Gram
| IDENT "Iota" -> <:ast< (Iota) >>
| IDENT "Zeta" -> <:ast< (Zeta) >>
| IDENT "Evar" -> <:ast< (Evar) >>
- | "["; idl = ne_qualidarg_list; "]" -> <:ast< (Unf ($LIST idl)) >>
+ | "["; idl = ne_qualidarg_list; "]" -> <:ast< (Unf ($LIST $idl)) >>
| "-"; "["; idl = ne_qualidarg_list; "]" ->
- <:ast< (UnfBut ($LIST idl)) >> ] ]
+ <:ast< (UnfBut ($LIST $idl)) >> ] ]
;
red_tactic:
[ [ IDENT "Red" -> <:ast< (Red) >>
| IDENT "Hnf" -> <:ast< (Hnf) >>
| IDENT "Simpl" -> <:ast< (Simpl) >>
- | IDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST s)) >>
- | IDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST s)) >>
+ | IDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST $s)) >>
+ | IDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST $s)) >>
| IDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Evar) (Iota) (Zeta)) >>
| IDENT "Unfold"; ul = ne_unfold_occ_list ->
- <:ast< (Unfold ($LIST ul)) >>
- | IDENT "Fold"; cl = constrarg_list -> <:ast< (Fold ($LIST cl)) >>
+ <:ast< (Unfold ($LIST $ul)) >>
+ | IDENT "Fold"; cl = constrarg_list -> <:ast< (Fold ($LIST $cl)) >>
| IDENT "Pattern"; pl = ne_pattern_list ->
<:ast< (Pattern ($LIST $pl)) >> ] ]
;
@@ -228,7 +228,7 @@ GEXTEND Gram
[ [ l = LIST1 hypident -> l ] ]
;
clausearg:
- [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST idl)) >>
+ [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST $idl)) >>
| -> <:ast< (CLAUSE) >> ] ]
;
fixdecl:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 20bc8732d4..b325dbba91 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -55,8 +55,8 @@ GEXTEND Gram
theorem_body_line:
[ [ n = numarg; ":"; tac = tacarg; "." ->
- <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >>
- | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
+ <:ast< (VERNACCALL "SOLVE" $n (TACTIC $tac)) >>
+ | tac = tacarg; "." -> <:ast< (VERNACCALL "SOLVE" 1 (TACTIC $tac)) >>
] ]
;
theorem_body_line_list:
@@ -113,8 +113,8 @@ GEXTEND Gram
| -> [] ] ]
;
binders_list:
- [ [ idl = Constr.ne_binders_list -> idl
- | -> [] ] ]
+ [ [ idl = Constr.ne_binders_list -> <:ast< (BINDERS ($LIST $idl)) >>
+ | -> <:ast< (BINDERS) >> ] ]
;
gallina:
(* Definition, Goal *)
@@ -170,8 +170,8 @@ GEXTEND Gram
| IDENT "Structure" -> <:ast< "Structure" >> ] ]
;
constructor:
- [ [ id = IDENT; ":"; c = Constr.constr ->
- <:ast< (BINDER $c ($VAR $id)) >> ] ]
+ [ [ id = identarg; ":"; c = Constr.constr ->
+ <:ast< (BINDER $c $id) >> ] ]
;
ne_constructor_list:
[ [ idc = constructor; "|"; l = ne_constructor_list -> idc :: l
@@ -346,16 +346,16 @@ GEXTEND Gram
(* Coercions *)
| IDENT "Coercion"; qid = qualidarg; ":="; c = def_body ->
- let s = Ast.coerce_to_var "qid" qid in
- <:ast< (DEFINITION "COERCION" ($VAR $s) $c) >>
+ let s = Ast.coerce_to_var qid in
+ <:ast< (DEFINITION "COERCION" $s $c) >>
| IDENT "Coercion"; IDENT "Local"; qid = qualidarg; ":=";
c = constrarg ->
- let s = Ast.coerce_to_var "qid" qid in
- <:ast< (DEFINITION "LCOERCION" ($VAR $s) $c) >>
+ let s = Ast.coerce_to_var qid in
+ <:ast< (DEFINITION "LCOERCION" $s $c) >>
| IDENT "Coercion"; IDENT "Local"; qid = qualidarg; ":=";
c1 = Constr.constr; ":"; c2 = Constr.constr ->
- let s = Ast.coerce_to_var "qid" qid in
- <:ast< (DEFINITION "LCOERCION" ($VAR $s) (CONSTR (CAST $c1 $c2))) >>
+ let s = Ast.coerce_to_var qid in
+ <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = qualidarg;
":"; c = qualidarg; ">->"; d = qualidarg ->
<:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
@@ -420,20 +420,20 @@ GEXTEND Gram
<:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
($STR $mname) ($STR $fname))>>
*)
- | IDENT "Read"; IDENT "Module"; id = identarg ->
- <:ast< (ReadModule $id) >>
+ | IDENT "Read"; IDENT "Module"; qid = qualidarg ->
+ <:ast< (ReadModule $qid) >>
| IDENT "Require"; import = import_tok; specif = specif_tok;
- id = identarg -> <:ast< (Require $import $specif $id) >>
+ qid = qualidarg -> <:ast< (Require $import $specif $qid) >>
| IDENT "Require"; import = import_tok; specif = specif_tok;
- id = identarg; filename = stringarg ->
- <:ast< (RequireFrom $import $specif $id $filename) >>
+ qid = qualidarg; filename = stringarg ->
+ <:ast< (RequireFrom $import $specif $qid $filename) >>
| IDENT "Write"; IDENT "Module"; id = identarg ->
<:ast< (WriteModule $id) >>
| IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg ->
<:ast< (WriteModule $id $s) >>
| IDENT "Declare"; IDENT "ML"; IDENT "Module";
l = ne_stringarg_list -> <:ast< (DeclareMLModule ($LIST $l)) >>
- | IDENT "Import"; id = identarg -> <:ast< (ImportModule $id) >>
+ | IDENT "Import"; qid = qualidarg -> <:ast< (ImportModule $qid) >>
]
]
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 96f9bc6111..8b94b4fd7b 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -17,9 +17,14 @@ open Ast
let get_z_sign loc =
let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
- ((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"),
- (ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"),
- (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1"))
+ ((ast_of_id (id_of_string "xI"),
+ ast_of_id (id_of_string "xO"),
+ ast_of_id (id_of_string "xH")),
+ (ast_of_id (id_of_string "ZERO"),
+ ast_of_id (id_of_string "POS"),
+ ast_of_id (id_of_string "NEG")),
+ (ast_of_id (id_of_string "My_special_variable0"),
+ ast_of_id (id_of_string "My_special_variable1")))
let int_array_of_string s =
let a = Array.create (String.length s) 0 in
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 065ed4350d..a3ea85e022 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -116,7 +116,8 @@ let add_token (con, str) = match con with
true
in
if normal_token then add_keyword str else add_special_token str
- | "METAIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" -> ()
+ | "METAIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
+ -> ()
| _ ->
raise (Token.Error ("\
the constructor \"" ^ con ^ "\" is not recognized by Lexer"))
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 8680734efd..05bf62b997 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -133,6 +133,7 @@ let parse_string f x =
let slam_ast (_,fin) id ast =
match id with
| Coqast.Nvar ((deb,_), s) -> Coqast.Slam ((deb,fin), Some s, ast)
+ | Coqast.Nmeta ((deb,_), s) -> Coqast.Smetalam ((deb,fin), s, ast)
| _ -> invalid_arg "Ast.slam_ast"
(* This is to interpret the macro $ABSTRACT used in binders *)
@@ -149,9 +150,11 @@ let abstract_binder_ast (_,fin as loc) name a b =
Coqast.Node((deb,fin),s', [d; List.fold_right (slam_ast loc) l b])
| _ -> invalid_arg "Bad usage of $ABSTRACT macro"
-let abstract_binders_ast loc name =
- List.fold_right (abstract_binder_ast loc name)
-
+let abstract_binders_ast loc name a b =
+ match a with
+ | Coqast.Node(_,"BINDERS",l) ->
+ List.fold_right (abstract_binder_ast loc name) l b
+ | _ -> invalid_arg "Bad usage of $ABSTRACT macro"
type entry_type = ETast | ETastl
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 807d5d8fd7..2f9c69b2e2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -34,7 +34,7 @@ val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
val slam_ast : Coqast.loc -> Coqast.t -> Coqast.t -> Coqast.t
val abstract_binders_ast :
- Coqast.loc -> string -> Coqast.t list -> Coqast.t -> Coqast.t
+ Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t
(* Entry types *)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
new file mode 100644
index 0000000000..da0398dcd5
--- /dev/null
+++ b/parsing/pretty.ml
@@ -0,0 +1,597 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Inductive
+open Sign
+open Reduction
+open Environ
+open Instantiate
+open Library
+open Declare
+open Impargs
+open Libobject
+open Printer
+open Nametab
+
+let print_basename sp = pr_global (ConstRef sp)
+
+let print_closed_sections = ref false
+
+let print_typed_value_in_env env (trm,typ) =
+ [< prterm_env env trm ; 'fNL ;
+ 'sTR " : "; prtype_env env typ ; 'fNL >]
+
+let print_typed_value x = print_typed_value_in_env (Global.env ()) x
+
+let pkprinters = function
+ | FW -> (fprterm,fprterm_env)
+ | CCI -> (prterm,prterm_env)
+ | _ -> anomaly "pkprinters"
+
+let print_impl_args = function
+ | [] -> [<>]
+ | [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >]
+ | l ->
+ [< 'sTR"Positions [";
+ prlist_with_sep (fun () -> [< 'sTR";" >]) (fun i -> [< 'iNT i >]) l;
+ 'sTR"] are implicit" >]
+
+(* To be improved; the type should be used to provide the types in the
+ abstractions. This should be done recursively inside prterm, so that
+ the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
+ synthesizes the type nat of the abstraction on u *)
+
+let print_named_def name body typ =
+ let pbody = prterm body in
+ let ptyp = prtype typ in
+ [< 'sTR "*** ["; 'sTR name ; 'sTR " ";
+ hOV 0 [< 'sTR ":="; 'bRK (1,2); pbody; 'sPC;
+ 'sTR ":"; 'bRK (1,2); ptyp >];
+ 'sTR "]"; 'fNL >]
+
+let print_named_assum name typ =
+ [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]
+
+let print_named_decl (id,c,typ) =
+ let s = string_of_id id in
+ match c with
+ | Some body -> print_named_def s body typ
+ | None -> print_named_assum s typ
+
+let assumptions_for_print lna =
+ List.fold_right (fun na env -> add_name na env) lna empty_names_context
+
+let implicit_args_id id l =
+ if l = [] then
+ [<>]
+ else
+ [< 'sTR"For "; pr_id id; 'sTR": "; print_impl_args l ; 'fNL >]
+
+let implicit_args_msg sp mipv =
+ [< prvecti
+ (fun i mip ->
+ let imps = inductive_implicits_list (sp,i) in
+ [< (implicit_args_id mip.mind_typename imps);
+ prvecti
+ (fun j idc ->
+ let imps = constructor_implicits_list ((sp,i),succ j) in
+ (implicit_args_id idc imps))
+ mip.mind_consnames
+ >])
+ mipv >]
+
+let print_params env params =
+ if List.length params = 0 then
+ [<>]
+ else
+ [< 'sTR "["; pr_rel_context env params; 'sTR "]"; 'bRK(1,2) >]
+
+let print_constructors envpar names types =
+ let pc =
+ [< prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
+ (fun (id,c) -> [< pr_id id; 'sTR " : "; prterm_env envpar c >])
+ (array_map2 (fun n t -> (n,t)) names types) >]
+ in hV 0 [< 'sTR " "; pc >]
+
+let build_inductive sp tyi =
+ let ctxt = context_of_global_reference (IndRef (sp,tyi)) in
+ let ctxt = Array.of_list (instance_from_section_context ctxt) in
+ let mis = Global.lookup_mind_specif ((sp,tyi),ctxt) in
+ let params = mis_params_ctxt mis in
+ let args = extended_rel_list 0 params in
+ let indf = make_ind_family (mis,args) in
+ let arity = get_arity_type indf in
+ let cstrtypes = get_constructors_types indf in
+ let cstrnames = mis_consnames mis in
+ (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
+
+let print_one_inductive sp tyi =
+ let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
+ let env = Global.env () in
+ let envpar = push_rels params env in
+ (hOV 0
+ [< (hOV 0
+ [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); print_params env params;
+ 'sTR ": "; prterm_env envpar arity; 'sTR " :=" >]);
+ 'bRK(1,2); print_constructors envpar cstrnames cstrtypes >])
+
+let print_mutual sp =
+ let mipv = (Global.lookup_mind sp).mind_packets in
+ if Array.length mipv = 1 then
+ let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp 0 in
+ let sfinite =
+ if mipv.(0).mind_finite then "Inductive " else "CoInductive " in
+ let env = Global.env () in
+ let envpar = push_rels params env in
+ (hOV 0 [<
+ 'sTR sfinite ;
+ pr_global (IndRef (sp,0)); 'bRK(1,2);
+ print_params env params; 'bRK(1,5);
+ 'sTR": "; prterm_env envpar arity; 'sTR" :=";
+ 'bRK(0,4); print_constructors envpar cstrnames cstrtypes; 'fNL;
+ implicit_args_msg sp mipv >] )
+ (* Mutual [co]inductive definitions *)
+ else
+ let _,(mipli,miplc) =
+ Array.fold_right
+ (fun mi (n,(li,lc)) ->
+ if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc)))
+ mipv (0,([],[]))
+ in
+ let strind =
+ if mipli = [] then [<>]
+ else [< 'sTR "Inductive"; 'bRK(1,4);
+ (prlist_with_sep
+ (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >])
+ (print_one_inductive sp) mipli); 'fNL >]
+ and strcoind =
+ if miplc = [] then [<>]
+ else [< 'sTR "CoInductive"; 'bRK(1,4);
+ (prlist_with_sep
+ (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >])
+ (print_one_inductive sp) miplc); 'fNL >]
+ in
+ (hV 0 [< 'sTR"Mutual " ;
+ if mipv.(0).mind_finite then
+ [< strind; strcoind >]
+ else
+ [<strcoind; strind>];
+ implicit_args_msg sp mipv >])
+
+(*
+ let env = Global.env () in
+ let evd = Evd.empty in
+ let {mind_packets=mipv} = mib in
+ (* On suppose que tous les inductifs ont les même paramètres *)
+ let nparams = mipv.(0).mind_nparams in
+ let (lpars,_) = decomp_n_prod env evd nparams
+ (body_of_type (mind_user_arity mipv.(0))) in
+ let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
+ let env_ar = push_rels lpars env in
+ let pr_constructor (id,c) =
+ [< pr_id id; 'sTR " : "; prterm_env env_ar c >] in
+ let print_constructors mis =
+ let (_,lC) = mis_type_mconstructs mis in
+ let lidC =
+ array_map2 (fun id c -> (id, snd (decomp_n_prod env evd nparams c)))
+ (mis_consnames mis) lC in
+ let plidC =
+ prvect_with_sep (fun () -> [<'bRK(0,0); 'sTR "| " >])
+ pr_constructor
+ lidC
+ in
+ hV 0 [< 'sTR " "; plidC >]
+ in
+ let params =
+ if nparams = 0 then
+ [<>]
+ else
+ [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in
+ let print_oneind tyi =
+ let mis =
+ build_mis
+ ((sp,tyi),
+ Array.of_list (instance_from_section_context mib.mind_hyps))
+ mib in
+ let (_,arity) = decomp_n_prod env evd nparams
+ (body_of_type (mis_user_arity mis)) in
+ (hOV 0
+ [< (hOV 0
+ [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); params;
+ 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]);
+ 'bRK(1,2); print_constructors mis >])
+ in
+ let mis0 =
+ build_mis
+ ((sp,0),Array.of_list (instance_from_section_context mib.mind_hyps))
+ mib in
+ (* Case one [co]inductive *)
+ if Array.length mipv = 1 then
+ let (_,arity) = decomp_n_prod env evd nparams
+ (body_of_type (mis_user_arity mis0)) in
+ let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in
+ (hOV 0 [< 'sTR sfinite ; pr_global (IndRef (sp,0));
+ if nparams = 0 then
+ [<>]
+ else
+ [< 'sTR" ["; pr_rel_context env lpars; 'sTR "]">];
+ 'bRK(1,5); 'sTR": "; prterm_env env_ar arity; 'sTR" :=";
+ 'bRK(0,4); print_constructors mis0; 'fNL;
+ implicit_args_msg sp mipv >] )
+ (* Mutual [co]inductive definitions *)
+ else
+ let _,(mipli,miplc) =
+ List.fold_left
+ (fun (n,(li,lc)) mi ->
+ if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc)))
+ (0,([],[])) (Array.to_list mipv)
+ in
+ let strind =
+ if mipli = [] then [<>]
+ else [< 'sTR "Inductive"; 'bRK(1,4);
+ (prlist_with_sep
+ (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >])
+ print_oneind
+ (List.rev mipli)); 'fNL >]
+ and strcoind =
+ if miplc = [] then [<>]
+ else [< 'sTR "CoInductive"; 'bRK(1,4);
+ (prlist_with_sep
+ (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >])
+ print_oneind (List.rev miplc)); 'fNL >]
+ in
+ (hV 0 [< 'sTR"Mutual " ;
+ if mis_finite mis0 then
+ [< strind; strcoind >]
+ else
+ [<strcoind; strind>];
+ implicit_args_msg sp mipv >])
+*)
+let print_section_variable sp =
+ let (d,_,_) = get_variable sp in
+ let l = implicits_of_var sp in
+ [< print_named_decl d; print_impl_args l; 'fNL >]
+
+let print_body = function
+ | Some c -> prterm c
+ | None -> [< 'sTR"<no body>" >]
+
+let print_typed_body (val_0,typ) =
+ [< print_body val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >]
+
+let print_constant with_values sep sp =
+ let cb = Global.lookup_constant sp in
+ if kind_of_path sp = CCI then
+ let val_0 = cb.const_body in
+ let typ = cb.const_type in
+ let impls = constant_implicits_list sp in
+ hOV 0 [< (match val_0 with
+ | None ->
+ [< 'sTR"*** [ ";
+ print_basename sp;
+ 'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
+ | _ ->
+ [< print_basename sp;
+ 'sTR sep; 'cUT ;
+ if with_values then
+ print_typed_body (val_0,typ)
+ else
+ [< prtype typ ; 'fNL >] >]);
+ print_impl_args impls; 'fNL >]
+ else
+ hOV 0 [< 'sTR"Fw constant " ;
+ print_basename sp ; 'fNL>]
+
+let print_inductive sp =
+ if kind_of_path sp = CCI then
+ [< print_mutual sp; 'fNL >]
+ else
+ hOV 0 [< 'sTR"Fw inductive definition ";
+ print_basename sp; 'fNL >]
+
+let print_syntactic_def sep sp =
+ let id = basename sp in
+ let c = Syntax_def.search_syntactic_definition sp in
+ [< 'sTR" Syntactif Definition "; pr_id id ; 'sTR sep; pr_rawterm c; 'fNL >]
+
+let print_leaf_entry with_values sep (sp,lobj) =
+ let tag = object_tag lobj in
+ match (sp,tag) with
+ | (_,"VARIABLE") ->
+ print_section_variable sp
+ | (_,("CONSTANT"|"PARAMETER")) ->
+ print_constant with_values sep sp
+ | (_,"INDUCTIVE") ->
+ print_inductive sp
+ | (_,"AUTOHINT") ->
+ [< 'sTR" Hint Marker"; 'fNL >]
+ | (_,"GRAMMAR") ->
+ [< 'sTR" Grammar Marker"; 'fNL >]
+ | (_,"SYNTAXCONSTANT") ->
+ print_syntactic_def sep sp
+ | (_,"PPSYNTAX") ->
+ [< 'sTR" Syntax Marker"; 'fNL >]
+ | (_,"TOKEN") ->
+ [< 'sTR" Token Marker"; 'fNL >]
+ | (_,"CLASS") ->
+ [< 'sTR" Class Marker"; 'fNL >]
+ | (_,"COERCION") ->
+ [< 'sTR" Coercion Marker"; 'fNL >]
+ | (_,"REQUIRE") ->
+ [< 'sTR" Require Marker"; 'fNL >]
+ | (_,"END-SECTION") -> [< >]
+ | (_,s) ->
+ [< 'sTR(string_of_path sp); 'sTR" : ";
+ 'sTR"Unrecognized object "; 'sTR s; 'fNL >]
+
+let rec print_library_entry with_values ent =
+ let sep = if with_values then " = " else " : " in
+ match ent with
+ | (sp,Lib.Leaf lobj) ->
+ [< print_leaf_entry with_values sep (sp,lobj) >]
+ | (_,Lib.OpenedSection (str,_)) ->
+ [< 'sTR(" >>>>>>> Section "^(string_of_id str)); 'fNL >]
+ | (sp,Lib.ClosedSection _) ->
+ [< 'sTR" >>>>>>> Closed Section "; pr_id (basename sp);
+ 'fNL >]
+ | (_,Lib.Module dir) ->
+ [< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >]
+ | (_,Lib.FrozenState _) ->
+ [< >]
+
+and print_context with_values =
+ let rec prec = function
+ | h::rest -> [< prec rest ; print_library_entry with_values h >]
+ | [] -> [< >]
+ in
+ prec
+
+let print_full_context () = print_context true (Lib.contents_after None)
+
+let print_full_context_typ () = print_context false (Lib.contents_after None)
+
+(* For printing an inductive definition with
+ its constructors and elimination,
+ assume that the declaration of constructors and eliminations
+ follows the definition of the inductive type *)
+
+let list_filter_vec f vec =
+ let rec frec n lf =
+ if n < 0 then lf
+ else if f vec.(n) then
+ frec (n-1) (vec.(n)::lf)
+ else
+ frec (n-1) lf
+ in
+ frec (Array.length vec -1) []
+
+let read_sec_context qid =
+ let dir = Nametab.locate_section qid in
+ let rec get_cxt in_cxt = function
+ | ((sp,Lib.OpenedSection (_,_)) as hd)::rest ->
+ let dir' = make_dirpath (wd_of_sp sp) in
+ if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+ | [] -> []
+ | hd::rest -> get_cxt (hd::in_cxt) rest
+ in
+ let cxt = (Lib.contents_after None) in
+ List.rev (get_cxt [] cxt)
+
+let print_sec_context sec = print_context true (read_sec_context sec)
+
+let print_sec_context_typ sec = print_context false (read_sec_context sec)
+
+let print_judgment env {uj_val=trm;uj_type=typ} =
+ print_typed_value_in_env env (trm, typ)
+
+let print_safe_judgment env j =
+ let trm = Safe_typing.j_val j in
+ let typ = Safe_typing.j_type j in
+ print_typed_value_in_env env (trm, typ)
+
+let print_eval red_fun env {uj_val=trm;uj_type=typ} =
+ let ntrm = red_fun env Evd.empty trm in
+ [< 'sTR " = "; print_judgment env {uj_val = ntrm; uj_type = typ} >]
+
+let print_name qid =
+ try
+ let sp = Nametab.locate_obj qid in
+ let (sp,lobj) =
+ let (sp,entry) =
+ List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
+ in
+ match entry with
+ | Lib.Leaf obj -> (sp,obj)
+ | _ -> raise Not_found
+ in
+ print_leaf_entry true " = " (sp,lobj)
+ with Not_found ->
+ try
+ match Nametab.locate qid with
+ | ConstRef sp -> print_constant true " = " sp
+ | IndRef (sp,_) -> print_inductive sp
+ | ConstructRef ((sp,_),_) -> print_inductive sp
+ | VarRef sp -> print_section_variable sp
+ with Not_found ->
+ try (* Var locale de but, pas var de section... donc pas d'implicits *)
+ let dir,str = repr_qualid qid in
+ if dir <> [] then raise Not_found;
+ let (c,typ) = Global.lookup_named str in
+ [< print_named_decl (str,c,typ) >]
+ with Not_found ->
+ try
+ let sp = Syntax_def.locate_syntactic_definition qid in
+ print_syntactic_def " = " sp
+ with Not_found ->
+ errorlabstrm "print_name"
+ [< pr_qualid qid; 'sPC; 'sTR "not a defined object" >]
+
+let print_opaque_name qid =
+ let sigma = Evd.empty in
+ let env = Global.env () in
+ let sign = Global.named_context () in
+ try
+ let x = global_qualified_reference qid in
+ match kind_of_term x with
+ | IsConst (sp,_ as cst) ->
+ let cb = Global.lookup_constant sp in
+ if is_defined cb then
+ print_constant true " = " sp
+ else
+ error "not a defined constant"
+ | IsMutInd ((sp,_),_) ->
+ print_mutual sp
+ | IsMutConstruct cstr ->
+ let ty = Typeops.type_of_constructor env sigma cstr in
+ print_typed_value (x, ty)
+ | IsVar id ->
+ let (c,ty) = lookup_named id env in
+ print_named_decl (id,c,ty)
+ | _ ->
+ assert false
+ with Not_found ->
+ errorlabstrm "print_opaque" [< pr_qualid qid; 'sPC; 'sTR "not declared" >]
+
+let print_local_context () =
+ let env = Lib.contents_after None in
+ let rec print_var_rec = function
+ | [] -> [< >]
+ | (sp,Lib.Leaf lobj)::rest ->
+ if "VARIABLE" = object_tag lobj then
+ let (d,_,_) = get_variable sp in
+ [< print_var_rec rest;
+ print_named_decl d >]
+ else
+ print_var_rec rest
+ | _::rest -> print_var_rec rest
+
+ and print_last_const = function
+ | (sp,Lib.Leaf lobj)::rest ->
+ (match object_tag lobj with
+ | "CONSTANT" | "PARAMETER" ->
+ let {const_body=val_0;const_type=typ} =
+ Global.lookup_constant sp in
+ [< print_last_const rest;
+ print_basename sp ;'sTR" = ";
+ print_typed_body (val_0,typ) >]
+ | "INDUCTIVE" ->
+ [< print_last_const rest;print_mutual sp; 'fNL >]
+ | "VARIABLE" -> [< >]
+ | _ -> print_last_const rest)
+ | _ -> [< >]
+ in
+ [< print_var_rec env; print_last_const env >]
+
+let fprint_var name typ =
+ [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >]
+
+let fprint_judge {uj_val=trm;uj_type=typ} =
+ [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >]
+
+let unfold_head_fconst =
+ let rec unfrec k = match kind_of_term k with
+ | IsConst cst -> constant_value (Global.env ()) cst
+ | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
+ | IsApp (f,v) -> appvect (unfrec f,v)
+ | _ -> k
+ in
+ unfrec
+
+(* for debug *)
+let inspect depth =
+ let rec inspectrec n res env =
+ if n=0 or env=[] then
+ res
+ else
+ inspectrec (n-1) (List.hd env::res) (List.tl env)
+ in
+ let items = List.rev (inspectrec depth [] (Lib.contents_after None)) in
+ print_context false items
+
+
+(*************************************************************************)
+(* Pretty-printing functions coming from classops.ml *)
+
+open Classops
+
+let string_of_strength = function
+ | NotDeclare -> "(temp)"
+ | NeverDischarge -> "(global)"
+ | DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
+
+let print_coercion_value v = prterm (get_coercion_value v)
+
+let print_index_coercion c =
+ let _,v = coercion_info_from_index c in
+ print_coercion_value v
+
+let print_class i =
+ let cl,_ = class_info_from_index i in
+ [< 'sTR (string_of_class cl) >]
+
+let print_path ((i,j),p) =
+ [< 'sTR"[";
+ prlist_with_sep (fun () -> [< 'sTR"; " >])
+ (fun c -> print_index_coercion c) p;
+ 'sTR"] : "; print_class i; 'sTR" >-> ";
+ print_class j >]
+
+let _ = Classops.install_path_printer print_path
+
+let print_graph () =
+ [< prlist_with_sep pr_fnl print_path (inheritance_graph()) >]
+
+let print_classes () =
+ [< prlist_with_sep pr_spc
+ (fun (_,(cl,x)) ->
+ [< 'sTR (string_of_class cl)
+ (*; 'sTR(string_of_strength x.cl_strength) *) >])
+ (classes()) >]
+
+let print_coercions () =
+ [< prlist_with_sep pr_spc
+ (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >]
+
+let cl_of_id id =
+ match string_of_id id with
+ | "FUNCLASS" -> CL_FUN
+ | "SORTCLASS" -> CL_SORT
+ | _ -> let v = Declare.global_reference CCI id in
+ let cl,_ = constructor_at_head v in
+ cl
+
+let index_cl_of_id id =
+ try
+ let cl = cl_of_id id in
+ let i,_ = class_info cl in
+ i
+ with _ ->
+ errorlabstrm "index_cl_of_id"
+ [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+
+let print_path_between ids idt =
+ let i = (index_cl_of_id ids) in
+ let j = (index_cl_of_id idt) in
+ let p =
+ try
+ lookup_path_between (i,j)
+ with _ ->
+ errorlabstrm "index_cl_of_id"
+ [< 'sTR"No path between ";'sTR(string_of_id ids);
+ 'sTR" and ";'sTR(string_of_id ids) >]
+ in
+ print_path ((i,j),p)
+
+(*************************************************************************)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6044767c2c..cbb0ba6640 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -340,13 +340,12 @@ let rec print_library_entry with_values ent =
match ent with
| (sp,Lib.Leaf lobj) ->
[< print_leaf_entry with_values sep (sp,lobj) >]
- | (_,Lib.OpenedSection (str,_)) ->
- [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
+ | (_,Lib.OpenedSection (id,_)) ->
+ [< 'sTR " >>>>>>> Section "; pr_id id; 'fNL >]
| (sp,Lib.ClosedSection _) ->
- [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
- 'fNL >]
+ [< 'sTR " >>>>>>> Closed Section "; pr_id (basename sp); 'fNL >]
| (_,Lib.Module dir) ->
- [< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >]
+ [< 'sTR " >>>>>>> Module "; pr_dirpath dir; 'fNL >]
| (_,Lib.FrozenState _) ->
[< >]
@@ -377,10 +376,13 @@ let list_filter_vec f vec =
frec (Array.length vec -1) []
let read_sec_context qid =
- let sp, _ = Nametab.locate_module qid in
+ let dir =
+ try Nametab.locate_section qid
+ with Not_found -> error "Unknown section" in
let rec get_cxt in_cxt = function
- | ((sp',Lib.OpenedSection (str,_)) as hd)::rest ->
- if sp' = sp then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+ | ((sp,Lib.OpenedSection (_,_)) as hd)::rest ->
+ let dir' = make_dirpath (wd_of_sp sp) in
+ if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
in
@@ -405,7 +407,7 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} =
let print_name qid =
try
- let sp,_ = Nametab.locate_obj qid in
+ let sp = Nametab.locate_obj qid in
let (sp,lobj) =
let (sp,entry) =
List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 858c806672..52300882a2 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -48,14 +48,14 @@ let global_constr_name ((sp,tyi),i) =
^","^(string_of_int i)^")") >]
let globpr gt = match gt with
- | Nvar(_,s) -> [< 'sTR s >]
+ | Nvar(_,s) -> [< pr_id s >]
| Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
- | Node(_,"CONST",[Path(_,sl,s)]) ->
- global_const_name (section_path sl s)
- | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
- global_ind_name (section_path sl s, tyi)
- | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
- global_constr_name ((section_path sl s, tyi), i)
+ | Node(_,"CONST",[Path(_,sl)]) ->
+ global_const_name (section_path sl)
+ | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
+ global_ind_name (section_path sl, tyi)
+ | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
+ global_constr_name ((section_path sl, tyi), i)
| gt -> dfltpr gt
let wrap_exception = function
@@ -135,18 +135,18 @@ let rec gentacpr gt =
Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt
and default_tacpr = function
- | Nvar(_,s) -> [< 'sTR s >]
+ | Nvar(_,s) -> [< pr_id s >]
(* constr's may occur inside tac expressions ! *)
| Node(_,"EVAR", [Num (_,ev)]) -> [< 'sTR ("?" ^ (string_of_int ev)) >]
- | Node(_,"CONST",[Path(_,sl,s)]) ->
- let sp = section_path sl s in
- pr_global (ConstRef (section_path sl s))
- | Node(_,"MUTIND",[Path(_,sl,s); Num(_,tyi)]) ->
- let sp = section_path sl s in
+ | Node(_,"CONST",[Path(_,sl)]) ->
+ let sp = section_path sl in
+ pr_global (ConstRef sp)
+ | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
+ let sp = section_path sl in
pr_global (IndRef (sp,tyi))
- | Node(_,"MUTCONSTRUCT",[Path(_,sl,s); Num(_,tyi); Num(_,i)]) ->
- let sp = section_path sl s in
+ | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
+ let sp = section_path sl in
pr_global (ConstructRef ((sp,tyi),i))
(* This should be tactics *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e8ee0c67d0..90d2f1babe 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -36,51 +36,62 @@ let anti loc x =
(* which will bind their actual ast value *)
let rec expr_of_ast = function
- | Coqast.Nvar loc id when is_meta id -> anti loc id
- | Coqast.Id loc id when is_meta id -> anti loc id
- | Coqast.Node _ "$VAR" [Coqast.Nvar loc x] ->
- <:expr< Coqast.Nvar loc $anti loc x$ >>
- | Coqast.Node loc "$PATH" l ->
- let extract_var = function
- | Coqast.Nvar loc id -> id
- | Coqast.Id loc id -> failwith ("Id"^id)
- | Coqast.Node _ s _ -> failwith ("Node"^s)
- | _ -> failwith "Path is not built from ast variables" in
- let l = List.map extract_var l in
- let l = expr_list_of_var_list l in
- <:expr< Coqast.Path loc $l$ Names.CCI >>
- | Coqast.Node _ "$ID" [Coqast.Nvar loc x] ->
+ | Coqast.Nmeta loc id -> anti loc id
+ | Coqast.Id loc id when is_meta id -> <:expr< Coqast.Id loc $anti loc id$ >>
+ | Coqast.Node _ "$VAR" [Coqast.Nmeta loc x] ->
+ <:expr< let s = $anti loc x$ in
+ if String.length s > 0 && s.[0] = '$' then
+ failwith "Wrong ast: $VAR should not be bound to a meta variable"
+ else
+ Coqast.Nvar loc (Names.id_of_string s) >>
+ | Coqast.Node _ "$PATH" [Coqast.Nmeta loc x] ->
+ <:expr< Coqast.Path loc $anti loc x$ >>
+ | Coqast.Node _ "$ID" [Coqast.Nmeta loc x] ->
<:expr< Coqast.Id loc $anti loc x$ >>
- | Coqast.Node _ "$STR" [Coqast.Nvar loc x] ->
+ | Coqast.Node _ "$STR" [Coqast.Nmeta loc x] ->
<:expr< Coqast.Str loc $anti loc x$ >>
- | Coqast.Node _ "$SLAM" [Coqast.Nvar loc idl; y] ->
+(* Obsolète
+ | Coqast.Node _ "$SLAM" [Coqast.Nmeta loc idl; y] ->
<:expr<
List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $expr_of_ast y$ >>
- | Coqast.Node _ "$ABSTRACT" [Coqast.Str _ s;Coqast.Nvar loc idl; y] ->
+*)
+ | Coqast.Node loc "$ABSTRACT" [Coqast.Str _ s; x; y] ->
<:expr<
- Pcoq.abstract_binders_ast loc $str:s$ $anti loc idl$ $expr_of_ast y$ >>
+ Pcoq.abstract_binders_ast loc $str:s$ $expr_of_ast x$ $expr_of_ast y$ >>
| Coqast.Node loc nn al ->
let e = expr_list_of_ast_list al in
<:expr< Coqast.Node loc $str:nn$ $e$ >>
- | Coqast.Nvar loc id -> <:expr< Coqast.Nvar loc $str:id$ >>
+ | Coqast.Nvar loc id ->
+ <:expr< Coqast.Nvar loc (Names.id_of_string $str:Names.string_of_id id$) >>
| Coqast.Slam loc None a ->
<:expr< Coqast.Slam loc None $expr_of_ast a$ >>
+ | Coqast.Smetalam loc s a ->
+ <:expr<
+ match $anti loc s$ with
+ [ Coqast.Nvar _ id -> Coqast.Slam loc (Some id) $expr_of_ast a$
+ | Coqast.Nmeta _ s -> Coqast.Smetalam loc s $expr_of_ast a$
+ | _ -> failwith "Slam expects a var or a metavar" ] >>
| Coqast.Slam loc (Some s) a ->
- let se = if is_meta s then anti loc s else <:expr< $str:s$ >> in
+ let se = <:expr< Names.id_of_string $str:Names.string_of_id s$ >> in
<:expr< Coqast.Slam loc (Some $se$) $expr_of_ast a$ >>
| Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >>
| Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >>
| Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >>
- | Coqast.Path loc sl s ->
- let e = expr_list_of_var_list sl in
- <:expr< Coqast.Path loc $e$ $str:s$ >>
+ | Coqast.Path loc qid ->
+ let l,a,_ = Names.repr_path qid in
+ let expr_of_modid id =
+ <:expr< Names.id_of_string $str:Names.string_of_id id$ >> in
+ let e = List.map expr_of_modid (Names.repr_dirpath l) in
+ let e = expr_list_of_var_list e in
+ <:expr< Coqast.Path loc (Names.make_path (Names.make_dirpath
+ $e$) (Names.id_of_string $str:Names.string_of_id a$) Names.CCI) >>
| Coqast.Dynamic _ _ ->
failwith "Q_Coqast: dynamic: not implemented"
and expr_list_of_ast_list al =
List.fold_right
(fun a e2 -> match a with
- | (Coqast.Node _ "$LIST" [Coqast.Nvar locv pv]) ->
+ | (Coqast.Node _ "$LIST" [Coqast.Nmeta locv pv]) ->
let e1 = anti locv pv in
let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
if e2 = (let loc = dummy_loc in <:expr< [] >>)
@@ -95,8 +106,7 @@ and expr_list_of_ast_list al =
and expr_list_of_var_list sl =
let loc = dummy_loc in
List.fold_right
- (fun s e2 ->
- let e1 = if is_meta s then anti loc s else <:expr< $str:s$ >> in
+ (fun e1 e2 ->
let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
<:expr< [$e1$ :: $e2$] >>)
sl <:expr< [] >>
diff --git a/parsing/search.ml b/parsing/search.ml
index 2b9a5dd448..839acb4b4e 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -108,15 +108,17 @@ let filter_by_module (module_list:dir_path list) (accept:bool)
let sp = sp_of_global env ref in
let sl = dirpath sp in
let rec filter_aux = function
- | m :: tl -> (not (dirpath_prefix_of m sl)) && (filter_aux tl)
+ | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
| [] -> true
in
xor accept (filter_aux module_list)
with No_section_path ->
false
-let gref_eq = IndRef (make_path ["Coq";"Init";"Logic"] (id_of_string "eq") CCI, 0)
-let gref_eqT = IndRef (make_path ["Coq";"Init";"Logic_Type"] (id_of_string "eqT") CCI, 0)
+let gref_eq =
+ IndRef (make_path Coqlib.logic_module (id_of_string "eq") CCI, 0)
+let gref_eqT =
+ IndRef (make_path Coqlib.logic_type_module (id_of_string "eqT") CCI, 0)
let mk_rewrite_pattern1 eq pattern =
PApp (PRef eq, [| PMeta None; pattern; PMeta None |])
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 448aa148a6..431743f13a 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -77,14 +77,14 @@ let ids_of_ctxt ctxt =
"Termast: arbitrary substitution of references not yet implemented")
ctxt)
-let ast_of_ident id = nvar (string_of_id id)
+let ast_of_ident id = nvar id
let ast_of_name = function
- | Name id -> nvar (string_of_id id)
- | Anonymous -> nvar "_"
+ | Name id -> nvar id
+ | Anonymous -> nvar wildcard
-let stringopt_of_name = function
- | Name id -> Some (string_of_id id)
+let idopt_of_name = function
+ | Name id -> Some id
| Anonymous -> None
let ast_of_constant_ref sp =
@@ -107,19 +107,19 @@ let ast_of_ref = function
let ast_of_qualid p =
let dir, s = repr_qualid p in
- let args = List.map nvar (dir@[string_of_id s]) in
+ let args = List.map nvar (dir@[s]) in
ope ("QUALID", args)
(**********************************************************************)
(* conversion of patterns *)
let rec ast_of_cases_pattern = function (* loc is thrown away for printing *)
- | PatVar (loc,Name id) -> nvar (string_of_id id)
- | PatVar (loc,Anonymous) -> nvar "_"
+ | PatVar (loc,Name id) -> nvar id
+ | PatVar (loc,Anonymous) -> nvar wildcard
| PatCstr(loc,(cstrsp,_),args,Name id) ->
let args = List.map ast_of_cases_pattern args in
ope("PATTAS",
- [nvar (string_of_id id);
+ [nvar id;
ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)])
| PatCstr(loc,(cstrsp,_),args,Anonymous) ->
ope("PATTCONSTRUCT",
@@ -128,7 +128,7 @@ let rec ast_of_cases_pattern = function (* loc is thrown away for printing *)
let ast_dependent na aty =
match na with
- | Name id -> occur_var_ast (string_of_id id) aty
+ | Name id -> occur_var_ast id aty
| Anonymous -> false
let decompose_binder = function
@@ -196,7 +196,7 @@ let rec ast_of_raw = function
ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
| RLetIn (_,na,t,c) ->
- ope("LETIN",[ast_of_raw t; slam(stringopt_of_name na,ast_of_raw c)])
+ ope("LETIN",[ast_of_raw t; slam(idopt_of_name na,ast_of_raw c)])
| RProd (_,na,t,c) ->
let (n,a) = factorize_binder 1 BProd na (ast_of_raw t) c in
@@ -287,7 +287,7 @@ and factorize_binder n oper na aty c =
-> factorize_binder (n+1) oper na' aty c'
| _ -> (n,ast_of_raw c)
in
- (p,slam(stringopt_of_name na, body))
+ (p,slam(idopt_of_name na, body))
let ast_of_rawconstr = ast_of_raw
@@ -345,8 +345,7 @@ let rec ast_of_pattern env = function
| Anonymous ->
anomaly "ast_of_pattern: index to an anonymous variable"
with Not_found ->
- let s = "[REL "^(string_of_int n)^"]"
- in nvar s)
+ nvar (id_of_string ("[REL "^(string_of_int n)^"]")))
| PApp (f,args) ->
let (f,args) =
@@ -364,7 +363,7 @@ let rec ast_of_pattern env = function
| PLetIn (na,b,c) ->
let c' = ast_of_pattern (add_name na env) c in
- ope("LETIN",[ast_of_pattern env b;slam(stringopt_of_name na,c')])
+ ope("LETIN",[ast_of_pattern env b;slam(idopt_of_name na,c')])
| PProd (Anonymous,t,c) ->
ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
@@ -415,4 +414,4 @@ and factorize_binder_pattern env n oper na aty c =
factorize_binder_pattern (add_name na' env) (n+1) oper na' aty c'
| _ -> (n,ast_of_pattern env c)
in
- (p,slam(stringopt_of_name na, body))
+ (p,slam(idopt_of_name na, body))
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 16:33:51 +0000