(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \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) *) (************************************************************************)
(** Abstract representations of values in a vo *)
(** NB: This needs updating when the types in declarations.ml and
their dependencies are changed. *)
(** We reify here the types of values present in a vo. in order to validate its structure. Maybe this reification could become automatically generated someday ?
See values.mli for the meaning of each constructor.
*)
type ('a,_) t =
| [] : ('a, [`O]) t
| (::) : 'a * ('a, 's) t -> ('a, [`S of's]) t
type'n size = (unit,'n) t
let rec vmap : 'n 'a 'b. ('a -> 'b) -> ('a,'n) t -> ('b, 'n) t = fun (type n) f (v:(_,n) t) : (_,n) t -> match v with
| [] -> []
| x :: tl -> let x = f x in
x :: vmap f tl
let rec viter2 : 'n 'a 'b. ('a -> 'b -> unit) -> ('a,'n) t -> ('b,'n) t -> unit = fun (type n) f (v1:(_,n) t) (v2:(_,n) t) -> match v1, v2 with
| [], []-> ()
| x1 :: tl1, x2 :: tl2 -> let () = f x1 x2 in
viter2 f tl1 tl2 end
module Internal : sig type value
val equal : value -> value -> bool
val kind : value -> value kind
val of_kind : value kind -> value
val mfix : 'n Vector.size -> ((value,'n) Vector.t -> (value,'n) Vector.t) -> (value,'n) Vector.t end = struct type value =
| V of value kind
| Proxy of value kind ref
let kind = function
| V v -> v
| Proxy v -> !v
(* Proxy is equal to its contents *) let equal a b = kind a == kind b
let of_kind v = V v
let check_productive = function
| Proxy _ -> assert false
| V v -> v
let mfix (type n) (n:n Vector.size) (f : (value,n) Vector.t -> (value,n) Vector.t) : (value,n) Vector.t = letopen Vector in let self = vmap (fun () -> Proxy (ref Any)) n in let ans = f self in let () = viter2 (fun self ans -> let ans = check_productive ans in match self with
| Proxy self -> self := ans
| _ -> assert false)
self ans in
ans
end
type nonrec value = Internal.value
let equal = Internal.equal
let kind = Internal.kind
let of_kind = Internal.of_kind
let mfix = Internal.mfix
let fix f = let [v] : _ Vector.t = mfix [()] (fun [v] -> [f v]) in
v
(** Some pseudo-constructors *)
let v_tuple name v = of_kind @@ Tuple(name,v) let v_sum name cc vv = of_kind @@ Sum(name,cc,vv) let v_enum name n = of_kind @@ Sum(name,n,[||]) let v_annot a v = of_kind @@ Annot (a, v) let v_fail f = of_kind @@ Fail f
(* uncurried forms *)
let v_tuple_c (name,v) = v_tuple name v let v_sum_c (name,cc,vv) = v_sum name cc vv let v_annot_c (a, v) = v_annot a v
(** Ocaml standard library *)
let v_any = of_kind Any let v_int = of_kind Int let v_int64 = of_kind Int64 let v_float64 = of_kind Float64 let v_string = of_kind String let v_opt v = of_kind @@ Opt v let v_list v = of_kind @@ List v let v_array v = of_kind @@ Array v let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 let v_unit = v_enum "unit" 1
let v_set v =
fix (fun s ->
v_sum_c ("Set.t",1,
[|[|s; v_annot_c ("elem", v); s; v_annot_c ("bal", v_int)|]|]))
let v_map vk vd =
fix (fun m ->
v_sum_c ("Map.t",1,
[|[|m; v_annot_c("key",vk); v_annot_c("data",vd); m; v_annot_c("bal",v_int)|]|]))
let v_hset v = v_map v_int (v_set v) let v_hmap vk vd = v_map v_int (v_map vk vd)
let v_pred v = v_pair v_bool (v_set v)
(** kernel/names *)
let v_id = v_string let v_dp = v_annot_c ("dirpath", v_list v_id) let v_name = v_sum "name" 1 [|[|v_id|]|] let v_uid = v_tuple "uniq_ident" [|v_int;v_string;v_dp|] let v_mp =
fix (fun v_mp ->
v_sum_c("module_path",0,
[|[|v_dp|];
[|v_uid|];
[|v_mp;v_id|]|])) let v_kn = v_tuple "kernel_name" [|v_mp;v_id;v_int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;v_int|] let v_cons = v_tuple "constructor" [|v_ind;v_int|]
(** kernel/univ *) let v_level_global = v_tuple "Level.Global.t" [|v_dp;v_string;v_int|] let v_raw_level = v_sum "raw_level" 1 (* Set *)
[|(*Level*)[|v_level_global|]; (*Var*)[|v_int|]|] let v_level = v_tuple "level" [|v_int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;v_int|] let v_univ = v_list v_expr
let v_qglobal = v_pair v_dp v_id
(* perhaps the "Unif" constructor should be forbidden in vo files *) let v_qvar = v_sum "qvar" 0 [|[|v_int|];[|v_string;v_int|];[|v_qglobal|]|]
let v_constant_quality = v_enum "constant_quality" 3
let v_quality = v_sum "quality" 0 [|[|v_qvar|];[|v_constant_quality|]|]
let v_instance = v_annot_c ("instance", v_pair (v_array v_quality) (v_array v_level)) let v_abs_context = v_tuple "abstract_universe_context" [|v_pair (v_array v_name) (v_array v_name); v_cstrs|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)
let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|];[|v_qvar;v_univ(*QSort*)|]|]
let v_relevance = v_sum "relevance" 2 [|[|v_qvar|]|] let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in let v_cprint = v_tuple "case_printing" [|v_cstyle|] in
v_tuple "case_info" [|v_ind;v_int;v_array v_int;v_array v_int;v_cprint|]
let v_cast = v_enum "cast_kind" 3
let v_proj_repr = v_tuple "projection_repr" [|v_ind;v_int;v_int;v_cst|] let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
let v_uint63 = if Sys.word_size == 64 then v_int else v_int64
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
