*)
open Printf
+
open MatitaTypes
exception Drop;;
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
let singleton = function
- | [x] -> x
+ | [x], _ -> x
| _ -> assert false
let disambiguate_term status_ref term =
cic, metasenv, ugraph)
let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
- let interp path =
- Disambiguate.interpretate_path [] !status_ref.aliases path
- in
+ let interp path = Disambiguate.interpretate_path [] path in
let goal_path = interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
let wanted =
let set_goals (status,_) goals = status,goals
let id_tac status =
- apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+ apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status
let mk_tactic tac = tac
List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
status new_coercions in
let statement_of name =
- GrafiteAstPp.pp_statement
- (GrafiteAst.Executable (Disambiguate.dummy_floc,
- (GrafiteAst.Command (Disambiguate.dummy_floc,
- (GrafiteAst.Coercion (Disambiguate.dummy_floc,
- (CicNotationPt.Ident (name, None)))))))) ^ "\n"
+ GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
+ (CicNotationPt.Ident (name, None)))
in
- let moo_content_rev =
- [statement_of (UriManager.name_of_uri coer_uri)] @
+ let moo_content =
+ statement_of (UriManager.name_of_uri coer_uri) ::
(List.map
(fun (uri, _, _) ->
statement_of (UriManager.name_of_uri uri))
- new_coercions) @ status.moo_content_rev
+ new_coercions)
in
- let status = {status with moo_content_rev = moo_content_rev} in
- {status with proof_status = No_proof}
+ let status = add_moo_content moo_content status in
+ { status with proof_status = No_proof }
let generate_elimination_principles uri status =
let elim sort status =
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
let (aliases, metasenv, cic, _) =
- match
- MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
- ~aliases:(status.aliases) ~uri obj
- with
- | [x] -> x
- | _ -> assert false
+ singleton
+ (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+ ~aliases:(status.aliases) ~uri obj)
in
let proof_status =
match status.proof_status with
match cmd with
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
- {status with moo_content_rev =
- (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+ add_moo_content [cmd] status
| GrafiteAst.Include (loc, path) ->
let absolute_path = make_absolute opts.include_paths path in
let moopath = MatitaMisc.obj_file_of_script absolute_path in
set_option status name value
| GrafiteAst.Drop loc -> raise Drop
| GrafiteAst.Qed loc ->
- let uri, metasenv, bo, ty =
+ let uri, metasenv, bo, ty =
match status.proof_status with
| Proof (Some uri, metasenv, body, ty) ->
uri, metasenv, body, ty
code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Id id)
(uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
status.aliases
| GrafiteAst.Symbol_alias (symb, instance, desc) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Symbol (symb,instance))
(DisambiguateChoices.lookup_symbol_by_dsc symb desc)
status.aliases
| GrafiteAst.Number_alias (instance,desc) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Num instance)
(DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
in
MatitaSync.set_proof_aliases status aliases
| GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
| GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *)
- | GrafiteAst.Interpretation _
- | GrafiteAst.Notation _ as stm ->
- { status with moo_content_rev =
- (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+ | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
+ let status' = add_moo_content [stm] status in
+ let aliases' =
+ DisambiguateTypes.Environment.cons
+ (DisambiguateTypes.Symbol (symbol, 0))
+ (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
+ status.aliases
+ in
+ MatitaSync.set_proof_aliases status' aliases'
+ | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with