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 ;;
| `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) ->
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
status, GrafiteAst.Obj (loc,obj)
let make_absolute paths path =
- 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 ->
- command_error ("File " ^ path ^ " not found")
+ 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 =
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 (UnableToInclude moopath) in
+ 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 _ _ -> ());