diff options
Diffstat (limited to 'lib')
54 files changed, 7423 insertions, 0 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml new file mode 100644 index 0000000000..7d04c8f5a1 --- /dev/null +++ b/lib/acyclicGraph.ml @@ -0,0 +1,852 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type constraint_type = Lt | Le | Eq + +module type Point = sig + type t + + module Set : CSig.SetS with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set + + module Constraint : CSet.S with type elt = (t * constraint_type * t) + + val equal : t -> t -> bool + val compare : t -> t -> int + + type explanation = (constraint_type * t) list + val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a + + val pr : t -> Pp.t +end + +module Make (Point:Point) = struct + + (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) + (* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *) + (* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *) + (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) + (* Support for universe polymorphism by MS [2014] *) + + (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu + Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) + + (* Points are stratified by a partial ordering $\le$. + Let $\~{}$ be the associated equivalence. We also have a strict ordering + $<$ between equivalence classes, and we maintain that $<$ is acyclic, + and contained in $\le$ in the sense that $[U]<[V]$ implies $U\le V$. + + At every moment, we have a finite number of points, and we + maintain the ordering in the presence of assertions $U<V$ and $U\le V$. + + The equivalence $\~{}$ is represented by a tree structure, as in the + union-find algorithm. The assertions $<$ and $\le$ are represented by + adjacency lists. + + We use the algorithm described in the paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. + + *) + + module PMap = Point.Map + module PSet = Point.Set + module Constraint = Point.Constraint + + type status = NoMark | Visited | WeakVisited | ToMerge + + (* Comparison on this type is pointer equality *) + type canonical_node = + { canon: Point.t; + ltle: bool PMap.t; (* true: strict (lt) constraint. + false: weak (le) constraint. *) + gtge: PSet.t; + rank : int; + klvl: int; + ilvl: int; + mutable status: status + } + + let big_rank = 1000000 + + (* A Point.t is either an alias for another one, or a canonical one, + for which we know the points that are above *) + + type entry = + | Canonical of canonical_node + | Equiv of Point.t + + type t = + { entries : entry PMap.t; + index : int; + n_nodes : int; n_edges : int } + + (** Used to cleanup mutable marks if a traversal function is + interrupted before it has the opportunity to do it itself. *) + let unsafe_cleanup_marks g = + let iter _ n = match n with + | Equiv _ -> () + | Canonical n -> n.status <- NoMark + in + PMap.iter iter g.entries + + let rec cleanup_marks g = + try unsafe_cleanup_marks g + with e -> + (* The only way unsafe_cleanup_marks may raise an exception is when + a serious error (stack overflow, out of memory) occurs, or a signal is + sent. In this unlikely event, we relaunch the cleanup until we finally + succeed. *) + cleanup_marks g; raise e + + (* Every Point.t has a unique canonical arc representative *) + + (* Low-level function : makes u an alias for v. + Does not removes edges from n_edges, but decrements n_nodes. + u should be entered as canonical before. *) + let enter_equiv g u v = + { entries = + PMap.modify u (fun _ a -> + match a with + | Canonical n -> + n.status <- NoMark; + Equiv v + | _ -> assert false) g.entries; + index = g.index; + n_nodes = g.n_nodes - 1; + n_edges = g.n_edges } + + (* Low-level function : changes data associated with a canonical node. + Resets the mutable fields in the old record, in order to avoid breaking + invariants for other users of this record. + n.canon should already been inserted as a canonical node. *) + let change_node g n = + { g with entries = + PMap.modify n.canon + (fun _ a -> + match a with + | Canonical n' -> + n'.status <- NoMark; + Canonical n + | _ -> assert false) + g.entries } + + (* canonical representative : we follow the Equiv links *) + let rec repr g u = + match PMap.find u g.entries with + | Equiv v -> repr g v + | Canonical arc -> arc + | exception Not_found -> + CErrors.anomaly ~label:"Univ.repr" + Pp.(str"Universe " ++ Point.pr u ++ str" undefined.") + + exception AlreadyDeclared + + (* Reindexes the given point, using the next available index. *) + let use_index g u = + let u = repr g u in + let g = change_node g { u with ilvl = g.index } in + assert (g.index > min_int); + { g with index = g.index - 1 } + + (* [safe_repr] is like [repr] but if the graph doesn't contain the + searched point, we add it. *) + let safe_repr g u = + let rec safe_repr_rec entries u = + match PMap.find u entries with + | Equiv v -> safe_repr_rec entries v + | Canonical arc -> arc + in + try g, safe_repr_rec g.entries u + with Not_found -> + let can = + { canon = u; + ltle = PMap.empty; gtge = PSet.empty; + rank = 0; + klvl = 0; ilvl = 0; + status = NoMark } + in + let g = { g with + entries = PMap.add u (Canonical can) g.entries; + n_nodes = g.n_nodes + 1 } + in + let g = use_index g u in + g, repr g u + + (* Returns 1 if u is higher than v in topological order. + -1 lower + 0 if u = v *) + let topo_compare u v = + if u.klvl > v.klvl then 1 + else if u.klvl < v.klvl then -1 + else if u.ilvl > v.ilvl then 1 + else if u.ilvl < v.ilvl then -1 + else (assert (u==v); 0) + + (* Checks most of the invariants of the graph. For debugging purposes. *) + let check_invariants ~required_canonical g = + let n_edges = ref 0 in + let n_nodes = ref 0 in + PMap.iter (fun l u -> + match u with + | Canonical u -> + PMap.iter (fun v _strict -> + incr n_edges; + let v = repr g v in + assert (topo_compare u v = -1); + if u.klvl = v.klvl then + assert (PSet.mem u.canon v.gtge || + PSet.exists (fun l -> u == repr g l) v.gtge)) + u.ltle; + PSet.iter (fun v -> + let v = repr g v in + assert (v.klvl = u.klvl && + (PMap.mem u.canon v.ltle || + PMap.exists (fun l _ -> u == repr g l) v.ltle)) + ) u.gtge; + assert (u.status = NoMark); + assert (Point.equal l u.canon); + assert (u.ilvl > g.index); + assert (not (PMap.mem u.canon u.ltle)); + incr n_nodes + | Equiv _ -> assert (not (required_canonical l))) + g.entries; + assert (!n_edges = g.n_edges); + assert (!n_nodes = g.n_nodes) + + let clean_ltle g ltle = + PMap.fold (fun u strict acc -> + let uu = (repr g u).canon in + if Point.equal uu u then acc + else ( + let acc = PMap.remove u (fst acc) in + if not strict && PMap.mem uu acc then (acc, true) + else (PMap.add uu strict acc, true))) + ltle (ltle, false) + + let clean_gtge g gtge = + PSet.fold (fun u acc -> + let uu = (repr g u).canon in + if Point.equal uu u then acc + else PSet.add uu (PSet.remove u (fst acc)), true) + gtge (gtge, false) + + (* [get_ltle] and [get_gtge] return ltle and gtge arcs. + Moreover, if one of these lists is dirty (e.g. points to a + non-canonical node), these functions clean this node in the + graph by removing some duplicate edges *) + let get_ltle g u = + let ltle, chgt_ltle = clean_ltle g u.ltle in + if not chgt_ltle then u.ltle, u, g + else + let sz = PMap.cardinal u.ltle in + let sz2 = PMap.cardinal ltle in + let u = { u with ltle } in + let g = change_node g u in + let g = { g with n_edges = g.n_edges + sz2 - sz } in + u.ltle, u, g + + let get_gtge g u = + let gtge, chgt_gtge = clean_gtge g u.gtge in + if not chgt_gtge then u.gtge, u, g + else + let u = { u with gtge } in + let g = change_node g u in + u.gtge, u, g + + (* [revert_graph] rollbacks the changes made to mutable fields in + nodes in the graph. + [to_revert] contains the touched nodes. *) + let revert_graph to_revert g = + List.iter (fun t -> + match PMap.find t g.entries with + | Equiv _ -> () + | Canonical t -> + t.status <- NoMark) to_revert + + exception AbortBackward of t + exception CycleDetected + + (* Implementation of the algorithm described in § 5.1 of the following paper: + + Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2011). A + new approach to incremental cycle detection and related + problems. arXiv preprint arXiv:1112.0784. + + The "STEP X" comments contained in this file refers to the + corresponding step numbers of the algorithm described in Section + 5.1 of this paper. *) + + (* [delta] is the timeout for backward search. It might be + useful to tune a multiplicative constant. *) + let get_delta g = + int_of_float + (min (float_of_int g.n_edges ** 0.5) + (float_of_int g.n_nodes ** (2./.3.))) + + let rec backward_traverse to_revert b_traversed count g x = + let x = repr g x in + let count = count - 1 in + if count < 0 then begin + revert_graph to_revert g; + raise (AbortBackward g) + end; + if x.status = NoMark then begin + x.status <- Visited; + let to_revert = x.canon::to_revert in + let gtge, x, g = get_gtge g x in + let to_revert, b_traversed, count, g = + PSet.fold (fun y (to_revert, b_traversed, count, g) -> + backward_traverse to_revert b_traversed count g y) + gtge (to_revert, b_traversed, count, g) + in + to_revert, x.canon::b_traversed, count, g + end + else to_revert, b_traversed, count, g + + let rec forward_traverse f_traversed g v_klvl x y = + let y = repr g y in + if y.klvl < v_klvl then begin + let y = { y with klvl = v_klvl; + gtge = if x == y then PSet.empty + else PSet.singleton x.canon } + in + let g = change_node g y in + let ltle, y, g = get_ltle g y in + let f_traversed, g = + PMap.fold (fun z _ (f_traversed, g) -> + forward_traverse f_traversed g v_klvl y z) + ltle (f_traversed, g) + in + y.canon::f_traversed, g + end else if y.klvl = v_klvl && x != y then + let g = change_node g + { y with gtge = PSet.add x.canon y.gtge } in + f_traversed, g + else f_traversed, g + + let rec find_to_merge to_revert g x v = + let x = repr g x in + match x.status with + | Visited -> false, to_revert | ToMerge -> true, to_revert + | NoMark -> + let to_revert = x::to_revert in + if Point.equal x.canon v then + begin x.status <- ToMerge; true, to_revert end + else + begin + let merge, to_revert = PSet.fold + (fun y (merge, to_revert) -> + let merge', to_revert = find_to_merge to_revert g y v in + merge' || merge, to_revert) x.gtge (false, to_revert) + in + x.status <- if merge then ToMerge else Visited; + merge, to_revert + end + | _ -> assert false + + let get_new_edges g to_merge = + (* Computing edge sets. *) + let to_merge_lvl = + List.fold_left (fun acc u -> PMap.add u.canon u acc) + PMap.empty to_merge + in + let ltle = + let fold _ n acc = + let fold u strict acc = + if strict then PMap.add u strict acc + else if PMap.mem u acc then acc + else PMap.add u false acc + in + PMap.fold fold n.ltle acc + in + PMap.fold fold to_merge_lvl PMap.empty + in + let ltle, _ = clean_ltle g ltle in + let ltle = + PMap.merge (fun _ a strict -> + match a, strict with + | Some _, Some true -> + (* There is a lt edge inside the new component. This is a + "bad cycle". *) + raise CycleDetected + | Some _, Some false -> None + | _, _ -> strict + ) to_merge_lvl ltle + in + let gtge = + PMap.fold (fun _ n acc -> PSet.union acc n.gtge) + to_merge_lvl PSet.empty + in + let gtge, _ = clean_gtge g gtge in + let gtge = PSet.diff gtge (PMap.domain to_merge_lvl) in + (ltle, gtge) + + + let reorder g u v = + (* STEP 2: backward search in the k-level of u. *) + let delta = get_delta g in + + (* [v_klvl] is the chosen future level for u, v and all + traversed nodes. *) + let b_traversed, v_klvl, g = + try + let to_revert, b_traversed, _, g = backward_traverse [] [] delta g u in + revert_graph to_revert g; + let v_klvl = (repr g u).klvl in + b_traversed, v_klvl, g + with AbortBackward g -> + (* Backward search was too long, use the next k-level. *) + let v_klvl = (repr g u).klvl + 1 in + [], v_klvl, g + in + let f_traversed, g = + (* STEP 3: forward search. Contrary to what is described in + the paper, we do not test whether v_klvl = u.klvl nor we assign + v_klvl to v.klvl. Indeed, the first call to forward_traverse + will do all that. *) + forward_traverse [] g v_klvl (repr g v) v + in + + (* STEP 4: merge nodes if needed. *) + let to_merge, b_reindex, f_reindex = + if (repr g u).klvl = v_klvl then + begin + let merge, to_revert = find_to_merge [] g u v in + let r = + if merge then + List.filter (fun u -> u.status = ToMerge) to_revert, + List.filter (fun u -> (repr g u).status <> ToMerge) b_traversed, + List.filter (fun u -> (repr g u).status <> ToMerge) f_traversed + else [], b_traversed, f_traversed + in + List.iter (fun u -> u.status <- NoMark) to_revert; + r + end + else [], b_traversed, f_traversed + in + let to_reindex, g = + match to_merge with + | [] -> List.rev_append f_reindex b_reindex, g + | n0::q0 -> + (* Computing new root. *) + let root, rank_rest = + List.fold_left (fun ((best, _rank_rest) as acc) n -> + if n.rank >= best.rank then n, best.rank else acc) + (n0, min_int) q0 + in + let ltle, gtge = get_new_edges g to_merge in + (* Inserting the new root. *) + let g = change_node g + { root with ltle; gtge; + rank = max root.rank (rank_rest + 1); } + in + + (* Inserting shortcuts for old nodes. *) + let g = List.fold_left (fun g n -> + if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon) + g to_merge + in + + (* Updating g.n_edges *) + let oldsz = + List.fold_left (fun sz u -> sz+PMap.cardinal u.ltle) + 0 to_merge + in + let sz = PMap.cardinal ltle in + let g = { g with n_edges = g.n_edges + sz - oldsz } in + + (* Not clear in the paper: we have to put the newly + created component just between B and F. *) + List.rev_append f_reindex (root.canon::b_reindex), g + + in + + (* STEP 5: reindex traversed nodes. *) + List.fold_left use_index g to_reindex + + (* Assumes [u] and [v] are already in the graph. *) + (* Does NOT assume that ucan != vcan. *) + let insert_edge strict ucan vcan g = + try + let u = ucan.canon and v = vcan.canon in + (* STEP 1: do we need to reorder nodes ? *) + let g = if topo_compare ucan vcan <= 0 then g else reorder g u v in + + (* STEP 6: insert the new edge in the graph. *) + let u = repr g u in + let v = repr g v in + if u == v then + if strict then raise CycleDetected else g + else + let g = + try let oldstrict = PMap.find v.canon u.ltle in + if strict && not oldstrict then + change_node g { u with ltle = PMap.add v.canon true u.ltle } + else g + with Not_found -> + { (change_node g { u with ltle = PMap.add v.canon strict u.ltle }) + with n_edges = g.n_edges + 1 } + in + if u.klvl <> v.klvl || PSet.mem u.canon v.gtge then g + else + let v = { v with gtge = PSet.add u.canon v.gtge } in + change_node g v + with + | CycleDetected as e -> raise e + | e -> + (* Unlikely event: fatal error or signal *) + let () = cleanup_marks g in + raise e + + let add ?(rank=0) v g = + try + let _arcv = PMap.find v g.entries in + raise AlreadyDeclared + with Not_found -> + assert (g.index > min_int); + let node = { + canon = v; + ltle = PMap.empty; + gtge = PSet.empty; + rank; + klvl = 0; + ilvl = g.index; + status = NoMark; + } + in + let entries = PMap.add v (Canonical node) g.entries in + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } + + exception Undeclared of Point.t + let check_declared g us = + let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in + PSet.iter check us + + exception Found_explanation of (constraint_type * Point.t) list + + let get_explanation strict u v g = + let v = repr g v in + let visited_strict = ref PMap.empty in + let rec traverse strict u = + if u == v then + if strict then None else Some [] + else if topo_compare u v = 1 then None + else + let visited = + try not (PMap.find u.canon !visited_strict) || strict + with Not_found -> false + in + if visited then None + else begin + visited_strict := PMap.add u.canon strict !visited_strict; + try + PMap.iter (fun u' strictu' -> + match traverse (strict && not strictu') (repr g u') with + | None -> () + | Some exp -> + let typ = if strictu' then Lt else Le in + raise (Found_explanation ((typ, u') :: exp))) + u.ltle; + None + with Found_explanation exp -> Some exp + end + in + let u = repr g u in + if u == v then [(Eq, v.canon)] + else match traverse strict u with Some exp -> exp | None -> assert false + + let get_explanation strict u v g = + Some (lazy (get_explanation strict u v g)) + + (* To compare two nodes, we simply do a forward search. + We implement two improvements: + - we ignore nodes that are higher than the destination; + - we do a BFS rather than a DFS because we expect to have a short + path (typically, the shortest path has length 1) + *) + exception Found of canonical_node list + let search_path strict u v g = + let rec loop to_revert todo next_todo = + match todo, next_todo with + | [], [] -> to_revert (* No path found *) + | [], _ -> loop to_revert next_todo [] + | (u, strict)::todo, _ -> + if u.status = Visited || (u.status = WeakVisited && strict) + then loop to_revert todo next_todo + else + let to_revert = + if u.status = NoMark then u::to_revert else to_revert + in + u.status <- if strict then WeakVisited else Visited; + if try PMap.find v.canon u.ltle || not strict + with Not_found -> false + then raise (Found to_revert) + else + begin + let next_todo = + PMap.fold (fun u strictu next_todo -> + let strict = not strictu && strict in + let u = repr g u in + if u == v && not strict then raise (Found to_revert) + else if topo_compare u v = 1 then next_todo + else (u, strict)::next_todo) + u.ltle next_todo + in + loop to_revert todo next_todo + end + in + if u == v then not strict + else + try + let res, to_revert = + try false, loop [] [u, strict] [] + with Found to_revert -> true, to_revert + in + List.iter (fun u -> u.status <- NoMark) to_revert; + res + with e -> + (* Unlikely event: fatal error or signal *) + let () = cleanup_marks g in + raise e + + (** Uncomment to debug the cycle detection algorithm. *) + (*let insert_edge strict ucan vcan g = + let check_invariants = check_invariants ~required_canonical:(fun _ -> false) in + check_invariants g; + let g = insert_edge strict ucan vcan g in + check_invariants g; + let ucan = repr g ucan.canon in + let vcan = repr g vcan.canon in + assert (search_path strict ucan vcan g); + g*) + + (** User interface *) + + type 'a check_function = t -> 'a -> 'a -> bool + + let check_eq g u v = + u == v || + let arcu = repr g u and arcv = repr g v in + arcu == arcv + + let check_smaller g strict u v = + search_path strict (repr g u) (repr g v) g + + let check_leq g u v = check_smaller g false u v + let check_lt g u v = check_smaller g true u v + + (* enforce_eq g u v will force u=v if possible, will fail otherwise *) + + let rec enforce_eq u v g = + let ucan = repr g u in + let vcan = repr g v in + if topo_compare ucan vcan = 1 then enforce_eq v u g + else + let g = insert_edge false ucan vcan g in (* Cannot fail *) + try insert_edge false vcan ucan g + with CycleDetected -> + Point.error_inconsistency Eq v u (get_explanation true u v g) + + (* enforce_leq g u v will force u<=v if possible, will fail otherwise *) + let enforce_leq u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge false ucan vcan g + with CycleDetected -> + Point.error_inconsistency Le u v (get_explanation true v u g) + + (* enforce_lt u v will force u<v if possible, will fail otherwise *) + let enforce_lt u v g = + let ucan = repr g u in + let vcan = repr g v in + try insert_edge true ucan vcan g + with CycleDetected -> + Point.error_inconsistency Lt u v (get_explanation false v u g) + + let empty = + { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + + (* Normalization *) + + (** [normalize g] returns a graph where all edges point + directly to the canonical representent of their target. The output + graph should be equivalent to the input graph from a logical point + of view, but optimized. We maintain the invariant that the key of + a [Canonical] element is its own name, by keeping [Equiv] edges. *) + let normalize g = + let g = + { g with + entries = PMap.map (fun entry -> + match entry with + | Equiv u -> Equiv ((repr g u).canon) + | Canonical ucan -> Canonical { ucan with rank = 1 }) + g.entries } + in + PMap.fold (fun _ u g -> + match u with + | Equiv _u -> g + | Canonical u -> + let _, u, g = get_ltle g u in + let _, _, g = get_gtge g u in + g) + g.entries g + + let constraints_of g = + let module UF = Unionfind.Make (PSet) (PMap) in + let uf = UF.create () in + let constraints_of u v acc = + match v with + | Canonical {canon=u; ltle; _} -> + PMap.fold (fun v strict acc-> + let typ = if strict then Lt else Le in + Constraint.add (u,typ,v) acc) ltle acc + | Equiv v -> UF.union u v uf; acc + in + let csts = PMap.fold constraints_of g.entries Constraint.empty in + csts, UF.partition uf + + (* domain g.entries = kept + removed *) + let constraints_for ~kept g = + (* rmap: partial map from canonical points to kept points *) + let rmap, csts = PSet.fold (fun u (rmap,csts) -> + let arcu = repr g u in + if PSet.mem arcu.canon kept then + PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts + else + match PMap.find arcu.canon rmap with + | v -> rmap, Constraint.add (u,Eq,v) csts + | exception Not_found -> PMap.add arcu.canon u rmap, csts) + kept (PMap.empty,Constraint.empty) + in + let rec add_from u csts todo = match todo with + | [] -> csts + | (v,strict)::todo -> + let v = repr g v in + (match PMap.find v.canon rmap with + | v -> + let d = if strict then Lt else Le in + let csts = Constraint.add (u,d,v) csts in + add_from u csts todo + | exception Not_found -> + (* v is not equal to any kept point *) + let todo = PMap.fold (fun v' strict' todo -> + (v',strict || strict') :: todo) + v.ltle todo + in + add_from u csts todo) + in + PSet.fold (fun u csts -> + let arc = repr g u in + PMap.fold (fun v strict csts -> add_from u csts [v,strict]) + arc.ltle csts) + kept csts + + let domain g = PMap.domain g.entries + + let choose p g u = + let exception Found of Point.t in + let ru = (repr g u).canon in + if p ru then Some ru + else + try PMap.iter (fun v -> function + | Canonical _ -> () (* we already tried [p ru] *) + | Equiv v' -> + let rv = (repr g v').canon in + if rv == ru && p v then raise (Found v) + (* NB: we could also try [p v'] but it will come up in the + rest of the iteration regardless. *) + ) g.entries; None + with Found v -> Some v + + let sort make_dummy first g = + let cans = + PMap.fold (fun _ u l -> + match u with + | Equiv _ -> l + | Canonical can -> can :: l + ) g.entries [] + in + let cans = List.sort topo_compare cans in + let lowest = + PMap.mapi (fun u _ -> if CList.mem_f Point.equal u first then 0 else 2) + (PMap.filter + (fun _ u -> match u with Equiv _ -> false | Canonical _ -> true) + g.entries) + in + let lowest = + List.fold_left (fun lowest can -> + let lvl = PMap.find can.canon lowest in + PMap.fold (fun u' strict lowest -> + let cost = if strict then 1 else 0 in + let u' = (repr g u').canon in + PMap.modify u' (fun _ lvl0 -> max lvl0 (lvl+cost)) lowest) + can.ltle lowest) + lowest cans + in + let max_lvl = PMap.fold (fun _ a b -> max a b) lowest 0 in + let types = Array.init (max_lvl + 1) (fun i -> + match List.nth_opt first i with + | Some u -> u + | None -> make_dummy (i-2)) + in + let g = Array.fold_left (fun g u -> + let g, u = safe_repr g u in + change_node g { u with rank = big_rank }) g types + in + let g = if max_lvl > List.length first && not (CList.is_empty first) then + enforce_lt (CList.last first) types.(List.length first) g + else g + in + let g = + PMap.fold (fun u lvl g -> enforce_eq u (types.(lvl)) g) + lowest g + in + normalize g + + (** Pretty-printing *) + + let pr_pmap sep pr map = + let cmp (u,_) (v,_) = Point.compare u v in + Pp.prlist_with_sep sep pr (List.sort cmp (PMap.bindings map)) + + let pr_arc prl = let open Pp in + function + | _, Canonical {canon=u; ltle; _} -> + if PMap.is_empty ltle then mt () + else + prl u ++ str " " ++ + v 0 + (pr_pmap spc (fun (v, strict) -> + (if strict then str "< " else str "<= ") ++ prl v) + ltle) ++ + fnl () + | u, Equiv v -> + prl u ++ str " = " ++ prl v ++ fnl () + + let pr prl g = + pr_pmap Pp.mt (pr_arc prl) g.entries + + (* Dumping constraints to a file *) + + let dump output g = + let dump_arc u = function + | Canonical {canon=u; ltle; _} -> + PMap.iter (fun v strict -> + let typ = if strict then Lt else Le in + output typ u v) ltle; + | Equiv v -> + output Eq u v + in + PMap.iter dump_arc g.entries + +end diff --git a/lib/acyclicGraph.mli b/lib/acyclicGraph.mli new file mode 100644 index 0000000000..b53a4c018f --- /dev/null +++ b/lib/acyclicGraph.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Graphs representing strict orders *) + +type constraint_type = Lt | Le | Eq + +module type Point = sig + type t + + module Set : CSig.SetS with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set + + module Constraint : CSet.S with type elt = (t * constraint_type * t) + + val equal : t -> t -> bool + val compare : t -> t -> int + + type explanation = (constraint_type * t) list + val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a + + val pr : t -> Pp.t +end + +module Make (Point:Point) : sig + + type t + + val empty : t + + val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit + + exception AlreadyDeclared + val add : ?rank:int -> Point.t -> t -> t + (** All points must be pre-declared through this function before + they can be mentioned in the others. NB: use a large [rank] to + keep the node canonical *) + + exception Undeclared of Point.t + val check_declared : t -> Point.Set.t -> unit + (** @raise Undeclared if one of the points is not present in the graph. *) + + type 'a check_function = t -> 'a -> 'a -> bool + + val check_eq : Point.t check_function + val check_leq : Point.t check_function + val check_lt : Point.t check_function + + val enforce_eq : Point.t -> Point.t -> t -> t + val enforce_leq : Point.t -> Point.t -> t -> t + val enforce_lt : Point.t -> Point.t -> t -> t + + val constraints_of : t -> Point.Constraint.t * Point.Set.t list + + val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t + + val domain : t -> Point.Set.t + + val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option + + val sort : (int -> Point.t) -> Point.t list -> t -> t + (** [sort mk first g] builds a totally ordered graph. The output + graph should imply the input graph (and the implication will be + strict most of the time), but is not necessarily minimal. The + lowest points in the result are identified with [first]. + Moreover, it adds levels [Type.n] to identify the points (not in + [first]) at level n. An artificial constraint (last first < mk + (length first)) is added to ensure that they are not merged. + Note: the result is unspecified if the input graph already + contains [mk n] nodes. *) + + val pr : (Point.t -> Pp.t) -> t -> Pp.t + + val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit +end diff --git a/lib/aux_file.ml b/lib/aux_file.ml new file mode 100644 index 0000000000..0f9476605b --- /dev/null +++ b/lib/aux_file.ml @@ -0,0 +1,98 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* The file format is a header + * ("COQAUX%d %s %s\n" version hex_hash path) + * followed by an arbitrary number of entries + * ("%d %d %s %S\n" loc_begin loc_end key value) *) + +open Filename + +let version = 1 + +let oc = ref None + +let aux_file_name_for vfile = + dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" + +let mk_absolute vfile = + let vfile = CUnix.remove_path_dot vfile in + if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ()) + else vfile + +let start_aux_file ~aux_file:output_file ~v_file = + let vfile = mk_absolute v_file in + oc := Some (open_out output_file); + Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n" + version (Digest.to_hex (Digest.file vfile)) vfile + +let stop_aux_file () = + close_out (Option.get !oc); + oc := None + +let recording () = not (Option.is_empty !oc) + +module H = Map.Make(struct type t = int * int let compare = compare end) +module M = Map.Make(String) +type data = string M.t +type aux_file = data H.t + +let contents x = x + +let empty_aux_file = H.empty + +let get ?loc aux key = M.find key (H.find (Option.cata Loc.unloc (0,0) loc) aux) + +let record_in_aux_at ?loc key v = + Option.iter (fun oc -> + match loc with + | Some loc -> let i, j = Loc.unloc loc in + Printf.fprintf oc "%d %d %s %S\n" i j key v + | None -> Printf.fprintf oc "0 0 %s %S\n" key v + ) !oc + +let current_loc : Loc.t option ref = ref None + +let record_in_aux_set_at ?loc () = current_loc := loc + +let record_in_aux key v = record_in_aux_at ?loc:!current_loc key v + +let set h loc k v = + let m = try H.find loc h with Not_found -> M.empty in + H.add loc (M.add k v m) h + +let load_aux_file_for vfile = + let vfile = mk_absolute vfile in + let ret3 x y z = x, y, z in + let ret4 x y z t = x, y, z, t in + let h = ref empty_aux_file in + let add loc k v = h := set !h loc k v in + let aux_fname = aux_file_name_for vfile in + try + let ib = Scanf.Scanning.from_channel (open_in aux_fname) in + let ver, hash, fname = + Scanf.bscanf ib "COQAUX%d %s %s\n" ret3 in + if ver <> version then raise (Failure "aux file version mismatch"); + if fname <> vfile then + raise (Failure "aux file name mismatch"); + let only_dummyloc = Digest.to_hex (Digest.file vfile) <> hash in + while true do + let i, j, k, v = Scanf.bscanf ib "%d %d %s %S\n" ret4 in + if not only_dummyloc || (i = 0 && j = 0) then add (i,j) k v; + done; + raise End_of_file + with + | End_of_file -> !h + | Sys_error s | Scanf.Scan_failure s + | Failure s | Invalid_argument s -> + Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s); + empty_aux_file + +let set ?loc h k v = set h (Option.cata Loc.unloc (0,0) loc) k v diff --git a/lib/aux_file.mli b/lib/aux_file.mli new file mode 100644 index 0000000000..efdd75fd39 --- /dev/null +++ b/lib/aux_file.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type aux_file + +val load_aux_file_for : string -> aux_file +val empty_aux_file : aux_file +val get : ?loc:Loc.t -> aux_file -> string -> string +val set : ?loc:Loc.t -> aux_file -> string -> string -> aux_file + +module H : Map.S with type key = int * int +module M : Map.S with type key = string +val contents : aux_file -> string M.t H.t + +val aux_file_name_for : string -> string +val start_aux_file : aux_file:string -> v_file:string -> unit +val stop_aux_file : unit -> unit +val recording : unit -> bool + +val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit +val record_in_aux : string -> string -> unit +val record_in_aux_set_at : ?loc:Loc.t -> unit -> unit diff --git a/lib/cAst.ml b/lib/cAst.ml new file mode 100644 index 0000000000..e1da072db2 --- /dev/null +++ b/lib/cAst.ml @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The ast type contains generic metadata for AST nodes. *) +type 'a t = { + v : 'a; + loc : Loc.t option; +} + +let make ?loc v = { v; loc } + +let map f n = { n with v = f n.v } +let map_with_loc f n = { n with v = f ?loc:n.loc n.v } +let map_from_loc f l = + let loc, v = l in + { v = f ?loc v ; loc } + +let with_val f n = f n.v +let with_loc_val f n = f ?loc:n.loc n.v diff --git a/lib/cAst.mli b/lib/cAst.mli new file mode 100644 index 0000000000..8443b1af34 --- /dev/null +++ b/lib/cAst.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The ast type contains generic metadata for AST nodes *) +type 'a t = private { + v : 'a; + loc : Loc.t option; +} + +val make : ?loc:Loc.t -> 'a -> 'a t + +val map : ('a -> 'b) -> 'a t -> 'b t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t + +val with_val : ('a -> 'b) -> 'a t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b diff --git a/lib/cErrors.ml b/lib/cErrors.ml new file mode 100644 index 0000000000..79f0a806a7 --- /dev/null +++ b/lib/cErrors.ml @@ -0,0 +1,139 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp + +(** Aliases *) + +let push = Backtrace.add_backtrace + +(* Errors *) + +exception Anomaly of string option * Pp.t (* System errors *) + +let _ = + let pr = function + | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"") + | _ -> None + in + Printexc.register_printer pr + +let make_anomaly ?label pp = + Anomaly (label, pp) + +let anomaly ?loc ?label pp = + Loc.raise ?loc (Anomaly (label, pp)) + +let is_anomaly = function +| Anomaly _ -> true +| _ -> false + +exception UserError of string option * Pp.t (* User errors *) + +let todo s = prerr_string ("TODO: "^s^"\n") + +let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) + +let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) + +exception AlreadyDeclared of Pp.t (* for already declared Schemes *) +let alreadydeclared pps = raise (AlreadyDeclared(pps)) + +exception Timeout + +let handle_stack = ref [] + +exception Unhandled + +let register_handler h = handle_stack := h::!handle_stack + +(** [print_gen] is a general exception printer which tries successively + all the handlers of a list, and finally a [bottom] handler if all + others have failed *) + +let rec print_gen bottom stk e = + match stk with + | [] -> bottom e + | h::stk' -> + try h e + with + | Unhandled -> print_gen bottom stk' e + | any -> print_gen bottom stk' any + +(** Only anomalies should reach the bottom of the handler stack. + In usual situation, the [handle_stack] is treated as it if was always + non-empty with [print_anomaly] as its bottom handler. *) + +let where = function +| None -> mt () +| Some s -> + if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () + +let raw_anomaly e = match e with + | Anomaly (s, pps) -> where s ++ pps + | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." + | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." + +let print_backtrace e = match Backtrace.get_backtrace e with +| None -> mt () +| Some bt -> + let bt = Backtrace.repr bt in + let pr_frame f = str (Backtrace.print_frame f) in + let bt = prlist_with_sep fnl pr_frame bt in + fnl () ++ hov 0 bt + +let print_anomaly askreport e = + if askreport then + hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++ + hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") + else + hov 0 (raw_anomaly e) + +(** The standard exception printer *) +let print ?(info = Exninfo.null) e = + print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info + +let iprint (e, info) = print ~info e + +(** Same as [print], except that the "Please report" part of an anomaly + isn't printed (used in Ltac debugging). *) +let print_no_report e = print_gen (print_anomaly false) !handle_stack e +let iprint_no_report (e, info) = + print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info + +(** Predefined handlers **) + +let _ = register_handler begin function + | UserError(s, pps) -> + where s ++ pps + | _ -> raise Unhandled +end + +(** Critical exceptions should not be caught and ignored by mistake + by inner functions during a [vernacinterp]. They should be handled + only at the very end of interp, to be displayed to the user. *) + +[@@@ocaml.warning "-52"] +let noncritical = function + | Sys.Break | Out_of_memory | Stack_overflow + | Assert_failure _ | Match_failure _ | Anomaly _ + | Timeout -> false + | Invalid_argument "equal: functional value" -> false + | _ -> true +[@@@ocaml.warning "+52"] + +(** Check whether an exception is handled *) + +exception Bottom + +let handled e = + let bottom _ = raise Bottom in + try let _ = print_gen bottom !handle_stack e in true + with Bottom -> false diff --git a/lib/cErrors.mli b/lib/cErrors.mli new file mode 100644 index 0000000000..4e2fe7621d --- /dev/null +++ b/lib/cErrors.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This modules implements basic manipulations of errors for use + throughout Coq's code. *) + +(** {6 Error handling} *) + +val push : exn -> Exninfo.iexn +(** Alias for [Backtrace.add_backtrace]. *) + +(** {6 Generic errors.} + + [Anomaly] is used for system errors and [UserError] for the + user's ones. *) + +val make_anomaly : ?label:string -> Pp.t -> exn +(** Create an anomaly. *) + +val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a +(** Raise an anomaly, with an optional location and an optional + label identifying the anomaly. *) + +val is_anomaly : exn -> bool +(** Check whether a given exception is an anomaly. + This is mostly provided for compatibility. Please avoid doing specific + tricks with anomalies thanks to it. See rather [noncritical] below. *) + +exception UserError of string option * Pp.t +(** Main error signaling exception. It carries a header plus a pretty printing + doc *) + +val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a +(** Main error raising primitive. [user_err ?loc ?hdr pp] signals an + error [pp] with optional header and location [hdr] [loc] *) + +exception AlreadyDeclared of Pp.t +val alreadydeclared : Pp.t -> 'a + +val invalid_arg : ?loc:Loc.t -> string -> 'a + +(** [todo] is for running of an incomplete code its implementation is + "do nothing" (or print a message), but this function should not be + used in a released code *) + +val todo : string -> unit + +exception Timeout + +(** [register_handler h] registers [h] as a handler. + When an expression is printed with [print e], it + goes through all registered handles (the most + recent first) until a handle deals with it. + + Handles signal that they don't deal with some exception + by raising [Unhandled]. + + Handles can raise exceptions themselves, in which + case, the exception is passed to the handles which + were registered before. + + The exception that are considered anomalies should not be + handled by registered handlers. +*) + +exception Unhandled + +val register_handler : (exn -> Pp.t) -> unit + +(** The standard exception printer *) +val print : ?info:Exninfo.info -> exn -> Pp.t +val iprint : Exninfo.iexn -> Pp.t + +(** Same as [print], except that the "Please report" part of an anomaly + isn't printed (used in Ltac debugging). *) +val print_no_report : exn -> Pp.t +val iprint_no_report : Exninfo.iexn -> Pp.t + +(** Critical exceptions should not be caught and ignored by mistake + by inner functions during a [vernacinterp]. They should be handled + only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user. + Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... +*) +val noncritical : exn -> bool + +(** Check whether an exception is handled by some toplevel printer. The + [Anomaly] exception is never handled. *) +val handled : exn -> bool diff --git a/lib/cProfile.ml b/lib/cProfile.ml new file mode 100644 index 0000000000..07a1145021 --- /dev/null +++ b/lib/cProfile.ml @@ -0,0 +1,716 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let word_length = Sys.word_size / 8 + +let float_of_time t = float_of_int t /. 100. +let time_of_float f = int_of_float (f *. 100.) + +let get_time () = + time_of_float (Sys.time ()) + +(* Since ocaml 3.01, gc statistics are in float *) +let get_alloc () = + (* If you are unlucky, a minor collection can occur between the *) + (* measurements and produces allocation; we trigger a minor *) + (* collection in advance to be sure the measure is not corrupted *) + Gc.minor (); + Gc.allocated_bytes () + +(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *) +(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *) + +let get_alloc_overhead = + let mark1 = get_alloc () in + let mark2 = get_alloc () in + let mark3 = get_alloc () in + (* If you are unlucky, a major collection can occur between the *) + (* measurements; with two measures the risk decreases *) + min (mark2 -. mark1) (mark3 -. mark2) + +let last_alloc = ref 0.0 (* set by init_profile () *) + +let spent_alloc () = + let now = get_alloc () in + let before = !last_alloc in + last_alloc := now; + now -. before -. get_alloc_overhead + +(* Profile records *) + +type profile_key = { + mutable owntime : int; + mutable tottime : int; + mutable ownalloc : float; + mutable totalloc : float; + mutable owncount : int; + mutable intcount : int; + mutable immcount : int; +} + +let create_record () = { + owntime=0; + tottime=0; + ownalloc=0.0; + totalloc=0.0; + owncount=0; + intcount=0; + immcount=0 +} + +let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw +let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw + +let reset_record (n,e) = + e.owntime <- 0; + e.tottime <- 0; + e.ownalloc <- 0.0; + e.totalloc <- 0.0; + e.owncount <- 0; + e.intcount <- 0; + e.immcount <- 0 + +(* Profile tables *) + +let prof_table = ref [] +let stack = ref [] +let init_time = ref 0 +let init_alloc = ref 0.0 + +let reset_profile () = List.iter reset_record !prof_table + +let init_profile () = + (* We test Flags.profile as a way to support declaring profiled + functions in plugins *) + if !prof_table <> [] || Flags.profile then begin + let outside = create_record () in + stack := [outside]; + last_alloc := get_alloc (); + init_alloc := !last_alloc; + init_time := get_time (); + outside.tottime <- - !init_time; + outside.owntime <- - !init_time + end + +let ajoute n o = + o.owntime <- o.owntime + n.owntime; + o.tottime <- o.tottime + n.tottime; + ajoute_ownalloc o n.ownalloc; + ajoute_totalloc o n.totalloc; + o.owncount <- o.owncount + n.owncount; + o.intcount <- o.intcount + n.intcount; + o.immcount <- o.immcount + n.immcount + +let ajoute_to_list ((name,n) as e) l = + try ajoute n (List.assoc name l); l + with Not_found -> e::l + +let magic = 1249 + +let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = + let (old_table, old_outside, old_total) = + try + let c = open_in filename in + if input_binary_int c <> magic + then Printf.printf "Incompatible recording file: %s\n" filename; + let old_data = input_value c in + close_in c; + old_data + with Sys_error msg -> + (Printf.printf "Unable to open %s: %s\n" filename msg; + new_data) in + let updated_data = + let updated_table = List.fold_right ajoute_to_list curr_table old_table in + ajoute curr_outside old_outside; + ajoute curr_total old_total; + (updated_table, old_outside, old_total) in + begin + (try + let c = + open_out_gen + [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in + output_binary_int c magic; + output_value c updated_data; + close_out c + with Sys_error _ -> Printf.printf "Unable to create recording file"); + updated_data + end + +(************************************************) +(* Compute a rough estimation of time overheads *) + +(* Time and space are not measured in the same way *) + +(* Byte allocation is an exact number and for long runs, the total + number of allocated bytes may exceed the maximum integer capacity + (2^31 on 32-bits architectures); therefore, allocation is measured + by small steps, total allocations are computed by adding elementary + measures and carries are controlled from step to step *) + +(* Unix measure of time is approximate and short delays are often + unperceivable; therefore, total times are measured in one (big) + step to avoid rounding errors and to get the best possible + approximation. + Note: Sys.time is the same as: + Unix.(let x = times () in x.tms_utime +. x.tms_stime) + *) + +(* +---------- start profile for f1 +overheadA| ... + ---------- [1w1] 1st call to get_time for f1 + overheadB| ... + ---------- start f1 + real 1 | ... + ---------- start profile for 1st call to f2 inside f1 + overheadA| ... + ---------- [2w1] 1st call to get_time for 1st f2 + overheadB| ... + ---------- start 1st f2 + real 2 | ... + ---------- end 1st f2 + overheadC| ... + ---------- [2w1] 2nd call to get_time for 1st f2 + overheadD| ... + ---------- end profile for 1st f2 + real 1 | ... + ---------- start profile for 2nd call to f2 inside f1 + overheadA| ... + ---------- [2'w1] 1st call to get_time for 2nd f2 + overheadB| ... + ---------- start 2nd f2 + real 2' | ... + ---------- end 2nd f2 + overheadC| ... + ---------- [2'w2] 2nd call to get_time for 2nd f2 + overheadD| ... + ---------- end profile for f2 + real 1 | ... + ---------- end f1 + overheadC| ... +---------- [1w1'] 2nd call to get_time for f1 +overheadD| ... +---------- end profile for f1 + +When profiling f2, overheadB + overheadC should be subtracted from measure +and overheadA + overheadB + overheadC + overheadD should be subtracted from +the amount for f1 + +Then the relevant overheads are : + + "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and + + "overheadA + overheadB + overheadC + overheadD" to be subtracted to + the measure of f as many time as f calls a profiled function (itself + included) +*) + +let dummy_last_alloc = ref 0.0 +let dummy_spent_alloc () = + let now = get_alloc () in + let before = !last_alloc in + last_alloc := now; + now -. before +let dummy_f x = x +let dummy_stack = ref [create_record ()] +let dummy_ov = 0 + +let loops = 10000 + +let time_overhead_A_D () = + let e = create_record () in + let before = get_time () in + for _i = 1 to loops do + (* This is a copy of profile1 for overhead estimation *) + let dw = dummy_spent_alloc () in + match !dummy_stack with [] -> assert false | p::_ -> + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let dt = get_time () - 1 in + e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime; + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + p.owntime <- p.owntime - e.tottime; + ajoute_totalloc p (e.totalloc-.totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !dummy_stack with [] -> assert false | _::s -> stack := s); + dummy_last_alloc := get_alloc () + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let time_overhead_B_C () = + let dummy_x = 0 in + let before = get_time () in + for _i = 1 to loops do + try + dummy_last_alloc := get_alloc (); + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in + () + with e when CErrors.noncritical e -> assert false + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let compute_alloc lo = lo /. (float_of_int word_length) + +(************************************************) +(* End a profiling session and print the result *) + +let format_profile (table, outside, total) = + print_newline (); + Printf.printf + "%-23s %9s %9s %10s %10s %10s\n" + "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; + let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in + List.iter (fun (name,e) -> + Printf.printf + "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" + name + (float_of_time e.owntime) (float_of_time e.tottime) + (compute_alloc e.ownalloc) + (compute_alloc e.totalloc) + e.owncount e.intcount) + l; + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" + "others" + (float_of_time outside.owntime) (float_of_time outside.tottime) + (compute_alloc outside.ownalloc) + (compute_alloc outside.totalloc) + outside.intcount; + (* Here, own contains overhead time/alloc *) + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n" + "Est. overhead/total" + (float_of_time total.owntime) (float_of_time total.tottime) + (compute_alloc total.ownalloc) + (compute_alloc total.totalloc); + Printf.printf + "Time in seconds and allocation in words (1 word = %d bytes)\n" + word_length + +let recording_file = ref "" +let set_recording s = recording_file := s + +let adjust_time ov_bc ov_ad e = + let bc_imm = float_of_int e.owncount *. ov_bc in + let ad_imm = float_of_int e.immcount *. ov_ad in + let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in + {e with + tottime = e.tottime - int_of_float (abcd_all +. bc_imm); + owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } + +let close_profile print = + if !prof_table <> [] then begin + let dw = spent_alloc () in + let t = get_time () in + match !stack with + | [outside] -> + outside.tottime <- outside.tottime + t; + outside.owntime <- outside.owntime + t; + ajoute_ownalloc outside dw; + ajoute_totalloc outside dw; + let ov_bc = time_overhead_B_C () (* B+C overhead *) in + let ov_ad = time_overhead_A_D () (* A+D overhead *) in + let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in + let adjtable = List.map adjust !prof_table in + let adjoutside = adjust_time ov_bc ov_ad outside in + let totalloc = !last_alloc -. !init_alloc in + let total = create_record () in + total.tottime <- outside.tottime; + total.totalloc <- totalloc; + (* We compute estimations of overhead, put into "own" fields *) + total.owntime <- outside.tottime - adjoutside.tottime; + total.ownalloc <- totalloc -. outside.totalloc; + let current_data = (adjtable, adjoutside, total) in + let updated_data = + match !recording_file with + | "" -> current_data + | name -> merge_profile !recording_file current_data + in + if print then format_profile updated_data; + init_profile () + | _ -> failwith "Inconsistency" + end + +let print_profile () = close_profile true + +let declare_profile name = + if name = "___outside___" || name = "___total___" then + failwith ("Error: "^name^" is a reserved keyword"); + let e = create_record () in + prof_table := (name,e)::!prof_table; + e + +(******************************) +(* Entry points for profiling *) +let profile1 e f a = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile2 e f a b = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile3 e f a b c = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile4 e f a b c d = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile5 e f a b c d g = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile6 e f a b c d g h = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile7 e f a b c d g h i = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile8 e f a b c d g h i j = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i j in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let print_logical_stats a = + let (c, s, d) = CObj.obj_stats a in + Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d + +let print_stats a = + let (c1, s, d) = CObj.obj_stats a in + let c2 = CObj.size a in + Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n" + c2 (s + c1) d +(* +let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 } +*) diff --git a/lib/cProfile.mli b/lib/cProfile.mli new file mode 100644 index 0000000000..764faf8d1a --- /dev/null +++ b/lib/cProfile.mli @@ -0,0 +1,121 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** {6 This program is a small time and allocation profiler for Objective Caml } *) + +(** Adapted from Christophe Raffalli *) + +(** To use it, link it with the program you want to profile. + +To trace a function "f" you first need to get a key for it by using : + +let fkey = declare_profile "f";; + +(the string is used to print the profile infomation). Warning: this +function does a side effect. Choose the ident you want instead "fkey". + +Then if the function has ONE argument add the following just after +the definition of "f" or just after the declare_profile if this one +follows the definition of f. + +let f = profile1 fkey f;; + +If f has two arguments do the same with profile2, idem with 3, ... +For more arguments than provided in this module, make a new copy of +function profile and adapt for the needed arity. + +If you want to profile two mutually recursive functions, you had better +to rename them : + +let fkey = declare_profile "f";; +let gkey = declare_profile "g";; +let f' = .... f' ... g' +and g' = .... f' .... g' +;; + +let f = profile fkey f';; +let g = profile gkey g';; + +Before the program quits, you should call "print_profile ();;". It +produces a result of the following kind: + +Function name Own time Total time Own alloc Tot. alloc Calls +f 0.28 0.47 116 116 5 4 +h 0.19 0.19 0 0 4 0 +g 0.00 0.00 0 0 0 0 +others 0.00 0.47 392 508 9 +Est. overhead/total 0.00 0.47 2752 3260 + +- The first column is the name of the function. +- The third column give the time (utime + stime) spent inside the function. +- The second column give the time spend inside the function minus the + time spend in other profiled functions called by it +- The 4th and 5th columns give the same for allocated words +- The 6th and 7th columns give the number of calls to the function and + the number of calls to profiled functions inside the scope of the + current function + +Remarks: + +- If a function has a polymorphic type, you need to supply it with at + least one argument as in "let f a = profile1 fkey f a;;" (instead of + "let f = profile1 fkey f;;") in order to get generalization of the + type. +- Each line of the form "let f a = profile1 fkey f a;;" in your code + counts for 5 words and each line of the form "let f + = profile1 fkey f;;" counts for 6 words (a word is 4 or 8 bytes + according to the architecture); this is counted for "others". +- Time fields for functions doing a little job is usually non pertinent. + +i*) + +type profile_key + +val set_recording : string -> unit + +val print_profile : unit -> unit +val reset_profile : unit -> unit +val init_profile : unit -> unit +val declare_profile : string -> profile_key + +val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b +val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c +val profile3 : + profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd +val profile4 : + profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e +val profile5 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f +val profile6 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g +val profile7 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h +val profile8 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i + + +(** Some utilities to compute the logical and physical sizes and depth + of ML objects *) + +(** Print logical size (in words) and depth of its argument + This function does not disturb the heap *) +val print_logical_stats : 'a -> unit + +(** Print physical size, logical size (in words) and depth of its argument + This function allocates itself a lot (the same order of magnitude + as the physical size of its argument) *) +val print_stats : 'a -> unit diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml new file mode 100644 index 0000000000..f199e2e608 --- /dev/null +++ b/lib/cWarnings.ml @@ -0,0 +1,175 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type status = + Disabled | Enabled | AsError + +type t = { + default : status; + category : string; + status : status; +} + +let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 +let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 + +let flags = ref "" + +let get_flags () = !flags + +let add_warning_in_category ~name ~category = + let ws = + try + Hashtbl.find categories category + with Not_found -> [] + in + Hashtbl.replace categories category (name::ws) + +let set_warning_status ~name status = + try + let w = Hashtbl.find warnings name in + Hashtbl.replace warnings name { w with status = status } + with Not_found -> () + +let reset_default_warnings () = + Hashtbl.iter (fun name w -> + Hashtbl.replace warnings name { w with status = w.default }) + warnings + +let set_all_warnings_status status = + Hashtbl.iter (fun name w -> + Hashtbl.replace warnings name { w with status }) + warnings + +let set_category_status ~name status = + let names = Hashtbl.find categories name in + List.iter (fun name -> set_warning_status ~name status) names + +let is_all_keyword name = CString.equal name "all" +let is_none_keyword s = CString.equal s "none" + +let parse_flag s = + if String.length s > 1 then + match String.get s 0 with + | '+' -> (AsError, String.sub s 1 (String.length s - 1)) + | '-' -> (Disabled, String.sub s 1 (String.length s - 1)) + | _ -> (Enabled, s) + else CErrors.user_err Pp.(str "Invalid warnings flag") + +let string_of_flag (status,name) = + match status with + | AsError -> "+" ^ name + | Disabled -> "-" ^ name + | Enabled -> name + +let string_of_flags flags = + String.concat "," (List.map string_of_flag flags) + +let set_status ~name status = + if is_all_keyword name then + set_all_warnings_status status + else + try + set_category_status ~name status + with Not_found -> + try + set_warning_status ~name status + with Not_found -> () + +let split_flags s = + let reg = Str.regexp "[ ,]+" in Str.split reg s + +(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the + "all" flag, and reverses the list. *) +let rec cut_before_all_rev acc = function + | [] -> acc + | (status,name as w) :: warnings -> + let acc = + if is_all_keyword name then [w] + else if is_none_keyword name then [(Disabled,"all")] + else w :: acc in + cut_before_all_rev acc warnings + +let cut_before_all_rev warnings = cut_before_all_rev [] warnings + +(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of + themselves or their categories, and reverses the list. *) +let uniquize_flags_rev flags = + let rec aux acc visited = function + | (_,name as flag)::flags -> + if CString.Set.mem name visited then aux acc visited flags else + let visited = + try + let warnings = Hashtbl.find categories name in + List.fold_left (fun v w -> CString.Set.add w v) visited warnings + with Not_found -> + visited + in + aux (flag::acc) (CString.Set.add name visited) flags + | [] -> acc + in aux [] CString.Set.empty flags + +(** [normalize_flags] removes redundant warnings. Unknown warnings are kept + because they may be declared in a plugin that will be linked later. *) +let normalize_flags warnings = + let warnings = cut_before_all_rev warnings in + uniquize_flags_rev warnings + +let flags_of_string s = List.map parse_flag (split_flags s) + +let normalize_flags_string s = + if is_none_keyword s then s + else + let flags = flags_of_string s in + let flags = normalize_flags flags in + string_of_flags flags + +let parse_warnings items = + CList.iter (fun (status, name) -> set_status ~name status) items + +(* For compatibility, we accept "none" *) +let parse_flags s = + if is_none_keyword s then begin + Flags.make_warn false; + set_all_warnings_status Disabled; + "none" + end + else begin + Flags.make_warn true; + let flags = flags_of_string s in + let flags = normalize_flags flags in + parse_warnings flags; + string_of_flags flags + end + +let set_flags s = + reset_default_warnings (); let s = parse_flags s in flags := s + +(* Adds a warning to the [warnings] and [category] tables. We then reparse the + warning flags string, because the warning being created might have been set + already. *) +let create ~name ~category ?(default=Enabled) pp = + let pp x = let open Pp in + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ + str category ++ str "]" + in + Hashtbl.replace warnings name { default; category; status = default }; + add_warning_in_category ~name ~category; + if default <> Disabled then + add_warning_in_category ~name ~category:"default"; + (* We re-parse and also re-normalize the flags, because the category of the + new warning is now known. *) + set_flags !flags; + fun ?loc x -> + let w = Hashtbl.find warnings name in + match w.status with + | Disabled -> () + | AsError -> CErrors.user_err ?loc (pp x) + | Enabled -> Feedback.msg_warning ?loc (pp x) diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli new file mode 100644 index 0000000000..f97a53c4d7 --- /dev/null +++ b/lib/cWarnings.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type status = Disabled | Enabled | AsError + +val create : name:string -> category:string -> ?default:status -> + ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit + +val get_flags : unit -> string +val set_flags : string -> unit + +(** Cleans up a user provided warnings status string, e.g. removing unknown + warnings (in which case a warning is emitted) or subsumed warnings . *) +val normalize_flags_string : string -> string diff --git a/lib/control.ml b/lib/control.ml new file mode 100644 index 0000000000..9054507e46 --- /dev/null +++ b/lib/control.ml @@ -0,0 +1,109 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(*s interruption *) + +let interrupt = ref false + +let steps = ref 0 + +let enable_thread_delay = ref false + +let check_for_interrupt () = + if !interrupt then begin interrupt := false; raise Sys.Break end; + incr steps; + if !enable_thread_delay && !steps = 1000 then begin + Thread.delay 0.001; + steps := 0; + end + +(** This function does not work on windows, sigh... *) +let unix_timeout n f x e = + let timeout_handler _ = raise e in + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + let _ = Unix.alarm n in + let restore_timeout () = + let _ = Unix.alarm 0 in + Sys.set_signal Sys.sigalrm psh + in + try + let res = f x in + restore_timeout (); + res + with e -> + let e = Backtrace.add_backtrace e in + restore_timeout (); + Exninfo.iraise e + +let windows_timeout n f x e = + let killed = ref false in + let exited = ref false in + let thread init = + while not !killed do + let cur = Unix.gettimeofday () in + if float_of_int n <= cur -. init then begin + interrupt := true; + exited := true; + Thread.exit () + end; + Thread.delay 0.5 + done + in + let init = Unix.gettimeofday () in + let _id = CThread.create thread init in + try + let res = f x in + let () = killed := true in + let cur = Unix.gettimeofday () in + (* The thread did not interrupt, but the computation took longer than + expected. *) + let () = if float_of_int n <= cur -. init then begin + exited := true; + raise Sys.Break + end in + res + with + | Sys.Break -> + (* Just in case, it could be a regular Ctrl+C *) + if not !exited then begin killed := true; raise Sys.Break end + else raise e + | e -> + let () = killed := true in + let e = Backtrace.add_backtrace e in + Exninfo.iraise e + +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } + +let timeout_fun = match Sys.os_type with +| "Unix" | "Cygwin" -> { timeout = unix_timeout } +| _ -> { timeout = windows_timeout } + +let timeout_fun_ref = ref timeout_fun +let set_timeout f = timeout_fun_ref := f + +let timeout n f e = !timeout_fun_ref.timeout n f e + +let protect_sigalrm f x = + let timed_out = ref false in + let timeout_handler _ = timed_out := true in + try + let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + try + let res = f x in + Sys.set_signal Sys.sigalrm old_handler; + match !timed_out, old_handler with + | true, Sys.Signal_handle f -> f Sys.sigalrm; res + | _, _ -> res + with e -> + let e = Backtrace.add_backtrace e in + Sys.set_signal Sys.sigalrm old_handler; + Exninfo.iraise e + with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) + f x diff --git a/lib/control.mli b/lib/control.mli new file mode 100644 index 0000000000..640d41a4f7 --- /dev/null +++ b/lib/control.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Global control of Coq. *) + +(** Will periodically call [Thread.delay] if set to true *) +val enable_thread_delay : bool ref + +val interrupt : bool ref +(** Coq interruption: set the following boolean reference to interrupt Coq + (it eventually raises [Break], simulating a Ctrl-C) *) + +val check_for_interrupt : unit -> unit +(** Use this function as a potential yield function. If {!interrupt} has been + set, il will raise [Sys.Break]. *) + +val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b +(** [timeout n f x e] tries to compute [f x], and if it fails to do so + before [n] seconds, it raises [e] instead. *) + +(** Set a particular timeout function; warning, this is an internal + API and it is scheduled to go away. *) +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +val set_timeout : timeout -> unit + +(** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that + computation, the signal handler is executed only once the computation is + terminated. Otherwise said, it makes the execution of [f] atomic w.r.t. + handling of SIGALRM. + + This is useful for example to prevent the implementation of `Timeout` to + interrupt I/O routines, generating ill-formed output. + +*) +val protect_sigalrm : ('a -> 'b) -> 'a -> 'b diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml new file mode 100644 index 0000000000..d908baa1e8 --- /dev/null +++ b/lib/coqProject_file.ml @@ -0,0 +1,281 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This needs to go trou feedback as it is invoked from IDEs, but + ideally we would like to make this independent so it can be + bootstrapped. *) + +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + +type project = { + project_file : string option; + makefile : string option; + install_kind : install option; + use_ocamlopt : bool; + + v_files : string sourced list; + mli_files : string sourced list; + mlg_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; + + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target sourced list; + subdirs : string sourced list; +} +and extra_target = { + target : string; + dependencies : string; + phony : bool; + command : string; +} +and logic_path = string +and path = { path : string; canonical_path : string } +and install = + | NoInstall + | TraditionalInstall + | UserInstall + +(* TODO generate with PPX *) +let mk_project project_file makefile install_kind use_ocamlopt = { + project_file; + makefile; + install_kind; + use_ocamlopt; + + v_files = []; + mli_files = []; + mlg_files = []; + ml_files = []; + mllib_files = []; + mlpack_files = []; + extra_targets = []; + subdirs = []; + ml_includes = []; + r_includes = []; + q_includes = []; + extra_args = []; + defs = []; +} + +(********************* utils ********************************************) + +let rec post_canonize f = + if Filename.basename f = Filename.current_dir_name + then let dir = Filename.dirname f in + if dir = Filename.current_dir_name then f else post_canonize dir + else f + +(********************* parser *******************************************) + +exception Parsing_error of string + +let buffer buf = + let ans = Buffer.contents buf in + let () = Buffer.clear buf in + ans + +let rec parse_string buf s = match Stream.next s with +| ' ' | '\n' | '\t' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string buf s +| exception Stream.Failure -> buffer buf + +and parse_string2 buf s = match Stream.next s with +| '"' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string2 buf s +| exception Stream.Failure -> raise (Parsing_error "unterminated string") + +and parse_skip_comment s = match Stream.next s with +| '\n' -> () +| _ -> parse_skip_comment s +| exception Stream.Failure -> () + +and parse_args buf accu s = match Stream.next s with +| ' ' | '\n' | '\t' -> parse_args buf accu s +| '#' -> + let () = parse_skip_comment s in + parse_args buf accu s +| '"' -> + let str = parse_string2 buf s in + parse_args buf (str :: accu) s +| c -> + let () = Buffer.add_char buf c in + let str = parse_string buf s in + parse_args buf (str :: accu) s +| exception Stream.Failure -> accu + +let parse f = + let c = open_in f in + let buf = Buffer.create 64 in + let res = parse_args buf [] (Stream.of_channel c) in + close_in c; + List.rev res +;; + +(* Copy from minisys.ml, since we don't see that file here *) +let exists_dir dir = + let rec strip_trailing_slash dir = + let len = String.length dir in + if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\') + then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in + try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false + + +let process_cmd_line ~warning_fn orig_dir proj args = + let parsing_project_file = ref (proj.project_file <> None) in + let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in + let orig_dir = (* avoids turning foo.v in ./foo.v *) + if orig_dir = "." then "" else orig_dir in + let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in + let mk_path d = + let p = CUnix.correct_path d orig_dir in + { path = CUnix.remove_path_dot (post_canonize p); + canonical_path = CUnix.canonical_path_name p } in + let rec aux proj = function + | [] -> proj + | "-impredicative-set" :: _ -> + error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\"" + | "-no-install" :: _ -> + error "Use \"-install none\" instead of \"-no-install\"" + | "-custom" :: _ -> + error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\"" + + | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r + | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r + | "-install" :: d :: r -> + if proj.install_kind <> None then + (warning_fn "-install set more than once."); + let install = match d with + | "user" -> UserInstall + | "none" -> NoInstall + | "global" -> TraditionalInstall + | _ -> error ("invalid option \""^d^"\" passed to -install") in + aux { proj with install_kind = Some install } r + | "-extra" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = false; command } in + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r + | "-extra-phony" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = true; command } in + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r + + | "-Q" :: d :: lp :: r -> + aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r + | "-I" :: d :: r -> + aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r + | "-R" :: d :: lp :: r -> + aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r + + | "-f" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); + let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in + let () = match proj.project_file with + | None -> () + | Some _ -> warning_fn "Multiple project files are deprecated." + in + parsing_project_file := true; + let proj = aux { proj with project_file = Some file } (parse file) in + parsing_project_file := false; + aux proj r + + | "-o" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); + if String.contains file '/' then + error "Output file must be in the current directory"; + if proj.makefile <> None then + error "Option -o given more than once"; + aux { proj with makefile = Some file } r + | v :: "=" :: def :: r -> + aux { proj with defs = proj.defs @ [sourced (v,def)] } r + | "-arg" :: a :: r -> + aux { proj with extra_args = proj.extra_args @ [sourced a] } r + | f :: r -> + let f = CUnix.correct_path f orig_dir in + let proj = + if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } + else match Filename.extension f with + | ".v" -> + { proj with v_files = proj.v_files @ [sourced f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } + | ".ml4" -> + let msg = Printf.sprintf "camlp5 macro files not supported anymore, please port %s to coqpp" f in + raise (Parsing_error msg) + | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } + | _ -> raise (Parsing_error ("Unknown option "^f)) in + aux proj r + in + aux proj args + + (******************************* API ************************************) + +let cmdline_args_to_project ~warning_fn ~curdir args = + process_cmd_line ~warning_fn curdir (mk_project None None None true) args + +let read_project_file ~warning_fn f = + process_cmd_line ~warning_fn (Filename.dirname f) + (mk_project (Some f) None (Some NoInstall) true) (parse f) + +let rec find_project_file ~from ~projfile_name = + let fname = Filename.concat from projfile_name in + if Sys.file_exists fname then Some fname + else + let newdir = Filename.dirname from in + if newdir = from then None + else find_project_file ~from:newdir ~projfile_name +;; + +let all_files { v_files; ml_files; mli_files; mlg_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files + +let map_sourced_list f l = List.map (fun x -> f x.thing) l +;; + +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + +let coqtop_args_from_project + { ml_includes; r_includes; q_includes; extra_args } += + let map = map_sourced_list in + let args = + map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ + map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ + map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ + [map (fun x -> x) extra_args] in + List.flatten args +;; + +let filter_cmdline l = CList.map_filter + (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) + l +;; + +let forget_source {thing} = thing + +(* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli new file mode 100644 index 0000000000..39c5d019d0 --- /dev/null +++ b/lib/coqProject_file.mli @@ -0,0 +1,68 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +exception Parsing_error of string + +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + +type project = { + project_file : string option; + makefile : string option; + install_kind : install option; + use_ocamlopt : bool; + + v_files : string sourced list; + mli_files : string sourced list; + mlg_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; + + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target sourced list; + subdirs : string sourced list; +} +and extra_target = { + target : string; + dependencies : string; + phony : bool; + command : string; +} +and logic_path = string +and path = { path : string; canonical_path : string } +and install = + | NoInstall + | TraditionalInstall + | UserInstall + +val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project +val read_project_file : warning_fn:(string -> unit) -> string -> project +val coqtop_args_from_project : project -> string list +val find_project_file : from:string -> projfile_name:string -> string option + +val all_files : project -> string sourced list + +val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val filter_cmdline : 'a sourced list -> 'a list + +val forget_source : 'a sourced -> 'a diff --git a/lib/dAst.ml b/lib/dAst.ml new file mode 100644 index 0000000000..803b2a0cff --- /dev/null +++ b/lib/dAst.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CAst + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +let map_thunk (type s) f : (_, s) thunk -> (_, s) thunk = function +| Value x -> Value (f x) +| Thunk k -> Thunk (lazy (f (Lazy.force k))) + +let get_thunk (type s) : ('a, s) thunk -> 'a = function +| Value x -> x +| Thunk k -> Lazy.force k + +let get x = get_thunk x.v + +let make ?loc v = CAst.make ?loc (Value v) + +let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v)) + +let force x = CAst.make ?loc:x.CAst.loc (Value (get_thunk x.v)) + +let map f n = CAst.map (fun x -> map_thunk f x) n + +let map_with_loc f n = + CAst.map_with_loc (fun ?loc x -> map_thunk (fun x -> f ?loc x) x) n + +let map_from_loc f (loc, x) = + make ?loc (f ?loc x) + +let with_val f n = f (get n) + +let with_loc_val f n = f ?loc:n.CAst.loc (get n) diff --git a/lib/dAst.mli b/lib/dAst.mli new file mode 100644 index 0000000000..2f58cfc41f --- /dev/null +++ b/lib/dAst.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Lazy AST node wrapper. Only used for [glob_constr] as of today. *) + +type ('a, _) thunk = +| Value : 'a -> ('a, 'b) thunk +| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk + +type ('a, 'b) t = ('a, 'b) thunk CAst.t + +val get : ('a, 'b) t -> 'a +val get_thunk : ('a, 'b) thunk -> 'a + +val make : ?loc:Loc.t -> 'a -> ('a, 'b) t +val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t +val force : ('a, 'b) t -> ('a, 'b) t + +val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> ('b, 'c) t + +val with_val : ('a -> 'b) -> ('a, 'c) t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> 'b diff --git a/lib/doc.tex b/lib/doc.tex new file mode 100644 index 0000000000..35bd15fa17 --- /dev/null +++ b/lib/doc.tex @@ -0,0 +1,7 @@ + +\newpage +\section*{Utility libraries} + +\ocwsection \label{lib} +This chapter describes the various utility libraries used in the code +of \Coq. diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000000..83783f9b5c --- /dev/null +++ b/lib/dune @@ -0,0 +1,7 @@ +(library + (name lib) + (synopsis "Coq's Utility Library [coq-specific]") + (public_name coq.lib) + (wrapped false) + (modules_without_implementation xml_datatype) + (libraries coq.clib coq.config)) diff --git a/lib/envars.ml b/lib/envars.ml new file mode 100644 index 0000000000..0f4670688b --- /dev/null +++ b/lib/envars.ml @@ -0,0 +1,184 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util + +(** {1 Helper functions} *) + +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + +let safe_getenv warning n = + getenv_else n (fun () -> + warning ("Environment variable "^n^" not found: using '$"^n^"' ."); + ("$"^n) + ) + +let ( / ) a b = + if Filename.is_relative b then a ^ "/" ^ b else b + +let coqify d = d / "coq" + +let home ~warn = + getenv_else "HOME" (fun () -> + try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> + getenv_else "USERPROFILE" (fun () -> + warn ("Cannot determine user home directory, using '.' ."); + Filename.current_dir_name)) + +let path_to_list p = + let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in + String.split_on_char sep p + +let expand_path_macros ~warn s = + let rec expand_atom s i = + let l = String.length s in + if i<l && (Util.is_digit s.[i] || Util.is_letter s.[i] || s.[i] == '_') + then expand_atom s (i+1) + else i in + let rec expand_macros s i = + let l = String.length s in + if Int.equal i l then s else + match s.[i] with + | '$' -> + let n = expand_atom s (i+1) in + let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in + let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in + expand_macros s (i + String.length v) + | '~' when Int.equal i 0 -> + let n = expand_atom s (i+1) in + let v = + if Int.equal n (i + 1) then home ~warn + else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir + in + let s = v^(String.sub s n (l-n)) in + expand_macros s (String.length v) + | c -> expand_macros s (i+1) + in expand_macros s 0 + +(** {1 Paths} *) + +(** {2 Coq paths} *) + +let coqbin = + CUnix.canonical_path_name (Filename.dirname Sys.executable_name) + +(** The following only makes sense when executables are running from + source tree (e.g. during build or in local mode). *) +let coqroot = + Filename.dirname coqbin + +(** On win32, we add coqbin to the PATH at launch-time (this used to be + done in a .bat script). *) +let _ = + if Coq_config.arch_is_win32 then + Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) + +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + +(** [check_file_else ~dir ~file oth] checks if [file] exists in + the installation directory [dir] given relatively to [coqroot], + which maybe has been relocated. + If the check fails, then [oth ()] is evaluated. + Using file system equality seems well enough for this heuristic *) +let check_file_else ~dir ~file oth = + let path = use_suffix coqroot dir in + if Sys.file_exists (path / file) then path else oth () + +let guess_coqlib fail = + getenv_else "COQLIB" (fun () -> + let prelude = "theories/Init/Prelude.vo" in + check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude + (fun () -> + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) + then Coq_config.coqlib + else + fail "cannot guess a path for Coq libraries; please use -coqlib option") + ) + +let coqlib : string option ref = ref None +let set_user_coqlib path = coqlib := Some path + +(** coqlib is now computed once during coqtop initialization *) + +let set_coqlib ~fail = + match !coqlib with + | Some _ -> () + | None -> + let lib = guess_coqlib fail in + coqlib := Some lib + +let coqlib () = Option.default "" !coqlib + +let docdir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.docdirsuffix in + if Sys.file_exists path then path else Coq_config.docdir + +let datadir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.datadirsuffix in + if Sys.file_exists path then path else Coq_config.datadir + +let configdir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.configdirsuffix in + if Sys.file_exists path then path else Coq_config.configdir + +let coqpath = + let coqpath = getenv_else "COQPATH" (fun () -> "") in + let make_search_path path = + let paths = path_to_list path in + let valid_paths = List.filter Sys.file_exists paths in + List.rev valid_paths + in + make_search_path coqpath + +(** {2 Caml paths} *) + +let ocamlfind () = Coq_config.ocamlfind + +(** {1 XDG utilities} *) + +let xdg_data_home warn = + coqify + (getenv_else "XDG_DATA_HOME" (fun () -> (home ~warn) / ".local/share")) + +let xdg_config_home warn = + coqify + (getenv_else "XDG_CONFIG_HOME" (fun () -> (home ~warn) / ".config")) + +let xdg_data_dirs warn = + let sys_dirs = + try + List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS")) + with + | Not_found -> [datadir ()] + in + xdg_data_home warn :: sys_dirs + +let xdg_dirs ~warn = + List.filter Sys.file_exists (xdg_data_dirs warn) + +(* Print the configuration information *) + +let print_config ?(prefix_var_name="") f coq_src_subdirs = + let open Printf in + fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); + fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); + fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); + fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); + fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name + (if Coq_config.has_natdynlink then "true" else "false"); + fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) + diff --git a/lib/envars.mli b/lib/envars.mli new file mode 100644 index 0000000000..ebf86d0650 --- /dev/null +++ b/lib/envars.mli @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This file provides a high-level interface to the environment variables + needed by Coq to run (such as coqlib). The values of these variables + may come from different sources (shell environment variables, + command line options, options set at the time Coq was build). *) + +(** [expand_path_macros warn s] substitutes environment variables + in a string by their values. This function also takes care of + substituting path of the form '~X' by an absolute path. + Use [warn] as a message displayer. *) +val expand_path_macros : warn:(string -> unit) -> string -> string + +(** [home warn] returns the root of the user directory, depending + on the OS. This information is usually stored in the $HOME + environment variable on POSIX shells. If no such variable + exists, then other common names are tried (HOMEDRIVE, HOMEPATH, + USERPROFILE). If all of them fail, [warn] is called. *) +val home : warn:(string -> unit) -> string + +(** [coqlib] is the path to the Coq library. *) +val coqlib : unit -> string + +(** [docdir] is the path to the installed documentation. *) +val docdir : unit -> string + +(** [datadir] is the path to the installed data directory. *) +val datadir : unit -> string + +(** [configdir] is the path to the installed config directory. *) +val configdir : unit -> string + +(** [set_coqlib] must be runned once before any access to [coqlib] *) +val set_coqlib : fail:(string -> string) -> unit + +(** [set_user_coqlib path] sets the coqlib directory explicitedly. *) +val set_user_coqlib : string -> unit + +(** [coqbin] is the name of the current executable. *) +val coqbin : string + +(** [coqroot] is the path to [coqbin]. + The following value only makes sense when executables are running from + source tree (e.g. during build or in local mode). +*) +val coqroot : string + +(** [coqpath] is the standard path to coq. + Notice that coqpath is stored in reverse order, since that is + the order it gets added to the search path. *) +val coqpath : string list + +(** [camlfind ()] is the path to the ocamlfind binary. *) +val ocamlfind : unit -> string + +(** Coq tries to honor the XDG Base Directory Specification to access + the user's configuration files. + + see [http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html] +*) +val xdg_config_home : (string -> unit) -> string +val xdg_data_home : (string -> unit) -> string +val xdg_data_dirs : (string -> unit) -> string list +val xdg_dirs : warn : (string -> unit) -> string list + +(** {6 Prints the configuration information } *) +val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit diff --git a/lib/explore.ml b/lib/explore.ml new file mode 100644 index 0000000000..4dc48ab668 --- /dev/null +++ b/lib/explore.ml @@ -0,0 +1,93 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp + +(*s Definition of a search problem. *) + +module type SearchProblem = sig + type state + val branching : state -> state list + val success : state -> bool + val pp : state -> Pp.t +end + +module Make = functor(S : SearchProblem) -> struct + + type position = int list + + let msg_with_position (p : position) pp = + let rec pp_rec = function + | [] -> mt () + | [i] -> int i + | i :: l -> pp_rec l ++ str "." ++ int i + in + Feedback.msg_debug (h 0 (pp_rec p) ++ pp) + + (*s Depth first search. *) + + let rec depth_first s = + if S.success s then s else depth_first_many (S.branching s) + and depth_first_many = function + | [] -> raise Not_found + | [s] -> depth_first s + | s :: l -> try depth_first s with Not_found -> depth_first_many l + + let debug_depth_first s = + let rec explore p s = + msg_with_position p (S.pp s); + if S.success s then s else explore_many 1 p (S.branching s) + and explore_many i p = function + | [] -> raise Not_found + | [s] -> explore (i::p) s + | s :: l -> + try explore (i::p) s with Not_found -> explore_many (succ i) p l + in + explore [1] s + + (*s Breadth first search. We use functional FIFOS à la Okasaki. *) + + type 'a queue = 'a list * 'a list + + exception Empty + + let empty = [],[] + + let push x (h,t) : _ queue = (x::h,t) + + let pop = function + | h, x::t -> x, (h,t) + | h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty + + let breadth_first s = + let rec explore q = + let (s, q') = try pop q with Empty -> raise Not_found in + enqueue q' (S.branching s) + and enqueue q = function + | [] -> explore q + | s :: l -> if S.success s then s else enqueue (push s q) l + in + enqueue empty [s] + + let debug_breadth_first s = + let rec explore q = + let ((p,s), q') = try pop q with Empty -> raise Not_found in + enqueue 1 p q' (S.branching s) + and enqueue i p q = function + | [] -> + explore q + | s :: l -> + let ps = i::p in + msg_with_position ps (S.pp s); + if S.success s then s else enqueue (succ i) p (push (ps,s) q) l + in + enqueue 1 [] empty [s] + +end diff --git a/lib/explore.mli b/lib/explore.mli new file mode 100644 index 0000000000..528a1b97c9 --- /dev/null +++ b/lib/explore.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** {6 Search strategies. } *) + +(** {6 ... } *) +(** A search problem implements the following signature [SearchProblem]. + [state] is the type of states of the search tree. + [branching] is the branching function; if [branching s] returns an + empty list, then search from [s] is aborted; successors of [s] are + recursively searched in the order they appear in the list. + [success] determines whether a given state is a success. + + [pp] is a pretty-printer for states used in debugging versions of the + search functions. *) + +module type SearchProblem = sig + + type state + + val branching : state -> state list + + val success : state -> bool + + val pp : state -> Pp.t + +end + +(** {6 ... } *) +(** Functor [Make] returns some search functions given a search problem. + Search functions raise [Not_found] if no success is found. + States are always visited in the order they appear in the + output of [branching] (whatever the search method is). + Debugging versions of the search functions print the position of the + visited state together with the state it-self (using [S.pp]). *) + +module Make : functor(S : SearchProblem) -> sig + + val depth_first : S.state -> S.state + val debug_depth_first : S.state -> S.state + + val breadth_first : S.state -> S.state + val debug_breadth_first : S.state -> S.state + +end diff --git a/lib/feedback.ml b/lib/feedback.ml new file mode 100644 index 0000000000..9654711ebb --- /dev/null +++ b/lib/feedback.ml @@ -0,0 +1,123 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Xml_datatype + +type level = + | Debug + | Info + | Notice + | Warning + | Error + +type doc_id = int +type route_id = int + +type feedback_content = + | Processed + | Incomplete + | Complete + | ProcessingIn of string + | InProgress of int + | WorkerStatus of string * string + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string + | FileDependency of string option * string + | FileLoaded of string * string + (* Extra metadata *) + | Custom of Loc.t option * string * xml + (* Generic messages *) + | Message of level * Loc.t option * Pp.t + +type feedback = { + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; + route : route_id; + contents : feedback_content; +} + +(** Feeders *) +let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7 + +let add_feeder = + let f_id = ref 0 in fun f -> + incr f_id; + Hashtbl.add feeders !f_id f; + !f_id + +let del_feeder fid = Hashtbl.remove feeders fid + +let default_route = 0 +let span_id = ref Stateid.dummy +let doc_id = ref 0 +let feedback_route = ref default_route + +let set_id_for_feedback ?(route=default_route) d i = + doc_id := d; + span_id := i; + feedback_route := route + +let warn_no_listeners = ref true +let feedback ?did ?id ?route what = + let m = { + contents = what; + route = Option.default !feedback_route route; + doc_id = Option.default !doc_id did; + span_id = Option.default !span_id id; + } in + if !warn_no_listeners && Hashtbl.length feeders = 0 then + Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!"; + Hashtbl.iter (fun _ f -> f m) feeders + +(* Logging messages *) +let feedback_logger ?loc lvl msg = + feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg)) + +let msg_info ?loc x = feedback_logger ?loc Info x +let msg_notice ?loc x = feedback_logger ?loc Notice x +let msg_warning ?loc x = feedback_logger ?loc Warning x +(* let msg_error ?loc x = feedback_logger ?loc Error x *) +let msg_debug ?loc x = feedback_logger ?loc Debug x + +(* Helper for tools willing to understand only the messages *) +let console_feedback_listener fmt = + let open Format in + let pp_lvl fmt lvl = match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let checker_feed (fb : feedback) = + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + | Message (lvl,loc,msg) -> + fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + in checker_feed diff --git a/lib/feedback.mli b/lib/feedback.mli new file mode 100644 index 0000000000..f407e2fd5b --- /dev/null +++ b/lib/feedback.mli @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Xml_datatype + +(* Legacy-style logging messages (used to be in Pp) *) +type level = + | Debug + | Info + | Notice + | Warning + | Error + + +(** Document unique identifier for serialization *) +type doc_id = int + +(** Coq "semantic" infos obtained during execution *) +type route_id = int + +val default_route : route_id + +type feedback_content = + (* STM mandatory data (must be displayed) *) + | Processed + | Incomplete + | Complete + (* STM optional data *) + | ProcessingIn of string + | InProgress of int + | WorkerStatus of string * string + (* Generally useful metadata *) + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string + | FileDependency of string option * string + | FileLoaded of string * string + (* Extra metadata *) + | Custom of Loc.t option * string * xml + (* Generic messages *) + | Message of level * Loc.t option * Pp.t + +type feedback = { + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; (* The document part concerned *) + route : route_id; (* Extra routing info *) + contents : feedback_content; (* The payload *) +} + +(** {6 Feedback sent, even asynchronously, to the user interface} *) + +(* The interpreter assignes an state_id to the ast, and feedbacks happening + * during interpretation are attached to it. + *) + +(** [add_feeder f] adds a feeder listiner [f], returning its id *) +val add_feeder : (feedback -> unit) -> int + +(** [del_feeder fid] removes the feeder with id [fid] *) +val del_feeder : int -> unit + +(** [feedback ?did ?sid ?route fb] produces feedback [fb], with + [route] and [did, sid] set appropiatedly, if absent, it will use + the defaults set by [set_id_for_feedback] *) +val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit + +(** [set_id_for_feedback route id] Set the defaults for feedback *) +val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit + +(** {6 output functions} + +[msg_notice] do not put any decoration on output by default. If +possible don't mix it with goal output (prefer msg_info or +msg_warning) so that interfaces can dispatch outputs easily. Once all +interfaces use the xml-like protocol this constraint can be +relaxed. *) +(* Should we advertise these functions more? Should they be the ONLY + allowed way to output something? *) + +val msg_info : ?loc:Loc.t -> Pp.t -> unit +(** Message that displays information, usually in verbose mode, such as [Foobar + is defined] *) + +val msg_notice : ?loc:Loc.t -> Pp.t -> unit +(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) + +val msg_warning : ?loc:Loc.t -> Pp.t -> unit +(** Message indicating that something went wrong, but without serious + consequences. *) + +val msg_debug : ?loc:Loc.t -> Pp.t -> unit +(** For debugging purposes *) + +val console_feedback_listener : Format.formatter -> feedback -> unit +(** Helper for tools willing to print to the feedback system *) + +val warn_no_listeners : bool ref +(** The library will print a warning to the console if no listener is + available by default; ML-clients willing to use Coq without a + feedback handler should set this to false. *) diff --git a/lib/flags.ml b/lib/flags.ml new file mode 100644 index 0000000000..452433d271 --- /dev/null +++ b/lib/flags.ml @@ -0,0 +1,110 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* If [restore] is false, whenever [f] modifies the ref, we will + preserve the modification. *) +let with_modified_ref ?(restore=true) r nf f x = + let old_ref = !r in r := nf !r; + try + let pre = !r in + let res = f x in + (* If r was modified don't restore its old value *) + if restore || pre == !r then r := old_ref; + res + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + r := old_ref; + Exninfo.iraise reraise + +let with_option o f x = with_modified_ref ~restore:false o (fun _ -> true) f x +let without_option o f x = with_modified_ref ~restore:false o (fun _ -> false) f x +let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x + +(* hide the [restore] option as internal *) +let with_modified_ref r nf f x = with_modified_ref r nf f x + +let with_options ol f x = + let vl = List.map (!) ol in + let () = List.iter (fun r -> r := true) ol in + try + let r = f x in + let () = List.iter2 (:=) ol vl in r + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = List.iter2 (:=) ol vl in + Exninfo.iraise reraise + +let record_aux_file = ref false + +let async_proofs_worker_id = ref "master" +let async_proofs_is_worker () = !async_proofs_worker_id <> "master" + +let debug = ref false + +let in_debugger = ref false +let in_toplevel = ref false + +let profile = false + +let raw_print = ref false + +let we_are_parsing = ref false + +(* Compatibility mode *) + +(* Current means no particular compatibility consideration. + For correct comparisons, this constructor should remain the last one. *) + +type compat_version = V8_8 | V8_9 | Current + +let compat_version = ref Current + +let version_compare v1 v2 = match v1, v2 with + | V8_8, V8_8 -> 0 + | V8_8, _ -> -1 + | _, V8_8 -> 1 + | V8_9, V8_9 -> 0 + | V8_9, _ -> -1 + | _, V8_9 -> 1 + | Current, Current -> 0 + +let version_strictly_greater v = version_compare !compat_version v > 0 +let version_less_or_equal v = not (version_strictly_greater v) + +let pr_version = function + | V8_8 -> "8.8" + | V8_9 -> "8.9" + | Current -> "current" + +(* Translate *) +let beautify = ref false +let beautify_file = ref false + +(* Silent / Verbose *) +let quiet = ref false +let silently f x = with_option quiet f x +let verbosely f x = without_option quiet f x + +let if_silent f x = if !quiet then f x +let if_verbose f x = if not !quiet then f x + +let warn = ref true +let make_warn flag = warn := flag; () +let if_warn f x = if !warn then f x + +(* Level of inlining during a functor application *) + +let default_inline_level = 100 +let inline_level = ref default_inline_level +let set_inline_level = (:=) inline_level +let get_inline_level () = !inline_level + +let profile_ltac = ref false +let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli new file mode 100644 index 0000000000..a70a23b902 --- /dev/null +++ b/lib/flags.mli @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Global options of the system. *) + +(** WARNING: don't add new entries to this file! + + This file is own its way to deprecation in favor of a purely + functional state, but meanwhile it will contain options that are + truly global to the system such as [compat] or [debug] + + If you are thinking about adding a global flag, well, just + don't. First of all, options make testins exponentially more + expensive, due to the growth of flag combinations. So please make + some effort in order for your idea to work in a configuration-free + manner. + + If you absolutely must pass an option to your new system, then do + so as a functional argument so flags are exposed to unit + testing. Then, register such parameters with the proper + state-handling mechanism of the top-level subsystem of Coq. + + *) + +(** Command-line flags *) + +(** Set by coqtop to tell the kernel to output to the aux file; will + be eventually removed by cleanups such as PR#1103 *) +val record_aux_file : bool ref + +(** Async-related flags *) +val async_proofs_worker_id : string ref +val async_proofs_is_worker : unit -> bool + +(** Debug flags *) +val debug : bool ref +val in_debugger : bool ref +val in_toplevel : bool ref + +val profile : bool + +(* development flag to detect race conditions, it should go away. *) +val we_are_parsing : bool ref + +(* Set Printing All flag. For some reason it is a global flag *) +val raw_print : bool ref + +type compat_version = V8_8 | V8_9 | Current +val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int +val version_strictly_greater : compat_version -> bool +val version_less_or_equal : compat_version -> bool +val pr_version : compat_version -> string + +(* Beautify command line flags, should move to printing? *) +val beautify : bool ref +val beautify_file : bool ref + +(* Coq quiet mode. Note that normal mode is called "verbose" here, + whereas [quiet] supresses normal output such as goals in coqtop *) +val quiet : bool ref +val silently : ('a -> 'b) -> 'a -> 'b +val verbosely : ('a -> 'b) -> 'a -> 'b +val if_silent : ('a -> unit) -> 'a -> unit +val if_verbose : ('a -> unit) -> 'a -> unit + +val warn : bool ref +val make_warn : bool -> unit +val if_warn : ('a -> unit) -> 'a -> unit + +(** [with_modified_ref r nf f x] Temporarily modify a reference in the + call to [f x] . Be very careful with these functions, it is very + easy to fall in the typical problem with effects: + + with_modified_ref r nf f x y != with_modified_ref r nf (f x) y + +*) +val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b + +(** Temporarily activate an option (to activate option [o] on [f x y z], + use [with_option o (f x y) z]) *) +val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b + +(** As [with_option], but on several flags. *) +val with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b + +(** Temporarily deactivate an option *) +val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b + +(** Temporarily extends the reference to a list *) +val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b + +(** Level of inlining during a functor application *) +val set_inline_level : int -> unit +val get_inline_level : unit -> int +val default_inline_level : int + +(** Global profile_ltac flag *) +val profile_ltac : bool ref +val profile_ltac_cutoff : float ref diff --git a/lib/future.ml b/lib/future.ml new file mode 100644 index 0000000000..6e7c6fd9e3 --- /dev/null +++ b/lib/future.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let not_ready_msg = ref (fun name -> + Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ + "Please wait or pass "^ + "the \"-async-proofs off\" option to CoqIDE to disable "^ + "asynchronous script processing and don't pass \"-quick\" to "^ + "coqc.")) +let not_here_msg = ref (fun name -> + Pp.strbrk("The value you are asking for ("^name^") is not available "^ + "in this process. If you really need this, pass "^ + "the \"-async-proofs off\" option to CoqIDE to disable "^ + "asynchronous script processing and don't pass \"-quick\" to "^ + "coqc.")) + +let customize_not_ready_msg f = not_ready_msg := f +let customize_not_here_msg f = not_here_msg := f + +exception NotReady of string +exception NotHere of string + +let _ = CErrors.register_handler (function + | NotReady name -> !not_ready_msg name + | NotHere name -> !not_here_msg name + | _ -> raise CErrors.Unhandled) + +type fix_exn = Exninfo.iexn -> Exninfo.iexn +let id x = x + +module UUID = struct + type t = int + let invalid = 0 + let fresh = + let count = ref invalid in + fun () -> incr count; !count + + let compare = compare + let equal = (==) +end + +module UUIDMap = Map.Make(UUID) +module UUIDSet = Set.Make(UUID) + +type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + +(* Val is not necessarily a final state, so the + computation restarts from the state stocked into Val *) +and 'a comp = + | Delegated of (unit -> unit) + | Closure of (unit -> 'a) + | Val of 'a + | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) + +and 'a comput = + | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key + | Finished of 'a + +and 'a computation = 'a comput ref + +let unnamed = "unnamed" + +let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = + ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) +let get x = + match !x with + | Finished v -> unnamed, UUID.invalid, id, ref (Val v) + | Ongoing (name, x) -> + try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c + with CEphemeron.InvalidKey -> + name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null)) + +type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] + +let is_over kx = let _, _, _, x = get kx in match !x with + | Val _ | Exn _ -> true + | Closure _ | Delegated _ -> false + +let is_val kx = let _, _, _, x = get kx in match !x with + | Val _ -> true + | Exn _ | Closure _ | Delegated _ -> false + +let is_exn kx = let _, _, _, x = get kx in match !x with + | Exn _ -> true + | Val _ | Closure _ | Delegated _ -> false + +let peek_val kx = let _, _, _, x = get kx in match !x with + | Val v -> Some v + | Exn _ | Closure _ | Delegated _ -> None + +let uuid kx = let _, id, _, _ = get kx in id + +let from_val ?(fix_exn=id) v = create fix_exn (Val v) +let from_here ?(fix_exn=id) v = create fix_exn (Val v) + +let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn + +let create_delegate ?(blocking=true) ~name fix_exn = + let assignment signal ck = fun v -> + let _, _, fix_exn, c = get ck in + assert (match !c with Delegated _ -> true | _ -> false); + begin match v with + | `Val v -> c := Val v + | `Exn e -> c := Exn (fix_exn e) + | `Comp f -> let _, _, _, comp = get f in c := !comp end; + signal () in + let wait, signal = + if not blocking then (fun () -> raise (NotReady name)), ignore else + let lock = Mutex.create () in + let cond = Condition.create () in + (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), + (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + let ck = create ~name fix_exn (Delegated wait) in + ck, assignment signal ck + +(* TODO: get rid of try/catch to be stackless *) +let rec compute ck : 'a value = + let _, _, fix_exn, c = get ck in + match !c with + | Val x -> `Val x + | Exn (e, info) -> `Exn (e, info) + | Delegated wait -> wait (); compute ck + | Closure f -> + try + let data = f () in + c := Val data; `Val data + with e -> + let e = CErrors.push e in + let e = fix_exn e in + match e with + | (NotReady _, _) -> `Exn e + | _ -> c := Exn e; `Exn e + +let force x = match compute x with + | `Val v -> v + | `Exn e -> Exninfo.iraise e + +let chain ck f = + let name, uuid, fix_exn, c = get ck in + create ~uuid ~name fix_exn (match !c with + | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) + | Exn _ as x -> x + | Val v -> Val (f v)) + +let create fix_exn f = create fix_exn (Closure f) + +let replace kx y = + let _, _, _, x = get kx in + match !x with + | Exn _ -> x := Closure (fun () -> force y) + | _ -> CErrors.anomaly + (Pp.str "A computation can be replaced only if is_exn holds.") + +let chain x f = + let y = chain x f in + if is_over x then ignore(force y); + y + +let join kx = + let v = force kx in + kx := Finished v; + v + +let sink kx = if is_val kx then ignore(join kx) + +let split2 x = + chain x (fun x -> fst x), chain x (fun x -> snd x) + +let map2 f x l = + CList.map_i (fun i y -> + let xi = chain x (fun x -> + try List.nth x i + with Failure _ | Invalid_argument _ -> + CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in + f xi y) 0 l + +let print f kx = + let open Pp in + let name, uid, _, x = get kx in + let uid = + if UUID.equal uid UUID.invalid then str "[#:" ++ str name ++ str "]" + else str "[" ++ int uid ++ str":" ++ str name ++ str "]" + in + match !x with + | Delegated _ -> str "Delegated" ++ uid + | Closure _ -> str "Closure" ++ uid + | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) + | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) diff --git a/lib/future.mli b/lib/future.mli new file mode 100644 index 0000000000..55f05518b0 --- /dev/null +++ b/lib/future.mli @@ -0,0 +1,117 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Futures: asynchronous computations. + * + * A Future.computation is like a lazy_t but with some extra bells and whistles + * to deal with eventual delegation to a slave process. + * + * One difference with lazy_t is that a future computation that produces + * and exception can be substituted for another computation of the same type. + * Moreover a future computation can be delegated to another execution entity + * that will be allowed to set the result. Finally future computations can + * always be marshalled: if they were joined before marshalling, they will + * hold the computed value (assuming it is itself marshallable), otherwise + * they will become invalid and accessing them raises a private exception. + *) + +(* Each computation has a unique id that is inherited by each offspring + * computation (chain, split, map...). Joined computations lose it. *) +module UUID : sig + type t + val invalid : t + + val compare : t -> t -> int + val equal : t -> t -> bool +end + +module UUIDMap : Map.S with type key = UUID.t +module UUIDSet : Set.S with type elt = UUID.t + +exception NotReady of string + +type 'a computation +type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] +type fix_exn = Exninfo.iexn -> Exninfo.iexn + +(* Build a computation, no snapshot of the global state is taken. If you need + to grab a copy of the state start with from_here () and then chain. + fix_exn is used to enrich any exception raised + by forcing the computations or any computation that is chained after + it. It is used by STM to attach errors to their corresponding states, + and to communicate to the code catching the exception a valid state id. *) +val create : fix_exn -> (unit -> 'a) -> 'a computation + +(* Usually from_val is used to create "fake" futures, to use the same API + as if a real asynchronous computations was there. In this case fixing + the exception is not needed, but *if* the future is chained, the fix_exn + argument should really be given *) +val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation + +(* Like from_val, but also takes a snapshot of the global state. Morally + the value is not just the 'a but also the global system state *) +val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation + +(* To get the fix_exn of a computation and build a Lemmas.declaration_hook. + * When a future enters the environment a corresponding hook is run to perform + * some work. If this fails, then its failure has to be annotated with the + * same state id that corresponds to the future computation end. I.e. Qed + * is split into two parts, the lazy one (the future) and the eager one + * (the hook), both performing some computations for the same state id. *) +val fix_exn_of : 'a computation -> fix_exn + +(* Run remotely, returns the function to assign. + If not blocking (the default) it raises NotReady if forced before the + delegate assigns it. *) +type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] +val create_delegate : + ?blocking:bool -> name:string -> + fix_exn -> 'a computation * ('a assignment -> unit) + +(* Given a computation that is_exn, replace it by another one *) +val replace : 'a computation -> 'a computation -> unit + +(* Inspect a computation *) +val is_over : 'a computation -> bool +val is_val : 'a computation -> bool +val is_exn : 'a computation -> bool +val peek_val : 'a computation -> 'a option +val uuid : 'a computation -> UUID.t + +(* [chain c f] chains computation [c] with [f]. + * [chain] is eager, that is to say, it won't suspend the new computation + * if the old one is_over (Exn or Val). +*) +val chain : 'a computation -> ('a -> 'b) -> 'b computation + +(* Forcing a computation *) +val force : 'a computation -> 'a +val compute : 'a computation -> 'a value + +(* Final call. + * Also the fix_exn function is lost, hence error reporting can be incomplete + * in a computation obtained by chaining on a joined future. *) +val join : 'a computation -> 'a + +(* Call this before stocking the future. If it is_val then it is joined *) +val sink : 'a computation -> unit + +(*** Utility functions ************************************************* ***) +val split2 : + ('a * 'b) computation -> 'a computation * 'b computation +val map2 : + ('a computation -> 'b -> 'c) -> + 'a list computation -> 'b list -> 'c list + +(** Debug: print a computation given an inner printing function. *) +val print : ('a -> Pp.t) -> 'a computation -> Pp.t + +val customize_not_ready_msg : (string -> Pp.t) -> unit +val customize_not_here_msg : (string -> Pp.t) -> unit diff --git a/lib/genarg.ml b/lib/genarg.ml new file mode 100644 index 0000000000..209d1b271e --- /dev/null +++ b/lib/genarg.ml @@ -0,0 +1,207 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open Util + +module ArgT = +struct + module DYN = Dyn.Make () + module Map = DYN.Map + type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag + type any = Any : ('a, 'b, 'c) tag -> any + let eq = DYN.eq + let repr = DYN.repr + let create = DYN.create + let name s = match DYN.name s with + | None -> None + | Some (DYN.Any t) -> + Some (Any (Obj.magic t)) (** All created tags are made of triples *) +end + +type (_, _, _) genarg_type = +| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type +| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type + +type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type + +let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2. + (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type -> + (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option = +fun t1 t2 -> match t1, t2 with +| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2 +| ListArg t1, ListArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| OptArg t1, OptArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| PairArg (t1, u1), PairArg (t2, u2) -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> + match genarg_type_eq u1 u2 with + | None -> None + | Some Refl -> Some Refl + end +| _ -> None + +let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function +| ListArg t -> pr_genarg_type t ++ spc () ++ str "list" +| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt" +| PairArg (t1, t2) -> + str "("++ pr_genarg_type t1 ++ spc () ++ + str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")" +| ExtraArg s -> str (ArgT.repr s) + +let argument_type_eq arg1 arg2 = match arg1, arg2 with +| ArgumentType t1, ArgumentType t2 -> + match genarg_type_eq t1 t2 with + | None -> false + | Some Refl -> true + +let pr_argument_type (ArgumentType t) = pr_genarg_type t + +type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type +(** Alias for concision *) + +(* Dynamics but tagged by a type expression *) + +type rlevel = [ `rlevel ] +type glevel = [ `glevel ] +type tlevel = [ `tlevel ] + +type (_, _) abstract_argument_type = +| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type + +type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument + +type raw_generic_argument = rlevel generic_argument +type glob_generic_argument = glevel generic_argument +type typed_generic_argument = tlevel generic_argument + +let rawwit t = Rawwit t +let glbwit t = Glbwit t +let topwit t = Topwit t + +let wit_list t = ListArg t + +let wit_opt t = OptArg t + +let wit_pair t1 t2 = PairArg (t1, t2) + +let in_gen t o = GenArg (t, o) + +let abstract_argument_type_eq : + type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option = + fun t1 t2 -> match t1, t2 with + | Rawwit t1, Rawwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Glbwit t1, Glbwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Topwit t1, Topwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + +let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a = + let GenArg (t', v) = o in + match abstract_argument_type_eq t t' with + | None -> failwith "out_gen" + | Some Refl -> v + +let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with +| None -> false +| Some _ -> true + +let unquote : type l. (_, l) abstract_argument_type -> _ = function +| Rawwit t -> ArgumentType t +| Glbwit t -> ArgumentType t +| Topwit t -> ArgumentType t + +let genarg_tag (GenArg (t, _)) = unquote t + +type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type +type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type + +(** Creating args *) + +module type Param = sig type ('raw, 'glb, 'top) t end +module ArgMap(M : Param) = +struct + type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack + include ArgT.Map(struct type 'a t = 'a pack end) +end + +let create_arg name = + match ArgT.name name with + | None -> ExtraArg (ArgT.create name) + | Some _ -> + CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".") + +let make0 = create_arg + +(** Registering genarg-manipulating functions *) + +module type GenObj = +sig + type ('raw, 'glb, 'top) obj + val name : string + val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option +end + +let get_arg_tag = function +| ExtraArg s -> s +| _ -> assert false + +module Register (M : GenObj) = +struct + module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) + let arg0_map = ref GenMap.empty + + let register0 arg f = + let s = get_arg_tag arg in + if GenMap.mem s !arg0_map then + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in + CErrors.anomaly msg + else + arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map + + let get_obj0 name = + try + let GenMap.Pack obj = GenMap.find name !arg0_map in obj + with Not_found -> + match M.default (ExtraArg name) with + | None -> + CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".") + | Some obj -> obj + + (** For now, the following function is quite dummy and should only be applied + to an extra argument type, otherwise, it will badly fail. *) + let obj t = get_obj0 @@ get_arg_tag t + +end diff --git a/lib/genarg.mli b/lib/genarg.mli new file mode 100644 index 0000000000..52db3df088 --- /dev/null +++ b/lib/genarg.mli @@ -0,0 +1,197 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Generic arguments used by the extension mechanisms of several Coq ASTs. *) + +(** The route of a generic argument, from parsing to evaluation. +In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. + +{% \begin{verbatim} %} + parsing in_raw out_raw + char stream ---> raw_object ---> raw_object generic_argument -------+ + encapsulation decaps| + | + V + raw_object + | + globalization | + V + glob_object + | + encaps | + in_glob | + V + glob_object generic_argument + | + out in out_glob | + object <--- object generic_argument <--- object <--- glob_object <---+ + | decaps encaps interp decaps + | + V +effective use +{% \end{verbatim} %} + +To distinguish between the uninterpreted, globalized and +interpreted worlds, we annotate the type [generic_argument] by a +phantom argument. + +*) + +(** {5 Generic types} *) + +module ArgT : +sig + type ('a, 'b, 'c) tag + val eq : ('a1, 'b1, 'c1) tag -> ('a2, 'b2, 'c2) tag -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option + val repr : ('a, 'b, 'c) tag -> string + type any = Any : ('a, 'b, 'c) tag -> any + val name : string -> any option +end + +(** Generic types. The first parameter is the OCaml lowest level, the second one + is the globalized level, and third one the internalized level. *) +type (_, _, _) genarg_type = +| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type +| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type + +type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type +(** Alias for concision when the three types agree. *) + +val make0 : string -> ('raw, 'glob, 'top) genarg_type +(** Create a new generic type of argument: force to associate + unique ML types at each of the three levels. *) + +val create_arg : string -> ('raw, 'glob, 'top) genarg_type +(** Alias for [make0]. *) + +(** {5 Specialized types} *) + +(** All of [rlevel], [glevel] and [tlevel] must be non convertible + to ensure the injectivity of the GADT type inference. *) + +type rlevel = [ `rlevel ] +type glevel = [ `glevel ] +type tlevel = [ `tlevel ] + +(** Generic types at a fixed level. The first parameter embeds the OCaml type + and the second one the level. *) +type (_, _) abstract_argument_type = +| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type + +type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type +(** Specialized type at raw level. *) + +type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type +(** Specialized type at globalized level. *) + +type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type +(** Specialized type at internalized level. *) + +(** {6 Projections} *) + +val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +(** Projection on the raw type constructor. *) + +val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +(** Projection on the globalized type constructor. *) + +val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type +(** Projection on the internalized type constructor. *) + +(** {5 Generic arguments} *) + +type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument +(** A inhabitant of ['level generic_argument] is a inhabitant of some type at + level ['level], together with the representation of this type. *) + +type raw_generic_argument = rlevel generic_argument +type glob_generic_argument = glevel generic_argument +type typed_generic_argument = tlevel generic_argument + +(** {6 Constructors} *) + +val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument +(** [in_gen t x] embeds an argument of type [t] into a generic argument. *) + +val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a +(** [out_gen t x] recovers an argument of type [t] from a generic argument. It + fails if [x] has not the right dynamic type. *) + +val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool +(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that + [out_gen t v] will not raise a dynamic type exception. *) + +(** {6 Type reification} *) + +type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type + +(** {6 Equalities} *) + +val argument_type_eq : argument_type -> argument_type -> bool +val genarg_type_eq : + ('a1, 'b1, 'c1) genarg_type -> + ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option +val abstract_argument_type_eq : + ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> + ('a, 'b) CSig.eq option + +val pr_argument_type : argument_type -> Pp.t +(** Print a human-readable representation for a given type. *) + +val genarg_tag : 'a generic_argument -> argument_type + +val unquote : ('a, 'co) abstract_argument_type -> argument_type + +(** {6 Registering genarg-manipulating functions} + + This is boilerplate code used here and there in the code of Coq. *) + +val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag +(** Works only on base objects (ExtraArg), otherwise fails badly. *) + +module type GenObj = +sig + type ('raw, 'glb, 'top) obj + (** An object manipulating generic arguments. *) + + val name : string + (** A name for such kind of manipulation, e.g. [interp]. *) + + val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option + (** A generic object when there is no registered object for this type. *) +end + +module Register (M : GenObj) : +sig + val register0 : ('raw, 'glb, 'top) genarg_type -> + ('raw, 'glb, 'top) M.obj -> unit + (** Register a ground type manipulation function. *) + + val obj : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) M.obj + (** Recover a manipulation function at a given type. *) + +end + +(** {5 Compatibility layer} + +The functions below are aliases for generic_type constructors. + +*) + +val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type diff --git a/lib/hook.ml b/lib/hook.ml new file mode 100644 index 0000000000..1e2a2f279d --- /dev/null +++ b/lib/hook.ml @@ -0,0 +1,34 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type 'a content = +| Unset +| Default of 'a +| Set of 'a + +type 'a t = 'a content ref + +type 'a value = 'a t + +let get (hook : 'a value) = match !hook with +| Unset -> assert false +| Default data | Set data -> data + +let set (hook : 'a t) data = match !hook with +| Unset | Default _ -> hook := Set data +| Set _ -> assert false + +let make ?default () = + let data = match default with + | None -> Unset + | Some data -> Default data + in + let ans = ref data in + (ans, ans) diff --git a/lib/hook.mli b/lib/hook.mli new file mode 100644 index 0000000000..67abd34dd6 --- /dev/null +++ b/lib/hook.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module centralizes the notions of hooks. Hooks are pointers that are to + be set at runtime exactly once. *) + +type 'a t +(** The type of hooks containing ['a]. Hooks can only be set. *) + +type 'a value +(** The content part of a hook. *) + +val make : ?default:'a -> unit -> ('a value * 'a t) +(** Create a new hook together with a way to retrieve its runtime value. *) + +val get : 'a value -> 'a +(** Access the content of a hook. If it was not set yet, try to recover the + default value if there is one. + @raise Assert_failure if undefined. *) + +val set : 'a t -> 'a -> unit +(** Register a hook. Assertion failure if already registered. *) diff --git a/lib/lib.mllib b/lib/lib.mllib new file mode 100644 index 0000000000..2db59712b9 --- /dev/null +++ b/lib/lib.mllib @@ -0,0 +1,29 @@ +Hook +Flags +Control +Util + +Pp +Pp_diff +Stateid +Loc +Feedback +CErrors +CWarnings + +AcyclicGraph +Rtree +System +Explore +CProfile +Future +Spawn + +CAst +DAst +Genarg + +RemoteCounter +Aux_file +Envars +CoqProject_file diff --git a/lib/loc.ml b/lib/loc.ml new file mode 100644 index 0000000000..6bcdcc0341 --- /dev/null +++ b/lib/loc.ml @@ -0,0 +1,99 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Locations management *) + +type source = + | InFile of string + | ToplevelInput + +type t = { + fname : source; (** filename or toplevel input *) + line_nb : int; (** start line number *) + bol_pos : int; (** position of the beginning of start line *) + line_nb_last : int; (** end line number *) + bol_pos_last : int; (** position of the beginning of end line *) + bp : int; (** start position *) + ep : int; (** end position *) +} + +let create fname line_nb bol_pos bp ep = { + fname = fname; line_nb = line_nb; bol_pos = bol_pos; + line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; +} + +let initial source = create source 1 0 0 0 + +let make_loc (bp, ep) = { + fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + bp = bp; ep = ep; +} + +let mergeable loc1 loc2 = + loc1.fname = loc2.fname + +let merge loc1 loc2 = + if not (mergeable loc1 loc2) then + failwith "Trying to merge unmergeable locations."; + if loc1.bp < loc2.bp then + if loc1.ep < loc2.ep then { + fname = loc1.fname; + line_nb = loc1.line_nb; + bol_pos = loc1.bol_pos; + line_nb_last = loc2.line_nb_last; + bol_pos_last = loc2.bol_pos_last; + bp = loc1.bp; ep = loc2.ep; + } + else loc1 + else if loc2.ep < loc1.ep then { + fname = loc2.fname; + line_nb = loc2.line_nb; + bol_pos = loc2.bol_pos; + line_nb_last = loc1.line_nb_last; + bol_pos_last = loc1.bol_pos_last; + bp = loc2.bp; ep = loc1.ep; + } + else loc2 + +let merge_opt l1 l2 = match l1, l2 with + | None, None -> None + | Some l , None -> Some l + | None, Some l -> Some l + | Some l1, Some l2 -> Some (merge l1 l2) + +let finer l1 l2 = match l1, l2 with + | None, _ -> false + | Some l , None -> true + | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2 + +let unloc loc = (loc.bp, loc.ep) + +let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } + +(** Located type *) +type 'a located = t option * 'a + +let tag ?loc x = loc, x +let map f (l,x) = (l, f x) + +(** Exceptions *) + +let location : t Exninfo.t = Exninfo.make () + +let add_loc e loc = Exninfo.add e location loc +let get_loc e = Exninfo.get e location + +let raise ?loc e = + match loc with + | None -> raise e + | Some loc -> + let info = Exninfo.add Exninfo.null location loc in + Exninfo.iraise (e, info) + diff --git a/lib/loc.mli b/lib/loc.mli new file mode 100644 index 0000000000..1eb3cc49e8 --- /dev/null +++ b/lib/loc.mli @@ -0,0 +1,76 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** {5 Basic types} *) + +type source = + | InFile of string + | ToplevelInput + +type t = { + fname : source; (** filename or toplevel input *) + line_nb : int; (** start line number *) + bol_pos : int; (** position of the beginning of start line *) + line_nb_last : int; (** end line number *) + bol_pos_last : int; (** position of the beginning of end line *) + bp : int; (** start position *) + ep : int; (** end position *) +} + +(** {5 Location manipulation} *) + +(** This is inherited from CAMPL4/5. *) + +val create : source -> int -> int -> int -> int -> t +(** Create a location from a filename, a line number, a position of the + beginning of the line, a start and end position *) + +val initial : source -> t +(** Create a location corresponding to the beginning of the given source *) + +val unloc : t -> int * int +(** Return the start and end position of a location *) + +val make_loc : int * int -> t +(** Make a location out of its start and end position *) + +val merge : t -> t -> t +val merge_opt : t option -> t option -> t option +(** Merge locations, usually generating the largest possible span *) + +val finer : t option -> t option -> bool +(** Answers [true] when the first location is more defined, or, when + both defined, included in the second one *) + +val shift_loc : int -> int -> t -> t +(** [shift_loc loc n p] shifts the beginning of location by [n] and + the end by [p]; it is assumed that the shifts do not change the + lines at which the location starts and ends *) + +(** {5 Located exceptions} *) + +val add_loc : Exninfo.info -> t -> Exninfo.info +(** Adding location to an exception *) + +val get_loc : Exninfo.info -> t option +(** Retrieving the optional location of an exception *) + +val raise : ?loc:t -> exn -> 'a +(** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *) + +(** {5 Objects with location information } *) + +type 'a located = t option * 'a + +val tag : ?loc:t -> 'a -> 'a located +(** Embed a location in a type *) + +val map : ('a -> 'b) -> 'a located -> 'b located +(** Modify an object carrying a location *) diff --git a/lib/pp.ml b/lib/pp.ml new file mode 100644 index 0000000000..cdde60f051 --- /dev/null +++ b/lib/pp.ml @@ -0,0 +1,366 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* The different kinds of blocks are: + \begin{description} + \item[hbox:] Horizontal block no line breaking; + \item[vbox:] Vertical block each break leads to a new line; + \item[hvbox:] Horizontal-vertical block: same as vbox, except if + this block is small enough to fit on a single line + \item[hovbox:] Horizontal or Vertical block: breaks lead to new line + only when necessary to print the content of the block + \end{description} + *) + +type pp_tag = string + +type block_type = + | Pp_hbox of int + | Pp_vbox of int + | Pp_hvbox of int + | Pp_hovbox of int + +type doc_view = + | Ppcmd_empty + | Ppcmd_string of string + | Ppcmd_glue of doc_view list + | Ppcmd_box of block_type * doc_view + | Ppcmd_tag of pp_tag * doc_view + (* Are those redundant? *) + | Ppcmd_print_break of int * int + | Ppcmd_force_newline + | Ppcmd_comment of string list + +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t = doc_view + +let repr x = x +let unrepr x = x + +(* Compute length of an UTF-8 encoded string + Rem 1 : utf8_length <= String.length (equal if pure ascii) + Rem 2 : if used for an iso8859_1 encoded string, the result is + wrong in very rare cases. Such a wrong case corresponds to any + sequence of a character in range 192..253 immediately followed by a + character in range 128..191 (typical case in french is "déçu" which + is counted 3 instead of 4); then no real harm to use always + utf8_length even if using an iso8859_1 encoding *) + +let utf8_length s = + let len = String.length s + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + while !p < len do + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + !cnt + +let rec app d1 d2 = match d1, d2 with + | Ppcmd_empty, d + | d, Ppcmd_empty -> d + + (* Optimizations *) + | Ppcmd_glue [l1;l2], Ppcmd_glue l3 -> Ppcmd_glue (l1 :: l2 :: l3) + | Ppcmd_glue [l1;l2], d2 -> Ppcmd_glue [l1 ; l2 ; d2] + | d1, Ppcmd_glue l2 -> Ppcmd_glue (d1 :: l2) + + | Ppcmd_tag(t1,d1), Ppcmd_tag(t2,d2) + when t1 = t2 -> Ppcmd_tag(t1,app d1 d2) + | d1, d2 -> Ppcmd_glue [d1; d2] + (* Optimizations deemed too costly *) + (* | Ppcmd_glue l1, Ppcmd_glue l2 -> Ppcmd_glue (l1 @ l2) *) + (* | Ppcmd_string s1, Ppcmd_string s2 -> Ppcmd_string (s1 ^ s2) *) + +let seq s = Ppcmd_glue s + +let (++) = app + +(* formatting commands *) +let str s = Ppcmd_string s +let brk (a,b) = Ppcmd_print_break (a,b) +let fnl () = Ppcmd_force_newline +let ws n = Ppcmd_print_break (n,0) +let comment l = Ppcmd_comment l + +(* derived commands *) +let mt () = Ppcmd_empty +let spc () = Ppcmd_print_break (1,0) +let cut () = Ppcmd_print_break (0,0) +let align () = Ppcmd_print_break (0,0) +let int n = str (string_of_int n) +let real r = str (string_of_float r) +let bool b = str (string_of_bool b) + +(* XXX: To Remove *) +let strbrk s = + let rec aux p n = + if n < String.length s then + if s.[n] = ' ' then + if p = n then spc() :: aux (n+1) (n+1) + else str (String.sub s p (n-p)) :: spc () :: aux (n+1) (n+1) + else aux p (n + 1) + else if p = n then [] else [str (String.sub s p (n-p))] + in Ppcmd_glue (aux 0 0) + +let ismt = function | Ppcmd_empty -> true | _ -> false + +(* boxing commands *) +let h n s = Ppcmd_box(Pp_hbox n,s) +let v n s = Ppcmd_box(Pp_vbox n,s) +let hv n s = Ppcmd_box(Pp_hvbox n,s) +let hov n s = Ppcmd_box(Pp_hovbox n,s) + +(* Opening and closing of tags *) +let tag t s = Ppcmd_tag(t,s) + +(* In new syntax only double quote char is escaped by repeating it *) +let escape_string s = + let rec escape_at s i = + if i<0 then s + else if s.[i] == '"' then + let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in + escape_at s' (i-1) + else escape_at s (i-1) in + escape_at s (String.length s - 1) + +let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" +let qs = qstring +let quote s = h 0 (str "\"" ++ s ++ str "\"") + +let rec pr_com ft s = + let (s1,os) = + try + let n = String.index s '\n' in + String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1)) + with Not_found -> s,None in + Format.pp_print_as ft (utf8_length s1) s1; + match os with + Some s2 -> Format.pp_force_newline ft (); pr_com ft s2 + | None -> () + +let start_pfx = "start." +let end_pfx = "end." + +let split_pfx pfx str = + let (str_len, pfx_len) = (String.length str, String.length pfx) in + if str_len >= pfx_len && (String.sub str 0 pfx_len) = pfx then + (pfx, String.sub str pfx_len (str_len - pfx_len)) else ("", str);; + +let split_tag tag = + let (pfx, ttag) = split_pfx start_pfx tag in + if pfx <> "" then (pfx, ttag) else + let (pfx, ttag) = split_pfx end_pfx tag in + (pfx, ttag);; + +(* pretty printing functions *) +let pp_with ft pp = + let cpp_open_box = function + | Pp_hbox n -> Format.pp_open_hbox ft () + | Pp_vbox n -> Format.pp_open_vbox ft n + | Pp_hvbox n -> Format.pp_open_hvbox ft n + | Pp_hovbox n -> Format.pp_open_hovbox ft n + in + let rec pp_cmd = let open Format in function + | Ppcmd_empty -> () + | Ppcmd_glue sl -> List.iter pp_cmd sl + | Ppcmd_string str -> let n = utf8_length str in + pp_print_as ft n str + | Ppcmd_box(bty,ss) -> cpp_open_box bty ; + if not (over_max_boxes ()) then pp_cmd ss; + pp_close_box ft () + | Ppcmd_print_break(m,n) -> pp_print_break ft m n + | Ppcmd_force_newline -> pp_force_newline ft () + | Ppcmd_comment coms -> List.iter (pr_com ft) coms + | Ppcmd_tag(tag, s) -> pp_open_tag ft tag; + pp_cmd s; + pp_close_tag ft () + in + try pp_cmd pp + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = Format.pp_print_flush ft () in + Exninfo.iraise reraise + +(* If mixing some output and a goal display, please use msg_warning, + so that interfaces (proofgeneral for example) can easily dispatch + them to different windows. *) + +(** Output to a string formatter *) +let string_of_ppcmds c = + Format.fprintf Format.str_formatter "@[%a@]" pp_with c; + Format.flush_str_formatter () + +(* Copy paste from Util *) + +let pr_comma () = str "," ++ spc () +let pr_semicolon () = str ";" ++ spc () +let pr_bar () = str "|" ++ spc () +let pr_spcbar () = str " |" ++ spc () +let pr_arg pr x = spc () ++ pr x +let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x +let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x +let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x + +(** TODO: merge with CString.ordinal *) +let pr_nth n = + let s = + if (n / 10) mod 10 = 1 then "th" + else match n mod 10 with + | 1 -> "st" + | 2 -> "nd" + | 3 -> "rd" + | _ -> "th" + in + int n ++ str s + +(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) + +let prlist pr l = Ppcmd_glue (List.map pr l) + +(* unlike all other functions below, [prlist] works lazily. + if a strict behavior is needed, use [prlist_strict] instead. + evaluation is done from left to right. *) + +let prlist_sep_lastsep no_empty sep_thunk lastsep_thunk elem l = + let sep = sep_thunk () in + let lastsep = lastsep_thunk () in + let elems = List.map elem l in + let filtered_elems = + if no_empty then + List.filter (fun e -> not (ismt e)) elems + else + elems + in + let rec insert_seps es = + match es with + | [] -> mt () + | [e] -> e + | h::[e] -> h ++ lastsep ++ e + | h::t -> h ++ sep ++ insert_seps t + in + insert_seps filtered_elems + +let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l +(* [prlist_with_sep sep pr [a ; ... ; c]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) +let prlist_with_sep sep pr l = prlist_sep_lastsep false sep sep pr l +(* Print sequence of objects separated by space (unless an element is empty) *) +let pr_sequence pr l = prlist_sep_lastsep true spc spc pr l +(* [pr_enum pr [a ; b ; ... ; c]] outputs + [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *) +let pr_enum pr l = prlist_sep_lastsep true pr_comma (fun () -> str " and" ++ spc ()) pr l + +let pr_vertical_list pr = function + | [] -> str "none" ++ fnl () + | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep fnl pr l) ++ fnl () + +(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs + [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) + +let prvecti_with_sep sep elem v = + let v = CArray.mapi (fun i x -> + let pp = if i = 0 then mt() else sep() in + pp ++ elem i x) + v + in + seq (Array.to_list v) + +(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) + +let prvecti elem v = prvecti_with_sep mt elem v + +(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) + +let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v + +(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *) + +let prvect elem v = prvect_with_sep mt elem v + +let surround p = hov 1 (str"(" ++ p ++ str")") + +(*** DEBUG code ***) + +let db_print_pp fmt pp = + let open Format in + let block_type fmt btype = + let (bt, v) = + match btype with + | Pp_hbox v -> ("Pp_hbox", v) + | Pp_vbox v -> ("Pp_vbox", v) + | Pp_hvbox v -> ("Pp_hvbox", v) + | Pp_hovbox v -> ("Pp_hovbox", v) + in + fprintf fmt "%s %d" bt v + in + let rec db_print_pp_r indent pp = + let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in + ind(); + match pp with + | Ppcmd_empty -> + fprintf fmt "Ppcmd_empty@;" + | Ppcmd_string str -> + fprintf fmt "Ppcmd_string '%s'@;" str + | Ppcmd_glue list -> + fprintf fmt "Ppcmd_glue@;"; + List.iter (fun x -> db_print_pp_r (indent + 1) (repr x)) list; + | Ppcmd_box (block, pp) -> + fprintf fmt "Ppcmd_box %a@;" block_type block; + db_print_pp_r (indent + 1) (repr pp); + | Ppcmd_tag (tag, pp) -> + fprintf fmt "Ppcmd_tag %s@;" tag; + db_print_pp_r (indent + 1) (repr pp); + | Ppcmd_print_break (i, j) -> + fprintf fmt "Ppcmd_print_break %d %d@;" i j + | Ppcmd_force_newline -> + fprintf fmt "Ppcmd_force_newline@;" + | Ppcmd_comment list -> + fprintf fmt "Ppcmd_comment@;"; + List.iter (fun x -> ind(); (fprintf fmt "%s@;" x)) list + in + pp_open_vbox fmt 0; + db_print_pp_r 0 pp; + pp_close_box fmt (); + pp_print_flush fmt () + +let db_string_of_pp pp = + Format.asprintf "%a" db_print_pp pp + +let rec flatten pp = + match pp with + | Ppcmd_glue l -> Ppcmd_glue (List.concat (List.map + (fun x -> let x = flatten x in + match x with + | Ppcmd_glue l2 -> l2 + | p -> [p]) + l)) + | Ppcmd_box (block, pp) -> Ppcmd_box (block, flatten pp) + | Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, flatten pp) + | p -> p diff --git a/lib/pp.mli b/lib/pp.mli new file mode 100644 index 0000000000..4ce6a535c8 --- /dev/null +++ b/lib/pp.mli @@ -0,0 +1,207 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Coq document type. *) + +(** Pretty printing guidelines ******************************************) +(* *) +(* `Pp.t` is the main pretty printing document type *) +(* in the Coq system. Documents are composed laying out boxes, and *) +(* users can add arbitrary tag metadata that backends are free *) +(* to interpret. *) +(* *) +(* The datatype has a public view to allow serialization or advanced *) +(* uses, however regular users are _strongly_ warned againt its use, *) +(* they should instead rely on the available functions below. *) +(* *) +(* Box order and number is indeed an important factor. Try to create *) +(* a proper amount of boxes. The `++` operator provides "efficient" *) +(* concatenation, but using the list constructors is usually preferred. *) +(* *) +(* That is to say, this: *) +(* *) +(* `hov [str "Term"; hov (pr_term t); str "is defined"]` *) +(* *) +(* is preferred to: *) +(* *) +(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")` *) +(* *) +(************************************************************************) + +(* XXX: Improve and add attributes *) +type pp_tag = string + +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t + +type block_type = + | Pp_hbox of int + | Pp_vbox of int + | Pp_hvbox of int + | Pp_hovbox of int + +type doc_view = + | Ppcmd_empty + | Ppcmd_string of string + | Ppcmd_glue of t list + | Ppcmd_box of block_type * t + | Ppcmd_tag of pp_tag * t + (* Are those redundant? *) + | Ppcmd_print_break of int * int + | Ppcmd_force_newline + | Ppcmd_comment of string list + +val repr : t -> doc_view +val unrepr : doc_view -> t + +(** {6 Formatting commands} *) + +val str : string -> t +val brk : int * int -> t +val fnl : unit -> t +val ws : int -> t +val mt : unit -> t +val ismt : t -> bool + +val comment : string list -> t + +(** {6 Manipulation commands} *) + +val app : t -> t -> t +(** Concatenation. *) + +val seq : t list -> t +(** Multi-Concatenation. *) + +val (++) : t -> t -> t +(** Infix alias for [app]. *) + +(** {6 Derived commands} *) + +val spc : unit -> t +val cut : unit -> t +val align : unit -> t +val int : int -> t +val real : float -> t +val bool : bool -> t +val qstring : string -> t +val qs : string -> t +val quote : t -> t +val strbrk : string -> t + +(** {6 Boxing commands} *) + +val h : int -> t -> t +val v : int -> t -> t +val hv : int -> t -> t +val hov : int -> t -> t + +(** {6 Tagging} *) + +val tag : pp_tag -> t -> t + +(** {6 Printing combinators} *) + +val pr_comma : unit -> t +(** Well-spaced comma. *) + +val pr_semicolon : unit -> t +(** Well-spaced semicolon. *) + +val pr_bar : unit -> t +(** Well-spaced pipe bar. *) + +val pr_spcbar : unit -> t +(** Pipe bar with space before and after. *) + +val pr_arg : ('a -> t) -> 'a -> t +(** Adds a space in front of its argument. *) + +val pr_non_empty_arg : ('a -> t) -> 'a -> t +(** Adds a space in front of its argument if non empty. *) + +val pr_opt : ('a -> t) -> 'a option -> t +(** Inner object preceded with a space if [Some], nothing otherwise. *) + +val pr_opt_no_spc : ('a -> t) -> 'a option -> t +(** Same as [pr_opt] but without the leading space. *) + +val pr_nth : int -> t +(** Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.). *) + +val prlist : ('a -> t) -> 'a list -> t +(** Concatenation of the list contents, without any separator. + + Unlike all other functions below, [prlist] works lazily. If a strict + behavior is needed, use [prlist_strict] instead. *) + +val prlist_strict : ('a -> t) -> 'a list -> t +(** Same as [prlist], but strict. *) + +val prlist_with_sep : + (unit -> t) -> ('a -> t) -> 'a list -> t +(** [prlist_with_sep sep pr [a ; ... ; c]] outputs + [pr a ++ sep () ++ ... ++ sep () ++ pr c]. + where the thunk sep is memoized, rather than being called each place + its result is used. +*) + +val prvect : ('a -> t) -> 'a array -> t +(** As [prlist], but on arrays. *) + +val prvecti : (int -> 'a -> t) -> 'a array -> t +(** Indexed version of [prvect]. *) + +val prvect_with_sep : + (unit -> t) -> ('a -> t) -> 'a array -> t +(** As [prlist_with_sep], but on arrays. *) + +val prvecti_with_sep : + (unit -> t) -> (int -> 'a -> t) -> 'a array -> t +(** Indexed version of [prvect_with_sep]. *) + +val pr_enum : ('a -> t) -> 'a list -> t +(** [pr_enum pr [a ; b ; ... ; c]] outputs + [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *) + +val pr_sequence : ('a -> t) -> 'a list -> t +(** Sequence of objects separated by space (unless an element is empty). *) + +val surround : t -> t +(** Surround with parenthesis. *) + +val pr_vertical_list : ('b -> t) -> 'b list -> t + +(** {6 Main renderers, to formatter and to string } *) + +(** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) +val pp_with : Format.formatter -> t -> unit + +val string_of_ppcmds : t -> string + + +(** Tag prefix to start a multi-token diff span *) +val start_pfx : string + +(** Tag prefix to end a multi-token diff span *) +val end_pfx : string + +(** Split a tag into prefix and base tag *) +val split_tag : string -> string * string + +(** Print the Pp in tree form for debugging *) +val db_print_pp : Format.formatter -> t -> unit + +(** Print the Pp in tree form for debugging, return as a string *) +val db_string_of_pp : t -> string + +(** Combine nested Ppcmd_glues *) +val flatten : t -> t diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml new file mode 100644 index 0000000000..a485bf31c0 --- /dev/null +++ b/lib/pp_diff.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* DEBUG/UNIT TEST *) +let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc) +let log_out_ch = ref stdout +let cprintf s = cfprintf !log_out_ch s + + +module StringDiff = Diff2.Make(struct + type elem = String.t + type t = elem array + let get t i = Array.get t i + let length t = Array.length t +end) + +type diff_type = + [ `Removed + | `Added + | `Common + ] + +type diff_list = StringDiff.elem Diff2.edit list + +(* debug print diff data structure *) +let db_print_diffs fmt diffs = + let open Format in + let print_diff = function + | `Common (opos, npos, s) -> + fprintf fmt "Common '%s' opos = %d npos = %d\n" s opos npos; + | `Removed (pos, s) -> + fprintf fmt "Removed '%s' opos = %d\n" s pos; + | `Added (pos, s) -> + fprintf fmt "Added '%s' npos = %d\n" s pos; + in + pp_open_vbox fmt 0; + List.iter print_diff diffs; + pp_close_box fmt (); + pp_print_flush fmt () + +let string_of_diffs diffs = + Format.asprintf "%a" db_print_diffs diffs + +(* Adjust the diffs returned by the Myers algorithm to reduce the span of the +changes. This gives more natural-looking diffs. + +While the Myers algorithm minimizes the number of changes between two +sequences, it doesn't minimize the span of the changes. For example, +representing elements in common in lower case and inserted elements in upper +case (but ignoring case in the algorithm), ABabC and abABC both have 3 changes +(A, B and C). However the span of the first sequence is 5 elements (ABabC) +while the span of the second is 3 elements (ABC). + +The algorithm modifies the changes iteratively, for example ABabC -> aBAbC -> abABC + +dtype: identifies which of Added OR Removed to use; the other one is ignored. +diff_list: output from the Myers algorithm +*) +let shorten_diff_span dtype diff_list = + let changed = ref false in + let diffs = Array.of_list diff_list in + let len = Array.length diffs in + let vinfo index = + match diffs.(index) with + | `Common (opos, npos, s) -> (`Common, opos, npos, s) + | `Removed (pos, s) -> (`Removed, pos, 0, s) + | `Added (pos, s) -> (`Added, 0, pos, s) in + let get_variant index = + let (v, _, _, _) = vinfo index in + v in + let get_str index = + let (_, _, _, s) = vinfo index in + s in + + let iter start len lt incr = begin + let src = ref start in + let dst = ref start in + while (lt !src len) do + if (get_variant !src) = dtype then begin + if (lt !dst !src) then + dst := !src; + while (lt !dst len) && (get_variant !dst) = dtype do + dst := !dst + incr; + done; + if (lt !dst len) && (get_str !src) = (get_str !dst) then begin + (* swap diff *) + let (_, c_opos, c_npos, str) = vinfo !dst + and (_, v_opos, v_npos, _) = vinfo !src in + changed := true; + if dtype = `Added then begin + diffs.(!src) <- `Common (c_opos, v_npos, str); + diffs.(!dst) <- `Added (c_npos, str); + end else begin + diffs.(!src) <- `Common (v_opos, c_npos, str); + diffs.(!dst) <- `Removed (c_opos, str) + end + end + end; + src := !src + incr + done + end in + + iter 0 len (<) 1; (* left to right *) + iter (len-1) (-1) (>) (-1); (* right to left *) + if !changed then Array.to_list diffs else diff_list;; + +let has_changes diffs = + let rec has_changes_r diffs added removed = + match diffs with + | `Added _ :: t -> has_changes_r t true removed + | `Removed _ :: t -> has_changes_r t added true + | h :: t -> has_changes_r t added removed + | [] -> (added, removed) in + has_changes_r diffs false false;; + +(* get the Myers diff of 2 lists of strings *) +let diff_strs old_strs new_strs = + let diffs = List.rev (StringDiff.diff old_strs new_strs) in + shorten_diff_span `Removed (shorten_diff_span `Added diffs);; + +(* Default string tokenizer. Makes each character a separate strin. +Whitespace is not ignored. Doesn't handle UTF-8 differences well. *) +let def_tokenize_string s = + let limit = (String.length s) - 1 in + let strs : string list ref = ref [] in + for i = 0 to limit do + strs := (String.make 1 s.[i]) :: !strs + done; + List.rev !strs + +(* get the Myers diff of 2 strings *) +let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str = + let old_toks = Array.of_list (tokenize_string old_str) + and new_toks = Array.of_list (tokenize_string new_str) in + diff_strs old_toks new_toks;; + +let get_dinfo = function + | `Common (_, _, s) -> (`Common, s) + | `Removed (_, s) -> (`Removed, s) + | `Added (_, s) -> (`Added, s) + +[@@@ocaml.warning "-32"] +let string_of_diff_type = function + | `Common -> "Common" + | `Removed -> "Removed" + | `Added -> "Added" +[@@@ocaml.warning "+32"] + +let wrap_in_bg diff_tag pp = + let open Pp in + (tag (Pp.start_pfx ^ diff_tag ^ ".bg") (str "")) ++ pp ++ + (tag (Pp.end_pfx ^ diff_tag ^ ".bg") (str "")) + +exception Diff_Failure of string + +let add_diff_tags which pp diffs = + let open Pp in + let diff_tag = if which = `Added then "diff.added" else "diff.removed" in + let diffs : diff_list ref = ref diffs in + let in_diff = ref false in (* true = buf chars need a tag *) + let in_span = ref false in (* true = last pp had a start tag *) + let trans = ref false in (* true = this diff starts/ends highlight *) + let buf = Buffer.create 16 in + let acc_pp = ref [] in + let diff_str, diff_ind, diff_len = ref "", ref 0, ref 0 in + let prev_dtype, dtype, next_dtype = ref `Common, ref `Common, ref `Common in + let is_white c = List.mem c [' '; '\t'; '\n'; '\r'] in + + let skip () = + while !diffs <> [] && + (let (t, _) = get_dinfo (List.hd !diffs) in + t <> `Common && t <> which) + do + diffs := List.tl !diffs + done + in + + let put_tagged case = + if Buffer.length buf > 0 then begin + let pp = str (Buffer.contents buf) in + Buffer.clear buf; + let tagged = match case with + | "" -> pp + | "tag" -> tag diff_tag pp + | "start" -> in_span := true; tag (start_pfx ^ diff_tag) pp + | "end" -> in_span := false; tag (end_pfx ^ diff_tag) pp + | _ -> raise (Diff_Failure "invalid tag id in put_tagged, should be impossible") in + acc_pp := tagged :: !acc_pp + end + in + + let output_pps () = + let next_diff_char_hl = if !diff_ind < !diff_len then !dtype = which else !next_dtype = which in + let tag = if not !in_diff then "" + else if !in_span then + if next_diff_char_hl then "" else "end" + else + if next_diff_char_hl then "start" else "tag" in + put_tagged tag; (* flush any remainder *) + let l = !acc_pp in + acc_pp := []; + match List.length l with + | 0 -> str "" + | 1 -> List.hd l + | _ -> seq (List.rev l) + in + + let maybe_next_diff () = + if !diff_ind = !diff_len && (skip(); !diffs <> []) then begin + let (t, s) = get_dinfo (List.hd !diffs) in + diff_str := s; diff_ind := 0; diff_len := String.length !diff_str; + diffs := List.tl !diffs; skip(); + prev_dtype := !dtype; + dtype := t; + next_dtype := (match !diffs with + | diff2 :: _ -> let (nt, _) = get_dinfo diff2 in nt + | [] -> `Common); + trans := !dtype <> !prev_dtype + end; + in + + let s_char c = + maybe_next_diff (); + (* matching first should handle tokens with spaces, e.g. in comments/strings *) + if !diff_ind < !diff_len && c = !diff_str.[!diff_ind] then begin + if !dtype = which && !trans && !diff_ind = 0 then begin + put_tagged ""; + in_diff := true + end; + Buffer.add_char buf c; + diff_ind := !diff_ind + 1; + if !dtype = which && !dtype <> !next_dtype && !diff_ind = !diff_len then begin + put_tagged (if !in_span then "end" else "tag"); + in_diff := false + end + end else if is_white c then + Buffer.add_char buf c + else begin + cprintf "mismatch: expected '%c' but got '%c'\n" !diff_str.[!diff_ind] c; + raise (Diff_Failure "string mismatch, shouldn't happen") + end + in + + (* rearrange so existing tags are inside diff tags, provided that those tags + only contain Ppcmd_string's. Other cases (e.g. tag of a box) are not supported. *) + (* todo: Is there a better way to do this in OCaml without multiple 'repr's? *) + let reorder_tags child pp_tag pp = + match repr child with + | Ppcmd_tag (t1, pp) -> tag t1 (tag pp_tag pp) + | Ppcmd_glue l -> + if List.exists (fun x -> + match repr x with + | Ppcmd_tag (_, _) -> true + | _ -> false) l + then seq (List.map (fun x -> + match repr x with + | Ppcmd_tag (t2, pp2) -> tag t2 (tag pp_tag pp2) + | pp2 -> tag pp_tag (unrepr pp2)) l) + else child + | _ -> tag pp_tag child + in + + let rec add_tags_r pp = + let r_pp = repr pp in + match r_pp with + | Ppcmd_string s -> String.iter s_char s; output_pps () + | Ppcmd_glue l -> seq (List.map add_tags_r l) + | Ppcmd_box (block_type, pp) -> unrepr (Ppcmd_box (block_type, add_tags_r pp)) + | Ppcmd_tag (pp_tag, pp) -> reorder_tags (add_tags_r pp) pp_tag pp + | _ -> pp + in + let (has_added, has_removed) = has_changes !diffs in + let rv = add_tags_r pp in + skip (); + if !diffs <> [] then + raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible"); + if has_added || has_removed then wrap_in_bg diff_tag rv else rv;; + +let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp = + let open Pp in + let o_str = string_of_ppcmds o_pp in + let n_str = string_of_ppcmds n_pp in + let diffs = diff_str ~tokenize_string o_str n_str in + (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);; + +let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp = + let open Pp in + let o_str = string_of_ppcmds o_pp in + let n_str = string_of_ppcmds n_pp in + let diffs = diff_str ~tokenize_string o_str n_str in + let (_, has_removed) = has_changes diffs in + let added = add_diff_tags `Added n_pp diffs in + if show_removed && has_removed then + let removed = add_diff_tags `Removed o_pp diffs in + (v 0 (removed ++ cut() ++ added)) + else added;; diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli new file mode 100644 index 0000000000..03468271d2 --- /dev/null +++ b/lib/pp_diff.mli @@ -0,0 +1,116 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** +Computes the differences between 2 Pp's and adds additional tags to a Pp +to highlight them. Strings are split into tokens using the Coq lexer, +then the lists of tokens are diffed using the Myers algorithm. A fixup routine, +shorten_diff_span, shortens the span of the diff result in some cases. + +Highlights use 4 tags to specify the color and underline/strikeout. These are +"diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The +first two are for added or removed text; the last two are for unmodified parts +of a modified item. Diffs that span multiple strings in the Pp are tagged with +"start.diff.*" and "end.diff.*", but only on the first and last strings of the span. + +If the inputs are not acceptable to the lexer, break the strings into +lists of tokens and call diff_strs, then add_diff_tags with a Pp.t that matches +the input lists of strings. Tokens that the lexer doesn't return exactly as they +appeared in the input will raise an exception in add_diff_tags (e.g. comments +and quoted strings). Fixing that requires tweaking the lexer. + +Limitations/Possible enhancements: + +- Make diff_pp immune to unlexable strings by adding a flag to the lexer. +*) + +(** Compute the diff between two Pp.t structures and return +versions of each with diffs highlighted as (old, new) *) +val diff_pp : ?tokenize_string:(string -> string list) -> Pp.t -> Pp.t -> Pp.t * Pp.t + +(** Compute the diff between two Pp.t structures and return +a highlighted Pp.t. If [show_removed] is true, show separate lines for +removals and additions, otherwise only show additions *) +val diff_pp_combined : ?tokenize_string:(string -> string list) -> ?show_removed:bool -> Pp.t -> Pp.t -> Pp.t + +(** Raised if the diff fails *) +exception Diff_Failure of string + +module StringDiff : +sig + type elem = String.t + type t = elem array +end + +type diff_type = + [ `Removed + | `Added + | `Common + ] + +type diff_list = StringDiff.elem Diff2.edit list + +(** Compute the difference between 2 strings in terms of tokens, using the +lexer to identify tokens. + +If the strings are not lexable, this routine will raise Diff_Failure. +(I expect to modify the lexer soon so this won't happen.) + +Therefore you should catch any exceptions. The workaround for now is for the +caller to tokenize the strings itself and then call diff_strs. +*) +val diff_str : ?tokenize_string:(string -> string list) -> string -> string -> StringDiff.elem Diff2.edit list + +(** Compute the differences between 2 lists of strings, treating the strings +in the lists as indivisible units. +*) +val diff_strs : StringDiff.t -> StringDiff.t -> StringDiff.elem Diff2.edit list + +(** Generate a new Pp that adds tags marking diffs to a Pp structure: +which: either `Added or `Removed, indicates which type of diffs to add +pp: the original structure. For `Added, must be the new pp passed to diff_pp + For `Removed, must be the old pp passed to diff_pp. Passing the wrong one + will likely raise Diff_Failure. +diffs: the diff list returned by diff_pp + +Diffs of single strings in the Pp are tagged with "diff.added" or "diff.removed". +Diffs that span multiple strings in the Pp are tagged with "start.diff.*" or +"end.diff.*", but only on the first and last strings of the span. + +Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends +in the middle of the string. Whitespace just before or just after a diff will +not be part of the highlight. + +Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +placed inside the diff tags to ensure proper nesting of tags within spans of +"start.diff.*" ... "end.diff.*". + +Under some "impossible" conditions, this routine may raise Diff_Failure. +If you want to make your call especially bulletproof, catch this +exception, print a user-visible message, then recall this routine with +the first argument set to None, which will skip the diff. +*) +val add_diff_tags : diff_type -> Pp.t -> StringDiff.elem Diff2.edit list -> Pp.t + +(** Returns a boolean pair (added, removed) for [diffs] where a true value +indicates that something was added/removed in the diffs. +*) +val has_changes : diff_list -> bool * bool + +val get_dinfo : StringDiff.elem Diff2.edit -> diff_type * string + +(** Returns a modified [pp] with the background highlighted with +"start.<diff_tag>.bg" and "end.<diff_tag>.bg" tags at the beginning +and end of the returned Pp.t +*) +val wrap_in_bg : string -> Pp.t -> Pp.t + +(** Displays the diffs to a printable format for debugging *) +val string_of_diffs : diff_list -> string diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml new file mode 100644 index 0000000000..978b8b7384 --- /dev/null +++ b/lib/remoteCounter.ml @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type 'a getter = unit -> 'a +type 'a installer = ('a getter) -> unit + +type remote_counters_status = (string * Obj.t) list + +let counters : remote_counters_status ref = ref [] + +let (!!) x = !(!x) + +let new_counter ~name a ~incr ~build = + assert(not (List.mem_assoc name !counters)); + let data = ref (ref a) in + counters := (name, Obj.repr data) :: !counters; + let m = Mutex.create () in + let mk_thsafe_local_getter f () = + (* - slaves must use a remote counter getter, not this one! *) + (* - in the main process there is a race condition between slave + managers (that are threads) and the main thread, hence the mutex *) + if Flags.async_proofs_is_worker () then + CErrors.anomaly(Pp.str"Slave processes must install remote counters."); + Mutex.lock m; let x = f () in Mutex.unlock m; + build x in + let mk_thsafe_remote_getter f () = + Mutex.lock m; let x = f () in Mutex.unlock m; x in + let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in + let installer f = + if not (Flags.async_proofs_is_worker ()) then + CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); + getter := mk_thsafe_remote_getter f in + (fun () -> !getter ()), installer + +let backup () = !counters + +let snapshot () = + List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters + +let restore l = + List.iter (fun (name, data) -> + assert(List.mem_assoc name !counters); + let dataref = Obj.obj (List.assoc name !counters) in + !dataref := !!(Obj.obj data)) + l diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli new file mode 100644 index 0000000000..ae0605cfb7 --- /dev/null +++ b/lib/remoteCounter.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Remote counters are *global* counters for fresh ids. In the master/slave + * scenario, the slave installs a getter that asks the master for a fresh + * value. In the scenario of a slave that runs after the death of the master + * on some marshalled data, a backup of all counters status should be taken and + * restored to avoid reusing ids. + * Counters cannot be created by threads, they must be created once and forall + * as toplevel module declarations. *) + + +type 'a getter = unit -> 'a +type 'a installer = ('a getter) -> unit + +val new_counter : name:string -> + 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer + +type remote_counters_status +val backup : unit -> remote_counters_status +(* like backup but makes a copy so that further increment does not alter + * the snapshot *) +val snapshot : unit -> remote_counters_status +val restore : remote_counters_status -> unit diff --git a/lib/rtree.ml b/lib/rtree.ml new file mode 100644 index 0000000000..e1c6a4c4d6 --- /dev/null +++ b/lib/rtree.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util + +(* Type of regular trees: + - Param denotes tree variables (like de Bruijn indices) + the first int is the depth of the occurrence, and the second int + is the index in the array of trees introduced at that depth. + Warning: Param's indices both start at 0! + - Node denotes the usual tree node, labelled with 'a + - Rec(j,v1..vn) introduces infinite tree. It denotes + v(j+1) with parameters 0..n-1 replaced by + Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively. + *) +type 'a t = + Param of int * int + | Node of 'a * 'a t array + | Rec of int * 'a t array + +(* Building trees *) +let mk_rec_calls i = Array.init i (fun j -> Param(0,j)) +let mk_node lab sons = Node (lab, sons) + +(* The usual lift operation *) +let rec lift_rtree_rec depth n = function + Param (i,j) as t -> if i < depth then t else Param (i+n,j) + | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons) + | Rec(j,defs) -> + Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs) + +let lift n t = if Int.equal n 0 then t else lift_rtree_rec 0 n t + +(* The usual subst operation *) +let rec subst_rtree_rec depth sub = function + Param (i,j) as t -> + if i < depth then t + else if i = depth then + lift depth (Rec (j, sub)) + else Param (i - 1, j) + | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons) + | Rec(j,defs) -> + Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs) + +let subst_rtree sub t = subst_rtree_rec 0 sub t + +(* To avoid looping, we must check that every body introduces a node + or a parameter *) +let rec expand = function + | Rec(j,defs) -> + expand (subst_rtree defs defs.(j)) + | t -> t + +(* Given a vector of n bodies, builds the n mutual recursive trees. + Recursive calls are made with parameters (0,0) to (0,n-1). We check + the bodies actually build something by checking it is not + directly one of the parameters of depth 0. Some care is taken to + accept definitions like rec X=Y and Y=f(X,Y) *) +let mk_rec defs = + let rec check histo d = match expand d with + | Param (0, j) -> + if Int.Set.mem j histo then failwith "invalid rec call" + else check (Int.Set.add j histo) defs.(j) + | _ -> () + in + Array.mapi (fun i d -> check (Int.Set.singleton i) d; Rec(i,defs)) defs +(* +let v(i,j) = lift i (mk_rec_calls(j+1)).(j);; +let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);; +let r = mk_rec[|v(0,1);v(1,0)|];; +the last one should be accepted +*) + +(* Tree destructors, expanding loops when necessary *) +let dest_param t = + match expand t with + Param (i,j) -> (i,j) + | _ -> failwith "Rtree.dest_param" + +let dest_node t = + match expand t with + Node (l,sons) -> (l,sons) + | _ -> failwith "Rtree.dest_node" + +let is_node t = + match expand t with + Node _ -> true + | _ -> false + +let rec map f t = match t with + Param(i,j) -> Param(i,j) + | Node (a,sons) -> Node (f a, Array.map (map f) sons) + | Rec(j,defs) -> Rec (j, Array.map (map f) defs) + +module Smart = +struct + + let map f t = match t with + Param _ -> t + | Node (a,sons) -> + let a'=f a and sons' = Array.Smart.map (map f) sons in + if a'==a && sons'==sons then t + else Node (a',sons') + | Rec(j,defs) -> + let defs' = Array.Smart.map (map f) defs in + if defs'==defs then t + else Rec(j,defs') + +end + +let smartmap = Smart.map + +(** Structural equality test, parametrized by an equality on elements *) + +let rec raw_eq cmp t t' = match t, t' with + | Param (i,j), Param (i',j') -> Int.equal i i' && Int.equal j j' + | Node (x, a), Node (x', a') -> cmp x x' && Array.equal (raw_eq cmp) a a' + | Rec (i, a), Rec (i', a') -> Int.equal i i' && Array.equal (raw_eq cmp) a a' + | _ -> false + +let raw_eq2 cmp (t,u) (t',u') = raw_eq cmp t t' && raw_eq cmp u u' + +(** Equivalence test on expanded trees. It is parametrized by two + equalities on elements: + - [cmp] is used when checking for already seen trees + - [cmp'] is used when comparing node labels. *) + +let equiv cmp cmp' = + let rec compare histo t t' = + List.mem_f (raw_eq2 cmp) (t,t') histo || + match expand t, expand t' with + | Node(x,v), Node(x',v') -> + cmp' x x' && + Int.equal (Array.length v) (Array.length v') && + Array.for_all2 (compare ((t,t')::histo)) v v' + | _ -> false + in compare [] + +(** The main comparison on rtree tries first physical equality, then + the structural one, then the logical equivalence *) + +let equal cmp t t' = + t == t' || raw_eq cmp t t' || equiv cmp cmp t t' + +(** Deprecated alias *) +let eq_rtree = equal + +(** Intersection of rtrees of same arity *) +let rec inter cmp interlbl def n histo t t' = + try + let (i,j) = List.assoc_f (raw_eq2 cmp) (t,t') histo in + Param (n-i-1,j) + with Not_found -> + match t, t' with + | Param (i,j), Param (i',j') -> + assert (Int.equal i i' && Int.equal j j'); t + | Node (x, a), Node (x', a') -> + (match interlbl x x' with + | None -> mk_node def [||] + | Some x'' -> Node (x'', Array.map2 (inter cmp interlbl def n histo) a a')) + | Rec (i,v), Rec (i',v') -> + (* If possible, we preserve the shape of input trees *) + if Int.equal i i' && Int.equal (Array.length v) (Array.length v') then + let histo = ((t,t'),(n,i))::histo in + Rec(i, Array.map2 (inter cmp interlbl def (n+1) histo) v v') + else + (* Otherwise, mutually recursive trees are transformed into nested trees *) + let histo = ((t,t'),(n,0))::histo in + Rec(0, [|inter cmp interlbl def (n+1) histo (expand t) (expand t')|]) + | Rec _, _ -> inter cmp interlbl def n histo (expand t) t' + | _ , Rec _ -> inter cmp interlbl def n histo t (expand t') + | _ -> assert false + +let inter cmp interlbl def t t' = inter cmp interlbl def 0 [] t t' + +(** Inclusion of rtrees. We may want a more efficient implementation. *) +let incl cmp interlbl def t t' = + equal cmp t (inter cmp interlbl def t t') + +(** Tests if a given tree is infinite, i.e. has a branch of infinite length. + This corresponds to a cycle when visiting the expanded tree. + We use a specific comparison to detect already seen trees. *) + +let is_infinite cmp t = + let rec is_inf histo t = + List.mem_f (raw_eq cmp) t histo || + match expand t with + | Node (_,v) -> Array.exists (is_inf (t::histo)) v + | _ -> false + in + is_inf [] t + +(* Pretty-print a tree (not so pretty) *) +open Pp + +let rec pp_tree prl t = + match t with + Param (i,j) -> str"#"++int i++str","++int j + | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") + | Node(lab,v) -> + hov 2 (str"("++prl lab++str","++brk(1,0)++ + prvect_with_sep pr_comma (pp_tree prl) v++str")") + | Rec(i,v) -> + if Int.equal (Array.length v) 0 then str"Rec{}" + else if Int.equal (Array.length v) 1 then + hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") + else + hov 2 (str"Rec{"++int i++str","++brk(1,0)++ + prvect_with_sep pr_comma (pp_tree prl) v++str"}") diff --git a/lib/rtree.mli b/lib/rtree.mli new file mode 100644 index 0000000000..5ab14f6039 --- /dev/null +++ b/lib/rtree.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Type of regular tree with nodes labelled by values of type 'a + The implementation uses de Bruijn indices, so binding capture + is avoided by the lift operator (see example below) *) +type 'a t + +(** Building trees *) + +(** build a node given a label and the vector of sons *) +val mk_node : 'a -> 'a t array -> 'a t + +(** Build mutually recursive trees: + X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n) + is obtained by the following pseudo-code + let vx = mk_rec_calls n in + let [|x_1;..;x_n|] = + mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|] + + First example: build rec X = a(X,Y) and Y = b(X,Y,Y) + let [|vx;vy|] = mk_rec_calls 2 in + let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|] + + Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y) + let [|vy|] = mk_rec_calls 1 in + let [|vx|] = mk_rec_calls 1 in + let [|x|] = mk_rec[|mk_node a vx;lift 1 vy|] + let [|y|] = mk_rec[|mk_node b x;vy;vy|] + (note the lift to avoid + *) +val mk_rec_calls : int -> 'a t array +val mk_rec : 'a t array -> 'a t array + +(** [lift k t] increases of [k] the free parameters of [t]. Needed + to avoid captures when a tree appears under [mk_rec] *) +val lift : int -> 'a t -> 'a t + +val is_node : 'a t -> bool + +(** Destructors (recursive calls are expanded) *) +val dest_node : 'a t -> 'a * 'a t array + +(** dest_param is not needed for closed trees (i.e. with no free variable) *) +val dest_param : 'a t -> int * int + +(** Tells if a tree has an infinite branch. The first arg is a comparison + used to detect already seen elements, hence loops *) +val is_infinite : ('a -> 'a -> bool) -> 'a t -> bool + +(** [Rtree.equiv eq eqlab t1 t2] compares t1 t2 (top-down). + If t1 and t2 are both nodes, [eqlab] is called on their labels, + in case of success deeper nodes are examined. + In case of loop (detected via structural equality parametrized + by [eq]), then the comparison is successful. *) +val equiv : + ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> 'a t -> 'a t -> bool + +(** [Rtree.equal eq t1 t2] compares t1 and t2, first via physical + equality, then by structural equality (using [eq] on elements), + then by logical equivalence [Rtree.equiv eq eq] *) +val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool + +val inter : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t + +val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> bool + +(** Iterators *) + +(** See also [Smart.map] *) +val map : ('a -> 'b) -> 'a t -> 'b t + +val smartmap : ('a -> 'a) -> 'a t -> 'a t +(** @deprecated Same as [Smart.map] *) + +(** A rather simple minded pretty-printer *) +val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t + +val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool +(** @deprecated Same as [Rtree.equal] *) + +module Smart : +sig + + (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *) + val map : ('a -> 'a) -> 'a t -> 'a t + +end diff --git a/lib/spawn.ml b/lib/spawn.ml new file mode 100644 index 0000000000..0652623b74 --- /dev/null +++ b/lib/spawn.ml @@ -0,0 +1,265 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let proto_version = 0 +let prefer_sock = Sys.os_type = "Win32" +let accept_timeout = 10.0 + +let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s +let prerr_endline s = if !Flags.debug then begin pr_err s end else () + +type req = ReqDie | Hello of int * int + +module type Control = sig + type handle + + val kill : handle -> unit + val wait : handle -> Unix.process_status + val unixpid : handle -> int + val uid : handle -> string + val is_alive : handle -> bool + +end + +module type MainLoopModel = sig + type async_chan + type condition + type watch_id + + val add_watch : callback:(condition list -> bool) -> async_chan -> watch_id + val remove_watch : watch_id -> unit + val read_all : async_chan -> string + val async_chan_of_file : Unix.file_descr -> async_chan + val async_chan_of_socket : Unix.file_descr -> async_chan +end + +(* Common code *) + +(* According to http://caml.inria.fr/mantis/view.php?id=5325 + * you can't use the same socket for both writing and reading (may change + * in 4.03 *) +let mk_socket_channel () = + let open Unix in + let sr = socket PF_INET SOCK_STREAM 0 in + bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1; + let sw = socket PF_INET SOCK_STREAM 0 in + bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1; + match getsockname sr, getsockname sw with + | ADDR_INET(host, portr), ADDR_INET(_, portw) -> + (sr, sw), + string_of_inet_addr host + ^":"^ string_of_int portr ^":"^ string_of_int portw + | _ -> assert false + +let accept (sr,sw) = + let r, _, _ = Unix.select [sr] [] [] accept_timeout in + if r = [] then raise (Failure (Printf.sprintf + "The spawned process did not connect back in %2.1fs" accept_timeout)); + let csr, _ = Unix.accept sr in + Unix.close sr; + let cin = Unix.in_channel_of_descr csr in + set_binary_mode_in cin true; + let w, _, _ = Unix.select [sw] [] [] accept_timeout in + if w = [] then raise (Failure (Printf.sprintf + "The spawned process did not connect back in %2.1fs" accept_timeout)); + let csw, _ = Unix.accept sw in + Unix.close sw; + let cout = Unix.out_channel_of_descr csw in + set_binary_mode_out cout true; + (csr, csw), cin, cout + +let spawn_sock env prog args = + let main_sock, main_sock_name = mk_socket_channel () in + let extra = [| prog; "-main-channel"; main_sock_name |] in + let args = Array.append extra args in + prerr_endline ("EXEC: " ^ String.concat " " (Array.to_list args)); + let pid = + Unix.create_process_env prog args env Unix.stdin Unix.stdout Unix.stderr in + if pid = 0 then begin + Unix.sleep 1; (* to avoid respawning like crazy *) + raise (Failure "create_process failed") + end; + let cs, cin, cout = accept main_sock in + pid, cin, cout, cs + +let spawn_pipe env prog args = + let master2worker_r,master2worker_w = Unix.pipe () in + let worker2master_r,worker2master_w = Unix.pipe () in + let extra = [| prog; "-main-channel"; "stdfds" |] in + let args = Array.append extra args in + Unix.set_close_on_exec master2worker_w; + Unix.set_close_on_exec worker2master_r; + prerr_endline ("EXEC: " ^ String.concat " " (Array.to_list args)); + let pid = + Unix.create_process_env + prog args env master2worker_r worker2master_w Unix.stderr in + if pid = 0 then begin + Unix.sleep 1; (* to avoid respawning like crazy *) + raise (Failure "create_process failed") + end; + prerr_endline ("PID " ^ string_of_int pid); + Unix.close master2worker_r; + Unix.close worker2master_w; + let cin = Unix.in_channel_of_descr worker2master_r in + let cout = Unix.out_channel_of_descr master2worker_w in + set_binary_mode_in cin true; + set_binary_mode_out cout true; + pid, cin, cout, (worker2master_r, master2worker_w) + +let filter_args args = + let rec aux = function + | "-control-channel" :: _ :: rest -> aux rest + | "-main-channel" :: _ :: rest -> aux rest + | x :: rest -> x :: aux rest + | [] -> [] in + Array.of_list (aux (Array.to_list args)) + +let spawn_with_control prefer_sock env prog args = + (* on non-Unix systems we create a control channel *) + let not_Unix = Sys.os_type <> "Unix" in + let args = filter_args args in + let args, control_sock = + if not_Unix then + let control_sock, control_sock_name = mk_socket_channel () in + let extra = [| "-control-channel"; control_sock_name |] in + Array.append extra args, Some control_sock + else + args, None in + let (pid, cin, cout, s), is_sock = + if not_Unix (* pipes only work well on Unix *) || prefer_sock + then spawn_sock env prog args, true + else spawn_pipe env prog args, false in + let oob_resp, oob_req = + if not_Unix then + let _, oob_resp, oob_req = accept (Option.get control_sock) in + Some oob_resp, Some oob_req + else + None, None in + pid, oob_resp, oob_req, cin, cout, s, is_sock + +let output_death_sentence pid oob_req = + prerr_endline ("death sentence for " ^ pid); + try output_value oob_req ReqDie; flush oob_req + with e -> prerr_endline ("death sentence: " ^ Printexc.to_string e) + +(* spawn a process and read its output asynchronously *) +module Async(ML : MainLoopModel) = struct + +type process = { + cin : in_channel; + cout : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; + gchan : ML.async_chan; + pid : int; + mutable watch : ML.watch_id option; + mutable alive : bool; +} + +type callback = ML.condition list -> read_all:(unit -> string) -> bool +type handle = process + +let is_alive p = p.alive +let uid { pid; } = string_of_int pid +let unixpid { pid; } = pid + +let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) = + p.alive <- false; + if not alive then prerr_endline "This process is already dead" + else begin try + Option.iter ML.remove_watch watch; + Option.iter (output_death_sentence (uid p)) oob_req; + close_in_noerr cin; + close_out_noerr cout; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; + if Sys.os_type = "Unix" then Unix.kill unixpid 9; + p.watch <- None + with e -> prerr_endline ("kill: "^Printexc.to_string e) end + +let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) + prog args callback += + let pid, oob_resp, oob_req, cin, cout, main, is_sock = + spawn_with_control prefer_sock env prog args in + Unix.set_nonblock (fst main); + let gchan = + if is_sock then ML.async_chan_of_socket (fst main) + else ML.async_chan_of_file (fst main) in + let alive, watch = true, None in + let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in + p.watch <- Some ( + ML.add_watch ~callback:(fun cl -> + try + let live = callback cl ~read_all:(fun () -> ML.read_all gchan) in + if not live then kill p; + live + with e when CErrors.noncritical e -> + pr_err ("Async reader raised: " ^ (Printexc.to_string e)); + kill p; + false) gchan + ); + p, cout + +let rec wait p = + (* On windows kill is not reliable, so wait may never return. *) + if Sys.os_type = "Unix" then + try snd (Unix.waitpid [] p.pid) + with + | Unix.Unix_error (Unix.EINTR, _, _) -> wait p + | Unix.Unix_error _ -> Unix.WEXITED 0o400 + else Unix.WEXITED 0o400 + +end + +module Sync () = struct + +type process = { + cin : in_channel; + cout : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; + pid : int; + mutable alive : bool; +} + +type handle = process + +let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) prog args = + let pid, oob_resp, oob_req, cin, cout, _, _ = + spawn_with_control prefer_sock env prog args in + { cin; cout; pid; oob_resp; oob_req; alive = true }, cin, cout + +let is_alive p = p.alive +let uid { pid; } = string_of_int pid +let unixpid { pid = pid; } = pid + +let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = + p.alive <- false; + if not alive then prerr_endline "This process is already dead" + else begin try + Option.iter (output_death_sentence (uid p)) oob_req; + close_in_noerr cin; + close_out_noerr cout; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; + if Sys.os_type = "Unix" then Unix.kill unixpid 9; + with e -> prerr_endline ("kill: "^Printexc.to_string e) end + +let rec wait p = + (* On windows kill is not reliable, so wait may never return. *) + if Sys.os_type = "Unix" then + try snd (Unix.waitpid [] p.pid) + with + | Unix.Unix_error (Unix.EINTR, _, _) -> wait p + | Unix.Unix_error _ -> Unix.WEXITED 0o400 + else Unix.WEXITED 0o400 + +end diff --git a/lib/spawn.mli b/lib/spawn.mli new file mode 100644 index 0000000000..944aa27a7f --- /dev/null +++ b/lib/spawn.mli @@ -0,0 +1,79 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This module implements spawning/killing managed processes with a + * synchronous or asynchronous comunication channel that works with + * threads or with a glib like main loop model. + * + * This module requires no threads and no main loop model. It takes care + * of using the fastest communication channel given the underlying OS and + * the requested kind of communication. + * + * The spawned process must use the Spawned module to init its communication + * channels. + *) + +(* This is the control panel for managed processes *) +module type Control = sig + type handle + + val kill : handle -> unit + val wait : handle -> Unix.process_status + val unixpid : handle -> int + + (* What is used in debug messages *) + val uid : handle -> string + + val is_alive : handle -> bool +end + +(* Abstraction to work with both threads and main loop models *) +module type MainLoopModel = sig + type async_chan + type condition + type watch_id + + val add_watch : callback:(condition list -> bool) -> async_chan -> watch_id + val remove_watch : watch_id -> unit + val read_all : async_chan -> string + val async_chan_of_file : Unix.file_descr -> async_chan + val async_chan_of_socket : Unix.file_descr -> async_chan +end + +(* spawn a process and read its output asynchronously *) +module Async(ML : MainLoopModel) : sig + type process + + (* If the returned value is false the callback is never called again and + * the process is killed *) + type callback = ML.condition list -> read_all:(unit -> string) -> bool + + val spawn : + ?prefer_sock:bool -> ?env:string array -> string -> string array -> + callback -> process * out_channel + + include Control with type handle = process +end + +(* spawn a process and read its output synchronously *) +module Sync () : sig + type process + + val spawn : + ?prefer_sock:bool -> ?env:string array -> string -> string array -> + process * in_channel * out_channel + + include Control with type handle = process +end + +(* This is exported to separate the Spawned module, that for simplicity assumes + * Threads so it is in a separate file *) +type req = ReqDie | Hello of int * int +val proto_version : int diff --git a/lib/stateid.ml b/lib/stateid.ml new file mode 100644 index 0000000000..8f45f3605d --- /dev/null +++ b/lib/stateid.ml @@ -0,0 +1,47 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = int +let initial = 1 +let dummy = 0 +let fresh = + let cur = ref initial in + fun () -> incr cur; !cur +let to_string = string_of_int +let of_int id = id +let to_int id = id +let newer_than id1 id2 = id1 > id2 + +let state_id_info : (t * t) Exninfo.t = Exninfo.make () +let add exn ~valid id = + Exninfo.add exn state_id_info (valid, id) +let get exn = Exninfo.get exn state_id_info + +let equal = Int.equal +let compare = Int.compare + +let print id = Pp.int id + +module Self = struct + type t = int + let compare = compare +end + +module Set = Set.Make(Self) + +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t option; + uuid : 'a; + name : string +} + diff --git a/lib/stateid.mli b/lib/stateid.mli new file mode 100644 index 0000000000..f6ce7ddc40 --- /dev/null +++ b/lib/stateid.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t + +val equal : t -> t -> bool +val compare : t -> t -> int + +module Self : Map.OrderedType with type t = t +module Set : Set.S with type elt = t and type t = Set.Make(Self).t + +val initial : t +val dummy : t +val fresh : unit -> t +val to_string : t -> string +val print : t -> Pp.t + +val of_int : int -> t +val to_int : t -> int + +val newer_than : t -> t -> bool + +(* Attaches to an exception the concerned state id, plus an optional + * state id that is a valid state id before the error. + * Backtracking to the valid id is safe. *) +val add : Exninfo.info -> valid:t -> t -> Exninfo.info +val get : Exninfo.info -> (t * t) option + +type ('a,'b) request = { + exn_info : t * t; + stop : t; + document : 'b; + loc : Loc.t option; + uuid : 'a; + name : string +} + diff --git a/lib/system.ml b/lib/system.ml new file mode 100644 index 0000000000..c408061852 --- /dev/null +++ b/lib/system.ml @@ -0,0 +1,313 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* $Id$ *) + +open Pp +open Util + +include Minisys + +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) + +let warn_cannot_open_dir = + CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem" + (fun dir -> str ("Cannot open directory " ^ dir)) + +let all_subdirs ~unix_path:root = + let l = ref [] in + let add f rel = l := (f, rel) :: !l in + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path + in + if exists_dir root then traverse root [] + else warn_cannot_open_dir root; + List.rev !l + +(* Caching directory contents for efficient syntactic equality of file + names even on case-preserving but case-insensitive file systems *) + +module StrMod = struct + type t = string + let compare = compare +end + +module StrMap = Map.Make(StrMod) +module StrSet = Set.Make(StrMod) + +let dirmap = ref StrMap.empty + +let make_dir_table dir = + let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) + +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false + +let exists_in_dir_respecting_case dir bf = + let cache_dir dir = + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + contents in + let contents, fresh = + try + (* in batch mode, assume the directory content is still fresh *) + StrMap.find dir !dirmap, !trust_file_cache + with Not_found -> + (* in batch mode, we are not yet sure the directory exists *) + if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true + else cache_dir dir, true in + StrSet.mem bf contents || + not fresh && + (* rescan, there is a new file we don't know about *) + StrSet.mem bf (cache_dir dir) + +let file_exists_respecting_case path f = + (* This function ensures that a file with expected lowercase/uppercase + is the correct one, even on case-insensitive file systems *) + let rec aux f = + let bf = Filename.basename f in + let df = Filename.dirname f in + (* When [df] is the same as [f], it means that the root of the file system + has been reached. There is no point in looking further up. *) + (String.equal df "." || String.equal f df || aux df) + && exists_in_dir_respecting_case (Filename.concat path df) bf + in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f + +let rec search paths test = + match paths with + | [] -> [] + | lpe :: rem -> test lpe @ search rem test + +let warn_ambiguous_file_name = + CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem" + (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++ + hov 0 (str "[ " ++ + hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) + (fun (lpe,_) -> str lpe) l) + ++ str " ];") ++ fnl () ++ + str "loading " ++ str f) + + +let where_in_path ?(warn=true) path filename = + let check_and_warn l = match l with + | [] -> raise Not_found + | (lpe, f) :: l' -> + let () = match l' with + | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f) + | _ -> () + in + (lpe, f) + in + check_and_warn (search path (fun lpe -> + let f = Filename.concat lpe filename in + if file_exists_respecting_case lpe filename then [lpe,f] else [])) + +let find_file_in_path ?(warn=true) paths filename = + if not (Filename.is_implicit filename) then + (* the name is considered to be a physical name and we use the file + system rules (e.g. possible case-insensitivity) to find it *) + if Sys.file_exists filename then + let root = Filename.dirname filename in + root, filename + else + CErrors.user_err ~hdr:"System.find_file_in_path" + (hov 0 (str "Can't find file" ++ spc () ++ str filename)) + else + (* the name is considered to be the transcription as a relative + physical name of a logical name, so we deal with it as a name + to be locate respecting case *) + try where_in_path ~warn paths filename + with Not_found -> + CErrors.user_err ~hdr:"System.find_file_in_path" + (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ + str "on loadpath")) + +let is_in_path lpath filename = + try ignore (where_in_path ~warn:false lpath filename); true + with Not_found -> false + +let warn_path_not_found = + CWarnings.create ~name:"path-not-found" ~category:"filesystem" + (fun () -> str "system variable PATH not found") + +let is_in_system_path filename = + try + let lpath = CUnix.path_to_list (Sys.getenv "PATH") in + is_in_path lpath filename + with Not_found -> + warn_path_not_found (); + false + +let open_trapping_failure name = + try open_out_bin name + with e when CErrors.noncritical e -> + CErrors.user_err ~hdr:"System.open" (str "Can't open " ++ str name) + +let warn_cannot_remove_file = + CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem" + (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!") + +let try_remove filename = + try Sys.remove filename + with e when CErrors.noncritical e -> + warn_cannot_remove_file filename + +let error_corrupted file s = + CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") + +let input_binary_int f ch = + try input_binary_int ch + with + | End_of_file -> error_corrupted f "premature end of file" + | Failure s -> error_corrupted f s +let output_binary_int ch x = output_binary_int ch x; flush ch + +let marshal_out ch v = Marshal.to_channel ch v []; flush ch +let marshal_in filename ch = + try Marshal.from_channel ch + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s -> error_corrupted filename s + +let digest_out = Digest.output +let digest_in filename ch = + try Digest.input ch + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s -> error_corrupted filename s + +let marshal_out_segment f ch v = + let start = pos_out ch in + output_binary_int ch 0; (* dummy value for stop *) + marshal_out ch v; + let stop = pos_out ch in + seek_out ch start; + output_binary_int ch stop; + seek_out ch stop; + digest_out ch (Digest.file f) + +let marshal_in_segment f ch = + let stop = (input_binary_int f ch : int) in + let v = marshal_in f ch in + let digest = digest_in f ch in + v, stop, digest + +let skip_in_segment f ch = + let stop = (input_binary_int f ch : int) in + seek_in ch stop; + stop, digest_in f ch + +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error + +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + let actual_magic = input_binary_int filename channel in + if not (Int.equal actual_magic magic) then + raise (Bad_magic_number { + filename=filename; + actual=actual_magic; + expected=magic}); + channel + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s + +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in + try + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = CErrors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + CErrors.user_err ~hdr:"System.intern_state" (str "System error: " ++ str s) + +let with_magic_number_check f a = + try f a + with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> + CErrors.user_err ~hdr:"with_magic_number_check" + (str"File " ++ str fname ++ strbrk" has bad magic number " ++ + int actual ++ str" (expected " ++ int expected ++ str")." ++ + spc () ++ + strbrk "It is corrupted or was compiled with another version of Coq.") + +(* Time stamps. *) + +type time = float * float * float + +let get_time () = + let t = Unix.times () in + (Unix.gettimeofday(), t.Unix.tms_utime, t.Unix.tms_stime) + +(* Keep only 3 significant digits *) +let round f = (floor (f *. 1e3)) *. 1e-3 + +let time_difference (t1,_,_) (t2,_,_) = round (t2 -. t1) + +let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = + real (round (stopreal -. startreal)) ++ str " secs " ++ + str "(" ++ + real (round (ustop -. ustart)) ++ str "u" ++ + str "," ++ + real (round (sstop -. sstart)) ++ str "s" ++ + str ")" + +let with_time ~batch ~header f x = + let tstart = get_time() in + let msg = if batch then "" else "Finished transaction in " in + try + let y = f x in + let tend = get_time() in + let msg2 = if batch then "" else " (successful)" in + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + y + with e -> + let tend = get_time() in + let msg = if batch then "" else "Finished failing transaction in " in + let msg2 = if batch then "" else " (failure)" in + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); + raise e + +(* We use argv.[0] as we don't want to resolve symlinks *) +let get_toplevel_path ?(byte=Sys.(backend_type = Bytecode)) top = + let open Filename in + let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) + then "" else dirname Sys.argv.(0) ^ dir_sep in + let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in + let eff = if byte then ".byte" else ".opt" in + dir ^ top ^ eff ^ exe diff --git a/lib/system.mli b/lib/system.mli new file mode 100644 index 0000000000..6dd1eb5a84 --- /dev/null +++ b/lib/system.mli @@ -0,0 +1,126 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** {5 Coqtop specific system utilities} *) + +(** {6 Directories} *) + +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +val (//) : unix_path -> string -> unix_path + +val exists_dir : unix_path -> bool + +(** [exclude_search_in_dirname path] excludes [path] when processing + directories *) + +val exclude_directory : unix_path -> unit + +(** [process_directory f path] applies [f] on contents of directory + [path]; fails with Unix_error if the latter does not exists; skips + all files or dirs starting with "." *) + +val process_directory : (file_kind -> unit) -> unix_path -> unit + +(** [process_subdirectories f path] applies [f path/file file] on each + [file] of the directory [path]; fails with Unix_error if the + latter does not exists; kips all files or dirs starting with "." *) + +val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit + +(** {6 Files and load paths} *) + +(** Load path entries remember the original root + given by the user. For efficiency, we keep the full path (field + [directory]), the root path and the path relative to the root. *) + +val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list +val is_in_path : CUnix.load_path -> string -> bool +val is_in_system_path : string -> bool +val where_in_path : + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string + +val find_file_in_path : + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string + +val trust_file_cache : bool ref +(** [trust_file_cache] indicates whether we trust the underlying + mapped file-system not to change along the execution of Coq. This + assumption greatly speds up file search, but it is often + inconvenient in interactive mode *) + +val file_exists_respecting_case : string -> string -> bool + +(** {6 I/O functions } *) +(** Generic input and output functions, parameterized by a magic number + and a suffix. The intern functions raise the exception [Bad_magic_number] + when the check fails, with the full file name and expected/observed magic + numbers. *) + +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error + +val raw_extern_state : int -> string -> out_channel + +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a + +val with_magic_number_check : ('a -> 'b) -> 'a -> 'b + +(** Clones of Marshal.to_channel (with flush) and + Marshal.from_channel (with nice error message) *) + +val marshal_out : out_channel -> 'a -> unit +val marshal_in : string -> in_channel -> 'a + +(** Clones of Digest.output and Digest.input (with nice error message) *) + +val digest_out : out_channel -> Digest.t -> unit +val digest_in : string -> in_channel -> Digest.t + +val marshal_out_segment : string -> out_channel -> 'a -> unit +val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t +val skip_in_segment : string -> in_channel -> int * Digest.t + +(** {6 Time stamps.} *) + +type time + +val get_time : unit -> time +val time_difference : time -> time -> float (** in seconds *) + +val fmt_time_difference : time -> time -> Pp.t + +val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b + +(** [get_toplevel_path program] builds a complete path to the + executable denoted by [program]. This involves: + + - locating the directory: we don't rely on PATH as to make calls to + /foo/bin/coqtop chose the right /foo/bin/coqproofworker + + - adding the proper suffixes: .opt/.byte depending on the current + mode, + .exe if in windows. + + Note that this function doesn't check that the executable actually + exists. This is left back to caller, as well as the choice of + fallback strategy. We could add a fallback strategy here but it is + better not to as in most cases if this function fails to construct + the right name you want you execution to fail rather than fall into + choosing some random binary from the system-wide installation of + Coq. *) +val get_toplevel_path : ?byte:bool -> string -> string diff --git a/lib/util.ml b/lib/util.ml new file mode 100644 index 0000000000..0389336258 --- /dev/null +++ b/lib/util.ml @@ -0,0 +1,190 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Mapping under pairs *) + +let on_fst f (a,b) = (f a,b) +let on_snd f (a,b) = (a,f b) +let map_pair f (a,b) = (f a,f b) + +(* Mapping under pairs *) + +let on_pi1 f (a,b,c) = (f a,b,c) +let on_pi2 f (a,b,c) = (a,f b,c) +let on_pi3 f (a,b,c) = (a,b,f c) + +(* Comparing pairs *) + +let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) = + if p1 == p2 then 0 else + let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c + +(* Projections from triplets *) + +let pi1 (a,_,_) = a +let pi2 (_,a,_) = a +let pi3 (_,_,a) = a + +(* Characters *) + +let is_letter c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') +let is_digit c = (c >= '0' && c <= '9') +let is_ident_tail c = + is_letter c || is_digit c || c = '\'' || c = '_' +let is_blank = function + | ' ' | '\r' | '\t' | '\n' -> true + | _ -> false + +module Empty = +struct + type t = { abort : 'a. 'a } + let abort (x : t) = x.abort +end + +(* Strings *) + +module String : CString.ExtS = CString + +let subst_command_placeholder s t = + let buff = Buffer.create (String.length s + String.length t) in + let i = ref 0 in + while (!i < String.length s) do + if s.[!i] = '%' && !i+1 < String.length s && s.[!i+1] = 's' + then (Buffer.add_string buff t;incr i) + else Buffer.add_char buff s.[!i]; + incr i + done; + Buffer.contents buff + +(* Lists *) + +module List : CList.ExtS = CList + +let (@) = CList.append + +(* Arrays *) + +module Array : CArray.ExtS = CArray + +(* Sets *) + +module Set = CSet + +(* Maps *) + +module Map = CMap + +(* Stacks *) + +module Stack = CStack + +(* Matrices *) + +let matrix_transpose mat = + List.fold_right (List.map2 (fun p c -> p::c)) mat + (if List.is_empty mat then [] else List.map (fun _ -> []) (List.hd mat)) + +(* Functions *) + +let identity x = x + +(** Left-to-right function composition: + + [f1 %> f2] is [fun x -> f2 (f1 x)]. + + [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))]. + + [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))] + + etc. +*) +let (%>) f g x = g (f x) + +let const x _ = x + +let iterate = + let rec iterate_f f n x = + if n <= 0 then x else iterate_f f (pred n) (f x) + in + iterate_f + +let repeat n f x = + let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n + +let app_opt f x = + match f with + | Some f -> f x + | None -> x + +(* Stream *) + +let stream_nth n st = + try List.nth (Stream.npeek (n+1) st) n + with Failure _ -> raise Stream.Failure + +let stream_njunk n st = + repeat n Stream.junk st + +(* Delayed computations *) + +type 'a delayed = unit -> 'a + +let delayed_force f = f () + +(* Misc *) + +type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b +type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq + +let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl + +module Union = +struct + let map f g = function + | Inl a -> Inl (f a) + | Inr b -> Inr (g b) + + (** Lifting equality onto union types. *) + let equal f g x y = match x, y with + | Inl x, Inl y -> f x y + | Inr x, Inr y -> g x y + | _, _ -> false + + let fold_left f g a = function + | Inl y -> f a y + | Inr y -> g a y +end + +let map_union = Union.map + +type iexn = Exninfo.iexn + +let iraise = Exninfo.iraise + +let open_utf8_file_in fname = + let is_bom s = + Int.equal (Char.code (Bytes.get s 0)) 0xEF && + Int.equal (Char.code (Bytes.get s 1)) 0xBB && + Int.equal (Char.code (Bytes.get s 2)) 0xBF + in + let in_chan = open_in fname in + let s = Bytes.make 3 ' ' in + if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; + in_chan + +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) + +let set_temporary_memory () = + let a = ref None in + (fun x -> assert (!a = None); a := Some x; x), + (fun () -> match !a with Some x -> x | None -> assert false) diff --git a/lib/util.mli b/lib/util.mli new file mode 100644 index 0000000000..fa3b622621 --- /dev/null +++ b/lib/util.mli @@ -0,0 +1,150 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** This module contains numerous utility functions on strings, lists, + arrays, etc. *) + +(** Mapping under pairs *) + +val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c +val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b +val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b + +(** Comparing pairs *) + +val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int) + +(** Mapping under triple *) + +val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd +val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd +val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b + +(** {6 Projections from triplets } *) + +val pi1 : 'a * 'b * 'c -> 'a +val pi2 : 'a * 'b * 'c -> 'b +val pi3 : 'a * 'b * 'c -> 'c + +(** {6 Chars. } *) + +val is_letter : char -> bool +val is_digit : char -> bool +val is_ident_tail : char -> bool +val is_blank : char -> bool + +(** {6 Empty type} *) + +module Empty : +sig + type t + val abort : t -> 'a +end + +(** {6 Strings. } *) + +module String : CString.ExtS + +(** Substitute %s in the first chain by the second chain *) +val subst_command_placeholder : string -> string -> string + +(** {6 Lists. } *) + +module List : CList.ExtS + +val (@) : 'a list -> 'a list -> 'a list + +(** {6 Arrays. } *) + +module Array : CArray.ExtS + +(** {6 Sets. } *) + +module Set : module type of CSet + +(** {6 Maps. } *) + +module Map : module type of CMap + +(** {6 Stacks.} *) + +module Stack : module type of CStack + +(** {6 Streams. } *) + +val stream_nth : int -> 'a Stream.t -> 'a +val stream_njunk : int -> 'a Stream.t -> unit + +(** {6 Matrices. } *) + +val matrix_transpose : 'a list list -> 'a list list + +(** {6 Functions. } *) + +val identity : 'a -> 'a + +(** Left-to-right function composition: + + [f1 %> f2] is [fun x -> f2 (f1 x)]. + + [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))]. + + [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))] + + etc. +*) +val ( %> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c + +val const : 'a -> 'b -> 'a +val iterate : ('a -> 'a) -> int -> 'a -> 'a +val repeat : int -> ('a -> unit) -> 'a -> unit +val app_opt : ('a -> 'a) option -> 'a -> 'a + +(** {6 Delayed computations. } *) + +type 'a delayed = unit -> 'a + +val delayed_force : 'a delayed -> 'a + +(** {6 Enriched exceptions} *) + +type iexn = Exninfo.iexn + +val iraise : iexn -> 'a + +(** {6 Misc. } *) + +type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b +(** Union type *) + +module Union : +sig + val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union + val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool + val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c +end + +val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union +(** Alias for [Union.map] *) + +type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a +(** Used for browsable-until structures. *) + +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq + +val sym : ('a, 'b) eq -> ('b, 'a) eq + +val open_utf8_file_in : string -> in_channel +(** Open an utf-8 encoded file and skip the byte-order mark if any. *) + +val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a) +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli new file mode 100644 index 0000000000..19c046e95c --- /dev/null +++ b/lib/xml_datatype.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** ['a gxml] is the type for semi-structured documents. They generalize + XML by allowing any kind of attributes. *) +type 'a gxml = + | Element of (string * 'a * 'a gxml list) + | PCData of string + +(** [xml] is a semi-structured documents where attributes are association + lists from string to string. *) +type xml = (string * string) list gxml + + |