(* Copyright (C) 2004, 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
* 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/
*)
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
-let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) =
- if what = None && hyp = [] && goal = None then "" else
+let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) =
+ if what = None && hyp = [] && goal = None then "" else
let what_text =
match what with
| None -> ""
let pp_just status just =
match just with
- `Term term -> "exact " ^ NotationPp.pp_term status term
- | `Auto params -> pp_auto_params params status
+ `Term term -> "using (" ^ NotationPp.pp_term status term ^ ") "
+ | `Auto params ->
+ match params with
+ | (None,[]) -> ""
+ | params -> "by " ^ pp_auto_params params status ^ " "
;;
let rec pp_ntactic status ~map_unicode_to_tex =
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
- | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^
+ | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
- | NDestruct (_,dom,skip) -> "ndestruct ..."
+ | NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"
| NPosbyname (_, s) -> s ^ ":"
| NWildcard _ -> "*:"
| NMerge _ -> "]"
- | NFocus (_,l) ->
- Printf.sprintf "focus %s"
+ | NFocus (_,l) ->
+ Printf.sprintf "focus %s"
(String.concat " " (List.map string_of_int l))
| NUnfocus _ -> "unfocus"
| NSkip _ -> "skip"
| NTry (_,tac) -> "ntry " ^ pp_ntactic status ~map_unicode_to_tex tac
| NAssumption _ -> "nassumption"
- | NBlock (_,l) ->
+ | NBlock (_,l) ->
"(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
| NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
- | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
- | Suppose (_,term,ident) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")"
- | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ "we proved" ^
- NotationPp.pp_term status term1 ^ (match ident with
+ | Assume (_, ident, term) -> "assume " ^ ident ^ ":(" ^ (NotationPp.pp_term status term) ^ ")"
+ | Suppose (_,term,ident) -> "suppose (" ^ (NotationPp.pp_term status term) ^ ") (" ^ ident ^ ") "
+ | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ " we proved (" ^
+ (NotationPp.pp_term status term1) ^ ")" ^ (match ident with
None -> "" | Some ident -> "(" ^ident^ ")")
- | We_need_to_prove (_,term,ident) -> "we need to prove" ^ NotationPp.pp_term status term ^
+ | We_need_to_prove (_,term,ident) -> "we need to prove (" ^ (NotationPp.pp_term status term) ^ ") " ^
(match ident with None -> "" | Some id -> "(" ^ id ^ ")")
- | BetaRewritingStep (_,t) -> "that is equivalent to" ^ (NotationPp.pp_term status t)
+ | BetaRewritingStep (_,t) -> "that is equivalent to (" ^ (NotationPp.pp_term status t) ^ ")"
| Bydone (_, just) -> pp_just status just ^ "done"
- | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ":"
- ^ NotationPp.pp_term status term ^ "such that" ^ NotationPp.pp_term status term1 ^ "(" ^ ident1 ^ ")"
- | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ "we have " ^
- NotationPp.pp_term status term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ NotationPp.pp_term status term2
- ^ " (" ^ ident2 ^ ")"
- | Thesisbecomes (_, t) -> "the thesis becomes" ^ NotationPp.pp_term status t
- | RewritingStep (_, rhs, just, cont) ->
- "=" ^
- NotationPp.pp_term status rhs ^
- (match just with
- | `Auto params -> pp_auto_params params status
- | `Term t -> " exact " ^ NotationPp.pp_term status t
+ | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": ("
+ ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")"
+ | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^
+ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status
+ term2)
+ ^ ") (" ^ ident2 ^ ")"
+ | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")"
+ | RewritingStep (_, rhs, just, cont) ->
+ "= (" ^
+ (NotationPp.pp_term status rhs) ^ ")" ^
+ (match just with
+ | `Auto params -> let s = pp_auto_params params status in
+ if s <> "" then " by " ^ s
+ else ""
+ | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")"
| `Proof -> " proof"
- | `SolveWith t -> " using " ^ NotationPp.pp_term status t)
+ | `SolveWith t -> " using (" ^ (NotationPp.pp_term status t) ^ ")"
+ )
^ (if cont then " done" else "")
- | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ NotationPp.pp_term status t1
- | Conclude (_,t1) -> "conclude " ^ NotationPp.pp_term status t1
- | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status term1
- | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ NotationPp.pp_term status term ^ "to prove" ^ NotationPp.pp_term status term1
- | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")"
+ | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ " (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | Conclude (_,t1) -> "conclude (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on (" ^ NotationPp.pp_term
+ status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on (" ^
+ NotationPp.pp_term status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | Byinduction (_, term, ident) -> "by induction hypothesis we know (" ^ NotationPp.pp_term status
+ term ^ ") (" ^ ident ^ ")"
| Case (_, id, args) ->
- "case" ^ id ^
+ "case " ^ id ^
String.concat " "
- (List.map (function (id,term) -> "(" ^ id ^ ": " ^ NotationPp.pp_term status term ^ ")")
+ (List.map (function (id,term) -> "(" ^ id ^ ": (" ^ NotationPp.pp_term status term ^ "))")
args)
;;
desc
| Number_alias (instance,desc) ->
sprintf "alias num (instance %d) = \"%s\"." instance desc
-
+
let pp_associativity = function
| Gramext.LeftA -> "left associative"
| Gramext.RightA -> "right associative"
done;
sprintf "%s%s" (Buffer.contents eta_buf) name
-let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
+let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
sprintf "interpretation \"%s\" '%s %s = %s."
dsc symbol
(String.concat " " (List.map pp_argument_pattern arg_patterns))
(NotationPp.pp_cic_appl_pattern cic_appl_pattern)
-
+
let pp_dir_opt = function
| None -> ""
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
-let pp_notation status dir_opt l1_pattern assoc prec l2_pattern =
+let pp_notation status dir_opt l1_pattern assoc prec l2_pattern =
sprintf "notation %s\"%s\" %s %s for %s."
(pp_dir_opt dir_opt)
(pp_l1_pattern status l1_pattern)
(pp_l2_pattern status l2_pattern)
let pp_ncommand status = function
- | UnificationHint (_,t, n) ->
+ | UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term status t
| NDiscriminator (_,_)
| NInverter (_,_,_,_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
- | NObj (_,obj,index) ->
- (if not index then "-" else "") ^
+ | NObj (_,obj,index) ->
+ (if not index then "-" else "") ^
NotationPp.pp_obj (NotationPp.pp_term status) obj
| NQed (_,true) -> "qed"
| NQed (_,false) -> "qed-"
- | NCopy (_,name,uri,map) ->
- "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
- String.concat " and "
- (List.map
- (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
+ | NCopy (_,name,uri,map) ->
+ "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
+ String.concat " and "
+ (List.map
+ (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b)
map)
| Include (_,mode,path) -> (* not precise, since path is absolute *)
if mode = WithPreferences then
| Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
pp_notation status dir_opt l1_pattern assoc prec l2_pattern
;;
-
+
let pp_executable status ~map_unicode_to_tex =
function
| NMacro (_, macro) -> pp_nmacro status macro ^ "."
| NTactic (_,tacl) ->
String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) tacl)
| NCommand (_, cmd) -> pp_ncommand status cmd ^ "."
-
+
let pp_comment status ~map_unicode_to_tex =
function
| Note (_,"") -> Printf.sprintf "\n"
let pp_statement status =
function
- | Executable (_, ex) -> pp_executable status ex
+ | Executable (_, ex) -> pp_executable status ex
| Comment (_, c) -> pp_comment status c
(* 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
* 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
class status baseuri =
- object
- inherit GrafiteTypes.status baseuri
- inherit ApplyTransformation.status
- end
+ object
+ inherit GrafiteTypes.status baseuri
+ inherit ApplyTransformation.status
+ end
exception TryingToAdd of string Lazy.t
exception EnrichedWithStatus of exn * status
let slash_n_RE = Pcre.regexp "\\n" ;;
-let pp_ast_statement status stm =
- let stm = GrafiteAstPp.pp_statement status stm
- ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+let first_line = ref true ;;
+
+let cases_or_induction_context stack =
+ match stack with
+ [] -> false
+ | (g,t,k,tag,p)::tl -> try
+ let s = List.assoc "context" p in
+ s = "cases" || s = "induction"
+ with
+ Not_found -> false
+;;
+
+let has_focused_goal stack =
+ match stack with
+ [] -> false
+ | (g,t,k,tag,p)::tl -> (List.length g) > 0
+;;
+
+let get_indentation status statement =
+ let base_ind =
+ match status#stack with
+ [] -> 0
+ | s -> List.length(s) * 2
+ in
+ if cases_or_induction_context status#stack then
+ (
+ if has_focused_goal status#stack then
+ base_ind + 2
+ else
+ base_ind
+ )
+ else
+ base_ind
+;;
+
+let pp_ind s n =
+ let rec aux s n =
+ match n with
+ 0 -> s
+ | n -> " " ^ (aux s (n-1))
in
- let stm = Pcre.replace ~rex:slash_n_RE stm in
- let stm =
+ aux s n
+
+let write_ast_to_file status fname statement =
+ let indentation = get_indentation status statement in
+ let str = match statement with
+ G.Comment _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.Executable (_,code) ->
+ (
+ match code with
+ G.NTactic _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.NCommand (_,cmd) ->
+ (
+ match cmd with
+ | G.NObj (_,obj,_) ->
+ (
+ match obj with
+ Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | G.NQed _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | _ -> ""
+ )
+ in
+ if str <> "" then
+ (
+ let s = pp_ind str indentation in
+ let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat]
+ else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
+ in
+ let out_channel =
+ Stdlib.open_out_gen flaglist 0o0644 fname in
+ let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
+ let _ = Stdlib.close_out out_channel in
+ str
+ )
+ else
+ str
+;;
+
+let pp_ast_statement status stm ~fname =
+ let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in
+ if stm <> "" then
+ (
+ let stm = Pcre.replace ~rex:slash_n_RE stm in
+ let stm =
if String.length stm > 50 then String.sub stm 0 50 ^ " ..."
else stm
- in
+ in
HLog.debug ("Executing: ``" ^ stm ^ "''")
+ )
+ else
+ HLog.debug ("Executing: `` Unprintable statement ''")
;;
let clean_exit baseuri exn =
raise (FailureCompiling (baseuri,exn))
;;
-let cut prefix s =
+let cut prefix s =
let lenp = String.length prefix in
let lens = String.length s in
assert (lens > lenp);
String.sub s lenp (lens-lenp)
;;
-let print_string =
- let indent = ref 0 in
- let print_string ~right_justify s =
- let ss =
- match right_justify with
- None -> ""
- | Some (ss,len_ss) ->
- let i = 80 - !indent - len_ss - String.length s in
- if i > 0 then String.make i ' ' ^ ss else ss
- in
- assert (!indent >=0);
- print_string (String.make !indent ' ' ^ s ^ ss) in
- fun enter ?right_justify s ->
- if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
+let print_string =
+ let indent = ref 0 in
+ let print_string ~right_justify s =
+ let ss =
+ match right_justify with
+ None -> ""
+ | Some (ss,len_ss) ->
+ let i = 80 - !indent - len_ss - String.length s in
+ if i > 0 then String.make i ' ' ^ ss else ss
+ in
+ assert (!indent >=0);
+ print_string (String.make !indent ' ' ^ s ^ ss) in
+ fun enter ?right_justify s ->
+ if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
;;
-let pp_times ss fname rc big_bang big_bang_u big_bang_s =
+let pp_times ss fname rc big_bang big_bang_u big_bang_s =
if not (Helm_registry.get_bool "matita.verbose") then
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
let u = u -. big_bang_u in
let s = s -. big_bang_s in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
- let rc =
+ let rc =
if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
- let times =
- let fmt t =
+ let times =
+ let fmt t =
let seconds = int_of_float t in
let cents = int_of_float ((t -. floor t) *. 100.0) in
let minutes = seconds / 60 in
;;
let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
- let baseuri = status#baseuri in
- let new_aliases,new_status =
- GrafiteDisambiguate.eval_with_new_aliases status
- (fun status ->
- let time0 = Unix.gettimeofday () in
- let status =
- GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast) in
- let time1 = Unix.gettimeofday () in
- HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s");
- status
- ) in
- let _,intermediate_states =
- List.fold_left
- (fun (status,acc) (k,value) ->
- let v = GrafiteAst.description_of_alias value in
- let b =
- try
- let NReference.Ref (uri,_) = NReference.reference_of_string v in
- NUri.baseuri_of_uri uri = baseuri
- with
- NReference.IllFormedReference _ ->
- false (* v is a description, not a URI *)
- in
- if b then
- status,acc
- else
- let status =
- GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
- GrafiteAst.WithPreferences [k,value]
- in
- status, (status ,Some (k,value))::acc
- ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
- in
+ let baseuri = status#baseuri in
+ let new_aliases,new_status =
+ GrafiteDisambiguate.eval_with_new_aliases status
+ (fun status ->
+ let time0 = Unix.gettimeofday () in
+ let status =
+ GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
+ (text,prefix_len,ast) in
+ let time1 = Unix.gettimeofday () in
+ HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s");
+ status
+ ) in
+ let _,intermediate_states =
+ List.fold_left
+ (fun (status,acc) (k,value) ->
+ let v = GrafiteAst.description_of_alias value in
+ let b =
+ try
+ let NReference.Ref (uri,_) = NReference.reference_of_string v in
+ NUri.baseuri_of_uri uri = baseuri
+ with
+ NReference.IllFormedReference _ ->
+ false (* v is a description, not a URI *)
+ in
+ if b then
+ status,acc
+ else
+ let status =
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
+ GrafiteAst.WithPreferences [k,value]
+ in
+ status, (status ,Some (k,value))::acc
+ ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
+ in
(new_status,None)::intermediate_states
;;
let baseuri_of_script ~include_paths fname =
- try Librarian.baseuri_of_script ~include_paths fname
- with
- Librarian.NoRootFor _ ->
+ try Librarian.baseuri_of_script ~include_paths fname
+ with
+ Librarian.NoRootFor _ ->
HLog.error ("The included file '"^fname^"' has no root file,");
HLog.error "please create it.";
raise (Failure ("No root file for "^fname))
- | Librarian.FileNotFound _ ->
+ | Librarian.FileNotFound _ ->
raise (Failure ("File not found: "^fname))
;;
(* given a path to a ma file inside the include_paths, returns the
new include_paths associated to that file *)
let read_include_paths ~include_paths file =
- try
- let root, _buri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] file in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
+ try
+ let root, _buri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:[] file in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ let rc = root :: includes in
List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- []
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ []
;;
-let rec get_ast status ~compiling ~asserted ~include_paths strm =
+let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
- (GrafiteAst.Executable
+ (GrafiteAst.Executable
(_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
- ->
- let already_included = NCicLibrary.get_transitively_included status in
- let asserted,_ =
- assert_ng ~already_included ~compiling ~asserted ~include_paths
- mafilename
- in
- asserted,cmd
- | cmd -> asserted,cmd
+ ->
+ let already_included = NCicLibrary.get_transitively_included status in
+ let asserted,_ =
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mafilename
+ in
+ asserted,cmd
+ | cmd -> asserted,cmd
and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status str =
- let asserted,stop,status,str =
- try
- let cont =
- try Some (get_ast status ~compiling ~asserted ~include_paths str)
- with End_of_file -> None in
- match cont with
- | None -> asserted, true, status, str
- | Some (asserted,ast) ->
- cb status ast;
- let new_statuses =
- eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
- let status =
- match new_statuses with
- [s,None] -> s
- | _::(_,Some (_,value))::_ ->
- raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
- | _ -> assert false in
- (* CSC: complex patch to re-build the lexer since the tokens may
- have changed. Note: this way we loose look-ahead tokens.
- Hence the "include" command must be terminated (no look-ahead) *)
- let str =
- match ast with
- (GrafiteAst.Executable
- (_,GrafiteAst.NCommand
- (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let rec loop asserted status str =
+ let asserted,stop,status,str =
+ try
+ let cont =
+ try Some (get_ast status ~compiling ~asserted ~include_paths str)
+ with End_of_file -> None in
+ match cont with
+ | None -> asserted, true, status, str
+ | Some (asserted,ast) ->
+ cb status ast;
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+ let status =
+ match new_statuses with
+ [s,None] -> s
+ | _::(_,Some (_,value))::_ ->
+ raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+ | _ -> assert false in
+ (* CSC: complex patch to re-build the lexer since the tokens may
+ have changed. Note: this way we loose look-ahead tokens.
+ Hence the "include" command must be terminated (no look-ahead) *)
+ let str =
+ match ast with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand
+ (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
GrafiteParser.parsable_statement status
- (GrafiteParser.strm_of_parsable str)
- | _ -> str
- in
- asserted, false, status, str
- with exn when not matita_debug ->
- raise (EnrichedWithStatus (exn, status))
+ (GrafiteParser.strm_of_parsable str)
+ | _ -> str
+ in
+ asserted, false, status, str
+ with exn when not matita_debug ->
+ raise (EnrichedWithStatus (exn, status))
+ in
+ if stop then asserted,status else loop asserted status str
in
- if stop then asserted,status else loop asserted status str
- in
loop asserted status str
and compile ~compiling ~asserted ~include_paths fname =
if List.mem fname compiling then raise (CircularDependency fname);
let compiling = fname::compiling in
let matita_debug = Helm_registry.get_bool "matita.debug" in
- let root,baseuri,fname,_tgt =
+ let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
let ocamldirname = Filename.dirname fname in
let ocamlfname = Filename.chop_extension (Filename.basename fname) in
let status,ocamlfname =
- Common.modname_of_filename status false ocamlfname in
+ Common.modname_of_filename status false ocamlfname in
let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
let big_bang = Unix.gettimeofday () in
- let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
- Unix.times ()
+ let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
+ Unix.times ()
in
let time = Unix.time () in
- let cc =
- let rex = Str.regexp ".*opt$" in
- if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
- else "matitac" in
+ let cc =
+ let rex = Str.regexp ".*opt$" in
+ if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
+ else "matitac" in
let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in
try
(* cleanup of previously compiled objects *)
if (not (Http_getter_storage.is_empty ~local:true baseuri))
- then begin
+ then begin
HLog.message ("baseuri " ^ baseuri ^ " is not empty");
HLog.message ("cleaning baseuri " ^ baseuri);
LibraryClean.clean_baseuris [baseuri];
end;
HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
if not (Helm_registry.get_bool "matita.verbose") then
- (print_string true (s ^ "\n"); flush stdout);
+ (print_string true (s ^ "\n"); flush stdout);
(* we dalay this error check until we print 'matitac file ' *)
assert (Http_getter_storage.is_empty ~local:true baseuri);
(* create dir for XML files *)
if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
- ~default:false)
+ ~default:false)
then
- HExtlib.mkdir
- (Filename.dirname
- (Http_getter.filename ~local:true ~writable:true (baseuri ^
- "foo.con")));
+ HExtlib.mkdir
+ (Filename.dirname
+ (Http_getter.filename ~local:true ~writable:true (baseuri ^
+ "foo.con")));
let buf =
- GrafiteParser.parsable_statement status
- (Ulexing.from_utf8_channel (open_in fname))
+ GrafiteParser.parsable_statement status
+ (Ulexing.from_utf8_channel (open_in fname))
in
let print_cb =
- if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
- else pp_ast_statement
+ if not (Helm_registry.get_bool "matita.verbose") then fun _ _ -> ()
+ else pp_ast_statement ~fname
in
let asserted, status =
- eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+ eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
let status = OcamlExtraction.close_file status in
let elapsed = Unix.time () -. time in
- (if Helm_registry.get_bool "matita.moo" then begin
- GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
- status
- end;
+ (if Helm_registry.get_bool "matita.moo" then begin
+ GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ status
+ end;
let tm = Unix.gmtime elapsed in
let sec = string_of_int tm.Unix.tm_sec ^ "''" in
- let min =
- if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
+ let min =
+ if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
in
- let hou =
+ let hou =
if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else ""
in
- HLog.message
+ HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times s fname true big_bang big_bang_u big_bang_s;
(*CSC: bad, one imperative bit is still there!
to be moved into functional status *)
NCicMetaSubst.pushmaxmeta ();
-(* MATITA 1.0: debbo fare time_travel sulla ng_library?
- LexiconSync.time_travel
- ~present:lexicon_status ~past:initial_lexicon_status;
-*)
+ (* MATITA 1.0: debbo fare time_travel sulla ng_library?
+ LexiconSync.time_travel
+ ~present:lexicon_status ~past:initial_lexicon_status;
+ *)
asserted)
- with
+ with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| exn when not matita_debug ->
-(* MATITA 1.0: debbo fare time_travel sulla ng_library?
- LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
- * *)
- (*CSC: bad, one imperative bit is still there!
- to be moved into functional status *)
- NCicMetaSubst.pushmaxmeta ();
- pp_times s fname false big_bang big_bang_u big_bang_s;
- clean_exit baseuri exn
+ (* MATITA 1.0: debbo fare time_travel sulla ng_library?
+ LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
+ * *)
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
+ pp_times s fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri exn
and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
- let root,baseuri,fullmapath,_ =
- Librarian.baseuri_of_script ~include_paths mapath in
- if List.mem fullmapath asserted then asserted,false
- else
- begin
- let include_paths =
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- root::includes @
- Helm_registry.get_list Helm_registry.string "matita.includes" in
- let baseuri = NUri.uri_of_string baseuri in
- let ngtime_of baseuri =
- let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
- try
- Some (Unix.stat ngpath).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
- let matime =
- try (Unix.stat fullmapath).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
- in
- let ngtime = ngtime_of baseuri in
- let asserted,to_be_compiled =
- match ngtime with
- Some ngtime ->
- let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
- let asserted,children_bad =
- List.fold_left
- (fun (asserted,b) mapath ->
- let asserted,b1 =
- try
- assert_ng ~already_included ~compiling ~asserted ~include_paths
- mapath
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- asserted, true
- in
- asserted, b || b1
- || let _,baseuri,_,_ =
- (*CSC: bug here? include_paths should be empty and
- mapath should be absolute *)
- Librarian.baseuri_of_script ~include_paths mapath in
- let baseuri = NUri.uri_of_string baseuri in
- (match ngtime_of baseuri with
- Some child_ngtime -> child_ngtime > ngtime
- | None -> assert false)
- ) (asserted,false) preamble
+ let root,baseuri,fullmapath,_ =
+ Librarian.baseuri_of_script ~include_paths mapath in
+ if List.mem fullmapath asserted then asserted,false
+ else
+ begin
+ let include_paths =
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
in
- asserted, children_bad || matime > ngtime
- | None -> asserted,true
- in
- if not to_be_compiled then fullmapath::asserted,false
- else
- if List.mem baseuri already_included then
- (* maybe recompiling it I would get the same... *)
- raise (AlreadyLoaded (lazy mapath))
- else
- let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
- fullmapath::asserted,true
- end
+ root::includes @
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let baseuri = NUri.uri_of_string baseuri in
+ let ngtime_of baseuri =
+ let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ try
+ Some (Unix.stat ngpath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
+ let matime =
+ try (Unix.stat fullmapath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
+ in
+ let ngtime = ngtime_of baseuri in
+ let asserted,to_be_compiled =
+ match ngtime with
+ Some ngtime ->
+ let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let asserted,children_bad =
+ List.fold_left
+ (fun (asserted,b) mapath ->
+ let asserted,b1 =
+ try
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mapath
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ asserted, true
+ in
+ asserted, b || b1
+ || let _,baseuri,_,_ =
+ (*CSC: bug here? include_paths should be empty and
+ mapath should be absolute *)
+ Librarian.baseuri_of_script ~include_paths mapath in
+ let baseuri = NUri.uri_of_string baseuri in
+ (match ngtime_of baseuri with
+ Some child_ngtime -> child_ngtime > ngtime
+ | None -> assert false)
+ ) (asserted,false) preamble
+ in
+ asserted, children_bad || matime > ngtime
+ | None -> asserted,true
+ in
+ if not to_be_compiled then fullmapath::asserted,false
+ else
+ if List.mem baseuri already_included then
+ (* maybe recompiling it I would get the same... *)
+ raise (AlreadyLoaded (lazy mapath))
+ else
+ let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+ fullmapath::asserted,true
+ end
;;
let assert_ng ~include_paths mapath =
- snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
- mapath)
+ snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
+ mapath)
let get_ast status ~include_paths strm =
- snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)
+ snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)
projects / helm.git / commitdiff