X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=24872ffd0c408ceffdb163eb58499baa125946c8;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=aff9144cc0cef8124fa492a9f7ea74ca7a7e4b64;hpb=2d1cecb1593f5d4f4f1bb697f983ac8db99c2987;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index aff9144cc..24872ffd0 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -27,12 +27,17 @@ open Printf open MatitaTypes exception Drop;; -exception UnableToInclude of string;; +exception UnableToInclude of string +exception IncludedFileNotCompiled of string let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -type options = { do_heavy_checks: bool ; include_paths: string list } +type options = { + do_heavy_checks: bool ; + include_paths: string list ; + clean_baseuri: bool +} type statement = (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement @@ -55,8 +60,9 @@ let tactic_of_ast = function | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width) -> - AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () + | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *) + AutoTactic.auto_tac ?depth ?width ?paramodulation + ~dbd:(MatitaDb.instance ()) () | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id @@ -68,7 +74,15 @@ let tactic_of_ast = function let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | GrafiteAst.DecideEquality _ -> Tactics.decide_equality - | GrafiteAst.Decompose (_,term) -> Tactics.decompose term + | GrafiteAst.Decompose (_, types, what, names) -> + let to_type = function + | GrafiteAst.Type (uri, typeno) -> uri, typeno + | GrafiteAst.Ident _ -> assert false + in + let user_types = List.rev_map to_type types in + let dbd = MatitaDb.instance () in + let mk_fresh_name_callback = namer_of names in + Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term | GrafiteAst.Elim (_, what, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what @@ -83,6 +97,7 @@ let tactic_of_ast = function | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] | `Reduce -> ProofEngineReduction.reduce | `Simpl -> ProofEngineReduction.simpl + | `Unfold what -> ProofEngineReduction.unfold ?what | `Whd -> CicReduction.whd ~delta:false ~subst:[] in Tactics.fold ~reduction ~term ~pattern @@ -111,6 +126,7 @@ let tactic_of_ast = function | `Normalize -> Tactics.normalize ~pattern | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern + | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity | GrafiteAst.Replace (_, pattern, with_what) -> @@ -157,6 +173,16 @@ let disambiguate_pattern status (wanted, hyp_paths, goal_path) = status, Some wanted in status, (wanted, hyp_paths ,goal_path) + +let disambiguate_reduction_kind status = function + | `Unfold (Some t) -> + let status, t = disambiguate_term status t in + status, `Unfold (Some t) + | `Normalize + | `Reduce + | `Simpl + | `Unfold None + | `Whd as kind -> status, kind let disambiguate_tactic status = function | GrafiteAst.Apply (loc, term) -> @@ -166,7 +192,7 @@ let disambiguate_tactic status = function let status, cic = disambiguate_term status term in status, GrafiteAst.Absurd (loc, cic) | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width) + | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *) | GrafiteAst.Change (loc, pattern, with_what) -> let status, with_what = disambiguate_term status with_what in let status, pattern = disambiguate_pattern status pattern in @@ -185,9 +211,18 @@ let disambiguate_tactic status = function status, GrafiteAst.Cut (loc, ident, cic) | GrafiteAst.DecideEquality loc -> status, GrafiteAst.DecideEquality loc - | GrafiteAst.Decompose (loc,term) -> - let status,term = disambiguate_term status term in - status, GrafiteAst.Decompose(loc,term) + | GrafiteAst.Decompose (loc, types, what, names) -> + let disambiguate (status, types) = function + | GrafiteAst.Type _ -> assert false + | GrafiteAst.Ident id -> + match disambiguate_term status (CicNotationPt.Ident (id, None)) with + | status, Cic.MutInd (uri, tyno, _) -> + status, (GrafiteAst.Type (uri, tyno) :: types) + | _ -> + raise Disambiguate.NoWellTypedInterpretation + in + let status, types = List.fold_left disambiguate (status, []) types in + status, GrafiteAst.Decompose(loc, types, what, names) | GrafiteAst.Discriminate (loc,term) -> let status,term = disambiguate_term status term in status, GrafiteAst.Discriminate(loc,term) @@ -210,10 +245,11 @@ let disambiguate_tactic status = function status, GrafiteAst.ElimType (loc, what, None, depth, idents) | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,reduction_kind, term, pattern) -> + | GrafiteAst.Fold (loc,red_kind, term, pattern) -> let status, pattern = disambiguate_pattern status pattern in let status, term = disambiguate_term status term in - status, GrafiteAst.Fold (loc,reduction_kind, term, pattern) + let status, red_kind = disambiguate_reduction_kind status red_kind in + status, GrafiteAst.Fold (loc,red_kind, term, pattern) | GrafiteAst.FwdSimpl (loc, hyp, names) -> status, GrafiteAst.FwdSimpl (loc, hyp, names) | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc @@ -239,9 +275,10 @@ let disambiguate_tactic status = function | GrafiteAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in status, GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, reduction_kind, pattern) -> + | GrafiteAst.Reduce (loc, red_kind, pattern) -> let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Reduce(loc, reduction_kind, pattern) + let status, red_kind = disambiguate_reduction_kind status red_kind in + status, GrafiteAst.Reduce(loc, red_kind, pattern) | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc | GrafiteAst.Replace (loc, pattern, with_what) -> let status, pattern = disambiguate_pattern status pattern in @@ -480,21 +517,20 @@ let disambiguate_command status = function let status,obj = disambiguate_obj status obj in status, GrafiteAst.Obj (loc,obj) -let try_open_in paths path = - let rec aux = function - | [] -> open_in path - | p :: tl -> - try - open_in (p ^ "/" ^ path) - with Sys_error _ -> aux tl - in - try - aux paths - with Sys_error _ as exc -> - MatitaLog.error ("Unable to read " ^ path); - MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); - MatitaLog.error ("current working directory is " ^ Unix.getcwd ()); - raise exc +let make_absolute paths path = + if path = "coq.ma" then path + else + let rec aux = function + | [] -> ignore (Unix.stat path); path + | p :: tl -> + let path = p ^ "/" ^ path in + try + ignore (Unix.stat path); path + with Unix.Unix_error _ -> aux tl + in + try + aux paths + with Unix.Unix_error _ as exc -> raise (UnableToInclude path) ;; let eval_command opts status cmd = @@ -509,14 +545,15 @@ let eval_command opts status cmd = {status with moo_content_rev = (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} | GrafiteAst.Include (loc, path) -> - let path = MatitaMisc.obj_file_of_script path in - let stream = - try - Stream.of_channel (try_open_in opts.include_paths path) - with Sys_error _ -> raise (UnableToInclude path) - in + let absolute_path = make_absolute opts.include_paths path in + let moopath = MatitaMisc.obj_file_of_script absolute_path in + let ic = + try open_in moopath with Sys_error _ -> + raise (IncludedFileNotCompiled moopath) in + let stream = Stream.of_channel ic in let status = ref status in !eval_from_stream_ref status stream (fun _ _ -> ()); + close_in ic; !status | GrafiteAst.Set (loc, name, value) -> let value = @@ -529,6 +566,15 @@ let eval_command opts status cmd = else value in + if not (MatitaMisc.is_empty value) then + begin + MatitaLog.warn ("baseuri " ^ value ^ " is not empty"); + if opts.clean_baseuri then + begin + MatitaLog.message ("cleaning baseuri " ^ value); + MatitacleanLib.clean_baseuris [value] + end + end; set_option status name value | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Qed loc -> @@ -597,6 +643,12 @@ let eval_command opts status cmd = begin let dbd = MatitaDb.instance () in let similar = MetadataQuery.match_term ~dbd ty in + let similar_len = List.length similar in + if similar_len> 30 then + (MatitaLog.message + ("Duplicate check will compare your theorem with " ^ + string_of_int similar_len ^ + " theorems, this may take a while.")); let convertible = List.filter ( fun u -> @@ -654,39 +706,47 @@ let eval_executable opts status ex = let eval_comment status c = status -let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st = - let opts = - {do_heavy_checks = do_heavy_checks ; include_paths = include_paths} +let eval_ast + ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st += + let opts = { + do_heavy_checks = do_heavy_checks ; + include_paths = include_paths; + clean_baseuri = clean_baseuri } in match st with | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c -let eval_from_stream ?do_heavy_checks ?include_paths status str cb = +let eval_from_stream + ?do_heavy_checks ?include_paths ?clean_baseuri status str cb += try while true do let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths !status ast + status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done with End_of_file -> () (* to avoid a long list of recursive functions *) let _ = eval_from_stream_ref := eval_from_stream -let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb = +let eval_from_stream_greedy + ?do_heavy_checks ?include_paths ?clean_baseuri status str cb += while true do print_string "matita> "; flush stdout; let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths !status ast + status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done ;; -let eval_string ?do_heavy_checks ?include_paths status str = +let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = eval_from_stream - ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->()) + ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->()) let default_options () = (*