Abstraction de constr

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

5 files changed, 45 insertions, 65 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index e23d3b7f95..d9193a8ff4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -124,13 +124,6 @@ let corecursive_message = function
   | l   -> hOV 0 [< prlist_with_sep pr_coma print_id l;
                     'sPC; 'sTR "are corecursively defined">]
 
-let put_DLAMSV_subst lid lc = 
-  match lid with
-    | [] -> anomaly "put_DLAM"
-    | id::lrest ->  
-        List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c)) 
-          (DLAMV(Name id,Array.map (subst_var id) lc)) lrest
-
 let build_mutual lparams lnamearconstrs finite =
   let allnames = 
     List.fold_left 
@@ -244,14 +237,18 @@ let build_recursive lnameargsardef =
     collect_non_rec lrecnames recdef (List.rev arityl) (Array.to_list nv) in
   let n = NeverDischarge in 
   if lnamerec <> [] then begin
-    let recvec = [|put_DLAMSV_subst (List.rev lnamerec)
-                       (Array.of_list ldefrec)|] in
+    let recvec = 
+      Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
     let varrec = Array.of_list (List.map incast_type larrec) in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
 	    { const_entry_body =
-		Cooked (mkFixDlam (Array.of_list nvrec) i varrec recvec);
+		Cooked 
+		  (mkFix ((Array.of_list nvrec,i),
+			  (varrec,List.map (fun id -> Name id) lnamerec,
+			   recvec)));
+		  (* (mkFixDlam (Array.of_list nvrec) i varrec recvec); *)
 	      const_entry_type = None } 
 	  in
 	  declare_constant fi (ce, n);
@@ -313,13 +310,15 @@ let build_corecursive lnameardef =
       if lnamerec = [] then 
 	[||] 
       else 
-	[|put_DLAMSV_subst (List.rev lnamerec) (Array.of_list ldefrec)|] 
-    in
+	Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
     let varrec = Array.of_list (List.map incast_type larrec) in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
