From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 23 Sep 2015 11:32:08 +0000 (+0000)
Subject: optional parameters added to the syntax of definitions,
X-Git-Tag: make_still_working~690
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b4d894e7349bba991823249f1716fb8f18239b7;p=helm.git

optional parameters added to the syntax of definitions,
like the one for Record and Inductive.
---

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 70fe2f415..fd9c2946d 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -66,6 +66,12 @@ let nmk_rec_corec src ind_kind defs loc index =
  let loc,t = mk_rec_corec src ind_kind defs loc in
   G.NObj (loc,t,index)
 
+let shift_vars binder (vars, ty) bo =
+   let map var bo = N.Binder (binder, (var, ty), bo) in
+   List.fold_right map vars bo
+
+let shift_params binder params bo = 
+   List.fold_right (shift_vars binder) params bo
 (*
 let nnon_punct_of_punct = function
   | G.Skip loc -> G.NSkip loc
@@ -501,12 +507,20 @@ EXTEND
   grafite_ncommand: [ [
       IDENT "qed" ;  i = index -> G.NQed (loc,i)
     | IDENT "defined" ;  i = index -> G.NQed (loc,i) (* FG: presentational qed for definitions *)
-    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+    | src = source; nflavour = ntheorem_flavour; name = IDENT;
+      params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term; (* FG: params added *)
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        let typ = shift_params `Forall params typ in
+        let body = match body with
+           | Some bo -> Some (shift_params `Lambda params bo)
+           | None    -> None
+        in
         let attrs = src, nflavour, `Regular in
 	G.NObj (loc, N.Theorem (name, typ, body, attrs),true)
-    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+    | src = source; nflavour = ntheorem_flavour; name = IDENT;
+      params = LIST0 protected_binder_vars; SYMBOL <:unicode<def>> (* ≝ *); (* FG: params added *)
       body = term ->
+        let body = shift_params `Lambda params body in
         let attrs = src, nflavour, `Regular in
         G.NObj (loc, 
           N.Theorem(name, N.Implicit `JustOne, Some body, attrs),