;;
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 <UriManager.uri> VARURI
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> 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 <((string * CicTextualParser0.uri) -> unit) -> (string list * ((string -> CicTextualParser0.uri option) -> Cic.term)) option> main
+%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
%%
main:
- expr { function _ -> Some $1 }
- | alias { function register -> register $1 ; None }
- | EOF { raise CicTextualParser0.Eof }
+ | 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
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
(mk_expr3 interp))
}
| fixheader LCURLY exprseplist RCURLY
- { let dom1,mk_fixheader = $1 in
+ { 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 fixfunsdecls = snd (mk_fixheader interp) in
+ 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 = (fst (mk_fixheader interp)) -> idx
+ | (name,_)::_ when name = foo -> idx
| _::tl -> find (idx+1) tl
in
- find 0 fixfunsdecls
+ find 0 ids_and_indexes
in
let fixfuns =
- List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
- fixfunsdecls fixfunsbodies
+ List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
+ (List.combine ids_and_indexes types) 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 dom1,mk_cofixheader = $1 in
+ { let dom1,foo,ids,mk_types = $1 in
let dom2,mk_exprseplist = $3 in
let dom = union dom1 dom2 in
dom,
function interp ->
- let cofixfunsdecls = (snd (mk_cofixheader interp)) in
- let cofixfunsbodies = mk_exprseplist interp in
+ 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 = (fst (mk_cofixheader interp)) -> idx
+ | name::_ when name = foo -> idx
| _::tl -> find (idx+1) tl
in
- find 0 cofixfunsdecls
+ find 0 ids
in
- let cofixfuns =
+ let fixfuns =
List.map2 (fun (name,ty) bo -> (name,ty,bo))
- cofixfunsdecls cofixfunsbodies
+ (List.combine ids types) fixfunsbodies
in
- for i = 1 to List.length cofixfuns do
+ for i = 1 to List.length fixfuns do
CicTextualParser0.binders := List.tl !CicTextualParser0.binders
done ;
- CoFix (idx,cofixfuns)
+ 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 }
{ let dom,mk_substitutionlist = $3 in
dom, function interp -> Meta ($1, mk_substitutionlist interp)
}
- | LPAREN expr expr exprlist RPAREN
- { let dom1,mk_expr1 = $2 in
- let dom2,mk_expr2 = $3 in
- let dom3,mk_exprlist = $4 in
- let dom = union dom1 (union dom2 dom3) in
- dom,
- function interp ->
- Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist 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 :
;
fixheader:
FIX ID LCURLY fixfunsdecl RCURLY
- { let dom,mk_fixfunsdecl = $4 in
- dom,
- function interp ->
- let bs =
- List.rev_map
- (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
- in
- CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
- $2,(mk_fixfunsdecl interp)
+ { 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, function interp -> [$1,$3,mk_expr interp]
+ dom, [$1,$3], function interp -> [mk_expr interp]
}
| ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
{ let dom1,mk_expr = $6 in
- let dom2,mk_fixfunsdecl = $8 in
+ let dom2,ids_and_indexes,mk_types = $8 in
let dom = union dom1 dom2 in
- dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+ dom, ($1,$3)::ids_and_indexes,
+ function interp -> (mk_expr interp)::(mk_types interp)
}
;
cofixheader:
COFIX ID LCURLY cofixfunsdecl RCURLY
- { let dom,mk_cofixfunsdecl = $4 in
- dom,
- function interp ->
- let bs =
- List.rev_map
- (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
- in
- CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
- $2,(mk_cofixfunsdecl interp)
+ { 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, function interp -> [$1,(mk_expr interp)]
+ dom, [$1], function interp -> [mk_expr interp]
}
| ID COLON expr SEMICOLON cofixfunsdecl
{ let dom1,mk_expr = $3 in
- let dom2,mk_cofixfunsdecl = $5 in
+ let dom2,ids,mk_types = $5 in
let dom = union dom1 dom2 in
- dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+ dom, $1::ids,
+ function interp -> (mk_expr interp)::(mk_types interp)
}
;
pihead:
let dom,mk_expr = $1 in
Anonymous, (dom, function interp -> mk_expr interp)
}
- | LPAREN expr RPAREN ARROW
- { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
- let dom,mk_expr = $2 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 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
;
exprlist:
- { [], function _ -> [] }
+ { 0, [], function _ -> [] }
| expr exprlist
{ let dom1,mk_expr = $1 in
- let dom2,mk_exprlist = $2 in
+ let length,dom2,mk_exprlist = $2 in
let dom = union dom1 dom2 in
- dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+ length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
}
;
exprseplist:
{ let dom,mk_exprsubstitutionlist = $3 in
dom, function interp -> None::(mk_exprsubstitutionlist interp)
}
-;
-alias:
- ALIAS ID CONURI
- { $2,(CicTextualParser0.ConUri $3) }
- | ALIAS ID VARURI
- { $2,(CicTextualParser0.VarUri $3) }
- | ALIAS ID INDTYURI
- { $2,(CicTextualParser0.IndTyUri (fst $3, snd $3)) }
- | ALIAS ID INDCONURI
- { let uri,indno,consno = $3 in
- $2,(CicTextualParser0.IndConUri (uri, indno, consno))
- }
projects / helm.git / blobdiff