From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 09:54:44 +0000 (+0000) Subject: New CicTextualParser: it now returns (approximately) a couple X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71b08b1ea99893b3c5e2d91fc26e1ab7330fd33d;p=helm.git New CicTextualParser: it now returns (approximately) a couple list of free names * function from an interpretation to a Cic term where an interpretation is a function from string (ids) to uris. --- diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index fc8bd12ba..dcb77c701 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -33,7 +33,16 @@ 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 = @@ -75,6 +84,12 @@ 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) ;; @@ -93,30 +108,29 @@ 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 ID %token META @@ -130,94 +144,122 @@ %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF %right ARROW %start main -%type 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 @@ -230,119 +272,222 @@ expr2: 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)) } diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index a0738ad7e..62bf7f23c 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -32,10 +32,5 @@ type uri = | IndConUri of UriManager.uri * int * int ;; -let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");; let binders = ref ([] : (Cic.name option) list);; let metasenv = ref ([] : Cic.metasenv);; -let locate_object = ref ((fun _ -> None):string->uri option);; - -let set_locate_object f = - locate_object := f diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml index bdf701d80..c51346e1a 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml @@ -23,14 +23,18 @@ * http://cs.unibo.it/helm/. *) -let main ~current_uri ~context ~metasenv lexer lexbuf = +let main ~context ~metasenv lexer lexbuf ~register_aliases = (* Warning: higly non-reentrant code!!! *) - CicTextualParser0.current_uri := current_uri ; CicTextualParser0.binders := context ; CicTextualParser0.metasenv := metasenv ; - match CicTextualParser.main lexer lexbuf with + match CicTextualParser.main lexer lexbuf register_aliases with None -> None - | Some res -> - CicTextualParser0.binders := [] ; - Some (!CicTextualParser0.metasenv,res) + | Some (dom,mk_term) -> + Some + (dom, + function interp -> + let term = mk_term interp in + let metasenv = !CicTextualParser0.metasenv in + metasenv,term + ) ;; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli index 837628b21..23ad4af11 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli @@ -24,6 +24,10 @@ *) val main : - current_uri:(UriManager.uri) -> context:((Cic.name option) list) -> - metasenv:Cic.metasenv -> (Lexing.lexbuf -> CicTextualParser.token) -> - Lexing.lexbuf -> (Cic.metasenv * Cic.term) option + context:((Cic.name option) list) -> + metasenv:Cic.metasenv -> + (Lexing.lexbuf -> CicTextualParser.token) -> Lexing.lexbuf -> + register_aliases:((string * CicTextualParser0.uri) -> unit) -> + (string list * + ((string -> CicTextualParser0.uri option) -> (Cic.metasenv * Cic.term)) + ) option