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
| 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) ->
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 ->
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
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Thesisbecomes (loc, cic)
| GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
- let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
let metasenv,cic' = disambiguate_term context metasenv term1 in
- let metasenv,cic''= disambiguate_term context metasenv term2 in
+ let cic''= disambiguate_lazy_term term2 in
metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
| GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
let metasenv,cic = disambiguate_term context metasenv term in
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)
let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
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 _