Merge pull request #136 from SkySkimmer/retype

Some cleanups and fix incorrect evar map passing in aac_reflexivity

Makefile

@@ -10,7 +10,10 @@ Makefile.coq: _CoqProject
 
 force _CoqProject Makefile: ;
 
+tests:
+	$(MAKE) -C tests
+
 %: Makefile.coq force
 	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean force
+.PHONY: all clean force tests

src/aac_rewrite.ml

@@ -17,22 +17,19 @@ module Control =   struct
 end
 
 module Debug = Helper.Debug (Control)
-open Debug
 
 let time_tac msg tac =
   if Control.time then  Proofview.tclTIME (Some msg) tac else tac
 
 let tclTac_or_exn (tac : 'a Proofview.tactic) exn msg : 'a Proofview.tactic =
   Proofview.tclORELSE tac
     (fun e ->
-      let open Proofview.Notations in
       let open Proofview in
-      tclEVARMAP >>= fun sigma ->
       Goal.enter_one (fun gl ->
-          let env = Proofview.Goal.env gl in
-          pr_constr env sigma "last goal" (Goal.concl gl);
-          exn msg e)
-    )
+          let env = Goal.env gl in
+          let sigma = Goal.sigma gl in
+          Debug.pr_constr env sigma "last goal" (Goal.concl gl);
+          exn msg e))
 
 
 open EConstr
@@ -188,7 +185,7 @@ let aac_conclude env sigma (concl:types): ( Evd.evar_map * constr * aac_lift * T
       let eq = Coq.Equivalence.to_relation lift.e in
       let tleft,tright, sigma = Theory.Trans.t_of_constr env sigma eq envs (left,right) in
       let sigma, ir = Theory.Trans.ir_of_envs env sigma eq envs in
-      let _ = pr_constr env sigma "concl" concl in
+      let () = Debug.pr_constr env sigma "concl" concl in
       (sigma,left,lift,ir,tleft,tright)
   with
   | Not_found -> Coq.user_error @@ Pp.strbrk "No lifting from the goal's relation to an equivalence"
@@ -199,12 +196,11 @@ let aac_normalise =
   let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in
   let norm_tac = KerName.make mp (Label.make "internal_normalize") in
   let norm_tac = Locus.ArgArg (None, norm_tac) in
-  let open Proofview.Notations in
   let open Proofview in
   Proofview.Goal.enter (fun goal -> 
       let ids = Tacmach.pf_ids_of_hyps goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let concl = Proofview.Goal.concl goal in
       let sigma,left,lift,ir,tleft,tright = aac_conclude env sigma concl in
       Tacticals.tclTHENLIST
@@ -218,9 +214,9 @@ let aac_normalise =
 let aac_reflexivity : unit Proofview.tactic =
   let open Proofview.Notations in
   let open Proofview in
-  tclEVARMAP >>= fun sigma ->
   Goal.enter (fun goal ->
       let env = Proofview.Goal.env goal in
+      let sigma = Proofview.Goal.sigma goal in
       let concl = Goal.concl goal in
       let sigma,zero,lift,ir,t,t' = aac_conclude env sigma concl in
       let x,r = Coq.Relation.split (lift.r) in
@@ -235,22 +231,16 @@ let aac_reflexivity : unit Proofview.tactic =
       Unsafe.tclEVARS sigma
       <*> Coq.tclRETYPE lift_reflexivity
       <*> Tactics.apply lift_reflexivity
-      <*> (let concl = Goal.concl goal in
-           tclEVARMAP >>= fun sigma ->
-           let _ = pr_constr env sigma "concl "concl in
-           by_aac_reflexivity zero lift.e ir t t')
-    )
+      <*> by_aac_reflexivity zero lift.e ir t t')
 
 
 (** A sub-tactic to lift the rewriting using Lift  *)
 let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): unit Proofview.tactic =
-  let open Proofview.Notations in
-  let open Proofview in
   Proofview.Goal.enter (fun goal ->
       (* catch the equation and the two members*)
       let concl = Proofview.Goal.concl goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let (left, right, _ ) = match  Coq.match_as_equation env sigma concl with
         | Some x -> x
         | None -> Coq.user_error @@ Pp.strbrk "The goal is not an equation"
@@ -286,11 +276,10 @@ let core_aac_rewrite ?abort
       subst
       (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> unit Proofview.tactic)
       (tr : constr) t left : unit Proofview.tactic =
-  let open Proofview.Notations in
   Proofview.Goal.enter (fun goal ->
       let env = Proofview.Goal.env goal in
-      Proofview.tclEVARMAP >>= fun sigma ->
-      pr_constr env sigma "transitivity through" tr;
+      let sigma = Proofview.Goal.sigma goal in
+      Debug.pr_constr env sigma "transitivity through" tr;
       let tran_tac =
         lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt
       in
@@ -332,13 +321,11 @@ let choose_subst  subterm sol m=
 (** rewrite the constr modulo AC from left to right in the left member
     of the goal *)
 let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ?extra ~occ_subterm ~occ_sol rew : unit Proofview.tactic =
-  let open Proofview.Notations in
-  let open Proofview in
   Proofview.Goal.enter (fun goal ->
       let envs = Theory.Trans.empty_envs () in
       let (concl : types) = Proofview.Goal.concl goal in
       let env = Proofview.Goal.env goal in
-      tclEVARMAP >>= fun sigma ->
+      let sigma = Proofview.Goal.sigma goal in
       let (_,_,rlt) as concl =
         match Coq.match_as_equation env sigma concl with
         | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation"

src/coq.ml

@@ -40,30 +40,17 @@ let get_fresh r = new_monomorphic_global (Lazy.force r)
 let get_efresh r = EConstr.of_constr (new_monomorphic_global (Lazy.force r))
 
 
-(* A clause specifying that the [let] should not try to fold anything
-   in the goal *)
-let nowhere =
-  { Locus.onhyps = Some [];
-    Locus.concl_occs = Locus.NoOccurrences
-  }
-
-let retype c =
-  Proofview.Goal.enter begin fun gl ->
-  let sigma, _ = Typing.type_of (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) c in
-  Proofview.Unsafe.tclEVARS sigma
-  end
-
-(* similar to retype above. No Idea when/why this is needed, I smell some ugly hack.
-  Apparently, it has to do with the need to recompute universe constrains if we just compose terms *)
-let tclRETYPE c=
+(* Typically needed to recompute universe constraints,
+   eg if we do [mkApp (id, [|some_ty; some_v|])]
+   (universe of some_ty must be <= universe of id argument) *)
+let tclRETYPE c =
   let open Proofview in
-  tclEVARMAP >>= fun sigma ->
-  Proofview.Goal.enter (fun goal ->
-      let env = Proofview.Goal.env goal in
+  Goal.enter_one ~__LOC__ (fun goal ->
+      let env = Goal.env goal in
+      let sigma = Goal.sigma goal in
       let sigma,_ = Typing.type_of env sigma c in
-      Unsafe.tclEVARS sigma
-    )
-
+      Unsafe.tclEVARS sigma)
+
 (** {1 Tacticals}  *)
 
 let tclTIME msg tac =
@@ -94,18 +81,6 @@ let show_proof pstate : unit =
   ()
 
 
-let cps_mk_letin
-    (name:string)
-    (c: constr)
-    (k : constr -> tactic)
-: tactic =
-  Proofview.Goal.enter begin fun goal ->
-    let name = (Id.of_string name) in
-    let name =  Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.pf_env goal) in
-    let letin = Tactics.letin_tac None (Name name) c None nowhere in
-    Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))]
-  end
-
 let mk_letin (name:string) (c: constr) : constr Proofview.tactic =
   let open Proofview in
   let name = (Id.of_string name) in

src/coq.mli

@@ -38,11 +38,8 @@ val cps_resolve_one_typeclass: ?error:Pp.t -> EConstr.types -> (EConstr.constr
 val evar_binary: Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
 val evar_relation: Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
 
-(** [cps_mk_letin name v] binds the constr [v] using a letin tactic  *)
-val cps_mk_letin : string -> EConstr.constr -> ( EConstr.constr -> tactic) -> tactic
 val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic
 
-val retype : EConstr.constr -> tactic
 val tclRETYPE : EConstr.constr -> unit Proofview.tactic
 
 val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term

src/theory.ml

@@ -990,12 +990,11 @@ module Trans = struct
       able to build the sigmas *)
   let build_sigma_maps (rlt : Coq.Relation.t) zero ir : (sigmas * sigma_maps) Proofview.tactic =
     let open Proofview.Notations in
-    let open Proofview in
-    tclEVARMAP >>= fun sigma ->
     Proofview.Goal.enter_one (fun goal ->
         let env = Proofview.Goal.env goal in
+        let sigma = Proofview.Goal.sigma goal in
         let sigma,rp = build_reif_params env sigma rlt zero in
-        Unsafe.tclEVARS sigma
+        Proofview.Unsafe.tclEVARS sigma
         <*> let renumbered_sym, to_local, to_global = renumber ir.sym  in
             let env_sym = Sigma.of_list
                             rp.sym_ty
@@ -1034,7 +1033,7 @@ module Trans = struct
 	        units_to_pos = (let units = f units in fun x ->  (List.assoc  x units));
               }
             in
-            tclUNIT (sigmas, sigma_maps))
+            Proofview.tclUNIT (sigmas, sigma_maps))
 
   (** builders for the reification *)
   type reif_builders =

