package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
1.5.1.tar.gz
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2
doc/src/logtk.parsers/parsing_utils.ml.html
Source file parsing_utils.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
(* This file is free software, part of Zipperposition. See file "license" for more details. *) open Logtk open CCResult.Infix type 'a or_error = ('a, string) CCResult.t let parse_tptp file : _ or_error = Util_tptp.parse_file ~recursive:true file >|= Iter.map Util_tptp.to_ast let parse_tip file = Util_tip.parse_file file >|= Util_tip.convert_seq let parse_dk file = Util_dk.parse_file file let guess_input (file:string): Input_format.t = if CCString.suffix ~suf:".p" file || CCString.suffix ~suf:".tptp" file then Input_format.tptp else if CCString.suffix ~suf:".smt2" file then Input_format.tip else if CCString.suffix ~suf:".zf" file then Input_format.zf else if CCString.suffix ~suf:".skp" file then Input_format.dk else ( let res = Input_format.default in Util.warnf "unable to guess syntax for `%s`, use default syntax (%a)" file Input_format.pp res; res ) (** Parse file using the input format chosen by the user *) let input_of_file (file:string): Input_format.t = match !Options.input with | Options.I_tptp -> Input_format.tptp | Options.I_zf -> Input_format.zf | Options.I_tip -> Input_format.tip | Options.I_dk -> Input_format.dk | Options.I_guess -> guess_input file let parse_file (i:Input_format.t) (file:string) = match i with | Input_format.I_tptp -> parse_tptp file | Input_format.I_zf -> Util_zf.parse_file file | Input_format.I_tip -> parse_tip file | Input_format.I_dk -> parse_dk file
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>