an expression can be disambiguated yelding totally different terms.
Required, for example, to disambiguate operators that have interpretations
with a different arity (as Leibniz equality and the decidable equality over
natural numbers).
let var_uri_of_id id interp =
let module CTP0 = CicTextualParser0 in
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
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
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
None -> raise (UnknownIdentifier id)
| Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
| Some _ -> raise InductiveTypeURIExpected
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%start main
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%start main
-%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
+%type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
%%
main:
| EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
%%
main:
| EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
with
Not_found ->
let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
with
Not_found ->
let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
- let dom = union dom1 [$1] in
+ let dom = union dom1 [CicTextualParser0.Id $1] in
+ 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 ()) ""
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
}
| 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
+ let dom = (union dom1 (union dom2 dom3)) in
dom,
function interp ->
MutCase
dom,
function interp ->
MutCase
{ let dom1,mk_expr1 = $3 in
let dom2,mk_expr2 = $7 in
let dom3,mk_expr3 = $10 in
{ let dom1,mk_expr1 = $3 in
let dom2,mk_expr2 = $7 in
let dom3,mk_expr3 = $10 in
- let dom = union [$5] (union dom1 (union dom2 dom3)) 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
dom,
function interp ->
let uri,typeno = indty_uri_of_id $5 interp in
dom, function interp -> [$1, mk_expr interp] }
| ID LETIN expr2
{ let dom1,mk_expr = $3 in
dom, function interp -> [$1, mk_expr interp] }
| ID LETIN expr2
{ let dom1,mk_expr = $3 in
- let dom = union [$1] dom1 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
dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
| VARURI LETIN expr2 SEMICOLON named_substs
{ let dom1,mk_expr = $3 in
| ID LETIN expr2 SEMICOLON named_substs
{ let dom1,mk_expr = $3 in
let dom2,mk_named_substs = $5 in
| ID LETIN expr2 SEMICOLON named_substs
{ let dom1,mk_expr = $3 in
let dom2,mk_named_substs = $5 in
- let dom = union [$1] (union dom1 dom2) 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)
dom,
function interp ->
(var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
| IndConUri of UriManager.uri * int * int
;;
| IndConUri of UriManager.uri * int * int
;;
+type interpretation_domain_item =
+ Id of string
+ | Symbol of string * (string * (interpretation -> Cic.term)) list
+and interpretation_codomain_item =
+ | Term of (interpretation -> Cic.term)
+and interpretation =
+ interpretation_domain_item -> interpretation_codomain_item option
;;
let binders = ref ([] : (Cic.name option) list);;
;;
let binders = ref ([] : (Cic.name option) list);;
context:((Cic.name option) list) ->
metasenv:Cic.metasenv ->
(Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf ->
context:((Cic.name option) list) ->
metasenv:Cic.metasenv ->
(Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf ->
- string list *
- ((string -> CicTextualParser0.interp_codomain option) ->
- (Cic.metasenv * Cic.term))
+ CicTextualParser0.interpretation_domain_item list *
+ (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term))