Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 144 insertions, 46 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 21ee9a9f..a04216cb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -37,6 +37,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
+  | MetaInType of constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
@@ -57,29 +58,18 @@ let rec catchable_exception = function
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
+  | Typeclasses_errors.TypeClassError 
+      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
 
+let error_no_such_hypothesis id =
+  error ("No such hypothesis: " ^ string_of_id id ^ ".")
+
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
 let check = ref false
 let with_check = Flags.with_option check
 
-(************************************************************************)
-(************************************************************************)
-(* Implementation of the structural rules (moving and deleting
-   hypotheses around) *)
-
-(* The Clear tactic: it scans the context for hypotheses to be removed
-   (instead of iterating on the list of identifier to be removed, which
-   forces the user to give them in order). *)
-
-let clear_hyps sigma ids sign cl =
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
-  (hyps,concl,evars_of !evdref)
-
-(* The ClearBody tactic *)
-
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
 let apply_to_hyp sign id f =
@@ -97,6 +87,22 @@ let apply_to_hyp_and_dependent_on sign id f g =
 let check_typability env sigma c =
   if !check then let _ = type_of env sigma c in () 
 
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the structural rules (moving and deleting
+   hypotheses around) *)
+
+(* The Clear tactic: it scans the context for hypotheses to be removed
+   (instead of iterating on the list of identifier to be removed, which
+   forces the user to give them in order). *)
+
+let clear_hyps sigma ids sign cl =
+  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+  (hyps,concl,evars_of !evdref)
+
+(* The ClearBody tactic *)
+
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
   with _ ->
@@ -126,6 +132,82 @@ let remove_hyp_body env sigma id =
   in
   reset_with_named_context sign env 
 
