aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
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-07-20 00:07:14 +0000