There were a big bug in both Fix and CoFix: the recursive functions were

not bounded in the bodies.

Fix and CoFix syntax changed to a less natural, but easier to parse one.
The above bug has been fixed.

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 844384f6265416b79e18384140082a60aa45931f..42869a2991ee617fc221c29e77a7d3c057697e38 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -67,31 +67,47 @@ expr:
            MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10)
          | _ -> raise InductiveTypeURIExpected
     }
- | FIX ID LCURLY fixfuns RCURLY
-    { let fixfuns = $4 in
+ | fixheader LCURLY exprseplist RCURLY
+    { let fixfunsdecls = snd $1 in
+      let fixfunsbodies = $3 in
        let idx =
         let rec find idx =
          function
             [] -> raise Not_found
-          | (name,_,_,_)::_  when name = $2 -> idx
+          | (name,_,_)::_  when name = (fst $1) -> idx
           | _::tl -> find (idx+1) tl
         in
-         find 0 fixfuns
+         find 0 fixfunsdecls
        in
-        Fix (idx,fixfuns)
+        let fixfuns =
+         List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
+          fixfunsdecls fixfunsbodies
+        in
+         for i = 1 to List.length fixfuns do
+          binders := List.tl !binders
+         done ;
+         Fix (idx,fixfuns)
     }
- | COFIX ID LCURLY cofixfuns RCURLY
-    { let cofixfuns = $4 in
+ | cofixheader LCURLY exprseplist RCURLY
+    { let cofixfunsdecls = (snd $1) in
+      let cofixfunsbodies = $3 in
        let idx =
         let rec find idx =
          function
             [] -> raise Not_found
-          | (name,_,_)::_  when name = $2 -> idx
+          | (name,_)::_  when name = (fst $1) -> idx
           | _::tl -> find (idx+1) tl
         in
-         find 0 cofixfuns
+         find 0 cofixfunsdecls
        in
-        CoFix (idx,cofixfuns)
+        let cofixfuns =
+         List.map2 (fun (name,ty) bo -> (name,ty,bo))
+          cofixfunsdecls cofixfunsbodies
+        in
+         for i = 1 to List.length cofixfuns do
+          binders := List.tl !binders
+         done ;
+         CoFix (idx,cofixfuns)
     }
  | IMPLICIT { Implicit }
  | SET { Sort Set }
@@ -107,17 +123,31 @@ expr:
  | letinhead expr 
     { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
 ;
-fixfuns:
-   ID LPAREN NUM RPAREN COLON expr LETIN expr
-    { [$1,$3,$6,$8] }
- | ID LPAREN NUM RPAREN COLON expr LETIN expr SEMICOLON fixfuns
-    { ($1,$3,$6,$8)::$10 }
+fixheader:
+   FIX ID LCURLY fixfunsdecl RCURLY
+    { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
+       binders := bs@(!binders) ;
+       $2,$4
+    }
 ;
-cofixfuns:
-   ID COLON expr LETIN expr
-    { [$1,$3,$5] }
- | ID COLON expr LETIN expr SEMICOLON cofixfuns
-    { ($1,$3,$5)::$7 }
+fixfunsdecl:
+   ID LPAREN NUM RPAREN COLON expr
+    { [$1,$3,$6] }
+ | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
+    { ($1,$3,$6)::$8 }
+;
+cofixheader:
+   COFIX ID LCURLY cofixfunsdecl RCURLY
+    { let bs = List.rev_map (function (name,_) -> Name name) $4 in
+       binders := bs@(!binders) ;
+       $2,$4
+    }
+;
+cofixfunsdecl:
+   ID COLON expr
+    { [$1,$3] }
+ | ID COLON expr SEMICOLON cofixfunsdecl
+    { ($1,$3)::$5 }
 ;
 pihead:
   PROD ID COLON expr DOT
@@ -140,6 +170,10 @@ exprlist:
                   { [] }
  | expr exprlist  { $1::$2 }
 ;
+exprseplist:
+   expr                        { [$1] }
+ | expr SEMICOLON exprseplist  { $1::$3 }
+;
 alias:
    ALIAS ID CONURI
     { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }