+++ /dev/null
-/* 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;;
- exception ExplicitNamedSubstitutionAppliedToRel;;
- exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
-
- (* merge removing duplicates of two lists free of duplicates *)
- let union dom1 dom2 =
- let rec filter =
- function
- [] -> []
- | he::tl ->
- if List.mem he dom1 then filter tl else he::(filter tl)
- in
- dom1 @ (filter dom2)
- ;;
-
- 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
- ;;
-
- (* 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)
- ;;
-
- let deoptionize_exp_named_subst =
- function
- None -> [], (function _ -> [])
- | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
- ;;
-
- let term_of_con_uri uri exp_named_subst =
- Const (uri,exp_named_subst)
- ;;
-
- let term_of_var_uri uri exp_named_subst =
- Var (uri,exp_named_subst)
- ;;
-
- let term_of_indty_uri (uri,tyno) exp_named_subst =
- MutInd (uri, tyno, exp_named_subst)
- ;;
-
- let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
- MutConstruct (uri, tyno, consno, exp_named_subst)
- ;;
-
- let term_of_uri uri =
- match uri with
- CicTextualParser0.ConUri uri ->
- term_of_con_uri uri
- | CicTextualParser0.VarUri uri ->
- term_of_var_uri uri
- | CicTextualParser0.IndTyUri (uri,tyno) ->
- term_of_indty_uri (uri,tyno)
- | CicTextualParser0.IndConUri (uri,tyno,consno) ->
- term_of_indcon_uri (uri,tyno,consno)
- ;;
-
- let var_uri_of_id id interp =
- let module CTP0 = CicTextualParser0 in
- match interp (CicTextualParser0.Id id) with
- None -> raise (UnknownIdentifier id)
- | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
- | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
- ;;
-
- let indty_uri_of_id id interp =
- let module CTP0 = CicTextualParser0 in
- match interp (CicTextualParser0.Id id) with
- None -> raise (UnknownIdentifier id)
- | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
- | Some _ -> raise InductiveTypeURIExpected
- ;;
-
- let mk_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 ;
- [], function _ -> Meta (newmeta+2,irl)
- ;;
-%}
-%token <string> ID
-%token <int> META
-%token <int> NUM
-%token <UriManager.uri> CONURI
-%token <UriManager.uri> VARURI
-%token <UriManager.uri * int> INDTYURI
-%token <UriManager.uri * int * int> INDCONURI
-%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 <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
-%%
-main:
- | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
- | expr EOF { $1 }
- | expr SEMICOLON { $1 } /* FG: to read several terms in a row
- * Do we need to clear some static variables?
- */
-;
-expr2:
- CONURI exp_named_subst
- { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
- }
- | VARURI exp_named_subst
- { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
- }
- | INDTYURI exp_named_subst
- { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
- }
- | INDCONURI exp_named_subst
- { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
- }
- | ID exp_named_subst
- { try
- let res =
- Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
- in
- (match $2 with
- None -> ([], function _ -> res)
- | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
- )
- with
- Not_found ->
- let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- let dom = union dom1 [CicTextualParser0.Id $1] in
- dom,
- function interp ->
- match interp (CicTextualParser0.Id $1) with
- None -> raise (UnknownIdentifier $1)
- | Some (CicTextualParser0.Uri uri) ->
- term_of_uri uri (mk_exp_named_subst interp)
- | Some CicTextualParser0.Implicit ->
- (*CSC: not very clean; to maximize code reusage *)
- snd (mk_implicit ()) ""
- | Some (CicTextualParser0.Term mk_term) ->
- (mk_term interp)
- }
- | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
- { let dom1,mk_expr1 = $3 in
- let dom2,mk_expr2 = $7 in
- let dom3,mk_expr3 = $10 in
- let dom = (union dom1 (union dom2 dom3)) in
- dom,
- function interp ->
- MutCase
- (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
- }
- | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
- { let dom1,mk_expr1 = $3 in
- let dom2,mk_expr2 = $7 in
- let dom3,mk_expr3 = $10 in
- let dom = union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) in
- dom,
- function interp ->
- let uri,typeno = indty_uri_of_id $5 interp in
- MutCase
- (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
- (mk_expr3 interp))
- }
- | fixheader LCURLY exprseplist RCURLY
- { 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 types = mk_types interp in
- let fixfunsbodies = (mk_exprseplist interp) in
- let idx =
- let rec find idx =
- function
- [] -> raise Not_found
- | (name,_)::_ when name = foo -> idx
- | _::tl -> find (idx+1) tl
- in
- find 0 ids_and_indexes
- in
- let fixfuns =
- List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
- (List.combine ids_and_indexes types) fixfunsbodies
- in
- Fix (idx,fixfuns)
- }
- | cofixheader LCURLY exprseplist RCURLY
- { let dom1,foo,ids,mk_types = $1 in
- let dom2,mk_exprseplist = $3 in
- let dom = union dom1 dom2 in
- dom,
- function interp ->
- 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 = foo -> idx
- | _::tl -> find (idx+1) tl
- in
- find 0 ids
- in
- let fixfuns =
- List.map2 (fun (name,ty) bo -> (name,ty,bo))
- (List.combine ids types) fixfunsbodies
- in
- for i = 1 to List.length fixfuns do
- CicTextualParser0.binders := List.tl !CicTextualParser0.binders
- done ;
- CoFix (idx,fixfuns)
- }
- | IMPLICIT
- { mk_implicit () }
- | SET { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
- | LPAREN expr CAST expr RPAREN
- { let dom1,mk_expr1 = $2 in
- let dom2,mk_expr2 = $4 in
- let dom = union dom1 dom2 in
- dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
- }
- | META LBRACKET substitutionlist RBRACKET
- { let dom,mk_substitutionlist = $3 in
- dom, function interp -> Meta ($1, mk_substitutionlist interp)
- }
- | LPAREN expr exprlist RPAREN
- { let length,dom2,mk_exprlist = $3 in
- match length with
- 0 -> $2
- | _ ->
- let dom1,mk_expr1 = $2 in
- let dom = union dom1 dom2 in
- dom,
- function interp ->
- Appl ((mk_expr1 interp)::(mk_exprlist interp))
- }
-;
-exp_named_subst :
- { None }
- | LCURLY named_substs RCURLY
- { Some $2 }
-;
-named_substs :
- VARURI LETIN expr2
- { let dom,mk_expr = $3 in
- dom, function interp -> [$1, mk_expr interp] }
- | ID LETIN expr2
- { let dom1,mk_expr = $3 in
- let dom = union [CicTextualParser0.Id $1] dom1 in
- dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
- | VARURI LETIN expr2 SEMICOLON named_substs
- { let dom1,mk_expr = $3 in
- let dom2,mk_named_substs = $5 in
- let dom = union dom1 dom2 in
- dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
- }
- | ID LETIN expr2 SEMICOLON named_substs
- { let dom1,mk_expr = $3 in
- let dom2,mk_named_substs = $5 in
- let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
- dom,
- function interp ->
- (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
- }
-;
-expr :
- pihead expr
- { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
- let dom1,mk_expr1 = snd $1 in
- let dom2,mk_expr2 = $2 in
- let dom = union dom1 dom2 in
- dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
- }
- | lambdahead expr
- { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
- let dom1,mk_expr1 = snd $1 in
- let dom2,mk_expr2 = $2 in
- let dom = union dom1 dom2 in
- dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
- }
- | letinhead expr
- { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
- let dom1,mk_expr1 = snd $1 in
- let dom2,mk_expr2 = $2 in
- let dom = union dom1 dom2 in
- dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
- }
- | expr2
- { $1 }
-;
-fixheader:
- FIX ID LCURLY fixfunsdecl RCURLY
- { 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, [$1,$3], function interp -> [mk_expr interp]
- }
- | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
- { let dom1,mk_expr = $6 in
- let dom2,ids_and_indexes,mk_types = $8 in
- let dom = union dom1 dom2 in
- dom, ($1,$3)::ids_and_indexes,
- function interp -> (mk_expr interp)::(mk_types interp)
- }
-;
-cofixheader:
- COFIX ID LCURLY cofixfunsdecl RCURLY
- { 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, [$1], function interp -> [mk_expr interp]
- }
- | ID COLON expr SEMICOLON cofixfunsdecl
- { let dom1,mk_expr = $3 in
- let dom2,ids,mk_types = $5 in
- let dom = union dom1 dom2 in
- dom, $1::ids,
- function interp -> (mk_expr interp)::(mk_types interp)
- }
-;
-pihead:
- PROD ID COLON expr DOT
- { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
- let dom,mk_expr = $4 in
- Cic.Name $2, (dom, function interp -> mk_expr interp)
- }
- | expr2 ARROW
- { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
- let dom,mk_expr = $1 in
- Anonymous, (dom, function interp -> mk_expr interp)
- }
- | PROD ID DOT
- { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
- 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)
- ] @ !CicTextualParser0.metasenv ;
- Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
- }
-;
-lambdahead:
- LAMBDA ID COLON expr DOT
- { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
- let dom,mk_expr = $4 in
- Cic.Name $2, (dom, function interp -> mk_expr interp)
- }
- | LAMBDA ID DOT
- { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
- 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)
- ] @ !CicTextualParser0.metasenv ;
- Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
- }
-;
-letinhead:
- LAMBDA ID LETIN expr DOT
- { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
- let dom,mk_expr = $4 in
- Cic.Name $2, (dom, function interp -> mk_expr interp)
- }
-;
-branches:
- { [], function _ -> [] }
- | expr SEMICOLON branches
- { let dom1,mk_expr = $1 in
- let dom2,mk_branches = $3 in
- let dom = union dom1 dom2 in
- dom, function interp -> (mk_expr interp)::(mk_branches interp)
- }
- | expr
- { let dom,mk_expr = $1 in
- dom, function interp -> [mk_expr interp]
- }
-;
-exprlist:
-
- { 0, [], function _ -> [] }
- | expr exprlist
- { let dom1,mk_expr = $1 in
- let length,dom2,mk_exprlist = $2 in
- let dom = union dom1 dom2 in
- length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
- }
-;
-exprseplist:
- expr
- { let dom,mk_expr = $1 in
- dom, function interp -> [mk_expr interp]
- }
- | expr SEMICOLON exprseplist
- { let dom1,mk_expr = $1 in
- let dom2,mk_exprseplist = $3 in
- let dom = union dom1 dom2 in
- dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
- }
-;
-substitutionlist:
- { [], function _ -> [] }
- | expr SEMICOLON substitutionlist
- { let dom1,mk_expr = $1 in
- let dom2,mk_substitutionlist = $3 in
- let dom = union dom1 dom2 in
- dom,
- function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
- }
- | NONE SEMICOLON substitutionlist
- { let dom,mk_exprsubstitutionlist = $3 in
- dom, function interp -> None::(mk_exprsubstitutionlist interp)
- }
projects / helm.git / blobdiff