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
| 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
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
| `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
| `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) ->
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) ->
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
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)
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
| 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
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 =
{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 =
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 ->
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 ->
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 () =
(*
projects / helm.git / blobdiff