-(* Copyright (C) 2005, HELM Team.
+(*
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
| `Unfold (Some t) ->
let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
`Unfold (Some t)
- | `Demodulate
| `Normalize
| `Reduce
| `Simpl
metasenv,GrafiteAst.ApplyS (loc, cic)
| GrafiteAst.Assumption loc ->
metasenv,GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
- metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+ | GrafiteAst.Auto (loc,params) ->
+ metasenv,GrafiteAst.Auto (loc,params)
| GrafiteAst.Change (loc, pattern, with_what) ->
let with_what = disambiguate_lazy_term with_what in
let pattern = disambiguate_pattern pattern in
List.fold_left disambiguate (metasenv,[]) types
in
metasenv,GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Demodulate loc ->
+ metasenv,GrafiteAst.Demodulate loc
| GrafiteAst.Discriminate (loc,term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Discriminate(loc,term)
| GrafiteAst.Inversion (loc, term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Inversion (loc, term)
- | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
let f term to_what =
let metasenv,term = disambiguate_term context metasenv term in
term :: to_what
in
let to_what = List.fold_right f to_what [] in
let metasenv,what = disambiguate_term context metasenv what in
- metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
| GrafiteAst.Left loc ->
metasenv,GrafiteAst.Left loc
| GrafiteAst.LetIn (loc, term, name) ->
| GrafiteAst.Transitivity (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Transitivity (loc, cic)
+ (* Nuovi casi *)
+ | GrafiteAst.Assume (loc, id, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Assume (loc, id, cic)
+ | GrafiteAst.Suppose (loc, term, id, term') ->
+ 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
+ metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
+ | GrafiteAst.Bydone (loc,term) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ |Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.Bydone (loc, cic)
+ | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
+ 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
+ metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
+ | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
+ 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 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
+ metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,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
+ metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
+ | GrafiteAst.Byinduction (loc, term, id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Byinduction(loc, cic, id)
+ | GrafiteAst.Thesisbecomes (loc, term) ->
+ 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' = disambiguate_term context metasenv term1 in
+ let metasenv,cic''= disambiguate_term context metasenv 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'= disambiguate_term context metasenv term1 in
+ let metasenv,cic''= disambiguate_term context metasenv term2 in
+ metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')
+ | GrafiteAst.Case (loc, id, params) ->
+ let metasenv,params' =
+ List.fold_right
+ (fun (id,term) (metasenv,params) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,(id,cic)::params
+ ) params (metasenv,[])
+ in
+ metasenv,GrafiteAst.Case(loc, id, params')
+ | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
+ let metasenv,cic =
+ match term1 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 term2 in
+ let metasenv,cic'' =
+ match term3 with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
+
let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
let uri =
| GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
+ | GrafiteAst.Print _
| GrafiteAst.Include _
| GrafiteAst.Qed _
| GrafiteAst.Set _ as cmd ->
| GrafiteAst.Hint _
| GrafiteAst.WLocate _ as macro ->
metasenv,macro
- | GrafiteAst.Quit _
- | GrafiteAst.Print _
- | GrafiteAst.Search_pat _
- | GrafiteAst.Search_term _ -> assert false