package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
doc/src/lambdapi.core/builtin.ml.html
Source file builtin.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
(** Registering and checking builtin symbols. *) open Lplib open Base open Extra open Timed open Common open Error open Pos open Term open Sig_state (** [get ss pos name] returns the symbol mapped to the builtin [name]. If the symbol cannot be found then [Fatal] is raised. *) let get : sig_state -> popt -> string -> sym = fun ss pos name -> try StrMap.find name ss.builtins with Not_found -> fatal pos "Builtin symbol \"%s\" undefined." name (** [get_opt ss name] returns [Some s] where [s] is the symbol mapped to the builtin [name], and [None] otherwise. *) let get_opt : sig_state -> string -> sym option = fun ss name -> try Some (StrMap.find name ss.builtins) with Not_found -> None (** Hash-table used to record checking functions for builtins. *) let htbl : (string, sig_state -> popt -> sym -> unit) Hashtbl.t = Hashtbl.create 17 (** [check ss pos name sym] runs the registered check for builtin symbol [name] on the symbol [sym] (if such a check has been registered). Note that the [bmap] argument is expected to contain the builtin symbols in scope, and the [pos] argument is used for error reporting. *) let check : sig_state -> popt -> string -> sym -> unit = fun ss pos name sym -> try Hashtbl.find htbl name ss pos sym with Not_found -> () (** [register name check] registers the checking function [check], for the builtin symbols named [name]. When the check is run, [check] receives as argument a position for error reporting as well as the map of every builtin symbol in scope. It is expected to raise the [Fatal] exception to signal an error. Note that this function should not be called using a [name] for which a check has already been registered. *) let register : string -> (sig_state -> popt -> sym -> unit) -> unit = fun name check -> if Hashtbl.mem htbl name then assert false; Hashtbl.add htbl name check (** [register_expected_type name build pp] registers a checking function that checks the type of a symbol defining the builtin [name] against a type constructed using the given [build] function. *) let register_expected_type : term eq -> term pp -> string -> (sig_state -> popt -> term) -> unit = fun eq pp name fn -> let check ss pos sym = let expected = fn ss pos in if not (eq !(sym.sym_type) expected) then fatal pos "The type of %s is not of the form %a." sym.sym_name pp expected in register name check
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>