new macro screenshot

[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 dfef4d237a0ea34c8883b2b23b1e734fb46b8fcd..52f151fc274a59a8dca825506429c10d9f051c20 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -79,7 +79,7 @@ let mk_rec_corec ind_kind defs loc =
   let name,ty = 
     match defs with
     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
-        let ty = match ty with Some ty -> ty | None -> N.Implicit in
+        let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
         let ty =
          List.fold_right
           (fun var ty -> N.Binder (`Pi,var,ty)
@@ -209,11 +209,11 @@ EXTEND
       let deannotate = function
         | N.AttributedTerm (_,t) | t -> t
       in match deannotate params with
-      | N.Implicit -> [false]
+      | N.Implicit _ -> [false]
       | N.UserInput -> [true]
       | N.Appl l -> 
          List.map (fun x -> match deannotate x with  
-           | N.Implicit -> false
+           | N.Implicit _ -> false
            | N.UserInput -> true
            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
@@ -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)
@@ -652,6 +657,12 @@ EXTEND
         in
         (params,name,typ,fields)
     ] ];
+
+    nmacro: [
+      [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+      | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
+      ]
+    ];
     
     macro: [
       [ [ IDENT "check"   ]; t = term ->
@@ -789,7 +800,7 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
-        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
+        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))
     | NLETCOREC ; defs = let_defs -> 
@@ -807,26 +818,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
-          | 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
-        let u2 =
-          match u2 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
-         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; 
@@ -836,6 +836,10 @@ EXTEND
           G.NCoercion(loc,name,t,ty,(id,source),target)     
     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
+    | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with"; 
+      m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
+        G.NCopy (loc,s,NUri.uri_of_string u,
+          List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
   ]];
 
   grafite_command: [ [
@@ -855,7 +859,7 @@ EXTEND
     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
         G.Obj (loc,
-          N.Theorem (flavour, name, N.Implicit, Some body))
+          N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
     | LETCOREC ; defs = let_defs -> 
@@ -934,6 +938,7 @@ EXTEND
         punct = punctuation_tactical ->
           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
+    | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
     ]
   ];
   comment: [