New: (temporary) concrete syntax to specify the morphism signature:

 "Add Morphism m @ arg1 ... argn @ out as ident"

where argi = constr arrow
and arrow =  "-->" | "++>" | "==>" (for contravariant, covariant and
 bi-variant morphisms).

The syntax should be improved by getting rid of the "@" and maybe choosing
better symbols to represent the arrows.


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

5 files changed, 58 insertions, 19 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index e8ea238ac6..119f6b3bf1 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -33,6 +33,16 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
+(* For Setoid rewrite *)
+let pr_morphism_argument _ _ = Setoid_replace.pr_morphism_argument
+
+ARGUMENT EXTEND morphism_argument
+ TYPED AS morphism_argument
+ PRINTED BY pr_morphism_argument
+  | [ constr(c) "++>" ] -> [ Some true,c ]
+  | [ constr(c) "-->" ] -> [ Some false,c ]
+  | [ constr(c) "==>"  ] -> [ None,c ]
+END
 
 let pr_gen prc _ c = prc c
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 6eb57e3f92..81a3851522 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -19,6 +19,13 @@ val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool closed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
+val rawwit_morphism_argument :
+ Setoid_replace.morphism_argument raw_abstract_argument_type
+val wit_morphism_argument :
+ Setoid_replace.morphism_argument closed_abstract_argument_type
+val morphism_argument :
+ Setoid_replace.morphism_argument Pcoq.Gram.Entry.e
+
 val rawwit_raw : constr_expr raw_abstract_argument_type
 val wit_raw : rawconstr closed_abstract_argument_type
 val raw : constr_expr Pcoq.Gram.Entry.e
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0d4b479b44..789e5c116c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -173,10 +173,12 @@ TACTIC EXTEND SetoidRewrite
   [ "Setoid_rewrite" orient(b) constr(c) ] -> [ general_s_rewrite b c ]
 END
 
-VERNAC COMMAND EXTEND AddSetoid
+VERNAC COMMAND EXTEND AddSetoid1
   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ]
 | [ "Add" "Morphism" constr(m) ":" ident(s) ] ->
    [ new_named_morphism s m None ]
+| [ "Add" "Morphism" constr(m) "@" ne_morphism_argument_list(l) "@" constr(out) "as" ident(s) ] ->
+    [ new_named_morphism s m (Some (l,out))]
 END
 
 VERNAC COMMAND EXTEND AddRelation1
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 67ffb6c21e..418a545cd1 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -211,13 +211,17 @@ let prrelation_class =
        str "[[ Error: setoid on equality " ++ prterm eq ++ str " not found! ]]")
   | Leibniz ty -> prterm ty
 
-let prargument_class (variance,rel) =
- prrelation_class rel ++
+let prmorphism_argument_gen prrelation (variance,rel) =
+ prrelation rel ++
   match variance with
-     None -> str " -> "
-   | Some true -> str " +-> "
+     None -> str " ==> "
+   | Some true -> str " ++> "
    | Some false -> str " --> "
 
+let prargument_class = prmorphism_argument_gen prrelation_class
+
+let pr_morphism_argument = prmorphism_argument_gen Ppconstrnew.pr_constr
+
 let prmorphism k m =
   prterm k ++ str ": " ++
   prlist prargument_class m.args ++
@@ -240,6 +244,14 @@ let default_relation_for_carrier a =
          str " is randomly chosen.") ;
      Relation relation
 
+let find_relation_class rel =
+ try Relation (relation_table_find rel)
+ with
+  Not_found ->
+   match kind_of_term (Reduction.whd_betadeltaiota (Global.env ()) rel) with
+    | App (eq,[|ty|]) when eq_constr eq (Lazy.force coq_eq) -> Leibniz ty
+    | _ -> raise Not_found
+
 let relation_morphism_of_constr_morphism =
  let relation_relation_class_of_constr_relation_class =
   function
@@ -600,29 +612,31 @@ let new_morphism m signature id hook =
            List.map (fun ty -> None,default_relation_for_carrier ty) args_ty,
            default_relation_for_carrier output
         | Some (args,output) ->
-           let relation_table_find t =
-            try relation_table_find t
+           let find_relation_class t =
+            try find_relation_class t
             with Not_found ->
              errorlabstrm "Add Morphism"
               (str "Not a valid signature: " ++ prterm t ++
-               str " is not a registered relation")
+               str " is neither a registered relation nor the Leibniz " ++
+               str " equality partially applied to a type.")
            in
-           let relation_table_find_v (variance,t) =
-            let relation = relation_table_find t in
-             match relation.rel_sym,variance with
-                Some _, None
-              | None, Some _ -> variance,Relation relation
-              | None,None ->
+           let find_relation_class_v (variance,t) =
+            let relation = find_relation_class t in
+             match find_relation_class t, variance with
+                Leibniz _, None
+              | Relation {rel_sym = Some _}, None
+              | Relation {rel_sym = None}, Some _ -> variance,relation
+              | Relation {rel_sym = None},None ->
                  errorlabstrm "Add Morphism"
                   (str "You must specify the variance in each argument " ++
                    str "whose relation is asymmetric.")
-              | Some _, Some _ ->
+              | Leibniz _, Some _
+              | Relation {rel_sym = Some _}, Some _ ->
                  errorlabstrm "Add Morphism"
                   (str "You cannot specify the variance of an argument " ++
-                   str "whose relation is asymmetric.")
+                   str "whose relation is symmetric.")
            in
-            List.map relation_table_find_v args,
-            Relation (relation_table_find output)
+            List.map find_relation_class_v args, find_relation_class output
       in
       let argsconstr,outputconstr,lem =
        gen_compat_lemma_statement output args m
@@ -685,6 +699,8 @@ let morphism_hook stre ref =
     add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
      (m,args,output); no_more_edited pf_id
 
+type morphism_argument = bool option * Topconstr.constr_expr
+
 let new_named_morphism id m sign =
  let sign =
   match sign with
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index a763f237ae..babd89f1a8 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -13,6 +13,10 @@ open Proof_type
 open Topconstr
 
 
+type morphism_argument = bool option * constr_expr
+
+val pr_morphism_argument : morphism_argument -> Pp.std_ppcmds
+
 val register_replace : (constr -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
@@ -34,4 +38,4 @@ val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
 
 val new_named_morphism :
  Names.identifier -> constr_expr ->
-  ((bool option * constr_expr) list * constr_expr) option -> unit
+  (morphism_argument list * constr_expr) option -> unit