exception ExplicitNamedSubstitutionAppliedToRel;;
exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
- let uri_of_id_map = Hashtbl.create 53;;
+ (* 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 =
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_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.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 =
- try
- (match Hashtbl.find uri_of_id_map id with
- CicTextualParser0.VarUri uri -> uri
- | _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
- )
- with
- Not_found ->
- match !CicTextualParser0.locate_object id with
- None -> raise (UnknownIdentifier id)
- | Some (CicTextualParser0.VarUri uri as varuri) ->
- Hashtbl.add uri_of_id_map id varuri;
- uri
- | Some _ ->
- raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ let var_uri_of_id id interp =
+ match interp id with
+ None -> raise (UnknownIdentifier id)
+ | Some (CicTextualParser0.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
+ ;;
%}
%token <string> ID
%token <int> META
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%start main
-%type <Cic.term option> main
+%type <((string * CicTextualParser0.uri) -> unit) -> (string list * ((string -> CicTextualParser0.uri option) -> Cic.term)) option> main
%%
main:
- expr { Some $1 }
- | alias { None }
+ expr { function _ -> Some $1 }
+ | alias { function register -> register $1 ; None }
| EOF { raise CicTextualParser0.Eof }
;
expr2:
CONURI exp_named_subst
- { term_of_con_uri $1 $2 }
+ { 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
- { term_of_var_uri $1 $2 }
+ { 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
- { term_of_indty_uri $1 $2 }
+ { 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
- { term_of_indcon_uri $1 $2 }
+ { 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
- if $2 = [] then res else raise (ExplicitNamedSubstitutionAppliedToRel)
+ (match $2 with
+ None -> ([], function _ -> res)
+ | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
+ )
with
Not_found ->
- try
- term_of_uri (Hashtbl.find uri_of_id_map $1) $2
- with
- Not_found ->
- match !CicTextualParser0.locate_object $1 with
- | None -> raise (UnknownIdentifier $1)
- | Some uri ->
- Hashtbl.add uri_of_id_map $1 uri;
- term_of_uri uri $2
+ let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+ let dom = union dom1 [$1] in
+ dom,
+ function interp ->
+ match interp $1 with
+ None -> raise (UnknownIdentifier $1)
+ | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
}
| CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
- { MutCase (fst $5, snd $5, $7, $3, $10) }
+ { 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
- { try
- let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
- raise InductiveTypeURIExpected
- with
- Not_found ->
- match Hashtbl.find uri_of_id_map $5 with
- CicTextualParser0.IndTyUri (uri,typeno) ->
- MutCase (uri, typeno, $7, $3, $10)
- | _ -> raise InductiveTypeURIExpected
+ { 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
+ 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 fixfunsdecls = snd $1 in
- let fixfunsbodies = $3 in
- let idx =
- let rec find idx =
- function
- [] -> raise Not_found
- | (name,_,_)::_ when name = (fst $1) -> idx
- | _::tl -> find (idx+1) tl
- in
- find 0 fixfunsdecls
- in
- let fixfuns =
- List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
- fixfunsdecls fixfunsbodies
- in
- for i = 1 to List.length fixfuns do
- CicTextualParser0.binders := List.tl !CicTextualParser0.binders
- done ;
- Fix (idx,fixfuns)
+ { let dom1,mk_fixheader = $1 in
+ let dom2,mk_exprseplist = $3 in
+ let dom = union dom1 dom2 in
+ dom,
+ function interp ->
+ let fixfunsdecls = snd (mk_fixheader 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
+ | _::tl -> find (idx+1) tl
+ in
+ find 0 fixfunsdecls
+ in
+ let fixfuns =
+ List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
+ fixfunsdecls 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 cofixfunsdecls = (snd $1) in
- let cofixfunsbodies = $3 in
- let idx =
- let rec find idx =
- function
- [] -> raise Not_found
- | (name,_)::_ when name = (fst $1) -> idx
- | _::tl -> find (idx+1) tl
- in
- find 0 cofixfunsdecls
- in
- let cofixfuns =
- List.map2 (fun (name,ty) bo -> (name,ty,bo))
- cofixfunsdecls cofixfunsbodies
- in
- for i = 1 to List.length cofixfuns do
- CicTextualParser0.binders := List.tl !CicTextualParser0.binders
- done ;
- CoFix (idx,cofixfuns)
+ { let dom1,mk_cofixheader = $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 idx =
+ let rec find idx =
+ function
+ [] -> raise Not_found
+ | (name,_)::_ when name = (fst (mk_cofixheader interp)) -> idx
+ | _::tl -> find (idx+1) tl
+ in
+ find 0 cofixfunsdecls
+ in
+ let cofixfuns =
+ List.map2 (fun (name,ty) bo -> (name,ty,bo))
+ cofixfunsdecls cofixfunsbodies
+ in
+ for i = 1 to List.length cofixfuns do
+ CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+ done ;
+ CoFix (idx,cofixfuns)
}
| IMPLICIT
{ let newmeta = new_meta () in
newmeta+1, new_canonical_context, Meta (newmeta,irl);
newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
] @ !CicTextualParser0.metasenv ;
- Meta (newmeta+2,irl)
+ [], function _ -> Meta (newmeta+2,irl)
+ }
+ | 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 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))
}
- | SET { Sort Set }
- | PROP { Sort Prop }
- | TYPE { Sort Type }
- | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
- | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
;
exp_named_subst :
- { [] }
+ { None }
| LCURLY named_substs RCURLY
- { $2 }
+ { Some $2 }
;
named_substs :
VARURI LETIN expr2
- { [$1,$3] }
+ { let dom,mk_expr = $3 in
+ dom, function interp -> [$1, mk_expr interp] }
| ID LETIN expr2
- { [var_uri_of_id $1,$3] }
+ { let dom1,mk_expr = $3 in
+ let dom = union [$1] dom1 in
+ dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
| VARURI LETIN expr2 SEMICOLON named_substs
- { ($1,$3)::$5 }
+ { 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
- { (var_uri_of_id $1,$3)::$5 }
+ { let dom1,mk_expr = $3 in
+ let dom2,mk_named_substs = $5 in
+ let dom = union [$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 ;
- Prod (fst $1, snd $1,$2) }
+ 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 ;
- Lambda (fst $1, snd $1,$2) }
+ 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 ;
- LetIn (fst $1, snd $1,$2) }
+ 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 bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
- CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
- $2,$4
+ { 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)
}
;
fixfunsdecl:
ID LPAREN NUM RPAREN COLON expr
- { [$1,$3,$6] }
+ { let dom,mk_expr = $6 in
+ dom, function interp -> [$1,$3,mk_expr interp]
+ }
| ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
- { ($1,$3,$6)::$8 }
+ { let dom1,mk_expr = $6 in
+ let dom2,mk_fixfunsdecl = $8 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+ }
;
cofixheader:
COFIX ID LCURLY cofixfunsdecl RCURLY
- { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
- CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
- $2,$4
+ { 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)
}
;
cofixfunsdecl:
ID COLON expr
- { [$1,$3] }
+ { let dom,mk_expr = $3 in
+ dom, function interp -> [$1,(mk_expr interp)]
+ }
| ID COLON expr SEMICOLON cofixfunsdecl
- { ($1,$3)::$5 }
+ { let dom1,mk_expr = $3 in
+ let dom2,mk_cofixfunsdecl = $5 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+ }
;
pihead:
PROD ID COLON expr DOT
{ CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
- (Cic.Name $2, $4) }
+ let dom,mk_expr = $4 in
+ Cic.Name $2, (dom, function interp -> mk_expr interp)
+ }
| expr2 ARROW
{ CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
- (Anonymous, $1) }
+ let dom,mk_expr = $1 in
+ Anonymous, (dom, function interp -> mk_expr interp)
+ }
| LPAREN expr RPAREN ARROW
{ CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
- (Anonymous, $2) }
+ let dom,mk_expr = $2 in
+ Anonymous, (dom, function interp -> mk_expr interp)
+ }
;
lambdahead:
LAMBDA ID COLON expr DOT
{ CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
- (Cic.Name $2, $4) }
+ let dom,mk_expr = $4 in
+ Cic.Name $2, (dom, function interp -> mk_expr interp)
+ }
;
letinhead:
LAMBDA ID LETIN expr DOT
{ CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
- (Cic.Name $2, $4) }
+ let dom,mk_expr = $4 in
+ Cic.Name $2, (dom, function interp -> mk_expr interp)
+ }
;
branches:
- { [] }
- | expr SEMICOLON branches { $1::$3 }
- | expr { [$1] }
+ { [], 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:
- { [] }
- | expr exprlist { $1::$2 }
+
+ { [], function _ -> [] }
+ | expr exprlist
+ { let dom1,mk_expr = $1 in
+ let dom2,mk_exprlist = $2 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+ }
;
exprseplist:
- expr { [$1] }
- | expr SEMICOLON exprseplist { $1::$3 }
+ 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:
- { [] }
- | expr SEMICOLON substitutionlist { (Some $1)::$3 }
- | NONE SEMICOLON substitutionlist { None::$3 }
+ { [], 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)
+ }
;
alias:
ALIAS ID CONURI
- { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.ConUri $3) }
+ { $2,(CicTextualParser0.ConUri $3) }
| ALIAS ID VARURI
- { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.VarUri $3) }
+ { $2,(CicTextualParser0.VarUri $3) }
| ALIAS ID INDTYURI
- { Hashtbl.add uri_of_id_map $2
- (CicTextualParser0.IndTyUri (fst $3, snd $3))
- }
+ { $2,(CicTextualParser0.IndTyUri (fst $3, snd $3)) }
| ALIAS ID INDCONURI
{ let uri,indno,consno = $3 in
- Hashtbl.add uri_of_id_map $2
- (CicTextualParser0.IndConUri (uri, indno, consno))
+ $2,(CicTextualParser0.IndConUri (uri, indno, consno))
}
projects / helm.git / commitdiff