* http://helm.cs.unibo.it/
*)
-open GrafiteTypes
+exception BaseUriNotSetYet
let singleton = function
| [x], _ -> x
| _ -> assert false
(** @param term not meaningful when context is given *)
-let disambiguate_term ?context status_ref goal term =
- let status = !status_ref in
- let context =
- match context with
- | Some c -> c
- | None -> GrafiteTypes.get_proof_context status goal
- in
+let disambiguate_term lexicon_status_ref context metasenv term =
+ let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term)
+ (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv term)
in
- let status = GrafiteTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status diff in
- status_ref := status;
- cic
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
+ metasenv,cic
(** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
* rationale: lazy_term will be invoked in different context to obtain a term,
* each invocation will disambiguate the term and can add aliases. Once all
* disambiguations have been performed, the first returned function can be
* used to obtain the resulting aliases *)
-let disambiguate_lazy_term status_ref term =
+let disambiguate_lazy_term lexicon_status_ref term =
(fun context metasenv ugraph ->
- let status = !status_ref in
+ let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, cic, ugraph) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
- ~initial_ugraph:ugraph ~aliases:status.aliases
- ~universe:(Some status.multi_aliases) ~context ~metasenv term)
- in
- let status = GrafiteTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status diff in
- status_ref := status;
+ (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv
+ term) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
cic, metasenv, ugraph)
-let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
+let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) =
let interp path = Disambiguate.interpretate_path [] path in
let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
match wanted with
None -> None
| Some wanted ->
- let wanted = disambiguate_lazy_term status_ref wanted in
+ let wanted = disambiguate_lazy_term lexicon_status_ref wanted in
Some wanted
in
(wanted, hyp_paths, goal_path)
-let disambiguate_reduction_kind aliases_ref = function
+let disambiguate_reduction_kind lexicon_status_ref = function
| `Unfold (Some t) ->
- let t = disambiguate_lazy_term aliases_ref t in
+ let t = disambiguate_lazy_term lexicon_status_ref t in
`Unfold (Some t)
| `Normalize
| `Reduce
| `Unfold None
| `Whd as kind -> kind
-let disambiguate_tactic status goal tactic =
- let status_ref = ref status in
- let tactic =
- match tactic with
+let disambiguate_tactic lexicon_status_ref context metasenv tactic =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+ let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in
+ let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in
+ let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in
+ match tactic with
| GrafiteAst.Absurd (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Absurd (loc, cic)
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Absurd (loc, cic)
| GrafiteAst.Apply (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.Assumption loc ->
+ metasenv,GrafiteAst.Assumption loc
| GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
- GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+ metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
| GrafiteAst.Change (loc, pattern, with_what) ->
- let with_what = disambiguate_lazy_term status_ref with_what in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+ let with_what = disambiguate_lazy_term with_what in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Change (loc, pattern, with_what)
+ | GrafiteAst.Clear (loc,id) ->
+ metasenv,GrafiteAst.Clear (loc,id)
+ | GrafiteAst.ClearBody (loc,id) ->
+ metasenv,GrafiteAst.ClearBody (loc,id)
| GrafiteAst.Compare (loc,term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Compare (loc,term)
- | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Compare (loc,term)
+ | GrafiteAst.Constructor (loc,n) ->
+ metasenv,GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc ->
+ metasenv,GrafiteAst.Contradiction loc
| GrafiteAst.Cut (loc, ident, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.DecideEquality loc ->
+ metasenv,GrafiteAst.DecideEquality loc
| GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate types = function
+ let disambiguate (metasenv,types) = function
| GrafiteAst.Type _ -> assert false
| GrafiteAst.Ident id ->
- (match disambiguate_term status_ref goal
- (CicNotationPt.Ident (id, None))
- with
- | Cic.MutInd (uri, tyno, _) ->
- (GrafiteAst.Type (uri, tyno) :: types)
- | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
+ (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
- let types = List.fold_left disambiguate [] types in
- GrafiteAst.Decompose (loc, types, what, names)
+ metasenv,GrafiteAst.Decompose (loc, types, what, names)
| GrafiteAst.Discriminate (loc,term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Discriminate(loc,term)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Discriminate(loc,term)
| GrafiteAst.Exact (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Exact (loc, cic)
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Exact (loc, cic)
| GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv,using = disambiguate_term context metasenv using in
+ metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
| GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.Elim (loc, what, None, depth, idents)
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
| GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv,using = disambiguate_term context metasenv using in
+ metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
| GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.ElimType (loc, what, None, depth, idents)
- | GrafiteAst.Exists loc -> GrafiteAst.Exists loc
- | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | GrafiteAst.Exists loc ->
+ metasenv,GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc ->
+ metasenv,GrafiteAst.Fail loc
| GrafiteAst.Fold (loc,red_kind, term, pattern) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let term = disambiguate_lazy_term status_ref term in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- GrafiteAst.Fold (loc, red_kind, term, pattern)
+ let pattern = disambiguate_pattern pattern in
+ let term = disambiguate_lazy_term term in
+ let red_kind = disambiguate_reduction_kind red_kind in
+ metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
| GrafiteAst.FwdSimpl (loc, hyp, names) ->
- GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+ metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc ->
+ metasenv,GrafiteAst.Fourier loc
| GrafiteAst.Generalize (loc,pattern,ident) ->
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
- | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Generalize (loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) ->
+ metasenv,GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc ->
+ metasenv,GrafiteAst.IdTac loc
| GrafiteAst.Injection (loc, term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Injection (loc,term)
- | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) ->
+ metasenv,GrafiteAst.Intros (loc, num, names)
| GrafiteAst.Inversion (loc, term) ->
- let term = disambiguate_term status_ref goal term in
- 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) ->
let f term to_what =
- let term = disambiguate_term status_ref goal term in
+ let metasenv,term = disambiguate_term context metasenv term in
term :: to_what
in
let to_what = List.fold_right f to_what [] in
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.LApply (loc, depth, to_what, what, ident)
- | GrafiteAst.Left loc -> GrafiteAst.Left loc
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc ->
+ metasenv,GrafiteAst.Left loc
| GrafiteAst.LetIn (loc, term, name) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.LetIn (loc,term,name)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.LetIn (loc,term,name)
| GrafiteAst.Reduce (loc, red_kind, pattern) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- GrafiteAst.Reduce(loc, red_kind, pattern)
- | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+ let pattern = disambiguate_pattern pattern in
+ let red_kind = disambiguate_reduction_kind red_kind in
+ metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
+ | GrafiteAst.Reflexivity loc ->
+ metasenv,GrafiteAst.Reflexivity loc
| GrafiteAst.Replace (loc, pattern, with_what) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let with_what = disambiguate_lazy_term status_ref with_what in
- GrafiteAst.Replace (loc, pattern, with_what)
+ 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) ->
- let term = disambiguate_term status_ref goal t in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+ let metasenv,term = disambiguate_term context metasenv t in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | GrafiteAst.Right loc ->
+ metasenv,GrafiteAst.Right loc
+ | GrafiteAst.Ring loc ->
+ metasenv,GrafiteAst.Ring loc
+ | GrafiteAst.Split loc ->
+ metasenv,GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc ->
+ metasenv,GrafiteAst.Symmetry loc
| GrafiteAst.Transitivity (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Transitivity (loc, cic)
- in
- status_ref, tactic
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Transitivity (loc, cic)
-let disambiguate_obj status obj =
+let disambiguate_obj lexicon_status ~baseuri metasenv obj =
let uri =
match obj with
| CicNotationPt.Inductive (_,(name,_,_,_)::_)
| CicNotationPt.Record (_,name,_,_) ->
- Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind"))
+ (match baseuri with
+ | Some baseuri ->
+ Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
+ | None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
- in
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof _
- | Proof _ ->
- raise (GrafiteTypes.Command_error "imbricated proofs not allowed")
- | Intermediate _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status diff in
- status, cic
+ (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri obj) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status, metasenv, cic
-let disambiguate_command status =
+let disambiguate_command lexicon_status ~baseuri metasenv =
function
- | GrafiteAst.Alias _
| GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
- | GrafiteAst.Dump _
| GrafiteAst.Include _
- | GrafiteAst.Interpretation _
- | GrafiteAst.Notation _
| GrafiteAst.Qed _
- | GrafiteAst.Render _
| GrafiteAst.Set _ as cmd ->
- status,cmd
+ lexicon_status,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->
- let status,obj = disambiguate_obj status obj in
- status, GrafiteAst.Obj (loc,obj)
-
+ let lexicon_status,metasenv,obj =
+ disambiguate_obj lexicon_status ~baseuri metasenv obj in
+ lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
projects / helm.git / blobdiff