X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=af67f1c1454a8a367ef033b3034e1275b4be7aa0;hb=85ccebb566c36671ca753debe09e6dd5c9dd0df7;hp=42869a2991ee617fc221c29e77a7d3c057697e38;hpb=f58a80f4ad1aaf26eecb7a8fb7ebef436fb0967a;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 42869a299..af67f1c14 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -1,23 +1,82 @@ +/* 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 binders = ref [];; - let get_index_in_list e = 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 ;; + + let get_cookingno uri = + UriManager.relative_depth !CicTextualParser0.current_uri uri 0 + ;; + + (* Returns the first meta whose number is above the *) + (* number of the higher meta. *) + (*CSC: cut&pasted from proofEngine.ml *) + let new_meta () = + let rec aux = + function + None,[] -> 1 + | Some n,[] -> n + | None,(n,_,_)::tl -> aux (Some n,tl) + | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + in + 1 + aux (None,!CicTextualParser0.metasenv) + ;; + + (* identity_relocation_list_for_metavariable i canonical_context *) + (* returns the identity relocation list, which is the list [1 ; ... ; n] *) + (* where n = List.length [canonical_context] *) + (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) + (*CSC: cut&pasted from proofEngine.ml *) + let identity_relocation_list_for_metavariable canonical_context = + let canonical_context_length = List.length canonical_context in + let rec aux = + function + (_,[]) -> [] + | (n,None::tl) -> None::(aux ((n+1),tl)) + | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) + in + aux (1,canonical_context) + ;; + %} %token ID %token META @@ -26,8 +85,9 @@ %token INDTYURI %token INDCONURI %token ALIAS -%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT -%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE 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 main %% @@ -36,35 +96,49 @@ main: | alias { None } | EOF { raise CicTextualParser0.Eof } ; -expr: +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" -> Const ($1,0) + "con" -> + let cookingno = get_cookingno $1 in + Const ($1,cookingno) | "var" -> Var $1 | _ -> raise (InvalidSuffix suff) } - | INDTYURI { MutInd (fst $1, 0, snd $1) } + | INDTYURI + { let cookingno = get_cookingno (fst $1) in + MutInd (fst $1, cookingno, snd $1) } | INDCONURI - { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) } + { 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) !binders) + Rel (get_index_in_list (Name $1) !CicTextualParser0.binders) with Not_found -> - Hashtbl.find uri_of_id_map $1 + try + Hashtbl.find uri_of_id_map $1 + with + Not_found -> + match ! CicTextualParser0.locate_object $1 with + | None -> raise (UnknownIdentifier $1) + | Some term -> Hashtbl.add uri_of_id_map $1 term; term } | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY - { MutCase (fst $5, 0, snd $5, $7, $3, $10) } + { 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) !binders in + 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,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10) + MutInd (uri,cookingno,typeno) -> + MutCase (uri, cookingno, typeno, $7, $3, $10) | _ -> raise InductiveTypeURIExpected } | fixheader LCURLY exprseplist RCURLY @@ -84,7 +158,7 @@ expr: fixfunsdecls fixfunsbodies in for i = 1 to List.length fixfuns do - binders := List.tl !binders + CicTextualParser0.binders := List.tl !CicTextualParser0.binders done ; Fix (idx,fixfuns) } @@ -105,28 +179,47 @@ expr: cofixfunsdecls cofixfunsbodies in for i = 1 to List.length cofixfuns do - binders := List.tl !binders + CicTextualParser0.binders := List.tl !CicTextualParser0.binders done ; CoFix (idx,cofixfuns) } - | IMPLICIT { Implicit } + | IMPLICIT + { let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + CicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl); + newmeta+2, new_canonical_context, Meta (newmeta+1,irl) + ] @ !CicTextualParser0.metasenv ; + Meta (newmeta+2,irl) + } | SET { Sort Set } | 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) } - | pihead expr - { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) } - | lambdahead expr - { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) } - | letinhead expr - { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) } +; +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,_,_) -> Name name) $4 in - binders := bs@(!binders) ; + { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in + CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } ; @@ -138,8 +231,8 @@ fixfunsdecl: ; cofixheader: COFIX ID LCURLY cofixfunsdecl RCURLY - { let bs = List.rev_map (function (name,_) -> Name name) $4 in - binders := bs@(!binders) ; + { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in + CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ; $2,$4 } ; @@ -150,16 +243,25 @@ cofixfunsdecl: { ($1,$3)::$5 } ; pihead: - PROD ID COLON expr DOT - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + 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 - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; + (Cic.Name $2, $4) } ; letinhead: LAMBDA ID LETIN expr DOT - { binders := (Name $2)::!binders ; (Cic.Name $2, $4) } + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; + (Cic.Name $2, $4) } ; branches: { [] } @@ -174,12 +276,24 @@ exprseplist: expr { [$1] } | expr SEMICOLON exprseplist { $1::$3 } ; +substitutionlist: + { [] } + | expr SEMICOLON substitutionlist { (Some $1)::$3 } + | NONE SEMICOLON substitutionlist { None::$3 } +; alias: ALIAS ID CONURI - { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) } + { let cookingno = get_cookingno $3 in + Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) } | ALIAS ID INDTYURI - { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) } + { 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 - Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno)) + let cookingno = get_cookingno uri in + Hashtbl.add uri_of_id_map $2 + (Cic.MutConstruct (uri, cookingno, indno ,consno)) } + + +