+(* Reordering of the context *)
+
+(* faire le minimum d'echanges pour que l'ordre donne soit un *)
+(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
+(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
+(* reculees par rapport aux autres (faire le contraire!) *)
+ 
+let mt_q = (Idmap.empty,[])
+let push_val y = function
+    (_,[] as q) -> q
+  | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
+let push_item x v (m,l) =
+  (Idmap.add x v m, (x,Idset.empty)::l)
+let mem_q x (m,_) = Idmap.mem x m
+let rec find_q x (m,q) =
+  let v = Idmap.find x m in
+  let m' = Idmap.remove x m in
+  let rec find accs acc = function
+      [] -> raise Not_found
+    | [(x',l)] ->
+        if x=x' then ((v,Idset.union accs l),(m',List.rev acc))
+        else raise Not_found
+    | (x',l as i)::((x'',l'')::q as itl) ->
+        if x=x' then
+          ((v,Idset.union accs l),
+           (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
+        else find (Idset.union l accs) (i::acc) itl in
+  find Idset.empty [] q
+
+let occur_vars_in_decl env hyps d =
+  if Idset.is_empty hyps then false else
+    let ohyps = global_vars_set_of_decl env d in
+    Idset.exists (fun h -> Idset.mem h ohyps) hyps
+
+let reorder_context env sign ord =
+  let ords = List.fold_right Idset.add ord Idset.empty in
+  if List.length ord <> Idset.cardinal ords then
+    error "Order list has duplicates";
+  let rec step ord expected ctxt_head moved_hyps ctxt_tail =
+    match ord with
+      | [] -> List.rev ctxt_tail @ ctxt_head
+      | top::ord' when mem_q top moved_hyps ->
+          let ((d,h),mh) = find_q top moved_hyps in
+          if occur_vars_in_decl env h d then
+            errorlabstrm "reorder_context"
+              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+              str "before " ++
+              prlist_with_sep pr_spc pr_id
+                (Idset.elements (Idset.inter h
+                  (global_vars_set_of_decl env d))));
+          step ord' expected ctxt_head mh (d::ctxt_tail)
+      | _ ->
+          (match ctxt_head with
+            | [] -> error_no_such_hypothesis (List.hd ord)
+            | (x,_,_ as d) :: ctxt ->
+                if Idset.mem x expected then
+                  step ord (Idset.remove x expected)
+                    ctxt (push_item x d moved_hyps) ctxt_tail
+                else
+                  step ord expected
+                    ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
+  step ord ords sign mt_q []
+
+let reorder_val_context env sign ord =
+  val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+
+
+
+
+let check_decl_position env sign (x,_,_ as d) =
+  let needed = global_vars_set_of_decl env d in
+  let deps = dependency_closure env (named_context_of_val sign) needed in
+  if List.mem x deps then
+    error ("Cannot create self-referring hypothesis "^string_of_id x);
+  x::deps
+
 (* Auxiliary functions for primitive MOVE tactic
  *
  * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
@@ -134,9 +216,6 @@ let remove_hyp_body env sigma id =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
-let error_no_such_hypothesis id =
-  error ("No such hypothesis: " ^ string_of_id id ^ ".")
-
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
   | (hyp,_,_) :: right ->
@@ -219,14 +298,23 @@ let rename_hyp id1 id2 sign =
 (* Will only be used on terms given to the Refine rule which have meta 
 variables only in Application and Case *)
 
+let error_unsupported_deep_meta c =
+  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+    strbrk "form contains metavariables deep inside the term is not " ++
+    strbrk "supported; try \"refine\" instead.")
+
 let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | Cast(c,_,_) -> collrec acc c
-    | (App _| Case _) -> fold_constr collrec acc c
-    | _ -> acc
-  in 
-  List.rev(collrec [] c)
+  let rec collrec deep acc c = match kind_of_term c with
+    | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
+    | Cast(c,_,_) -> collrec deep acc c
+    | (App _| Case _) -> fold_constr (collrec deep) acc c
+    | _ -> fold_constr (collrec true) acc c
+  in
+  List.rev (collrec false [] c)
+
+let check_meta_variables c = 
+  if not (list_distinct (collect_meta_variables c)) then
+    raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check & not (is_conv_leq env sigma ty conclty) then 
@@ -248,9 +336,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if !check && occur_meta conclty then
-	  anomaly "refined called with a dependent meta";
-	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+	let conclty = nf_betaiota conclty in
+	  if !check && occur_meta conclty then
+	    raise (RefinerError (MetaInType conclty));
+	  (mk_goal hyps conclty)::goalacc, conclty
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
@@ -261,12 +350,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',hdty) =
 	  match kind_of_term f with
 	    | Ind _ | Const _
-		when not (array_exists occur_meta l) (* we could be finer *)
-		  & (isInd f or has_polymorphic_type (destConst f))
-		  ->
+		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
-		type_of_global_reference_knowing_parameters env sigma f l
+                type_of_global_reference_knowing_conclusion env sigma f conclty
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in
@@ -288,6 +375,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | _ -> 
 	if occur_meta trm then
 	  anomaly "refiner called with a meta in non app/case subterm";
+
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
@@ -358,14 +446,19 @@ and mk_casegoals sigma goal goalacc p c =
 
 
 let convert_hyp sign sigma (id,b,bt as d) =
-  apply_to_hyp sign id
-    (fun _ (_,c,ct) _ ->
-       let env = Global.env_of_context sign in
-       if !check && not (is_conv env sigma bt ct) then
-	 error ("Incorrect change of the type of "^(string_of_id id)^".");
-       if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
-	 error ("Incorrect change of the body of "^(string_of_id id)^".");
-       d)
+  let env = Global.env() in
+  let reorder = ref [] in
+  let sign' =
+    apply_to_hyp sign id
+      (fun _ (_,c,ct) _ ->
+        let env = Global.env_of_context sign in
+        if !check && not (is_conv env sigma bt ct) then
+	  error ("Incorrect change of the type of "^(string_of_id id)^".");
+        if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
+	  error ("Incorrect change of the body of "^(string_of_id id)^".");
+       if !check then reorder := check_decl_position env sign d;
+       d) in
+  reorder_val_context env sign' !reorder
 
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
@@ -418,7 +511,9 @@ let prim_refiner r sigma goal =
 	      nexthyp,
 	      cl,sigma
 	  else
-	    (push_named_context_val (id,None,t) sign),cl,sigma in
+            (if !check && mem_named_context id (named_context_of_val sign) then
+                error "New variable is already declared";
+	     push_named_context_val (id,None,t) sign,cl,sigma) in
         let sg2 = mk_goal sign cl in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
@@ -478,8 +573,7 @@ let prim_refiner r sigma goal =
 	  (mk_sign sign all, sigma)
 
     | Refine c ->
-        if not (list_distinct (collect_meta_variables c)) then
-          raise (RefinerError (NonLinearProof c));
+	check_meta_variables c;
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	  (sgl, sigma)
@@ -518,6 +612,10 @@ let prim_refiner r sigma goal =
 	  move_hyp withdep toleft (left,declfrom,right) hto in
   	  ([mk_goal hyps' cl], sigma)
 
+    | Order ord ->
+        let hyps' = reorder_val_context env sign ord in
+        ([mk_goal hyps' cl], sigma)
+
     | Rename (id1,id2) ->
         if !check & id1 <> id2 &&
 	  List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
@@ -628,7 +726,7 @@ let prim_extractor subfun vl pft =
       | Some (Prim (ThinBody _),[pf]) ->
 	  subfun vl pf
 	    
-      | Some (Prim (Move _),[pf]) ->
+      | Some (Prim (Move _|Order _),[pf]) ->
 	  subfun vl pf
 
       | Some (Prim (Rename (id1,id2)),[pf]) ->