amelioration de la consommation memoire de la conversion en eta-expansant

les definitions.


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

1 files changed, 40 insertions, 50 deletions

diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 4eec7bb5fc..6611eba55b 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -42,11 +42,6 @@ let inductive = Grammar.Entry.create gram "inductive"
 let constructor = Grammar.Entry.create gram "constructor"
 let command = Grammar.Entry.create gram "command"
 
-let new_univ =
-  let uc = ref 0 in
-  let univ = id_of_string "univ" in
-  fun () -> incr uc; { u_sp = make_path [] univ CCI; u_num = !uc }
-
 let path_of_string s = make_path [] (id_of_string s) CCI
 
 EXTEND
@@ -59,39 +54,39 @@ EXTEND
   ] ];
   term: 
   [ [ id = IDENT -> 
-	VAR (id_of_string id) 
+	mkVar (id_of_string id) 
     | IDENT "Rel"; n = INT ->
-	Rel (int_of_string n)
+	mkRel (int_of_string n)
     | "Set" ->
-	DOP0 (Sort (Prop Pos))
+	mkSet
     | "Prop" ->
-	DOP0 (Sort (Prop Null))
+	mkProp
     | "Type" ->
-	DOP0 (Sort (Type (new_univ())))
+	mkType (new_univ())
     | "Const"; id = IDENT ->
-	DOPN (Const (path_of_string id), [||])
+	mkConst (path_of_string id, [||])
     | "Ind"; id = IDENT; n = INT ->
 	let n = int_of_string n in
-	DOPN (MutInd (path_of_string id, n), [||])
+	mkMutInd ((path_of_string id, n), [||])
     | "Construct"; id = IDENT; n = INT; i = INT ->
 	let n = int_of_string n and i = int_of_string i in
-	DOPN (MutConstruct ((path_of_string id, n), i), [||])
+	mkMutConstruct (((path_of_string id, n), i), [||])
     | "["; na = name; ":"; t = term; "]"; c = term ->
-	DOP2 (Lambda, t, DLAM (na, c))
+	mkLambda (na,t,c)
     | "("; na = name; ":"; t = term; ")"; c = term ->
-	DOP2 (Prod, t, DLAM (na, c))
+	mkProd (na,t,c)
     | c1 = term; "->"; c2 = term ->
-	DOP2 (Prod, c1, DLAM (Anonymous, c2))
+	mkArrow c1 c2
     | "("; id = IDENT; cl = LIST1 term; ")" ->
-	let c = VAR (id_of_string id) in
-	DOPN (AppL, Array.of_list (c::cl))
+	let c = mkVar (id_of_string id) in
+	mkApp (c, Array.of_list cl)
     | "("; cl = LIST1 term; ")" ->
 	begin match cl with
 	  | [c] -> c
-	  | _ -> DOPN (AppL, Array.of_list cl)
+	  | c::cl -> mkApp (c, Array.of_list cl)
 	end
     | "("; c = term; "::"; t = term; ")" ->
-	DOP2 (Cast, c, t)
+	mkCast (c, t)
     | "<"; p = term; ">"; 
 	IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT;
 	"of"; bl = LIST0 term; "end" ->
@@ -99,7 +94,7 @@ EXTEND
 	  let nc = List.length bl in
 	  let dummy_pats = Array.create nc RegularPat in
 	  let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in
-	  DOPN (MutCase dummy_ci, Array.of_list (p :: c :: bl))
+	  mkMutCase (dummy_ci, p, c, Array.of_list bl)
   ] ];
   command: 
   [ [ "Definition"; id = IDENT; ":="; c = term; "." ->
@@ -131,17 +126,12 @@ let print_univers = ref false
 let print_casts = ref false
 
 let print_type u =
-  let sp = u.u_sp and num = u.u_num in
-  [< 'sTR "Type";
-     if !print_univers then 
-       [< 'sTR "("; print_id (basename sp); 'sPC; 'iNT num >] 
-     else 
-       [< >] 
-  >]
-  
+  if !print_univers then [< 'sTR "Type"; pr_uni u >]
+  else [< 'sTR "Type" >]
+
 let print_name = function
   | Anonymous -> [< 'sTR "_" >]
-  | Name id -> print_id id
+  | Name id -> pr_id id
 
 let print_rel bv n = print_name (List.nth bv (pred n))
 
@@ -154,34 +144,34 @@ let rename bv = function
       in
       if List.mem na bv then Name (next_ident_away id idl) else na
 
-let rec pp bv = function
-  | DOP0 (Sort (Prop Pos)) -> [< 'sTR "Set" >]
-  | DOP0 (Sort (Prop Null)) -> [< 'sTR "Prop" >]
-  | DOP0 (Sort (Type u)) -> print_type u
-  | DOP2 (Lambda, t, DLAM(na, c)) ->
+let rec pp bv t =
+  match kind_of_term t with
+  | IsSort (Prop Pos) -> [< 'sTR "Set" >]
+  | IsSort (Prop Null) -> [< 'sTR "Prop" >]
+  | IsSort (Type u) -> print_type u
+  | IsLambda (na, t, c) ->
       [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >]
-  | DOP2 (Prod, t, DLAM(Anonymous, c)) ->
+  | IsProd (Anonymous, t, c) ->
       [< pp bv t; 'sTR"->"; pp (Anonymous::bv) c >]
-  | DOP2 (Prod, t, DLAM(na, c)) ->
+  | IsProd (na, t, c) ->
       [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >]
-  | DOP2 (Cast, c, t) ->
+  | IsCast (c, t) ->
       if !print_casts then 
 	[< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >]
       else 
 	pp bv c
-  | DOPN (AppL, [|c|]) ->
-      pp bv c
-  | DOPN (AppL, v) ->
-      [< 'sTR"("; prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >]
-  | DOPN (Const sp, _) ->
-      [< 'sTR"Const "; print_id (basename sp) >]
-  | DOPN (MutInd (sp,i), _) ->
-      [< 'sTR"Ind "; print_id (basename sp); 'sTR" "; 'iNT i >]
-  | DOPN (MutConstruct ((sp,i),j), _) ->
-      [< 'sTR"Construct "; print_id (basename sp); 'sTR" "; 'iNT i; 
+  | IsApp(h, v) ->
+      [< 'sTR"("; pp bv h; 'sPC;
+         prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >]
+  | IsConst (sp, _) ->
+      [< 'sTR"Const "; pr_id (basename sp) >]
+  | IsMutInd ((sp,i), _) ->
+      [< 'sTR"Ind "; pr_id (basename sp); 'sTR" "; 'iNT i >]
+  | IsMutConstruct (((sp,i),j), _) ->
+      [< 'sTR"Construct "; pr_id (basename sp); 'sTR" "; 'iNT i; 
 	 'sTR" "; 'iNT j >]
-  | VAR id -> print_id id
-  | Rel n -> print_rel bv n
+  | IsVar id -> pr_id id
+  | IsRel n -> print_rel bv n
   | _ -> [< 'sTR"<???>" >]
 
 let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])