compact coercion command: "coercion foo."

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 4894218e8fa28ad10f78c67bc6c2ba027ca055ab..e34b690d311a37f16e76891c0fc6a8950d6d8d5f 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -321,9 +321,9 @@ let extract_term_production status pattern =
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
           | Ast.List0 (_, Some l) -> 
-              Gramext.Slist0sep (s, gram_of_literal status l)
+              Gramext.Slist0sep (s, gram_of_literal status l, true)
           | Ast.List1 (_, Some l) -> 
-              Gramext.Slist1sep (s, gram_of_literal status l)
+              Gramext.Slist1sep (s, gram_of_literal status l, true)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 9d4d3490a9ce7b3729b85e50484bf3790b174ad2..0db31e94dd9e104cc754196796353c7f1eee0cec 100644 (file)
--- a/matitaB/components/grafite/grafiteAst.ml
+++ b/matitaB/components/grafite/grafiteAst.ml
@@ -103,8 +103,8 @@ type command =
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
-      NotationPt.term * NotationPt.term *
-      (string * NotationPt.term) * NotationPt.term
+      (NotationPt.term * NotationPt.term *
+        (string * NotationPt.term) * NotationPt.term) option
   | NQed of loc
   (* ex lexicon commands *)
   | Alias of loc * alias_spec

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index cbaa4d93a8f38f8b845476910d89ca51cb8422d9..c0d9baee7e56c814773cdc993337d778cba68bf3 100644 (file)
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -493,7 +493,32 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, None) ->
+     let status, t, ty, source, target =
+       let o_t = NotationPt.Ident (name,`Ambiguous) in
+       let metasenv,subst, status,t =
+         GrafiteDisambiguate.disambiguate_nterm 
+           status None [] [] [] ("",0,o_t) in
+       assert( metasenv = [] && subst = []);
+       let ty = NCicTypeChecker.typeof status [] [] [] t in
+       let source, target =
+         let clean = function
+         | NCic.Appl (NCic.Const _ as r :: l) -> 
+             NotationPt.Appl (NotationPt.NCic r ::
+               List.map (fun _ -> NotationPt.Implicit `JustOne)l)
+         | NCic.Const _ as r -> NotationPt.NCic r
+         | _ -> assert false in
+         let rec aux = function
+         | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+         | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+         | _ -> assert false in aux ty in
+       status, o_t, NotationPt.NCic ty, source, target in
+     let status, composites =
+      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+     let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+     let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
+      eval_alias status (mode,aliases)
+  | GrafiteAst.NCoercion (loc, name, Some (t, ty, source, target)) ->
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name t ty source target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)

diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index 30a97a3e3e130a28aee11926b17ce043b80dc48e..3e77258e0f0e2843d20dc98f0f0c96ac3190de3b 100644 (file)
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -221,7 +221,7 @@ EXTEND
                 G.NMacro(loc,
              G.NAutoInteractive (loc, (None,["depth",depth]@params))))
     | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc)
-    | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
+    | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t))
     | IDENT "screenshot"; fname = QSTRING -> 
         G.NMacro(loc,G.Screenshot (loc, fname))
     | IDENT "cases"; what = tactic_term ; where = pattern_spec ->
@@ -576,11 +576,11 @@ EXTEND
          G.NUnivConstraint (loc,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
-    | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term; 
+    | IDENT "coercion"; name = IDENT; spec = OPT [ SYMBOL ":"; ty = term; 
         SYMBOL <:unicode<def>>; t = term; "on"; 
         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
-        "to"; target = term ->
-          G.NCoercion(loc,name,t,ty,(id,source),target)     
+        "to"; target = term -> t,ty,(id,source),target ] ->
+        G.NCoercion(loc,name,spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
     | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; 

diff --git a/matitaB/components/grafite_parser/print_grammar.ml b/matitaB/components/grafite_parser/print_grammar.ml
index 5bc87f247296fba632b30781bcef587f4a6256b3..6bcc1468730dc9e2ef5cce86a486dccd45c9ca12 100644 (file)
--- a/matitaB/components/grafite_parser/print_grammar.ml
+++ b/matitaB/components/grafite_parser/print_grammar.ml
@@ -87,7 +87,7 @@ and is_symbol_dummy = function
   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
   | Snterm e | Snterml (e, _) -> is_entry_dummy e
   | Slist1 x | Slist0 x -> is_symbol_dummy x
-  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+  | Slist1sep (x,y,_) | Slist0sep (x,y,_) -> is_symbol_dummy x && is_symbol_dummy y
   | Sopt x -> is_symbol_dummy x
   | Sself | Snext -> false
   | Stree t -> is_tree_dummy t
@@ -186,7 +186,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]} @ ";
         todo
-    | Slist0sep (symbol,sep) ->
+    | Slist0sep (symbol,sep,_) ->
         Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "{@[<hov2> ";
@@ -200,7 +200,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]}+ @ ";
         todo 
-    | Slist1sep (symbol,sep) ->
+    | Slist1sep (symbol,sep,_) ->
         let todo = visit_symbol symbol todo is_son  in
         Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol sep todo is_son in