X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=0c64bbb0794ece3e80c68de116ce640dfbfde413;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=6df39bfc40e497a8623b1f2dd09eca1b69643305;hpb=ccd1ec9a248921b2c81817b1a7f6f0a2f27d5c32;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 6df39bfc4..0c64bbb07 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -123,13 +123,16 @@ let disambiguate_tactic | GrafiteAst.Apply (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Apply (loc, cic) - | GrafiteAst.ApplyS (loc, term) -> + | GrafiteAst.ApplyS (loc, term, params) -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.ApplyS (loc, cic) + metasenv,GrafiteAst.ApplyS (loc, cic, params) | GrafiteAst.Assumption loc -> metasenv,GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,params) -> metasenv,GrafiteAst.Auto (loc,params) + | GrafiteAst.Cases (loc, what, idents) -> + let metasenv,what = disambiguate_term context metasenv what in + metasenv,GrafiteAst.Cases (loc, what, idents) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term with_what in let pattern = disambiguate_pattern pattern in @@ -145,24 +148,8 @@ let disambiguate_tactic | GrafiteAst.Cut (loc, ident, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate (metasenv,types) = function - | GrafiteAst.Type _ -> assert false - | GrafiteAst.Ident id -> - (match - disambiguate_term context metasenv - (CicNotationPt.Ident(id, None)) - with - | metasenv,Cic.MutInd (uri, tyno, _) -> - metasenv,(GrafiteAst.Type (uri, tyno) :: types) - | _ -> - raise (GrafiteDisambiguator.DisambiguationError - (0,[[None,lazy "Decompose works only on inductive types"]]))) - in - let metasenv,types = - List.fold_left disambiguate (metasenv,[]) types - in - metasenv,GrafiteAst.Decompose (loc, types, what, names) + | GrafiteAst.Decompose (loc, names) -> + metasenv,GrafiteAst.Decompose (loc, names) | GrafiteAst.Demodulate loc -> metasenv,GrafiteAst.Demodulate loc | GrafiteAst.Destruct (loc,term) -> @@ -233,10 +220,10 @@ let disambiguate_tactic let pattern = disambiguate_pattern pattern in let with_what = disambiguate_lazy_term with_what in metasenv,GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern) -> + | GrafiteAst.Rewrite (loc, dir, t, pattern, names) -> let metasenv,term = disambiguate_term context metasenv t in let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern) + metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names) | GrafiteAst.Right loc -> metasenv,GrafiteAst.Right loc | GrafiteAst.Ring loc -> @@ -295,6 +282,10 @@ let disambiguate_tactic let metasenv,t = disambiguate_term context metasenv t in metasenv,Some t in metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'') + | GrafiteAst.We_proceed_by_cases_on (loc, term, term') -> + let metasenv,cic = disambiguate_term context metasenv term in + let metasenv,cic' = disambiguate_term context metasenv term' in + metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic') | GrafiteAst.We_proceed_by_induction_on (loc, term, term') -> let metasenv,cic = disambiguate_term context metasenv term in let metasenv,cic' = disambiguate_term context metasenv term' in @@ -328,16 +319,16 @@ let disambiguate_tactic let metasenv,cic = match term1 with None -> metasenv,None - | Some t -> + | Some (start,t) -> let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + metasenv,Some (start,t) in let metasenv,cic'= disambiguate_term context metasenv term2 in let metasenv,cic'' = match term3 with - None -> metasenv,None - | Some t -> + `Auto _ as t -> metasenv,t + | `Term t -> let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + metasenv,`Term t in metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) @@ -362,19 +353,50 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = lexicon_status, metasenv, cic let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)= - match cmd with - | GrafiteAst.Coercion _ - | GrafiteAst.Default _ - | GrafiteAst.Drop _ - | GrafiteAst.Print _ - | GrafiteAst.Include _ - | GrafiteAst.Qed _ - | GrafiteAst.Set _ as cmd -> - lexicon_status,metasenv,cmd - | GrafiteAst.Obj (loc,obj) -> - let lexicon_status,metasenv,obj = - disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in - lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + match cmd with + | GrafiteAst.Index(loc,key,uri) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = + disambiguate_term text prefix_len lexicon_status_ref [] in + let disambiguate_term_option metasenv = + function + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term metasenv t in + metasenv, Some t + in + let metasenv,key = disambiguate_term_option metasenv key in + !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri) + | GrafiteAst.Coercion _ + | GrafiteAst.Default _ + | GrafiteAst.Drop _ + | GrafiteAst.Include _ + | GrafiteAst.Print _ + | GrafiteAst.Qed _ + | GrafiteAst.Set _ as cmd -> + lexicon_status,metasenv,cmd + | GrafiteAst.Obj (loc,obj) -> + let lexicon_status,metasenv,obj = + disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in + lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = + disambiguate_term text prefix_len lexicon_status_ref [] in + let disambiguate_term_option metasenv = + function + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term metasenv t in + metasenv, Some t + in + let metasenv,a = disambiguate_term metasenv a in + let metasenv,aeq = disambiguate_term metasenv aeq in + let metasenv,refl = disambiguate_term_option metasenv refl in + let metasenv,sym = disambiguate_term_option metasenv sym in + let metasenv,trans = disambiguate_term_option metasenv trans in + !lexicon_status_ref, metasenv, + GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) let disambiguate_macro lexicon_status_ref metasenv context (text,prefix_len, macro) @@ -397,5 +419,6 @@ let disambiguate_macro let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Check (loc,term) | GrafiteAst.Hint _ - | GrafiteAst.WLocate _ as macro -> + | GrafiteAst.WLocate _ + | GrafiteAst.Inline _ as macro -> metasenv,macro