closed bug 1898: fold x in x; added a reordering primitive tactic

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

1 files changed, 142 insertions, 28 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 48ed610b9..391d6f466 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,27 +62,14 @@ let rec catchable_exception = function
       (_, 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 =
@@ -100,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 _ ->
@@ -129,6 +132,111 @@ 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 q =
+  let (m,l) = push_val x q in
+  (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.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 =
+    list_map_filter (fun (id,_,_) ->
+      if Idset.mem id needed then Some id else None)
+      (named_context_of_val sign) in
+  if List.mem x deps then
+    error ("Cannot create self-referring hypothesis "^string_of_id x);
+  x::deps
+
+
+(******)
+(* older version (performs more swapping) 
+let reorder_context sign ord =
+  let ords = List.fold_left Idset.add Idset.empty sign in
+  let rec step expected moved_hyps ctxt_head ctxt_tail =
+    if not (Idset.is_empty expected) then
+      match ctxt_head with
+          [] -> failwith "some hyps not found" (* those in expected *)
+        | (x,_,_ as d) :: ctxt ->
+            if Idset.mem x expected then
+              step
+                (Idset.remove x expected)
+                (Idmap.add x (d,Idset.empty) move_hyps)
+                ctxt ctxt_tail
+            else
+              step expected (push_hyp x moved_hyps) ctxt (d::ctxt_tail)
+    else begin
+      (* TODO: check free var constraints *)
+      let ctxt_mid =
+        List.map (fun h -> fst (Idmap.find h moved_hyps)) ords
+
+      in List.rev ctxt_tail @ ctxt_mid @ ctxt_head
+    end in
+  step ords Idmap.empty sign []
+*)
+
 (* Auxiliary functions for primitive MOVE tactic
  *
  * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
@@ -137,9 +245,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 ->
@@ -360,14 +465,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
@@ -522,6 +632,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
@@ -632,7 +746,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]) ->