From f58a80f4ad1aaf26eecb7a8fb7ebef436fb0967a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Jan 2002 18:25:37 +0000 Subject: [PATCH] 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. --- .../cic_textual_parser/cicTextualParser.mly | 74 ++++++++++++++----- 1 file changed, 54 insertions(+), 20 deletions(-) diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 844384f62..42869a299 100644 --- 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)) } -- 2.39.2