X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=e5bb82786a3b742989a72746aa05f7971491f44c;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=f3ac49e16deb10355e3bdbad14c7f250c3931b33;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f3ac49e16..f0d8ee46c 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -1,479 +1,142 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) open Printf -open MatitaTypes - - -(** create a ProofEngineTypes.mk_fresh_name_type function which uses given - * names as long as they are available, then it fallbacks to name generation - * using FreshNamesGenerator module *) -let namer_of names = - let len = List.length names in - let count = ref 0 in - fun metasenv context name ~typ -> - if !count < len then begin - let name = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - -let tactic_of_ast = function - | TacticAst.Intros (_, _, names) -> - (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Reflexivity _ -> Tactics.reflexivity - | TacticAst.Assumption _ -> Tactics.assumption - | TacticAst.Contradiction _ -> Tactics.contradiction - | TacticAst.Exists _ -> Tactics.exists - | TacticAst.Fourier _ -> Tactics.fourier - | TacticAst.Goal (_, n) -> Tactics.set_goal n - | TacticAst.Left _ -> Tactics.left - | TacticAst.Right _ -> Tactics.right - | TacticAst.Ring _ -> Tactics.ring - | TacticAst.Split _ -> Tactics.split - | TacticAst.Symmetry _ -> Tactics.symmetry - | TacticAst.Transitivity (_, term) -> Tactics.transitivity term - | TacticAst.Apply (_, term) -> Tactics.apply term - | TacticAst.Absurd (_, term) -> Tactics.absurd term - | TacticAst.Exact (_, term) -> Tactics.exact term - | TacticAst.Cut (_, term) -> Tactics.cut term - | TacticAst.Elim (_, term, _) -> - (* TODO Zack implement "using" argument *) - Tactics.elim_intros_simpl term - | TacticAst.ElimType (_, term) -> Tactics.elim_type term - | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what -(* | TacticAst.Auto _ -> Tactics.auto_new ~dbd *) - | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what -(* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Discriminate of 'ident - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option - | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option -*) - | _ -> assert false - -let eval_tactical status tac = - let apply_tactic tactic = - let (proof, goals) = - ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) - in - let new_status = - match goals with - | [] -> - let (_,metasenv,_,_) = proof in - (match metasenv with - | [] -> Proof proof - | (ng,_,_)::_ -> Incomplete_proof (proof,ng)) - | ng::_ -> Incomplete_proof (proof, ng) - in - { status with proof_status = new_status } - in - let rec tactical_of_ast = function - | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic - | TacticAst.Fail loc -> Tacticals.fail - | TacticAst.Do (loc, num, tactical) -> - Tacticals.do_tactic num (tactical_of_ast tactical) - | TacticAst.IdTac loc -> Tacticals.id_tac - | TacticAst.Repeat (loc, tactical) -> - Tacticals.repeat_tactic (tactical_of_ast tactical) - | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - Tacticals.seq (List.map tactical_of_ast tacticals) - | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - Tacticals.thens (tactical_of_ast tactical) - (List.map tactical_of_ast tacticals) - | TacticAst.Tries (loc, tacticals) -> - Tacticals.try_tactics - (List.map (fun t -> "", tactical_of_ast t) tacticals) - | TacticAst.Try (loc, tactical) -> - Tacticals.try_tactic (tactical_of_ast tactical) - in - apply_tactic (tactical_of_ast tac) - -let eval_command status cmd = - match cmd with - | TacticAst.Set (loc, name, value) -> set_option status name value - | TacticAst.Qed loc -> - let uri, metasenv, bo, ty = - match status.proof_status with - | Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | Proof (None, metasenv, body, ty) -> - command_error - ("Someone allows to start a thm without giving the "^ - "name/uri. This should be fixed!") - | _-> command_error "You can't qed an uncomplete theorem" - in - let suri = UriManager.string_of_uri uri in - if metasenv <> [] then - command_error "Proof not completed! metasenv is not empty!"; - let proved_ty,ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph - in - let b,ugraph = - CicReduction.are_convertible [] proved_ty ty ugraph - in - if not b then - command_error - ("The type of your proof is not convertible with the "^ - "type you've declared!"); - MatitaLog.message (sprintf "%s defined" suri); - let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in - {status with proof_status = No_proof } - | TacticAst.Inductive (loc, dummy_params, types) -> - (* dummy_params are not real params, it is a list of nothing, and the only - * semantic content is the len, that is leftno (note: leftno and pamaters - * have nothing in common). - *) - let suri = - match types with - | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind" - | _ -> assert false - in - let uri = UriManager.uri_of_string suri in - let leftno = List.length dummy_params in - let obj = Cic.InductiveDefinition (types, [], leftno, []) in - let ugraph = - CicTypeChecker.typecheck_mutual_inductive_defs uri - (types, [], leftno) CicUniv.empty_ugraph - in - MatitaSync.add_inductive_def - ~uri ~types ~params:[] ~leftno ~ugraph status; - | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> - let uri = - UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") - in - let goalno = 1 in - let metasenv, body = - match status.proof_status with - | Intermediate metasenv -> - ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[]) - | _-> assert false - in - let initial_proof = (Some uri, metasenv, body, ty) in - { status with proof_status = Incomplete_proof (initial_proof,goalno)} - | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) -> - let uri = - UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") - in - let metasenv = MatitaMisc.get_proof_metasenv status in - let (body_type, ugraph) = - CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph - in - let (subst, metasenv, ugraph) = - CicUnification.fo_unif metasenv [] body_type ty ugraph - in - if metasenv <> [] then - command_error - "metasenv not empty while giving a definition with body"; - let body = CicMetaSubst.apply_subst subst body in - let ty = CicMetaSubst.apply_subst subst ty in - MatitaSync.add_constant ~uri ~body ~ty ~ugraph status - | TacticAst.Theorem (_, _, None, _, _) -> - command_error "The grammas should avoid having unnamed theorems!" - | TacticAst.Coercion (loc, term) -> assert false (** TODO *) - | TacticAst.Alias (loc, spec) -> - match spec with - | TacticAst.Ident_alias (id,uri) -> - {status with aliases = - DisambiguateTypes.Environment.add - (DisambiguateTypes.Id id) - ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) - status.aliases } - | TacticAst.Symbol_alias (symb, instance, desc) -> - {status with aliases = - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symb,instance)) - (DisambiguateChoices.lookup_symbol_by_dsc symb desc) - status.aliases } - | TacticAst.Number_alias (instance,desc) -> - {status with aliases = - DisambiguateTypes.Environment.add - (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } - -let eval status st = - match st with - | TacticAst.Tactical (_, tac) -> eval_tactical status tac - | TacticAst.Command (_, cmd) -> eval_command status cmd - | TacticAst.Macro (_, mac) -> - command_error (sprintf "The macro %s can't be in a script" - (TacticAstPp.pp_macro_cic mac)) - -let disambiguate_term status term = - let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) - ~metasenv:(MatitaMisc.get_proof_metasenv status) term - with - | [x] -> x - | _ -> assert false - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof ((uri, _, proof, ty), goal) -> - Incomplete_proof ((uri, metasenv, proof, ty), goal) - | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false - in - let status = - { status with - aliases = aliases; - proof_status = proof_status } - in - status, cic - -let disambiguate_terms status terms = - let term = CicAst.pack terms in - let status, term = disambiguate_term status term in - status, CicUtil.unpack term - -let disambiguate_tactic status = function - | TacticAst.Transitivity (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Transitivity (loc, cic) - | TacticAst.Apply (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Apply (loc, cic) - | TacticAst.Absurd (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Absurd (loc, cic) - | TacticAst.Exact (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Exact (loc, cic) - | TacticAst.Cut (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Cut (loc, cic) - | TacticAst.Elim (loc, term, Some term') -> - let status, cic1 = disambiguate_term status term in - let status, cic2 = disambiguate_term status term' in - status, TacticAst.Elim (loc, cic1, Some cic2) - | TacticAst.Elim (loc, term, None) -> - let status, cic = disambiguate_term status term in - status, TacticAst.Elim (loc, cic, None) - | TacticAst.ElimType (loc, term) -> - let status, cic = disambiguate_term status term in - status, TacticAst.ElimType (loc, cic) - | TacticAst.Replace (loc, what, with_what) -> - let status, cic1 = disambiguate_term status what in - let status, cic2 = disambiguate_term status with_what in - status, TacticAst.Replace (loc, cic1, cic2) - | TacticAst.Change (loc, what, with_what, ident) -> - let status, cic1 = disambiguate_term status what in - let status, cic2 = disambiguate_term status with_what in - status, TacticAst.Change (loc, cic1, cic2, ident) -(* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Discriminate of 'ident - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option - | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option -*) - | TacticAst.Intros (loc, num, names) -> - status, TacticAst.Intros (loc, num, names) - | TacticAst.Auto loc -> status, TacticAst.Auto loc - | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc - | TacticAst.Assumption loc -> status, TacticAst.Assumption loc - | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc - | TacticAst.Exists loc -> status, TacticAst.Exists loc - | TacticAst.Fourier loc -> status, TacticAst.Fourier loc - | TacticAst.Left loc -> status, TacticAst.Left loc - | TacticAst.Right loc -> status, TacticAst.Right loc - | TacticAst.Ring loc -> status, TacticAst.Ring loc - | TacticAst.Split loc -> status, TacticAst.Split loc - | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc - | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) - | x -> - print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x); - assert false - -let rec disambiguate_tactical status = function - | TacticAst.Tactic (loc, tactic) -> - let status, tac = disambiguate_tactic status tactic in - status, TacticAst.Tactic (loc, tac) - | TacticAst.Do (loc, num, tactical) -> - let status, tac = disambiguate_tactical status tactical in - status, TacticAst.Do (loc, num, tac) - | TacticAst.Repeat (loc, tactical) -> - let status, tac = disambiguate_tactical status tactical in - status, TacticAst.Repeat (loc, tac) - | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - let status, tacticals = disambiguate_tacticals status tacticals in - let tacticals = List.rev tacticals in - status, TacticAst.Seq (loc, tacticals) - | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - let status, tactical = disambiguate_tactical status tactical in - let status, tacticals = disambiguate_tacticals status tacticals in - status, TacticAst.Then (loc, tactical, tacticals) - | TacticAst.Tries (loc, tacticals) -> - let status, tacticals = disambiguate_tacticals status tacticals in - status, TacticAst.Tries (loc, tacticals) - | TacticAst.Try (loc, tactical) -> - let status, tactical = disambiguate_tactical status tactical in - status, TacticAst.Try (loc, tactical) - | (TacticAst.IdTac _ | TacticAst.Fail _) as tac -> - status, tac - -and disambiguate_tacticals status tacticals = - let status, tacticals = - List.fold_left - (fun (status, tacticals) tactical -> - let status, tac = disambiguate_tactical status tactical in - status, tac :: tacticals) - (status, []) - tacticals +let debug = false ;; +let debug_print = if debug then prerr_endline else ignore ;; + +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 grafite_status "baseuri") + with + GrafiteTypes.Option_error _ -> None) + !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd + in + lexicon_status_ref := lexicon_status; + GrafiteTypes.set_metasenv metasenv grafite_status,cmd + +let disambiguate_macro lexicon_status_ref grafite_status macro context = + let metasenv,macro = + GrafiteDisambiguate.disambiguate_macro + lexicon_status_ref + (GrafiteTypes.get_proof_metasenv grafite_status) + context macro + in + GrafiteTypes.set_metasenv metasenv grafite_status,macro + +let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + grafite_status ast += + let lexicon_status_ref = ref lexicon_status in + let new_grafite_status,new_objs = + 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 + let new_aliases = + LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in + let _,intermediate_states = + let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in + List.fold_left + (fun (lexicon_status,acc) (k,((v,_) as value)) -> + let b = + try + UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri + with + UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) + in + if b then + lexicon_status,acc + else + let new_lexicon_status = + LexiconEngine.set_proof_aliases lexicon_status [k,value] + in + new_lexicon_status, + ((new_grafite_status,new_lexicon_status),Some (k,value))::acc + ) (lexicon_status,[]) new_aliases + in + ((new_grafite_status,new_lexicon_status),None)::intermediate_states + +let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) + ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb += + let rec loop lexicon_status grafite_status statuses = + let loop = + if first_statement_only then + fun _ _ _ -> raise End_of_file + else + loop in - let tacticals = List.rev tacticals in - status, tacticals - -let disambiguate_inddef status params indTypes = - let add_pi binders t = - List.fold_right - (fun (name, ast) acc -> - CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) - binders t - in - let ind_binders = - List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes - in - let binders = ind_binders @ params in - let asts = ref [] in - let add_ast ast = asts := ast :: !asts in - let paramsno = List.length params in - let indbindersno = List.length ind_binders in - List.iter - (fun (name, _, typ, constructors) -> - add_ast (add_pi params typ); - List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) - indTypes; - let status, terms = disambiguate_terms status !asts in - let terms = ref (List.rev terms) in - let get_term () = - match !terms with [] -> assert false | hd :: tl -> terms := tl; hd - in - let uri = - match indTypes with - | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind" - | _ -> assert false - in - let mutinds = - let counter = ref 0 in - List.map - (fun _ -> - incr counter; - CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter)) - indTypes - in - let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in - let cicIndTypes = - List.fold_left - (fun acc (name, inductive, typ, constructors) -> - let cicTyp = get_term () in - let cicConstructors = - List.fold_left - (fun acc (name, _) -> - let typ = - subst_mutinds (CicUtil.strip_prods indbindersno (get_term ())) - in - (name, typ) :: acc) - [] constructors - in - (name, inductive, cicTyp, List.rev cicConstructors) :: acc) - [] indTypes - in - let cicIndTypes = List.rev cicIndTypes in - status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) - -let disambiguate_command status = function - | TacticAst.Inductive (loc, params, types) -> - let (status, (uri, (ind_types, vars, paramsno))) = - disambiguate_inddef status params types - in - let rec mk_list = function - | 0 -> [] - | n -> ("", Cic.Rel ~-117) :: mk_list (n-1) - in - (* once we've built the cic inductive types we no longer need terms - corresponding to parameters, but we need the leftno, and we encode - it as the length of dummy_params - *) - let dummy_params = mk_list paramsno in - status, TacticAst.Inductive (loc, dummy_params, ind_types) - | TacticAst.Theorem (loc, thm_flavour, name, ty, body) -> - let status, ty = disambiguate_term status ty in - let status, body = - match body with - | None -> status, None - | Some body -> - let status, body = disambiguate_term status body in - status, Some body - in - status, TacticAst.Theorem (loc, thm_flavour, name, ty, body) - | TacticAst.Coercion (loc, term) -> assert false (** TODO *) - | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> - status, cmd - | TacticAst.Alias _ as x -> status, x - -let disambiguate_statement status statement = - match statement with - | TacticAst.Tactical (loc, tac) -> - let status, tac = disambiguate_tactical status tac in - status, (TacticAst.Tactical (loc, tac)) - | TacticAst.Command (loc, cmd) -> - let status, cmd = disambiguate_command status cmd in - status, (TacticAst.Command (loc, cmd)) - | TacticAst.Macro (_, mac) -> - command_error - (sprintf ("The engine is not allowed to disambiguate any macro, "^^ - "in particular %s") (TacticAstPp.pp_macro_ast mac)) - -let eval_ast status ast = - let status,st = disambiguate_statement status ast in - (* this disambiguation step should be deferred to support tacticals *) - eval status st - -let eval_from_stream status str = - let st = CicTextualParser2.parse_statement str in - eval_ast status st - -let eval_string status str = - eval_from_stream status (Stream.of_string str) - -let default_options () = - let options = - StringMap.add "baseuri" - (String - (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner")) - no_options - in - let options = - StringMap.add "basedir" - (String (Helm_registry.get "matita.basedir" )) - options - in - options - -let initial_status = - lazy { - aliases = DisambiguateTypes.empty_environment; - proof_status = No_proof; - options = default_options (); - coercions = []; - objects = []; - } - + if prompt then (print_string "matita> "; flush stdout); + try + let lexicon_status,ast = + GrafiteParser.parse_statement ~include_paths str lexicon_status + in + (match ast with + GrafiteParser.LNone _ -> + loop lexicon_status grafite_status + (((grafite_status,lexicon_status),None)::statuses) + | GrafiteParser.LSome ast -> + cb grafite_status ast; + let new_statuses = + eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + grafite_status ast in + let grafite_status,lexicon_status = + match new_statuses with + [] -> assert false + | (s,_)::_ -> s + in + loop lexicon_status grafite_status (new_statuses @ statuses)) + with + End_of_file -> statuses + in + loop lexicon_status grafite_status [] +;; + +let eval_string ~first_statement_only ~include_paths ?do_heavy_checks + ?clean_baseuri lexicon_status status str += + eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks + ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str) + (fun _ _ -> ())