Drastic performance improvement

Share string by hashconsing the string objects (reduces memory
consumption by half on the Gcd example of certicoq). We do it for whole
idents right now, the current Coq string representation does not allow
to share prefixes sadly.

Also remove the externalisation + elaboration phases when introducing
quoted terms, we can bypass it completely and give the term directly for
the kernel to check (without bypassing any checks though!).
There is still an inefficiency due to retypechecking strings which does
not seem so easy to avoid.
We went from 240s to 24s when quoting CertiCoq's Gcd example.

src/reify.ml4

@@ -13,8 +13,8 @@ let _ = Goptions.declare_bool_option {
 }
 
 (* whether Set Template Cast Propositions is on, as needed for erasure in Certicoq *)
-let is_cast_prop () = !cast_prop                     
-                     
+let is_cast_prop () = !cast_prop
+
 let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
 
 module TermReify =
@@ -99,7 +99,7 @@ struct
   let sSet = r_reify "sSet"
   let sType = r_reify "sType"
   let tident = r_reify "ident"
-  let tInd = r_reify "inductive"
+  let tIndTy = r_reify "inductive"
   let tmkInd = r_reify "mkInd"
   let (tTerm,tRel,tVar,tMeta,tEvar,tSort,tCast,tProd,
        tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tUnknown) =
@@ -164,19 +164,32 @@ struct
 
   let quote_bool b =
     if b then ttrue else tfalse
-
-  let quote_char c =
-    let i = int_of_char c in
+
+  let quote_char i =
     Term.mkApp (tAscii, Array.of_list (List.map (fun m -> quote_bool ((i land m) = m))
 					 (List.rev [128;64;32;16;8;4;2;1])))
 
+  let chars = Array.init 255 quote_char 
+
+  let quote_char c = chars.(int_of_char c)
+
+  let string_hash = Hashtbl.create 420
+
   let quote_string s =
+    let len = String.length s in
     let rec go from acc =
       if from < 0 then acc
       else
-	go (from - 1) (Term.mkApp (tString, [| quote_char (String.get s from) ; acc |]))
+        let term = Term.mkApp (tString, [| quote_char (String.get s from) ; acc |]) in
+        go (from - 1) term
     in
-    go (String.length s - 1) tEmptyString
+    go (len - 1) tEmptyString
+
+  let quote_string s =
+    try Hashtbl.find string_hash s
+    with Not_found ->
+      let term = quote_string s in
+      Hashtbl.add string_hash s term; term
 
   let quote_ident i =
     let s = Names.string_of_id i in
@@ -288,7 +301,7 @@ struct
       | Term.Case (ci,a,b,e) ->
         let ind = quote_inductive env ci.Term.ci_ind in
         let npar = int_to_nat ci.Term.ci_npar in
-        let info = pair tInd tnat ind npar in
+        let info = pair tIndTy tnat ind npar in
 	let (a',acc) = quote_term acc env a in
 	let (b',acc) = quote_term acc env b in
 	let (branches,acc) =
@@ -761,7 +774,7 @@ let check_inside_section () =
     Errors.errorlabstrm "Quote" (Pp.str "You can not quote within a section.")
   else ()
 
-
+open Pp
 
 TACTIC EXTEND get_goal
     | [ "quote_term" constr(c) tactic(tac) ] ->
@@ -797,10 +810,8 @@ VERNAC COMMAND EXTEND Make_vernac CLASSIFIED AS SIDEFF
 	let (evm,env) = Lemmas.get_current_context () in
 	let def = Constrintern.interp_constr env evm def in
 	let trm = TermReify.quote_term env (fst def) in
-	let result = Constrextern.extern_constr true env evm trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition ~kind:Decl_kinds.Definition name
+                                          (trm, Univ.ContextSet.empty)) ]
 END;;
 
 VERNAC COMMAND EXTEND Make_vernac_reduce CLASSIFIED AS SIDEFF
@@ -812,10 +823,8 @@ VERNAC COMMAND EXTEND Make_vernac_reduce CLASSIFIED AS SIDEFF
 	let red = fst (Redexpr.reduction_of_red_expr env red) in
 	let def = red env evm2 (fst def) in
 	let trm = TermReify.quote_term env (snd def) in
-	let result = Constrextern.extern_constr true env (fst def) trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition ~kind:Decl_kinds.Definition
+                                          name (trm, Univ.ContextSet.empty)) ]
 END;;
 
 
@@ -825,12 +834,12 @@ VERNAC COMMAND EXTEND Make_recursive CLASSIFIED AS SIDEFF
 	let (evm,env) = Lemmas.get_current_context () in
 	let def = Constrintern.interp_constr env evm def in
 	let trm = TermReify.quote_term_rec env (fst def) in
-	let result = Constrextern.extern_constr true env evm trm in
-	declare_definition name
-	  (Decl_kinds.Global, false, Decl_kinds.Definition)
-	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
+	ignore(Declare.declare_definition 
+	  ~kind:Decl_kinds.Definition name
+	  (trm, (* No new universe constraints can be generated by typing the AST *)
+           Univ.ContextSet.empty)) ]
 END;;
-
+        
 VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF
     | [ "Make" "Definition" ident(name) ":=" constr(def) ] ->
       [ check_inside_section () ;