package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/src/coq-core.checklib/validate.ml.html
Source file validate.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
(************************************************************************) (* * The Coq Proof Assistant / The Coq 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) *) (************************************************************************) open Analyze (* This module defines validation functions to ensure an imported value (using input_value) has the correct structure. *) let rec pr_obj_rec mem o = match o with | Int i -> Format.print_int i | Ptr p -> let v = LargeArray.get mem p in begin match v with | Struct (tag, data) -> let n = Array.length data in Format.print_string ("#"^string_of_int tag^"("); Format.open_hvbox 0; for i = 0 to n-1 do pr_obj_rec mem (Array.get data i); if i<>n-1 then (Format.print_string ","; Format.print_cut()) done; Format.close_box(); Format.print_string ")" | String s -> Format.print_string ("\""^String.escaped s^"\"") | Int64 _ | Float64 _ -> Format.print_string "?" end | Atm tag -> Format.print_string ("#"^string_of_int tag^"()"); | Fun addr -> Format.printf "fun@%x" addr let pr_obj mem o = pr_obj_rec mem o; Format.print_newline() (**************************************************************************) (* Obj low-level validators *) type error_frame = | CtxAnnot of string | CtxType of string | CtxField of int | CtxTag of int type error_context = error_frame list let mt_ec : error_context = [] let (/) (ctx:error_context) s : error_context = s::ctx exception ValidObjError of string * error_context * data let fail _mem ctx o s = raise (ValidObjError(s,ctx,o)) let is_block mem o = match o with | Ptr _ | Atm _ -> true | Fun _ | Int _ -> false let is_int _mem o = match o with | Int _ -> true | Fun _ | Ptr _ | Atm _ -> false let is_int64 mem o = match o with | Int _ | Fun _ | Atm _ -> false | Ptr p -> match LargeArray.get mem p with | Int64 _ -> true | Float64 _ | Struct _ | String _ -> false let is_float64 mem o = match o with | Int _ | Fun _ | Atm _ -> false | Ptr p -> match LargeArray.get mem p with | Float64 _ -> true | Int64 _ | Struct _ | String _ -> false let get_int _mem = function | Int i -> i | Fun _ | Ptr _ | Atm _ -> assert false let tag mem o = match o with | Atm tag -> tag | Fun _ -> Obj.out_of_heap_tag | Int _ -> Obj.int_tag | Ptr p -> match LargeArray.get mem p with | Struct (tag, _) -> tag | String _ -> Obj.string_tag | Float64 _ -> Obj.double_tag | Int64 _ -> Obj.custom_tag let size mem o = match o with | Atm _ -> 0 | Fun _ | Int _ -> assert false | Ptr p -> match LargeArray.get mem p with | Struct (tag, blk) -> Array.length blk | String _ | Float64 _ | Int64 _ -> assert false let field mem o i = match o with | Atm _ | Fun _ | Int _ -> assert false | Ptr p -> match LargeArray.get mem p with | Struct (tag, blk) -> Array.get blk i | String _ | Float64 _ | Int64 _ -> assert false (* Check that object o is a block with tag t *) let val_tag t mem ctx o = if is_block mem o && tag mem o = t then () else fail mem ctx o ("expected tag "^string_of_int t) let val_block mem ctx o = if is_block mem o then (if tag mem o > Obj.no_scan_tag then fail mem ctx o "block: found no scan tag") else fail mem ctx o "expected block obj" let val_dyn mem ctx o = let fail () = fail mem ctx o "expected a Dyn.t" in if not (is_block mem o) then fail () else if not (size mem o = 2) then fail () else if not (tag mem (field mem o 0) = Obj.int_tag) then fail () else () open Values let rec val_gen v mem ctx o = match v with | Tuple (name,vs) -> val_tuple ~name vs mem ctx o | Sum (name,cc,vv) -> val_sum name cc vv mem ctx o | Array v -> val_array v mem ctx o | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] mem ctx o | Opt v -> val_sum "option" 1 [|[|v|]|] mem ctx o | Int -> if not (is_int mem o) then fail mem ctx o "expected an int" | String -> (try val_tag Obj.string_tag mem ctx o with Failure _ -> fail mem ctx o "expected a string") | Any -> () | Fail s -> fail mem ctx o ("unexpected object " ^ s) | Annot (s,v) -> val_gen v mem (ctx/CtxAnnot s) o | Dyn -> val_dyn mem ctx o | Proxy { contents = v } -> val_gen v mem ctx o | Int64 -> val_int64 mem ctx o | Float64 -> val_float64 mem ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the expected size of the object. *) and val_tuple ?name vs mem ctx o = let ctx = match name with | Some n -> ctx/CtxType n | _ -> ctx in let n = Array.length vs in let val_fld i v = val_gen v mem (ctx/(CtxField i)) (field mem o i) in val_block mem ctx o; if size mem o = n then Array.iteri val_fld vs else fail mem ctx o ("tuple size: found "^string_of_int (size mem o)^ ", expected "^string_of_int n) (* Check that the object is either a constant constructor of tag < cc, or a constructed variant. each element of vv is an array of value representations of the constructor arguments. The size of vv corresponds to the number of non-constant constructors, and the size of vv.(i) is the expected arity of the i-th non-constant constructor. *) and val_sum name cc vv mem ctx o = let ctx = ctx/CtxType name in if is_block mem o then (val_block mem ctx o; let n = Array.length vv in let i = tag mem o in let ctx' = if n=1 then ctx else ctx/CtxTag i in if i < n then val_tuple vv.(i) mem ctx' o else fail mem ctx' o ("sum: unexpected tag")) else if is_int mem o then let (n:int) = get_int mem o in (if n<0 || n>=cc then fail mem ctx o ("bad constant constructor "^string_of_int n)) else fail mem ctx o "not a sum" (* Check the o is an array of values satisfying f. *) and val_array v mem ctx o = val_block mem (ctx/CtxType "array") o; for i = 0 to size mem o - 1 do val_gen v mem ctx (field mem o i) done and val_int64 mem ctx o = if not (is_int64 mem o) then fail mem ctx o "not a 63-bit unsigned integer" and val_float64 mem ctx o = if not (is_float64 mem o) then fail mem ctx o "not a 64-bit float" let print_frame = function | CtxType t -> t | CtxAnnot t -> t | CtxField i -> Printf.sprintf "fld=%i" i | CtxTag i -> Printf.sprintf "tag=%i" i let validate v (o, mem) = try val_gen v mem mt_ec o with ValidObjError(msg,ctx,obj) -> let rctx = List.rev_map print_frame ctx in print_endline ("Context: "^String.concat"/"rctx); pr_obj mem obj; failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>