Imported Upstream version 8.5~beta1+dfsg

1 files changed, 89 insertions, 67 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 3c2431a1..18588867 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,25 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
 open Declarations
-open Libnames
-open Glob_term
+open Globnames
+open Genredexpr
 open Pattern
 open Reductionops
 open Tacred
 open Closure
 open RedFlags
 open Libobject
-open Summary
+open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -28,13 +29,35 @@ let cbv_vm env sigma c =
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp
 
+let cbv_native env sigma c =
+  let ctyp = Retyping.get_type_of env sigma c in
+  let evars = Nativenorm.evars_of_evar_map sigma in
+  Nativenorm.native_norm env evars c ctyp
+
+let whd_cbn flags env sigma t =
+  let (state,_) =
+    (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty))
+  in Reductionops.Stack.zip ~refold:true state
+
+let strong_cbn flags =
+  strong (whd_cbn flags)
+
+let simplIsCbn = ref (false)
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Plug the simpl tactic to the new cbn mechanism";
+  Goptions.optkey = ["SimplIsCbn"];
+  Goptions.optread = (fun () -> !simplIsCbn);
+  Goptions.optwrite = (fun a -> simplIsCbn:=a);
+}
 
 let set_strategy_one ref l  =
   let k =
     match ref with
       | EvalConstRef sp -> ConstKey sp
       | EvalVarRef id -> VarKey id in
-  Conv_oracle.set_strategy k l;
+  Global.set_strategy k l;
   match k,l with
       ConstKey sp, Conv_oracle.Opaque ->
         Csymtable.set_opaque_const sp
@@ -44,7 +67,7 @@ let set_strategy_one ref l  =
 	  | OpaqueDef _ ->
             errorlabstrm "set_transparent_const"
               (str "Cannot make" ++ spc () ++
-		 Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+		 Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
 		 spc () ++ str "transparent because it was declared opaque.");
 	  | _ -> Csymtable.set_transparent_const sp)
     | _ -> ()
@@ -56,9 +79,9 @@ let cache_strategy (_,str) =
 
 let subst_strategy (subs,(local,obj)) =
   local,
-  list_smartmap
+  List.smartmap
     (fun (k,ql as entry) ->
-      let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
@@ -71,8 +94,8 @@ let map_strategy f l =
           match f q with
               Some q' -> q' :: ql
             | None -> ql) ql [] in
-      if ql'=[] then str else (lev,ql')::str) l [] in
-  if l'=[] then None else Some (false,l')
+      if List.is_empty ql' then str else (lev,ql')::str) l [] in
+  if List.is_empty l' then None else Some (false,l')
 
 let classify_strategy (local,_ as obj) =
   if local then Dispose else Substitute obj
@@ -103,12 +126,6 @@ let inStrategy : strategy_obj -> obj =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ = declare_summary "Transparent constants and variables"
-    { freeze_function = Conv_oracle.freeze;
-      unfreeze_function = Conv_oracle.unfreeze;
-      init_function = Conv_oracle.init }
-
-
 (* Generic reduction: reduction functions used in reduction tactics *)
 
 type red_expr =
@@ -118,7 +135,7 @@ let make_flag_constant = function
   | EvalVarRef id -> fVAR id
   | EvalConstRef sp -> fCONST sp
 
-let make_flag f =
+let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
   let red = if f.rIota then red_add red fIOTA else red in
@@ -126,7 +143,8 @@ let make_flag f =
   let red =
     if f.rDelta then (* All but rConst *)
         let red = red_add red fDELTA in
-        let red = red_add_transparent red (Conv_oracle.get_transp_state()) in
+        let red = red_add_transparent red 
+                    (Conv_oracle.get_transp_state (Environ.oracle env)) in
 	List.fold_right
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
@@ -141,81 +159,90 @@ let is_reference = function PRef _ | PVar _ -> true | _ -> false
 
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
-let reduction_tab = ref Stringmap.empty
+let reduction_tab = ref String.Map.empty
 
 (* table of custom reduction expressions, synchronized,
    filled by command Declare Reduction *)
-let red_expr_tab = ref Stringmap.empty
+let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
-  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
   then error ("There is already a reduction expression of name "^s)
-  else reduction_tab := Stringmap.add s f !reduction_tab
+  else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
-      if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab)
+      if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
       then error ("Reference to undefined reduction expression "^s)
   |_ -> ()
 
 let decl_red_expr s e =
