bugs #667 and #783 (mimick_evar and loc_table on large files)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5894 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 13 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index a3652c8d7a..88891b2d92 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -470,26 +470,30 @@ let rec next_token = parser bp
 
 let locerr () = invalid_arg "Lexer: location function"
 
-let loct_create () = ref (Array.create 1024 None)
+let tsz = 256   (* up to 2^29 entries on a 32-bit machine, 2^61 on 64-bit *)
+
+let loct_create () = ref [| [| |] |]
 
 let loct_func loct i =
   match
-    if i < 0 || i >= Array.length !loct then None
-    else Array.unsafe_get !loct i
+    if i < 0 || i/tsz >= Array.length !loct then None
+    else if !loct.(i/tsz) = [| |] then None
+    else !loct.(i/tsz).(i mod tsz)
   with
     | Some loc -> loc
     | _ -> locerr ()
 
 let loct_add loct i loc =
-  if i >= Array.length !loct then begin
+  while i/tsz >= Array.length !loct do
     let new_tmax = Array.length !loct * 2 in
-    let new_loct = Array.create new_tmax None in
+    let new_loct = Array.make new_tmax [| |] in
     Array.blit !loct 0 new_loct 0 (Array.length !loct);
-    loct := new_loct
-  end;
-  !loct.(i) <- Some loc
+    loct := new_loct;
+  done;
+  if !loct.(i/tsz) = [| |] then !loct.(i/tsz) <- Array.make tsz None;
+  !loct.(i/tsz).(i mod tsz) <- Some loc
 
-let current_location_table = ref (ref [||])
+let current_location_table = ref (ref [| [| |] |])
 
 let location_function n =
   loct_func !current_location_table n
@@ -505,7 +509,7 @@ let func cs =
   current_location_table := loct;
   (ts, loct_func loct)
 
-type location_table = (int * int) option array ref
+type location_table = (int * int) option array array ref
 let location_table () = !current_location_table
 let restore_location_table t = current_location_table := t
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d3c835be43..cc7ab87107 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -534,6 +534,11 @@ let applyHead n c wc =
   in 
   apprec n c (w_type_of wc c) wc
 
+let is_mimick_head f =
+  match kind_of_term f with
+      (Const _|Var _|Rel _|Construct _|Ind _) -> true
+    | _ -> false
+
 let rec mimick_evar hdc nargs sp wc =
   let evd = Evd.map wc.sigma sp in
   let wc' = extract_decl sp wc in
@@ -571,7 +576,7 @@ and w_resrec metas evars wc =
 		 w_resrec metas t (w_Define evn rhs wc)
                with ex when catchable_exception ex ->
 		 (match krhs with
-             	    | App (f,cl) when isConst f ->
+             	    | App (f,cl) when is_mimick_head f ->
 			let wc' = mimick_evar f (Array.length cl) evn wc in
 			w_resrec metas evars wc'
 		    | _ -> raise ex (* error "w_Unify" *)))
@@ -624,12 +629,12 @@ let clenv_merge with_types metas evars clenv =
 		    (clenv_wtactic (w_Define evn rhs') clenv) 
 		with ex when catchable_exception ex ->
 		  (match krhs with
-		     | App (f,cl) when isConst f or isConstruct f ->
+		     | App (f,cl) when is_mimick_head f ->
 			 clenv_resrec metas evars 
 			   (clenv_wtactic
 			      (mimick_evar f (Array.length cl) evn)
 			      clenv)
-           	     | _ -> raise ex(********* error  "w_Unify" *))
+           	     | _ -> raise ex (* error  "w_Unify" *))
 	      end
 
 	  | _ -> anomaly "clenv_resrec"))