;;
let var_uri_of_id id interp =
- match interp id with
- None -> raise (UnknownIdentifier id)
- | Some (CicTextualParser0.VarUri uri) -> uri
- | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ let module CTP0 = CicTextualParser0 in
+ match interp id with
+ None -> raise (UnknownIdentifier id)
+ | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
+ | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
;;
let indty_uri_of_id id interp =
- match interp id with
- None -> raise (UnknownIdentifier id)
- | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
- | Some _ -> raise InductiveTypeURIExpected
+ let module CTP0 = CicTextualParser0 in
+ match interp 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 LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%start main
-%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
+%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
%%
main:
expr EOF { $1 }
function interp ->
match interp $1 with
None -> raise (UnknownIdentifier $1)
- | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
+ | 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 ()) ""
}
| CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
{ let dom1,mk_expr1 = $3 in
CoFix (idx,fixfuns)
}
| 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)
- }
+ { mk_implicit () }
| SET { [], function _ -> Sort Set }
| PROP { [], function _ -> Sort Prop }
| TYPE { [], function _ -> Sort Type }