From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Dec 2002 14:27:22 +0000 (+0000)
Subject: Completely broken parsing of Fix and CoFix fixed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5080a6659b18fbb57937ce3f76acb1f6be10061;p=helm.git

Completely broken parsing of Fix and CoFix fixed.
---

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 9fd6ec52a..bb9113403 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -208,56 +208,56 @@ expr2:
              (mk_expr3 interp))
     }
  | fixheader LCURLY exprseplist RCURLY
-    { let dom1,mk_fixheader = $1 in
+    { let dom1,foo,ids_and_indexes,mk_types = $1 in
       let dom2,mk_exprseplist = $3 in
        let dom = union dom1 dom2 in
+        for i = 1 to List.length ids_and_indexes do
+         CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+        done ;
         dom,
          function interp ->
-          let fixfunsdecls = snd (mk_fixheader interp) in
+          let types = mk_types interp in
           let fixfunsbodies = (mk_exprseplist interp) in
            let idx =
             let rec find idx =
              function
                 [] -> raise Not_found
-              | (name,_,_)::_  when name = (fst (mk_fixheader interp)) -> idx
+              | (name,_)::_  when name = foo -> idx
               | _::tl -> find (idx+1) tl
             in
-             find 0 fixfunsdecls
+             find 0 ids_and_indexes
            in
             let fixfuns =
-             List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
-              fixfunsdecls fixfunsbodies
+             List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
+              (List.combine ids_and_indexes types) fixfunsbodies
             in
-             for i = 1 to List.length fixfuns do
-              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-             done ;
              Fix (idx,fixfuns)
     }
  | cofixheader LCURLY exprseplist RCURLY
-    { let dom1,mk_cofixheader = $1 in
+    { let dom1,foo,ids,mk_types = $1 in
       let dom2,mk_exprseplist = $3 in
        let dom = union dom1 dom2 in
         dom,
          function interp ->
-          let cofixfunsdecls = (snd (mk_cofixheader interp)) in
-          let cofixfunsbodies = mk_exprseplist interp in
+          let types = mk_types interp in
+          let fixfunsbodies = (mk_exprseplist interp) in
            let idx =
             let rec find idx =
              function
                 [] -> raise Not_found
-              | (name,_)::_  when name = (fst (mk_cofixheader interp)) -> idx
+              | name::_  when name = foo -> idx
               | _::tl -> find (idx+1) tl
             in
-             find 0 cofixfunsdecls
+             find 0 ids
            in
-            let cofixfuns =
+            let fixfuns =
              List.map2 (fun (name,ty) bo -> (name,ty,bo))
-              cofixfunsdecls cofixfunsbodies
+              (List.combine ids types) fixfunsbodies
             in
-             for i = 1 to List.length cofixfuns do
+             for i = 1 to List.length fixfuns do
               CicTextualParser0.binders := List.tl !CicTextualParser0.binders
              done ;
-             CoFix (idx,cofixfuns)
+             CoFix (idx,fixfuns)
     }
  | IMPLICIT
     { let newmeta = new_meta () in
@@ -350,52 +350,48 @@ expr :
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
-    { let dom,mk_fixfunsdecl = $4 in
-       dom,
-        function interp ->
-         let bs =
-          List.rev_map
-           (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
-         in
-          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-          $2,(mk_fixfunsdecl interp)
+    { let dom,ids_and_indexes,mk_types = $4 in
+       let bs =
+        List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
+       in
+        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+        dom, $2, ids_and_indexes, mk_types
     }
 ;
 fixfunsdecl:
    ID LPAREN NUM RPAREN COLON expr
     { let dom,mk_expr = $6 in
-       dom, function interp -> [$1,$3,mk_expr interp]
+       dom, [$1,$3], function interp -> [mk_expr interp]
     }
  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
     { let dom1,mk_expr = $6 in
-      let dom2,mk_fixfunsdecl = $8 in
+      let dom2,ids_and_indexes,mk_types = $8 in
        let dom = union dom1 dom2 in
-        dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+        dom, ($1,$3)::ids_and_indexes,
+         function interp -> (mk_expr interp)::(mk_types interp)
     }
 ;
 cofixheader:
    COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let dom,mk_cofixfunsdecl = $4 in
-       dom,
-        function interp ->
-         let bs =
-          List.rev_map
-           (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
-         in
-          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-          $2,(mk_cofixfunsdecl interp)
+    { let dom,ids,mk_types = $4 in
+       let bs =
+        List.rev_map (function name -> Some (Name name)) ids
+       in
+        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+        dom, $2, ids, mk_types
     }
 ;
 cofixfunsdecl:
    ID COLON expr
     { let dom,mk_expr = $3 in
-       dom, function interp -> [$1,(mk_expr interp)]
+       dom, [$1], function interp -> [mk_expr interp]
     }
  | ID COLON expr SEMICOLON cofixfunsdecl
     { let dom1,mk_expr = $3 in
-      let dom2,mk_cofixfunsdecl = $5 in
+      let dom2,ids,mk_types = $5 in
        let dom = union dom1 dom2 in
-        dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+        dom, $1::ids,
+         function interp -> (mk_expr interp)::(mk_types interp)
     }
 ;
 pihead: