Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index c92e3175f45d9f84d80aa4c88df4272db669a2bb..8a418200d94604127cd7aad3a000aafdca921417 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -253,10 +253,15 @@ EXTEND
         G.NCases (loc, what, where)
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
         G.NChange (loc, what, with_what)
+    | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term -> 
+        G.NConstructor (loc,
+           (match num with None -> None | Some x -> Some (int_of_string x)),l)
+    | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->
         G.NGeneralize (loc, p)
+    | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->
         G.NLetIn (loc,where,t,name)
@@ -655,6 +660,7 @@ EXTEND
 
     nmacro: [
       [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+      | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
       ]
     ];
     
@@ -797,6 +803,8 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term -> 
+        G.NInverter (loc,name,indty)
     | NLETCOREC ; defs = let_defs -> 
         nmk_rec_corec `CoInductive defs loc
     | NLETREC ; defs = let_defs -> 
@@ -812,26 +820,15 @@ EXTEND
         in
         G.NObj (loc, N.Inductive (params, ind_types))
     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
-        strict = [ SYMBOL <:unicode<lt>> -> true 
-                 | SYMBOL <:unicode<leq>> -> false ]; 
-        u2 = tactic_term ->
-        let u1 =
-          match u1 with
+        SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+        let urify = function 
           | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
-          | _ -> raise (Failure "only a sort can be constrained")
+          | _ -> raise (Failure "only a Type[…] sort can be constrained")
         in
-        let u2 =
-          match u2 with
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
-          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
-              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
-          | _ -> raise (Failure "only a sort can be constrained")
-        in
-         G.NUnivConstraint (loc, strict,u1,u2)
+        let u1 = urify u1 in
+        let u2 = urify u2 in
+         G.NUnivConstraint (loc,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
     | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;