tests/Makefile

@@ -0,0 +1,16 @@
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
+
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+force _CoqProject Makefile: ;
+
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force tests

tests/_CoqProject

@@ -0,0 +1,7 @@
+-Q ../src AAC_tactics
+-Q ../theories AAC_tactics
+-I ../src
+
+-R . Test
+
+aac_135.v

tests/aac_135.v

@@ -0,0 +1,33 @@
+From Coq Require PeanoNat ZArith List Permutation Lia.
+From AAC_tactics Require Import AAC.
+From AAC_tactics Require Instances.
+
+(** ** Introductory example
+
+   Here is a first example with relative numbers ([Z]): one can
+   rewrite an universally quantified hypothesis modulo the
+   associativity and commutativity of [Z.add]. *)
+
+Section introduction.
+  Import ZArith.
+  Import Instances.Z.
+
+  Variables a b : Z.
+
+  Goal a + b = b + a.
+    aac_reflexivity.
+  Qed.
+
+  Goal forall c: bool, a + b = b + a.
+    intros c.
+    destruct c.
+    1,2: aac_reflexivity.
+  Qed. (* The command has indeed failed with message: Some unresolved existential variables remain *)
+
+  Goal forall c: bool, a + b = b + a.
+    intros c.
+    destruct c.
+    - aac_reflexivity.
+    - aac_reflexivity.
+  Qed.
+End introduction.