X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;fp=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=3f6afc79a4685838fd9bb90a3f3990fe98119c5b;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly deleted file mode 100644 index 3f6afc79a..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ /dev/null @@ -1,255 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -%{ - open Cic;; - module U = UriManager;; - - exception InvalidSuffix of string;; - exception InductiveTypeURIExpected;; - exception UnknownIdentifier of string;; - - let uri_of_id_map = Hashtbl.create 53;; - - let get_index_in_list e = - let rec aux i = - function - [] -> raise Not_found - | (Some he)::_ when he = e -> i - | _::tl -> aux (i+1) tl - in - aux 1 -;; - - let get_cookingno uri = - UriManager.relative_depth !CicTextualParser0.current_uri uri 0 - ;; - -%} -%token ID -%token META -%token NUM -%token CONURI -%token INDTYURI -%token INDCONURI -%token ALIAS -%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 main -%% -main: - expr { Some $1 } - | alias { None } - | EOF { raise CicTextualParser0.Eof } -; -expr2: - CONURI - { let uri = UriManager.string_of_uri $1 in - let suff = (String.sub uri (String.length uri - 3) 3) in - match suff with - "con" -> - let cookingno = get_cookingno $1 in - Const ($1,cookingno) - | "var" -> Var $1 - | _ -> raise (InvalidSuffix suff) - } - | INDTYURI - { let cookingno = get_cookingno (fst $1) in - MutInd (fst $1, cookingno, snd $1) } - | INDCONURI - { let (uri,tyno,consno) = $1 in - let cookingno = get_cookingno uri in - MutConstruct (uri, cookingno, tyno, consno) } - | ID - { try - Rel (get_index_in_list (Name $1) !CicTextualParser0.binders) - with - Not_found -> - try - Hashtbl.find uri_of_id_map $1 - with - Not_found -> - raise (UnknownIdentifier $1) - } - | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY - { let cookingno = get_cookingno (fst $5) in - MutCase (fst $5, cookingno, snd $5, $7, $3, $10) } - | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY - { try - let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in - raise InductiveTypeURIExpected - with - Not_found -> - match Hashtbl.find uri_of_id_map $5 with - MutInd (uri,cookingno,typeno) -> - MutCase (uri, cookingno, typeno, $7, $3, $10) - | _ -> raise InductiveTypeURIExpected - } - | 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 = (fst $1) -> idx - | _::tl -> find (idx+1) tl - in - find 0 fixfunsdecls - in - let fixfuns = - List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo)) - fixfunsdecls 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 cofixfunsdecls = (snd $1) in - let cofixfunsbodies = $3 in - let idx = - let rec find idx = - function - [] -> raise Not_found - | (name,_)::_ when name = (fst $1) -> idx - | _::tl -> find (idx+1) tl - in - find 0 cofixfunsdecls - in - let cofixfuns = - List.map2 (fun (name,ty) bo -> (name,ty,bo)) - cofixfunsdecls cofixfunsbodies - in - for i = 1 to List.length cofixfuns do - CicTextualParser0.binders := List.tl !CicTextualParser0.binders - done ; - CoFix (idx,cofixfuns) - } - | IMPLICIT { Implicit } - | SET { Sort Set } - | PROP { Sort Prop } - | TYPE { Sort Type } - | LPAREN expr CAST expr RPAREN { Cast ($2,$4) } - | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } - | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) } -; -expr : - pihead expr - { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; - Prod (fst $1, snd $1,$2) } - | lambdahead expr - { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; - Lambda (fst $1, snd $1,$2) } - | letinhead expr - { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ; - LetIn (fst $1, snd $1,$2) } - | expr2 - { $1 } -; -fixheader: - FIX ID LCURLY fixfunsdecl RCURLY - { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in - CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; - $2,$4 - } -; -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,_) -> Some (Name name)) $4 in - CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; - $2,$4 - } -; -cofixfunsdecl: - ID COLON expr - { [$1,$3] } - | ID COLON expr SEMICOLON cofixfunsdecl - { ($1,$3)::$5 } -; -pihead: - PROD ID COLON expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; - (Cic.Name $2, $4) } - | expr2 ARROW - { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; - (Anonimous, $1) } - | LPAREN expr RPAREN ARROW - { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; - (Anonimous, $2) } -; -lambdahead: - LAMBDA ID COLON expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; - (Cic.Name $2, $4) } -; -letinhead: - LAMBDA ID LETIN expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; - (Cic.Name $2, $4) } -; -branches: - { [] } - | expr SEMICOLON branches { $1::$3 } - | expr { [$1] } -; -exprlist: - { [] } - | expr exprlist { $1::$2 } -; -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 - Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) } - | ALIAS ID INDTYURI - { let cookingno = get_cookingno (fst $3) in - Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) } - | ALIAS ID INDCONURI - { let uri,indno,consno = $3 in - let cookingno = get_cookingno uri in - Hashtbl.add uri_of_id_map $2 - (Cic.MutConstruct (uri, cookingno, indno ,consno)) - } - - -