aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml18
-rw-r--r--interp/constrintern.mli5
-rw-r--r--toplevel/vernac.ml11
-rw-r--r--translate/ppconstrnew.ml31
-rw-r--r--translate/ppvernacnew.ml8
5 files changed, 54 insertions, 19 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8a16a56db..8ac87a4d4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -123,6 +123,22 @@ let error_bad_inductive_type loc =
(**********************************************************************)
(* Dump of globalization (to be used by coqdoc) *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+ let lt = Lexer.location_table() in
+ let state = (lt,!token_number,!last_pos) in
+ token_number := 0;
+ last_pos := 0;
+ state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+ Lexer.restore_location_table lt;
+ token_number := tn;
+ last_pos := lp
let add_glob loc ref =
(*i
@@ -148,8 +164,6 @@ let ntn_loc = loc_of_notation constr_loc
let patntn_loc = loc_of_notation cases_pattern_loc
let dump_notation_location =
- let token_number = ref 0 in
- let last_pos = ref 0 in
fun pos ntn ((path,df),sc) ->
let rec next growing =
let (bp,_ as loc) = Lexer.location_function !token_number in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 91a345476..aac3f44c3 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -116,6 +116,11 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
+(* Coqdoc utility functions *)
+type coqdoc_state
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
+
(* For v8 translation *)
val set_temporary_implicits_in :
(identifier * Impargs.implicits_list) list -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7768fa95b..2607ca411 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -163,10 +163,13 @@ let pr_new_syntax loc ocom =
let rec vernac_com interpfun (loc,com) =
let rec interp = function
| VernacLoad (verbosely, fname) ->
+ (* translator state *)
let ch = !chan_translate in
let cs = Lexer.com_state() in
- let lt = Lexer.location_table() in
let cl = !Pp.comments in
+ (* end translator state *)
+ (* coqdoc state *)
+ let cds = Constrintern.coqdoc_freeze() in
if !Options.translate_file then begin
let _,f = find_file_in_path (Library.get_load_path ())
(make_suffix fname ".v") in
@@ -178,14 +181,14 @@ let rec vernac_com interpfun (loc,com) =
if !Options.translate_file then close_out !chan_translate;
chan_translate := ch;
Lexer.restore_com_state cs;
- Lexer.restore_location_table lt;
- Pp.comments := cl
+ Pp.comments := cl;
+ Constrintern.coqdoc_unfreeze cds;
with e ->
if !Options.translate_file then close_out !chan_translate;
chan_translate := ch;
Lexer.restore_com_state cs;
- Lexer.restore_location_table lt;
Pp.comments := cl;
+ Constrintern.coqdoc_unfreeze cds;
raise e end;
| VernacList l -> List.iter (fun (_,v) -> interp v) l
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 8fdc68f93..629201328 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -278,10 +278,13 @@ let split_product na' = function
rename na na' t (CProdN(loc,(nal,t)::bl,c))
| _ -> anomaly "ill-formed fixpoint body"
-let merge_binders (na1,ty1) (na2,ty2) codom =
+let merge_binders (na1,ty1) cofun (na2,ty2) codom =
let na =
match snd na1, snd na2 with
- Anonymous, Name id -> na2
+ Anonymous, Name id ->
+ if occur_var_constr_expr id cofun then
+ failwith "avoid capture"
+ else na2
| Name id, Anonymous ->
if occur_var_constr_expr id codom then
failwith "avoid capture"
@@ -298,29 +301,30 @@ let merge_binders (na1,ty1) (na2,ty2) codom =
ty2 in
(LocalRawAssum ([na],ty), codom)
-let rec strip_domain bvar c =
+let rec strip_domain bvar cofun c =
match c with
| CArrow(loc,a,b) ->
- merge_binders bvar ((dummy_loc,Anonymous),a) b
+ merge_binders bvar cofun ((dummy_loc,Anonymous),a) b
| CProdN(loc,[([na],ty)],c') ->
- merge_binders bvar (na,ty) c'
+ merge_binders bvar cofun (na,ty) c'
| CProdN(loc,([na],ty)::bl,c') ->
- merge_binders bvar (na,ty) (CProdN(loc,bl,c'))
+ merge_binders bvar cofun (na,ty) (CProdN(loc,bl,c'))
| CProdN(loc,(na::nal,ty)::bl,c') ->
- merge_binders bvar (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
+ merge_binders bvar cofun (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
| _ -> failwith "not a product"
(* Note: binder sharing is lost *)
-let rec strip_domains (nal,ty) c =
+let rec strip_domains (nal,ty) cofun c =
match nal with
[] -> assert false
| [na] ->
- let bnd, c' = strip_domain (na,ty) c in
+ let bnd, c' = strip_domain (na,ty) cofun c in
([bnd],None,c')
| na::nal ->
- let bnd, c1 = strip_domain (na,ty) c in
+ let f = CLambdaN(dummy_loc,[(nal,ty)],cofun) in
+ let bnd, c1 = strip_domain (na,ty) f c in
(try
- let bl, rest, c2 = strip_domains (nal,ty) c1 in
+ let bl, rest, c2 = strip_domains (nal,ty) cofun c1 in
(bnd::bl, rest, c2)
with Failure _ -> ([bnd],Some (nal,ty), c1))
@@ -340,11 +344,12 @@ let rec extract_def_binders c ty =
match c with
| CLambdaN(loc,bvar::lams,b) ->
(try
- let bvar', rest, ty' = strip_domains bvar ty in
+ let f = CLambdaN(loc,lams,b) in
+ let bvar', rest, ty' = strip_domains bvar f ty in
let c' =
match rest, lams with
None,[] -> b
- | None, _ -> CLambdaN(loc,lams,b)
+ | None, _ -> f
| Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
let (bl,c2,ty2) = extract_def_binders c' ty' in
(factorize_binders (bvar'@bl), c2, ty2)
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index be37b110f..4df737fa8 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -770,6 +770,10 @@ let rec pr_vernac = function
| LocalRawDef (_,_) -> [] in
let pr_onerec = function
| (id,n,bl,type_,def),ntn ->
+ let (bl',def,type_) =
+ if Options.do_translate() then extract_def_binders def type_
+ else ([],def,type_) in
+ let bl = bl @ bl' in
let ids = List.flatten (List.map name_of_binder bl) in
let name =
try snd (List.nth ids n)
@@ -792,6 +796,10 @@ let rec pr_vernac = function
| VernacCoFixpoint corecs ->
let pr_onecorec (id,bl,c,def) =
+ let (bl',def,c) =
+ if Options.do_translate() then extract_def_binders def c
+ else ([],def,c) in
+ let bl = bl @ bl' in
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_type c ++
str" :=" ++ brk(1,1) ++ pr_lconstr def in
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-23 12:17:04 +0000