Commit 3fcc2aae authored by François Bobot's avatar François Bobot

typing : type propositional logic (close : #11564)

parent 83a6c42b
......@@ -583,9 +583,13 @@ and dfmla_node ~localize loc env = function
| PPnamed (x, f1) ->
let f1 = dfmla ~localize env f1 in
Fnamed (x, f1)
| PPvar x ->
| PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
let pr = find_prop x env.uc in
Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
| PPvar x ->
let s, tyl = specialize_psymbol x env.uc in
let tl = dtype_args s.ls_name loc env tyl [] in
Fapp (s, tl)
| PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
error ~loc PredicateExpected
......
......@@ -147,6 +147,9 @@ let split_string_rev s c =
| Invalid_argument _ -> ""::acc in
aux [] 0
(** usefule function on char *)
let is_uppercase c = 'A' <= c && c <= 'Z'
(* Set and Map on ints and strings *)
module Int = struct type t = int let compare = Pervasives.compare end
......
......@@ -114,6 +114,9 @@ val ttrue : 'a -> bool
(* useful function on string *)
val split_string_rev : string -> char -> string list
(* useful function on char *)
val is_uppercase : char -> bool
(* Set and Map on ints and strings *)
module Mint : Map.S with type key = int
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment