citadelle-devel/LICENSE0.thy

312 lines
13 KiB
Plaintext

(******************************************************************************
* LICENSE
*
* Copyright (c) 2017-2018 Virginia Tech, USA
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
theory LICENSE0
imports Main
keywords "portions"
and "project" "country" "holder" "copyright" "license"
"check_license" "insert_license" "map_license" :: thy_decl
begin
ML\<open>
structure Resources' = struct
fun check_path' check_file ctxt dir (name, pos) =
let
fun err msg pos = error (msg ^ Position.here pos)
val _ = Context_Position.report ctxt pos Markup.language_path;
val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
val path' = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
val _ =
(case check_file of
NONE => path
| SOME check => (check path handle ERROR msg => err msg pos));
in path' end
fun check_dir thy = check_path' (SOME File.check_dir)
(Proof_Context.init_global thy)
(Resources.master_directory thy)
end
fun fold_dir f path =
File.fold_dir
(fn s =>
let val path = Path.append path (Path.explode s)
in if File.is_dir path then fold_dir f path else f path end)
path
\<close>
ML\<open>
datatype ('a, 'b) either = Left of 'a | Right of 'b
fun the_left (Left a) = a
signature OBJECT = sig
type T
val key : string
val pretty : T -> string
end
functor Theory_Data' (Obj : OBJECT) : THEORY_DATA = Theory_Data
(type T = Obj.T Name_Space.table
val empty = Name_Space.empty_table Obj.key
val extend = I
val merge = Name_Space.merge_tables)
val pretty_input = Input.source_content #> split_lines #> trim (fn s => s = "") #> cat_lines
structure Country0 : OBJECT = struct
type T = Input.source
val key = "country"
val pretty = pretty_input
end
structure Country = Theory_Data' (Country0)
structure Holder0 : OBJECT = struct
type T = Input.source list * Country0.T option
val key = "holder"
fun pretty (l, country) =
let val sep = ", " in
String.concatWith sep (map (fn s => s |> Input.source_explode |> trim (Symbol.is_blank o Symbol_Pos.symbol) |> Symbol_Pos.content) l)
^ (case country of NONE => "" | SOME country => sep ^ Country0.pretty country)
end
end
structure Holder = Theory_Data' (Holder0)
datatype date = D_interval of int (*date min*) * int (*date max*)
| D_discrete of int list
structure Date0 : OBJECT where type T = date = struct
type T = date
val key = "date"
val pretty = fn D_interval (d_min, d_max) => Int.toString d_min ^ "-" ^ Int.toString d_max
| D_discrete l => String.concatWith "," (map Int.toString l)
end
structure Copyright0 : OBJECT = struct
type T = (bool (*false: portions copyright*) * Date0.T * Holder0.T list) list
val key = "copyright"
fun pretty l =
let
val s_copy = "Copyright (c) "
fun s_portions b = if b then Symbol.spaces (String.size s_copy) else "Portions " ^ s_copy
in
case map (fn (b, date, l) => (b, case l of h :: hs => let val s_date = Date0.pretty date ^ " "
in s_date ^ Holder0.pretty h
:: map (fn h => Symbol.spaces (String.size s_date) ^ Holder0.pretty h) hs end)) l
of (true, l) :: ls =>
let fun f s_copy (l :: ls) =
s_copy ^ l ^ String.concat (map (fn s => "\n" ^ Symbol.spaces (String.size s_copy) ^ s) ls)
in f s_copy l ^ String.concat (map (fn (b, l) => "\n" ^ f (s_portions b) l) ls) end
end
end
structure Copyright = Theory_Data' (Copyright0)
structure License0 : OBJECT = struct
type T = Input.source
val key = "license"
val pretty = pretty_input
end
structure License = Theory_Data' (License0)
type project_head = (Input.source * Copyright0.T) list
structure Project0 : sig include OBJECT val pretty0 : bool -> project_head * Input.source -> string
end = struct
type T = project_head * License0.T
val key = "project"
fun wrap_stars s =
let val stars = "******************************************************************************" in
cat_lines
("(" ^ stars
:: map ((fn s => " *" ^ s) o (fn "" => "" | s => " " ^ s)) (split_lines s)
@ [" " ^ stars ^ ")"])
end
fun pretty0 stars (l, lic) =
let val s_end = case l of [_] => "" | _ => "\n\n * * * * * * * * * * * * * * * * * * * * * * * * *"
in String.concat (map (fn (src, copy) => pretty_input src ^ (if stars then "" else " " ^ Symbol.open_) ^ "\n\n" ^ Copyright0.pretty copy ^ s_end ^ (if stars then "" else " " ^ Symbol.close ^ Symbol.open_) ^ "\n\n") l)
^ License0.pretty lic
|> (if stars then wrap_stars else fn s => s ^ "\n" ^ Symbol.close)
end
val pretty = pretty0 true
end
structure Project = Theory_Data' (Project0)
fun define0 data_map n thy = data_map (#2 o Name_Space.define (Context.Theory thy) true n) thy
fun define key data_map n =
( key
, Toplevel.theory
(fn thy => data_map (#2 o Name_Space.define (Context.Theory thy) true n)
thy))
local
fun check0 f_map key data_get f n f_left =
( key
, Toplevel.theory
(fn thy => f (f_map (fn (Right a, v) => (Right a, v)
| (Left k, v) => (Left (f_left (Name_Space.check (Context.Theory thy) (data_get thy)) k), v)) n) thy))
in
fun check key data_get f n = check0 (fn f => Option.map (the_left o #1 o f)) key data_get f (Option.map (fn n => (Left n, ())) n)
fun check' key = check0 map key
end
structure Parse' = struct
datatype copyright = C_ref of string * Position.T
| C_def of (((string option * int) * (bool * int) option) * (string * Position.T) list) list
val copyright =
Scan.repeat (Scan.option (Parse.$$$ "portions") -- Parse.nat -- Scan.option ((Parse.$$$ "," >> K false || Parse.minus >> K true) -- Parse.nat) -- Parse.list1 (Parse.position Parse.name))
fun copyright_check key f = check' key Holder.get f
fun copyright_check' h ((portions, d0), opt_d) =
( portions = NONE
, case opt_d of SOME (true, d_max) => D_interval (d0, d_max)
| SOME (false, d1) => D_discrete [d0, d1]
| NONE => D_discrete [d0]
, h)
end
val _ =
Outer_Syntax.commands @{command_keyword project} "formal comment (primary style)"
(Parse.binding --| Parse.$$$ "::" -- Parse.position Parse.name -- Scan.repeat1 (Parse.where_ |-- Parse.document_source --
( Parse.$$$ "imports" |-- Parse.position Parse.name >> Parse'.C_ref
|| Parse.$$$ "defines" |-- Parse'.copyright >> Parse'.C_def)) >>
(fn ((n, lic), l_pj) =>
[( @{command_keyword project}
, Toplevel.theory
(fn thy =>
define0
Project.map
( n
, ( map (fn (x, opt_n) =>
(x, case opt_n of
Parse'.C_ref n => #2 (Name_Space.check (Context.Theory thy) (Copyright.get thy) n)
| Parse'.C_def l_src => map (fn (v, holder) => Parse'.copyright_check' (map (#2 o Name_Space.check (Context.Theory thy) (Holder.get thy)) holder) v) l_src))
l_pj
, #2 (Name_Space.check (Context.Theory thy) (License.get thy) lic)))
thy))]));
val _ =
Outer_Syntax.commands @{command_keyword country} "formal comment (primary style)"
(Parse.binding --| Parse.where_ -- Parse.document_source >>
(fn (n, src) =>
[ define @{command_keyword country} Country.map (n, src)
, (@{command_keyword country}, Pure_Syn.document_command {markdown = true} (NONE, src))]));
val _ =
Outer_Syntax.commands @{command_keyword holder} "formal comment (primary style)"
(Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.position Parse.name) --| Parse.where_ -- Parse.list Parse.document_source >>
(fn ((name, country), l_src) =>
check
@{command_keyword holder}
Country.get
(fn country => define0 Holder.map (name, (l_src, Option.map #2 country)))
country
I
:: map (fn src =>
(@{command_keyword holder}, Pure_Syn.document_command {markdown = true} (NONE, src)))
l_src));
val _ =
Outer_Syntax.commands @{command_keyword copyright} "formal comment (primary style)"
(Parse.binding --| Parse.where_ -- Parse'.copyright >>
(fn (n, l_src) =>
[Parse'.copyright_check
@{command_keyword copyright}
(fn l => define0
Copyright.map
(n, map (fn (Left h, d) => Parse'.copyright_check' h d) l))
(map (fn (a, b) => (Left b, a)) l_src)
(fn f => map (#2 o f))]));
val _ =
Outer_Syntax.commands @{command_keyword license} "formal comment (primary style)"
(Parse.binding --| Parse.where_ -- Parse.document_source (* ignored for bootstrapping *)
-- Parse.document_source >>
(fn ((n, _), src) =>
[ define @{command_keyword license} License.map (n, src)
, (@{command_keyword license}, Pure_Syn.document_command {markdown = true} (NONE, src))]));
val _ =
Outer_Syntax.commands' @{command_keyword check_license} "formal comment (primary style)"
(Scan.repeat (Parse.position Parse.name) --| Parse.$$$ "in" -- Scan.option (Parse.$$$ "file") -- Parse.position Parse.path >>
(fn ((pj, file), loc) => fn thy => fn _ =>
let
fun head stars = map (fn n => Project0.pretty0 stars (#2 (Name_Space.check (Context.Theory thy) (Project.get thy) n))) pj
val l_head = head true
val l_head0 = head false
(*val _ = List.app (fn s => writeln s) l_head0*)
fun f s =
let
fun f_exists f_un s l = fold (fn p => fn b => b orelse try (f_un p) s <> NONE) l false
in
cons ( @{command_keyword check_license}
, Toplevel.keep
(fn _ =>
let val base_name = Path.base_name s
in
if f_exists unprefix (File.read s) (if base_name = "LICENSE.thy" then l_head0 else l_head) then
writeln (@{make_string} s)
else if f_exists unsuffix base_name [".thy", ".ml", ".ML", "ROOT"] then
error (@{make_string} s)
else
warning (@{make_string} s)
end))
end
in
(case file of NONE => fold_dir f (Resources'.check_dir thy loc)
| SOME _ => f (Resources'.check_path' (SOME File.check_file) (Proof_Context.init_global thy) (Resources.master_directory thy) loc))
[]
end))
val _ =
Outer_Syntax.command @{command_keyword insert_license} "formal comment (primary style)"
(Scan.option Parse.binding >>
(fn _ => Toplevel.keep (fn _ => warning "to be implemented")))
val _ =
Outer_Syntax.command @{command_keyword map_license} "formal comment (primary style)"
(Scan.option Parse.binding >>
(fn _ => Toplevel.keep (fn _ => warning "to be implemented")))
\<close>
end