New experimental commit: metavariables representation is changed again,

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index f3dc1b05e0cb001c9f03c8e5496dc184a19149c4..3f6afc79a4685838fd9bb90a3f3990fe98119c5b 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -37,7 +37,7 @@
   let rec aux i =
    function
       [] -> raise Not_found
-    | he::_ when he = e -> i
+    | (Some he)::_ when he = e -> i
     | _::tl -> aux (i+1) tl
   in
    aux 1
@@ -55,8 +55,8 @@
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
 %token ALIAS
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
-%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
 %type <Cic.term option> main
@@ -156,7 +156,7 @@ expr2:
  | PROP { Sort Prop }
  | TYPE { Sort Type }
  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META { Meta $1 }
+ | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } 
  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 ;
 expr :
@@ -174,7 +174,7 @@ expr :
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
+    { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
        $2,$4
     }
@@ -187,7 +187,7 @@ fixfunsdecl:
 ;
 cofixheader:
    COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_) -> Name name) $4 in
+    { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
        $2,$4
     }
@@ -200,23 +200,23 @@ cofixfunsdecl:
 ;
 pihead:
    PROD ID COLON expr DOT
-    { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       (Cic.Name $2, $4) }
  | expr2 ARROW
-   { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
      (Anonimous, $1) }
  | LPAREN expr RPAREN ARROW
-   { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
      (Anonimous, $2) }
 ;
 lambdahead:
   LAMBDA ID COLON expr DOT
-   { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
      (Cic.Name $2, $4) }
 ;
 letinhead:
   LAMBDA ID LETIN expr DOT
-   { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
      (Cic.Name $2, $4) }
 ;
 branches:
@@ -232,6 +232,11 @@ exprseplist:
    expr                        { [$1] }
  | expr SEMICOLON exprseplist  { $1::$3 }
 ;
+substitutionlist:
+                                     { [] }
+ | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
+ | NONE SEMICOLON substitutionlist   { None::$3 }
+;
 alias:
    ALIAS ID CONURI
     { let cookingno = get_cookingno $3 in
@@ -245,3 +250,6 @@ alias:
         Hashtbl.add uri_of_id_map $2
          (Cic.MutConstruct (uri, cookingno, indno ,consno))
     }
+
+
+