-	    { const_entry_body = Cooked (mkCoFixDlam i varrec recvec);
+	    { const_entry_body =
+		Cooked 
+		  (mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
+			      recvec)));
 	      const_entry_type = None } 
 	  in
           declare_constant fi (ce,n);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 3240e9db51..d136821a63 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -32,7 +32,12 @@ type modification_action = ABSTRACT | ERASE
 
 let interp_modif absfun oper (oper',modif) cl = 
   let rec interprec = function
-    | ([], cl) -> DOPN(oper',Array.of_list cl)
+    | ([], cl) -> 
+	(match oper' with
+	   | Const sp -> mkConst (sp,Array.of_list cl)
+	   | MutConstruct sp -> mkMutConstruct (sp,Array.of_list cl)
+	   | MutInd sp -> mkMutInd (sp,Array.of_list cl)
+	   | _ -> anomaly "not a reference operator")
     | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
     | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
     | _ -> assert false
@@ -64,10 +69,10 @@ let modify_opers replfun absfun oper_alist =
 	  (try
 	     match List.assoc (MutInd spi) oper_alist with
 	       | DO_ABSTRACT (MutInd spi',_) ->
-		   DOPN(MutCase(n,(spi',a,b,c,d)),cl')
+		   gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
 	       | _ -> raise Not_found
 	   with
-	     | Not_found -> DOPN(MutCase oper,cl'))
+	     | Not_found -> gather_constr (op,cl'))
 
       | OpMutInd spi ->
 	  (try
@@ -79,9 +84,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (MutInd spi) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(MutInd spi,cl'))))
+		| DO_REPLACE -> assert false)
 	   with 
-	     | Not_found -> DOPN(MutInd spi,cl'))
+	     | Not_found -> mkMutInd (spi,cl'))
 
       | OpMutConstruct spi ->
 	  (try
@@ -93,9 +98,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (MutConstruct spi) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(MutConstruct spi,cl'))))
+		| DO_REPLACE -> assert false)
 	   with 
-	     | Not_found -> DOPN(MutConstruct spi,cl'))
+	     | Not_found -> mkMutConstruct (spi,cl'))
 
       | OpConst sp ->
 	  (try
@@ -107,9 +112,9 @@ let modify_opers replfun absfun oper_alist =
 		    else 
 		      interp_modif absfun (Const sp) (oper',modif)
 			(Array.to_list cl')
-		| DO_REPLACE -> substrec (replfun (DOPN(Const sp,cl'))))
+		| DO_REPLACE -> substrec (replfun (sp,cl')))
 	   with 
-	     | Not_found -> DOPN(Const sp,cl'))
+	     | Not_found -> mkConst (sp,cl'))
   
     | _ -> gather_constr (op, cl')
   in 
@@ -117,18 +122,11 @@ let modify_opers replfun absfun oper_alist =
 
 (**)
 
-let under_dlams f = 
-  let rec apprec = function 
-    | DLAMV(na,c) -> DLAMV(na,Array.map f c)
-    | DLAM(na,c)  -> DLAM(na,apprec c)
-    | _           -> failwith "under_dlams"
-  in 
-  apprec 
-
 let abstract_inductive ids_to_abs hyps inds =
   let abstract_one_var d inds =
     let ntyp = List.length inds in 
-    let new_refs = list_tabulate (fun k -> applist(Rel (k+2),[Rel 1])) ntyp in 
+    let new_refs =
+      list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
     let inds' =
       List.map
       	(function (tname,arity,cnames,lc) -> 
@@ -191,8 +189,8 @@ let expmod_constr oldenv modlist c =
   let expfun cst = 
     try 
       constant_value oldenv cst
-    with Failure _ ->
-      let (sp,_) = destConst cst in
+    with NotEvaluableConst Opaque ->
+      let (sp,_) = cst in
       errorlabstrm "expmod_constr"
 	[< 'sTR"Cannot unfold the value of " ;
            'sTR(string_of_path sp) ; 'sPC;
@@ -200,13 +198,13 @@ let expmod_constr oldenv modlist c =
            'sTR"and then require that theorems which use them"; 'sPC;
            'sTR"be transparent" >];
   in
-  let under_casts f = function
-    | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t))
-    | c -> f c 
+  let under_casts f c = match kind_of_term c with
+    | IsCast (c,t) -> mkCast (f c,f t)
+    | _ -> f c 
   in
   let c' = modify_opers expfun (fun a b -> mkAppL (a, [|b|])) modlist c in
-  match c' with
-    | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
+  match kind_of_term c' with
+    | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
 let expmod_type oldenv modlist c = 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index cefa4d823d..773525ea43 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -268,7 +268,7 @@ let explain_occur_check k ctx ev rhs =
      'sTR" with term"; 'bRK(1,1); pt >]
 
 let explain_not_clean k ctx ev t =
-  let c = Rel (Intset.choose (free_rels t)) in
+  let c = mkRel (Intset.choose (free_rels t)) in
   let id = "?" ^ string_of_int ev in
   let var = prterm_env ctx c in
   [< 'sTR"Tried to define "; 'sTR id;
@@ -396,6 +396,9 @@ let explain_refiner_bad_tactic_args s l =
   [< 'sTR "Internal tactic "; 'sTR s; 'sTR " cannot be applied to ";
      Tacmach.pr_tactic (s,l) >]
 
+let explain_intro_needs_product () =
+  [< 'sTR "Introduction tactics needs products" >]
+
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
   | OccurMeta t -> explain_refiner_occur_meta t
@@ -404,6 +407,7 @@ let explain_refiner_error = function
   | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
+  | IntroNeedsProduct -> explain_intro_needs_product ()
 
 let error_non_strictly_positive k env c v  =
   let pc = prterm_env env c in
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 7e2b1f5bd6..4305b61ce7 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -17,14 +17,13 @@ let (env : safe_environment ref) = ref empty_environment
 
 let lookup_var id =
   let rec look n = function
-    | [] -> VAR id
+    | [] -> mkVar id
     | (Name id')::_ when id = id' -> Rel n
     | _::r -> look (succ n) r
   in
   look 1
 
-let args sign = 
-  Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
+let args sign = Array.of_list (List.map mkVar (ids_of_var_context sign))
 
 let rec globalize bv c = match kind_of_term c with
   | IsVar id -> lookup_var id bv
@@ -36,26 +35,6 @@ let rec globalize bv c = match kind_of_term c with
       let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
   | _ -> map_constr_with_binders (fun na l -> na::l) globalize bv c
 
-(*
-let rec globalize bv = function
-  | VAR id -> lookup_var id bv
-  | DOP1 (op,c) -> DOP1 (op, globalize bv c)
-  | DOP2 (op,c1,c2) -> DOP2 (op, globalize bv c1, globalize bv c2)
-  | DOPN (Const sp as op, _) ->
-      let cb = lookup_constant sp !env in DOPN (op, args cb.const_hyps)
-  | DOPN (MutInd (sp,_) as op, _) ->
-      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
-  | DOPN (MutConstruct ((sp,_),_) as op, _) ->
-      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
-  | DOPN (op,v) -> DOPN (op, Array.map (globalize bv) v)
-  | DLAM (na,c) -> DLAM (na, globalize (na::bv) c)
-  | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v)
-  | CLam(n,t,c)   -> CLam (n, globalize bv t, globalize (n::bv) c)  
-  | CPrd(n,t,c)   -> CPrd (n, globalize bv t, globalize (n::bv) c)
-  | CLet(n,b,t,c) -> CLet (n,globalize bv b,globalize bv t,globalize (n::bv) c)
-  | Rel _ | DOP0 _ as c -> c
-*)
-
 let check c = 
   let c = globalize [] c in
   let (j,u) = safe_infer !env c in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index fbf2586525..faf1f34336 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -128,13 +128,13 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
            (None::sp_projs,fi::ids_not_ok,subst)
          end else 
 	   let p = mkLambda (x, rp2, replace_vars subst ti) in
-	   let branch = mk_LambdaCit newfs (VAR fi) in
+	   let branch = mk_LambdaCit newfs (mkVar fi) in
 	   let ci = Inductive.make_case_info
 		      (Global.lookup_mind_specif (destMutInd r))
 		      (Some PrintLet) [| RegularPat |] in
 	   let proj = mk_LambdaCit newps 
 			(mkLambda (x, rp1,
-				   mkMutCase (ci, p, Rel 1, [|branch|]))) in
+				   mkMutCase (ci, p, mkRel 1, [|branch|]))) in
 	   let ok = 
 	     try
 	       let cie =
@@ -152,7 +152,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
              let constr_fi = global_reference CCI fi in
              let constr_fip = (* Rel 1 refers to "x" *)
-               applist (constr_fi,(List.map (fun id -> VAR id) idps)@[Rel 1])
+               applist (constr_fi,(List.map mkVar idps)@[mkRel 1])
              in (Some(path_of_const constr_fi)::sp_projs,
 		 ids_not_ok, (fi,constr_fip)::subst)
 	   end)