From 93703370bfac25b4d342278388f54cc5e27cd531 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jan 2006 17:20:59 +0000 Subject: [PATCH] 1. Macros are now handled using an execption that is caught by matitacLib (raising an error) or matitaScript. As a result matitaScript is now simpler. 2. svn:ignore property refined for several directories in ocaml --- helm/matita/matitaEngine.ml | 33 ++- helm/matita/matitaScript.ml | 215 +++++++----------- helm/matita/matitacLib.ml | 19 +- helm/ocaml/grafite_engine/grafiteEngine.ml | 31 ++- helm/ocaml/grafite_engine/grafiteEngine.mli | 8 + .../grafite_parser/grafiteDisambiguate.ml | 28 ++- .../grafite_parser/grafiteDisambiguate.mli | 7 + 7 files changed, 184 insertions(+), 157 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index bd240032c..f5527bec9 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -28,28 +28,38 @@ open Printf let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -let disambiguate_command lexicon_status_ref status cmd = +let disambiguate_tactic lexicon_status_ref grafite_status goal tac = + let metasenv,tac = + GrafiteDisambiguate.disambiguate_tactic + lexicon_status_ref + (GrafiteTypes.get_proof_context grafite_status goal) + (GrafiteTypes.get_proof_metasenv grafite_status) + tac + in + GrafiteTypes.set_metasenv metasenv grafite_status,tac + +let disambiguate_command lexicon_status_ref grafite_status cmd = let lexicon_status,metasenv,cmd = GrafiteDisambiguate.disambiguate_command ~baseuri:( try - Some (GrafiteTypes.get_string_option status "baseuri") + Some (GrafiteTypes.get_string_option grafite_status "baseuri") with GrafiteTypes.Option_error _ -> None) - !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd + !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd in lexicon_status_ref := lexicon_status; - GrafiteTypes.set_metasenv metasenv status,cmd + GrafiteTypes.set_metasenv metasenv grafite_status,cmd -let disambiguate_tactic lexicon_status_ref status goal tac = - let metasenv,tac = - GrafiteDisambiguate.disambiguate_tactic +let disambiguate_macro lexicon_status_ref grafite_status macro goal = + let metasenv,macro = + GrafiteDisambiguate.disambiguate_macro lexicon_status_ref - (GrafiteTypes.get_proof_context status goal) - (GrafiteTypes.get_proof_metasenv status) - tac + (GrafiteTypes.get_proof_metasenv grafite_status) + (GrafiteTypes.get_proof_context grafite_status goal) + macro in - GrafiteTypes.set_metasenv metasenv status,tac + GrafiteTypes.set_metasenv metasenv grafite_status,macro let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status ast @@ -59,6 +69,7 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status GrafiteEngine.eval_ast ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref) ~disambiguate_command:(disambiguate_command lexicon_status_ref) + ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) ?do_heavy_checks ?clean_baseuri grafite_status ast in let new_lexicon_status = LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index e4b1544f9..183846ef6 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -208,24 +208,11 @@ let eval_with_engine | Some d -> handle_with_devel d ;; -let disambiguate_macro_term term lexicon_status grafite_status user_goal = - let module MD = GrafiteDisambiguator in - let dbd = LibraryDb.instance () in - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = GrafiteTypes.get_proof_context grafite_status user_goal in - let interps = - MD.disambiguate_term ~dbd ~context ~metasenv - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in - match interps with - | [_,_,x,_], _ -> x - | _ -> assert false - let pp_eager_statement_ast = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) -let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = +let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = LibraryDb in @@ -239,72 +226,67 @@ let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text pa match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> - let term = - disambiguate_macro_term term lexicon_status grafite_status user_goal in - let l = Whelp.match_term ~dbd term in - let query_url = - MatitaMisc.strip_suffix ~suffix:"." - (HExtlib.trim_blanks unparsed_text) - in - let entry = `Whelp (query_url, l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + let l = Whelp.match_term ~dbd term in + let query_url = + MatitaMisc.strip_suffix ~suffix:"." + (HExtlib.trim_blanks unparsed_text) + in + let entry = `Whelp (query_url, l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], parsed_text_length | TA.WInstance (loc, term) -> - let term = - disambiguate_macro_term term lexicon_status grafite_status user_goal in - let l = Whelp.instance ~dbd term in - let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + let l = Whelp.instance ~dbd term in + let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], parsed_text_length | TA.WLocate (loc, s) -> - let l = Whelp.locate ~dbd s in - let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + let l = Whelp.locate ~dbd s in + let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], parsed_text_length | TA.WElim (loc, term) -> - let term = - disambiguate_macro_term term lexicon_status grafite_status user_goal in - let uri = - match term with - | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None - | _ -> failwith "Not a MutInd" - in - let l = Whelp.elim ~dbd uri in - let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + let uri = + match term with + | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None + | _ -> failwith "Not a MutInd" + in + let l = Whelp.elim ~dbd uri in + let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], parsed_text_length | TA.WHint (loc, term) -> - let term = - disambiguate_macro_term term lexicon_status grafite_status user_goal in - let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in - let l = List.map fst (MQ.experimental_hint ~dbd s) in - let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in - guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length + let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in + let l = List.map fst (MQ.experimental_hint ~dbd s) in + let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], parsed_text_length (* REAL macro *) | TA.Hint loc -> let proof = GrafiteTypes.get_current_proof grafite_status in - let proof_status = proof, user_goal in + let proof_status = proof,user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in (match selected with | [] -> [], parsed_text_length | [uri] -> let suri = UriManager.string_of_uri uri in - let ast = + let ast loc = TA.Executable (loc, (TA.Tactical (loc, TA.Tactic (loc, TA.Apply (loc, CicNotationPt.Uri (suri, None))), - Some (TA.Dot loc)))) + Some (TA.Dot loc)))) in + let text = + comment parsed_text ^ "\n" ^ + pp_eager_statement_ast (ast HExtlib.dummy_floc) in + let text_len = String.length text in + let loc = HExtlib.floc_of_loc (0,text_len) in + let statement = `Ast (GrafiteParser.LSome (ast loc),text) in + let res,_parsed_text_len = + eval_statement buffer guistuff lexicon_status grafite_status + user_goal script statement in -(* - let new_lexicon_status,new_grafite_status = - MatitaEngine.eval_ast lexicon_status grafite_status ast in - let extra_text = - comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in - [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ], - parsed_text_length -*) assert false (* implementarla con una ricorsione *) + (* we need to replace all the parsed_text *) + res,String.length parsed_text | _ -> HLog.error "The result of the urichooser should be only 1 uri, not:\n"; @@ -315,81 +297,52 @@ let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text pa | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in let context = GrafiteTypes.get_proof_context grafite_status user_goal in - let interps = - GrafiteDisambiguator.disambiguate_term ~dbd ~context ~metasenv - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in - let _, metasenv , term, ugraph = - match interps with - | [x], _ -> x - | _ -> assert false - in - let ty,_ = CTC.type_of_aux' metasenv context term ugraph in + let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], parsed_text_length -(* | TA.Abort _ -> - let rec go_back () = - let grafite_status = script#grafite_status.proof_status in - match status with - | No_proof -> () - | _ -> script#retract ();go_back() - in - [], parsed_text_length, Some go_back - | TA.Redo (_, Some i) -> [], parsed_text_length, - Some (fun () -> for j = 1 to i do advance () done) - | TA.Redo (_, None) -> [], parsed_text_length, - Some (fun () -> advance ()) - | TA.Undo (_, Some i) -> [], parsed_text_length, - Some (fun () -> for j = 1 to i do script#retract () done) - | TA.Undo (_, None) -> [], parsed_text_length, - Some (fun () -> script#retract ()) *) (* TODO *) | TA.Quit _ -> failwith "not implemented" | TA.Print (_,kind) -> failwith "not implemented" | TA.Search_pat (_, search_kind, str) -> failwith "not implemented" | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script ex +and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex = - let module TAPp = GrafiteAstPp in - let module MD = GrafiteDisambiguator in - let module ML = MatitaMisc in - match ex with - TA.Tactical (loc, _, _) -> - eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text - (TA.Executable (loc, ex)) - | TA.Command (loc, cmd) -> - (try - begin - match cmd with - | TA.Set (loc',"baseuri",u) -> - if not (GrafiteMisc.is_empty u) then - (match - guistuff.ask_confirmation - ~title:"Baseuri redefinition" - ~message:( - "Baseuri " ^ u ^ " already exists.\n" ^ - "Do you want to redefine the corresponding "^ - "part of the library?") - with - | `YES -> - let basedir = Helm_registry.get "matita.basedir" in - LibraryClean.clean_baseuris ~basedir [u] - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel) - | _ -> () - end; - eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text - (TA.Executable (loc, ex)) - with MatitaTypes.Cancel -> [], 0) - | TA.Macro (_,mac) -> - eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text - parsed_text script mac - -let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status + let module TAPp = GrafiteAstPp in + let module MD = GrafiteDisambiguator in + let module ML = MatitaMisc in + try + begin + match ex with + | TA.Command (_,TA.Set (_,"baseuri",u)) -> + if not (GrafiteMisc.is_empty u) then + (match + guistuff.ask_confirmation + ~title:"Baseuri redefinition" + ~message:( + "Baseuri " ^ u ^ " already exists.\n" ^ + "Do you want to redefine the corresponding "^ + "part of the library?") + with + | `YES -> + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir [u] + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel) + | _ -> () + end; + eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text + (TA.Executable (loc, ex)) + with + MatitaTypes.Cancel -> [], 0 + | GrafiteEngine.Macro (_loc,lazy_macro) -> + let grafite_status,macro = lazy_macro user_goal in + eval_macro buffer guistuff lexicon_status grafite_status user_goal + unparsed_text parsed_text script macro + +and eval_statement (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal script statement = let (lexicon_status,st), unparsed_text = @@ -433,9 +386,9 @@ let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status (statuses,parsed_text ^ text)::tl,parsed_text_length + len | [] -> [], 0) | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let parsed_text, parsed_text_length = text_of_loc loc in - eval_executable guistuff lexicon_status grafite_status user_goal - unparsed_text parsed_text script ex + let parsed_text, parsed_text_length = text_of_loc loc in + eval_executable buffer guistuff lexicon_status grafite_status user_goal + unparsed_text parsed_text script loc ex let fresh_script_id = let i = ref 0 in diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 7150c6f77..eeac8d6c9 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -117,15 +117,20 @@ let rec interactive_loop () = "matita.includes")) with | GrafiteEngine.Drop -> pp_ocaml_mode () + | GrafiteEngine.Macro (floc,_) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error + (sprintf "A macro has been found in a script at %d-%d" x y); + interactive_loop () | Sys.Break -> HLog.error "user break!"; interactive_loop () | GrafiteTypes.Command_error _ -> interactive_loop () | End_of_file -> print_newline (); clean_exit (Some 0) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let (x, y) = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err); - interactive_loop () + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); + interactive_loop () | exn -> HLog.error (Printexc.to_string exn); interactive_loop () let go () = @@ -234,6 +239,14 @@ let main ~mode = clean_exit (Some 1) else pp_ocaml_mode () + | GrafiteEngine.Macro (floc,_) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error + (sprintf "A macro has been found in a script at %d-%d" x y); + if mode = `COMPILER then + clean_exit (Some 1) + else + pp_ocaml_mode () | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let (x, y) = HExtlib.loc_of_floc floc in HLog.error (sprintf "Parse error at %d-%d: %s" x y err); diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml index c820986b3..a035a68e1 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -25,6 +25,9 @@ exception Drop exception IncludedFileNotCompiled of string (* file name *) +(* the integer is expected to be the goal the user is currently seeing *) +exception Macro of + GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) type options = { do_heavy_checks: bool ; @@ -330,6 +333,11 @@ type eval_ast = 'obj GrafiteAst.command -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + disambiguate_macro: + (GrafiteTypes.status -> + 'term GrafiteAst.macro -> + int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + ?do_heavy_checks:bool -> ?clean_baseuri:bool -> GrafiteTypes.status -> @@ -361,6 +369,11 @@ type 'a eval_executable = 'obj GrafiteAst.command -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + disambiguate_macro: + (GrafiteTypes.status -> + 'term GrafiteAst.macro -> + int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + options -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> @@ -648,7 +661,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris | _ -> status,uris -} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex -> +} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status ex -> match ex with | GrafiteAst.Tactical (_, tac, None) -> eval_tactical ~disambiguate_tactic status tac,[] @@ -657,12 +670,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> eval_tactical ~disambiguate_tactic status punct,[] | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status cmd - | GrafiteAst.Macro (_, mac) -> -(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO - raise (Command_error - (Printf.sprintf "The macro %s can't be in a script" - (GrafiteAstPp.pp_macro_ast mac))) -*) assert false + | GrafiteAst.Macro (loc, macro) -> + raise (Macro (loc,disambiguate_macro status macro)) } and eval_from_moo = {efm_go = fun status fname -> let ast_of_cmd cmd = @@ -678,13 +687,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> eval_ast.ea_go ~disambiguate_tactic:(fun status _ tactic -> status,tactic) ~disambiguate_command:(fun status cmd -> status,cmd) + ~disambiguate_macro:(fun _ _ -> assert false) status ast in assert (lemmas=[]); status) status moo -} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status - st +} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status st -> let opts = { do_heavy_checks = do_heavy_checks ; @@ -692,8 +701,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~disambiguate_tactic - ~disambiguate_command opts status ex + eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command + ~disambiguate_macro opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c,[] } diff --git a/helm/ocaml/grafite_engine/grafiteEngine.mli b/helm/ocaml/grafite_engine/grafiteEngine.mli index 4043e8072..a87bb5a95 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.mli +++ b/helm/ocaml/grafite_engine/grafiteEngine.mli @@ -25,6 +25,9 @@ exception Drop exception IncludedFileNotCompiled of string +(* the integer is expected to be the goal the user is currently seeing *) +exception Macro of + GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) val eval_ast : disambiguate_tactic: @@ -39,6 +42,11 @@ val eval_ast : 'obj GrafiteAst.command -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + disambiguate_macro: + (GrafiteTypes.status -> + 'term GrafiteAst.macro -> + int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + ?do_heavy_checks:bool -> ?clean_baseuri:bool -> GrafiteTypes.status -> diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml index da7294478..4be748460 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -246,7 +246,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv obj = lexicon_status, metasenv, cic let disambiguate_command lexicon_status ~baseuri metasenv = - function + function | GrafiteAst.Coercion _ | GrafiteAst.Default _ | GrafiteAst.Drop _ @@ -258,3 +258,29 @@ let disambiguate_command lexicon_status ~baseuri metasenv = let lexicon_status,metasenv,obj = disambiguate_obj lexicon_status ~baseuri metasenv obj in lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + +let disambiguate_macro lexicon_status_ref metasenv context macro = + let disambiguate_term = disambiguate_term lexicon_status_ref in + match macro with + | GrafiteAst.WMatch (loc,term) -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.WMatch (loc,term) + | GrafiteAst.WInstance (loc,term) -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.WInstance (loc,term) + | GrafiteAst.WElim (loc,term) -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.WElim (loc,term) + | GrafiteAst.WHint (loc,term) -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.WHint (loc,term) + | GrafiteAst.Check (loc,term) -> + let metasenv,term = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Check (loc,term) + | GrafiteAst.Hint _ + | GrafiteAst.WLocate _ as macro -> + metasenv,macro + | GrafiteAst.Quit _ + | GrafiteAst.Print _ + | GrafiteAst.Search_pat _ + | GrafiteAst.Search_term _ -> assert false diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli index 9944825e6..b04aa3cde 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli @@ -39,3 +39,10 @@ val disambiguate_command: Cic.metasenv -> CicNotationPt.obj GrafiteAst.command -> LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command + +val disambiguate_macro: + LexiconEngine.status ref -> + Cic.metasenv -> + Cic.context -> + CicNotationPt.term GrafiteAst.macro -> + Cic.metasenv * Cic.term GrafiteAst.macro -- 2.39.2