-  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
   then error ("There is already a reduction expression of name "^s)
   else begin
     check_custom e;
-    red_expr_tab := Stringmap.add s e !red_expr_tab
+    red_expr_tab := String.Map.add s e !red_expr_tab
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
-let out_with_occurrences ((b,l),c) =
-  ((b,List.map out_arg l), c)
+let out_with_occurrences (occs,c) =
+  (Locusops.occurrences_map (List.map out_arg) occs, c)
+
+let e_red f env evm c = evm, f env evm c
+
+let head_style = false (* Turn to true to have a semantics where simpl
+   only reduce at the head when an evaluable reference is given, e.g.
+   2+n would just reduce to S(1+n) instead of S(S(n)) *)
+
+let contextualize f g = function
+  | Some (occs,c) ->
+      let l = Locusops.occurrences_map (List.map out_arg) occs in
+      let b,c,h = match c with
+        | Inl r -> true,PRef (global_of_evaluable_reference r),f
+        | Inr c -> false,c,f in
+      e_red (contextually b (l,c) (fun _ -> h))
+  | None -> e_red g
 
-let rec reduction_of_red_expr = function
+let reduction_of_red_expr env =
+  let make_flag = make_flag env in
+  let rec reduction_of_red_expr = function
   | Red internal ->
-      if internal then (try_red_product,DEFAULTcast)
-      else (red_product,DEFAULTcast)
-  | Hnf -> (hnf_constr,DEFAULTcast)
-  | Simpl (Some (_,c as lp)) ->
-    (contextually (is_reference c) (out_with_occurrences lp)
-      (fun _ -> simpl),DEFAULTcast)
-  | Simpl None -> (simpl,DEFAULTcast)
-  | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
-  | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
-  | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
-  | Fold cl -> (fold_commands cl,DEFAULTcast)
+      if internal then (e_red try_red_product,DEFAULTcast)
+      else (e_red red_product,DEFAULTcast)
+  | Hnf -> (e_red hnf_constr,DEFAULTcast)
+  | Simpl (f,o) ->
+     let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in
+     let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
+     let () =
+       if not (!simplIsCbn || List.is_empty f.rConst) then
+	 Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+     (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
+  | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
+  | Cbn f ->
+     (e_red (strong_cbn (make_flag f)), DEFAULTcast)
+  | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+  | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
+  | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
-      (try (Stringmap.find s !reduction_tab,DEFAULTcast)
+      (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
-	(try reduction_of_red_expr (Stringmap.find s !red_expr_tab)
+	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
 	   error("unknown user-defined reduction \""^s^"\"")))
-  | CbvVm -> (cbv_vm ,VMcast)
+  | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
+  | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
+  in
+    reduction_of_red_expr
 
-
-let subst_flags subs flags =
-  { flags with rConst = List.map subs flags.rConst }
-
-let subst_occs subs (occ,e) = (occ,subs e)
-
-let subst_gen_red_expr subs_a subs_b subs_c = function
-  | Fold l -> Fold (List.map subs_a l)
-  | Pattern occs_l -> Pattern (List.map (subst_occs subs_a) occs_l)
-  | Simpl occs_o -> Simpl (Option.map (subst_occs subs_c) occs_o)
-  | Unfold occs_l -> Unfold (List.map (subst_occs subs_b) occs_l)
-  | Cbv flags -> Cbv (subst_flags subs_b flags)
-  | Lazy flags -> Lazy (subst_flags subs_b flags)
-  | e -> e
-
-let subst_red_expr subs e =
-  subst_gen_red_expr
+let subst_red_expr subs =
+  Miscops.map_red_expr_gen
     (Mod_subst.subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Pattern.subst_pattern subs)
-    e
+    (Patternops.subst_pattern subs)
 
 let inReduction : bool * string * red_expr -> obj =
   declare_object
@@ -229,8 +256,3 @@ let inReduction : bool * string * red_expr -> obj =
 
 let declare_red_expr locality s expr =
     Lib.add_anonymous_leaf (inReduction (locality,s,expr))
-
-let _ = declare_summary "Declare Reduction"
-  { freeze_function = (fun () -> !red_expr_tab);
-    unfreeze_function = ((:=) red_expr_tab);
-    init_function = (fun () -> red_expr_tab := Stringmap.empty) }