diff --git a/Makefile.in b/Makefile.in index 571bb9f90e18ef69b217f21cd58a2e89dfa31d9c..efd5fb6532e1598ddec4cf0a02e11b0faf6cb063 100644 --- a/Makefile.in +++ b/Makefile.in @@ -169,7 +169,7 @@ LIB_UTIL = config bigInt util opt lists strings \ hashcons stdlib exn_printer pp json debug loc lexlib print_tree \ cmdline warning sysutil rc plugin bigInt number pqueue -LIB_CORE = ident ty term pattern decl theory \ +LIB_CORE = ident ty term pattern decl coercion theory \ task pretty dterm env trans printer model_parser LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \ @@ -1748,7 +1748,7 @@ MODULESTODOC = \ util/util util/opt util/lists util/strings \ util/extmap util/extset util/exthtbl \ util/weakhtbl util/stdlib util/rc util/debug \ - core/ident core/ty core/term core/decl core/theory \ + core/ident core/ty core/term core/decl core/coercion core/theory \ core/env core/task \ driver/whyconf driver/call_provers driver/driver \ session/session session/session_tools session/session_scheduler diff --git a/bench/typing/bad/coercion_already.mlw b/bench/typing/bad/coercion_already.mlw new file mode 100644 index 0000000000000000000000000000000000000000..1728a3841f1e1486a7c4105d40f5d7861858e9a4 --- /dev/null +++ b/bench/typing/bad/coercion_already.mlw @@ -0,0 +1,10 @@ +type a +type b +type c + +function b_to_c b : c +meta coercion function b_to_c +function a_to_b a : b +meta coercion function a_to_b +function a_to_c a : c +meta coercion function a_to_c diff --git a/bench/typing/bad/coercion_already1.mlw b/bench/typing/bad/coercion_already1.mlw new file mode 100644 index 0000000000000000000000000000000000000000..ccaec14de213ff0e1f5fc0ab2a562023f16b1467 --- /dev/null +++ b/bench/typing/bad/coercion_already1.mlw @@ -0,0 +1,9 @@ +type a +type b + +function f a : b +meta coercion function f + +function g a : b +meta coercion function g + diff --git a/bench/typing/bad/coercion_already3.mlw b/bench/typing/bad/coercion_already3.mlw new file mode 100644 index 0000000000000000000000000000000000000000..6075db4df084f6374fb9e1d8d2316717dc37cc0d --- /dev/null +++ b/bench/typing/bad/coercion_already3.mlw @@ -0,0 +1,11 @@ +type a +type b +type c + +function f a : c +meta coercion function f +function g b : c +meta coercion function g +function h a : b +meta coercion function h + diff --git a/bench/typing/bad/coercion_cycle1.mlw b/bench/typing/bad/coercion_cycle1.mlw new file mode 100644 index 0000000000000000000000000000000000000000..f9f79e83ee539d9d7a25cb1062122327e8763ca2 --- /dev/null +++ b/bench/typing/bad/coercion_cycle1.mlw @@ -0,0 +1,9 @@ +type a +type b + +function f a : b +meta coercion function f + +function g b : a +meta coercion function g + diff --git a/bench/typing/bad/coercion_cycle2.mlw b/bench/typing/bad/coercion_cycle2.mlw new file mode 100644 index 0000000000000000000000000000000000000000..a358d3aa4b149029e585159b8b0a86813d93faf4 --- /dev/null +++ b/bench/typing/bad/coercion_cycle2.mlw @@ -0,0 +1,13 @@ +type a +type b +type c + +function f a : b +meta coercion function f +function g b : c +meta coercion function g + +function h c : a +meta coercion function h + + diff --git a/bench/typing/bad/coercion_cycle3.mlw b/bench/typing/bad/coercion_cycle3.mlw new file mode 100644 index 0000000000000000000000000000000000000000..df52d2e97568f11100af50a11c13477a7beb3944 --- /dev/null +++ b/bench/typing/bad/coercion_cycle3.mlw @@ -0,0 +1,13 @@ +type a +type b +type c + +function g b : c +meta coercion function g +function f a : b +meta coercion function f + +function h c : a +meta coercion function h + + diff --git a/bench/typing/good/coercions.mlw b/bench/typing/good/coercions.mlw new file mode 100644 index 0000000000000000000000000000000000000000..54121cd163a97e62cf5db023a0598e36a23e5c6a --- /dev/null +++ b/bench/typing/good/coercions.mlw @@ -0,0 +1,23 @@ + +type t +function f t : int +meta coercion function f +goal G: forall x: t. 42 = x + +type a +type b +type c + +function b_to_c b : c +meta coercion function b_to_c +function a_to_b a : b +meta coercion function a_to_b + +predicate is_c c +goal G2: forall x: a. is_c x + +function is_zero int : bool +meta coercion function is_zero + +goal G3: if 42 then 1=2 else 3=4 + diff --git a/examples/leftist_heap.mlw b/examples/leftist_heap.mlw index d69eee7b7ce27b12a510c2329c40e851ab2f07e8..71746c34ea49aa2d867fb7b13f2c5ca638426b9e 100644 --- a/examples/leftist_heap.mlw +++ b/examples/leftist_heap.mlw @@ -18,7 +18,7 @@ module Heap type heap - function size heap : int + val function size heap : int function occ elt heap : int @@ -39,9 +39,6 @@ module Heap val is_empty (h: heap) : bool ensures { result <-> size h = 0 } - val size (h: heap) : int - ensures { result = size h } - val merge (h1 h2: heap) : heap ensures { forall x. occ x result = occ x h1 + occ x h2 } ensures { size result = size h1 + size h2 } @@ -74,7 +71,7 @@ module Size use import TreeRank use import int.Int - function size (t: tree 'a) : int = match t with + let rec function size (t: tree 'a) : int = match t with | E -> 0 | N _ l _ r -> 1 + size l + size r end @@ -105,7 +102,7 @@ end module LeftistHeap type elt - predicate le elt elt + val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le use import TreeRank @@ -117,7 +114,7 @@ module LeftistHeap type t = tree elt (* [e] is no greater than the root of [h], if any *) - predicate le_root (e: elt) (h: t) = match h with + let predicate le_root (e: elt) (h: t) = match h with | E -> true | N _ _ x _ -> le e x end @@ -144,8 +141,8 @@ module LeftistHeap = match h with | E -> absurd | N _ l _ r -> - if l <> E then root_is_miminum l; - if r <> E then root_is_miminum r + match l with E -> root_is_miminum l | _ -> () end; + match r with E -> root_is_miminum r | _ -> () end end function rank (h: t) : int = match h with @@ -172,11 +169,7 @@ module LeftistHeap let is_empty (h: t) : bool ensures { result <-> size h = 0 } - = h = E - - let size (h: t) : int - ensures { result = size h } - = size h + = match h with E -> true | N _ _ _ _ -> false end let rank (h: t) : int requires { leftist_heap h } diff --git a/examples/vstte10_queens.mlw b/examples/vstte10_queens.mlw index fbb64a0d3bb9c4416005dfb8cc136b542eef924d..73e5efe7f9663cba16b0eb1ef82877820edda27b 100644 --- a/examples/vstte10_queens.mlw +++ b/examples/vstte10_queens.mlw @@ -155,19 +155,19 @@ module NQueens63 predicate is_board (board: array int63) (pos: int) = forall q: int. 0 <= q < pos -> - 0 <= to_int board[q] < to_int (length board) + 0 <= board[q] < (length board) exception MInconsistent let check_is_consistent (board: array int63) (pos: int63) - requires { 0 <= to_int pos < to_int (length board) } - requires { is_board board (to_int pos + 1) } + requires { 0 <= pos < (length board) } + requires { is_board board (pos + 1) } = try let q = ref (of_int 0) in while !q < pos do - invariant { 0 <= to_int !q <= to_int pos } - invariant { is_board board (to_int pos + 1) } - variant { to_int pos - to_int !q } + invariant { 0 <= !q <= pos } + invariant { is_board board (pos + 1) } + variant { pos - !q } let bq = board[!q] in let bpos = board[pos] in if bq = bpos then raise MInconsistent; @@ -184,20 +184,20 @@ module NQueens63 let rec count_bt_queens (solutions: ref P.t) (board: array int63) (n: int63) (pos: int63) - requires { to_int (length board) = to_int n } - requires { 0 <= to_int pos <= to_int n } - requires { is_board board (to_int pos) } - variant { to_int n - to_int pos } - ensures { is_board board (to_int pos) } + requires { (length board) = n } + requires { 0 <= pos <= n } + requires { is_board board (pos) } + variant { n - pos } + ensures { is_board board (pos) } = if eq pos n then solutions := P.succ !solutions else let i = ref (of_int 0) in while !i < n do - invariant { 0 <= to_int !i <= to_int n } - invariant { is_board board (to_int pos) } - variant { to_int n - to_int !i } + invariant { 0 <= !i <= n } + invariant { is_board board (pos) } + variant { n - !i } board[pos] <- !i; if check_is_consistent board pos then count_bt_queens solutions board n (pos + of_int 1); @@ -205,7 +205,7 @@ module NQueens63 done let count_queens (n: int63) : P.t - requires { to_int n >= 0 } + requires { n >= 0 } ensures { true } = let solutions = ref (P.zero ()) in diff --git a/examples/vstte10_queens/why3session.xml b/examples/vstte10_queens/why3session.xml index 052e1266b7bb9e1997ad200ecdd77a188c5308ac..35622a2a0835f7966261754a63172c1c35bf94c0 100644 --- a/examples/vstte10_queens/why3session.xml +++ b/examples/vstte10_queens/why3session.xml @@ -2,147 +2,97 @@ - - - + - + - + - + - + - + - + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - - + + - - + + - - + + - - + + - - - + + - - + + - - + + - - + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + diff --git a/examples/vstte10_queens/why3shapes.gz b/examples/vstte10_queens/why3shapes.gz index 3ed7ec6e17f52e50a2a9feb57ce2d9a1fd6f1463..42e77ff4ecc64f3fd8d94204edb252b2b3ab1784 100644 Binary files a/examples/vstte10_queens/why3shapes.gz and b/examples/vstte10_queens/why3shapes.gz differ diff --git a/modules/mach/int.mlw b/modules/mach/int.mlw index 0c92187c8488d7ded8c90a90b1c2128a08594d49..2288c6e7f83a5f3d13e2923ed081b7328d8e02ef 100644 --- a/modules/mach/int.mlw +++ b/modules/mach/int.mlw @@ -45,6 +45,7 @@ module Bounded_int constant max : int val function to_int (n:t) : int + meta coercion function to_int predicate in_bounds (n:int) = min <= n <= max diff --git a/src/core/coercion.ml b/src/core/coercion.ml new file mode 100644 index 0000000000000000000000000000000000000000..eeb9325ce4f78097bc9ea6833200c3fa5bd37f35 --- /dev/null +++ b/src/core/coercion.ml @@ -0,0 +1,103 @@ + +open Ident +open Ty +open Term + +type coercion_kind = + | CRCleaf of lsymbol + | CRCcomp of coercion_kind * coercion_kind + +type coercion = { + crc_kind: coercion_kind; + crc_src : Ty.tysymbol; + crc_tar : Ty.tysymbol; + crc_len : int; +} + +type t = (coercion Mts.t) Mts.t + (** invariant: transitively closed *) + +let empty = Mts.empty + +exception NotACoercion of lsymbol +exception CoercionCycle of coercion +exception CoercionAlreadyDefined of coercion + +let create_crc ls = + match ls.ls_args, ls.ls_value with + | [{ty_node = Tyapp (ty1,_)}], Some {ty_node = Tyapp (ty2,_)} -> + if ts_equal ty1 ty2 then raise (NotACoercion ls); + { crc_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 } + | _ -> raise (NotACoercion ls) + +let mem crcmap ts1 ts2 = + try let m = Mts.find ts1 crcmap in Mts.mem ts2 m + with Not_found -> false + +let find crcmap ts1 ts2 = + Mts.find ts2 (Mts.find ts1 crcmap) + +(* replace an old coercion by a new one, or fail *) +let replace c_old c_new _m1 m = + match c_old.crc_kind, c_new.crc_kind with + | CRCleaf ls_old, CRCleaf ls_new when ls_equal ls_old ls_new -> m + | _ -> raise (CoercionAlreadyDefined c_old) + +(* add a new coercion c, without making the transitive closure *) +let insert crc m = + let put crc m1 m2 = Mts.add crc.crc_src (Mts.add crc.crc_tar crc m1) m2 in + if mem m crc.crc_tar crc.crc_src then + raise (CoercionCycle (find m crc.crc_tar crc.crc_src)); + let m1 = Mts.find_def Mts.empty crc.crc_src m in + if Mts.mem crc.crc_tar m1 then replace (Mts.find crc.crc_tar m1) crc m1 m + else put crc m1 m + +let compose crc1 crc2 = + { crc_kind = CRCcomp (crc1.crc_kind, crc2.crc_kind); + crc_src = crc1.crc_src; + crc_tar = crc2.crc_tar; + crc_len = crc1.crc_len + crc2.crc_len } + +(* add a new coercion crc, and make the transitive closure *) +let add_crc crcmap crc = + let close_right c1 _ty c2 macc = insert (compose c1 c2) macc in + let close_left_right _ty1 m1 macc = + if Mts.mem crc.crc_src m1 then + let c1 = Mts.find crc.crc_src m1 in + let m2 = Mts.find_def Mts.empty crc.crc_tar macc in + Mts.fold (close_right c1) (Mts.add crc.crc_tar crc m2) macc + else macc in + let crcmap_uc1 = insert crc crcmap in + let crcmap_uc2 = + let m1 = Mts.find_def Mts.empty crc.crc_tar crcmap_uc1 in + Mts.fold (close_right crc) m1 crcmap_uc1 in + Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2 + +let add crcmap ls = + add_crc crcmap (create_crc ls) + +let union s1 s2 = + Mts.fold (fun _ m1 s -> Mts.fold (fun _ c s -> add_crc s c) m1 s) s2 s1 + +let rec print_kind fmt = function + | CRCleaf ls -> + Format.fprintf fmt "%s" ls.ls_name.id_string + | CRCcomp (k1, k2) -> + Format.fprintf fmt "%a o %a" print_kind k2 print_kind k1 + +let already_a_coercion fmt crc = + Format.fprintf fmt "already a coercion from type %s to type %s@ (%a)" + crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string + print_kind crc.crc_kind + +let () = Exn_printer.register + begin fun fmt exn -> match exn with + | NotACoercion ls -> + Format.fprintf fmt "Function %s cannot be used as a coercion" + ls.ls_name.id_string + | CoercionCycle crc -> + Format.fprintf fmt "This coercion introduces a cycle;@ "; + already_a_coercion fmt crc + | CoercionAlreadyDefined crc -> + already_a_coercion fmt crc + | _ -> raise exn end diff --git a/src/core/coercion.mli b/src/core/coercion.mli new file mode 100644 index 0000000000000000000000000000000000000000..29f6e417b28093584e20880f776eb9e937244b46 --- /dev/null +++ b/src/core/coercion.mli @@ -0,0 +1,29 @@ + + +type coercion_kind = + | CRCleaf of Term.lsymbol + | CRCcomp of coercion_kind * coercion_kind + +type coercion = private { + crc_kind: coercion_kind; + crc_src : Ty.tysymbol; + crc_tar : Ty.tysymbol; + crc_len : int; +} + +type t + (** a set of coercions *) + +val empty: t + +val add: t -> Term.lsymbol -> t + (** adds a new coercion + raises an error if this introduces a cycle *) + +val find: t -> Ty.tysymbol -> Ty.tysymbol -> coercion + (** returns the coercion, or raises [Not_found] *) + +val union: t -> t -> t + (** [union s1 s2] merges the coercions from [s2] into [s1] + (as a new set of coercions) + this is asymetric: a coercion from [s2] may hide a coercion from [s1] *) diff --git a/src/core/dterm.ml b/src/core/dterm.ml index 8b35e6cdcd1360740bc22394d742d51542728573..1d2db6890f2e8cc60e2c6414752fb9b5e49d7eb4 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -235,6 +235,10 @@ let dty_unify_app ls unify (l1: 'a list) (l2: dty list) = try List.iter2 unify l1 l2 with Invalid_argument _ -> raise (BadArity (ls, List.length l1)) +let dty_unify_app_map ls unify (l1: 'a list) (l2: dty list) = + try List.map2 unify l1 l2 with Invalid_argument _ -> + raise (BadArity (ls, List.length l1)) + let dpat_expected_type dp dty = try dty_unify dp.dp_dty dty with Exit -> Loc.errorm ?loc:dp.dp_loc "This pattern has type %a,@ but is expected to have type %a" @@ -290,42 +294,97 @@ let dpattern ?loc node = let dty, vars = Loc.try1 ?loc get_dty node in { dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc } -let dterm ?loc node = - let get_dty = function +let slab_coercion = Slab.singleton Pretty.label_coercion + +let rec apply_coercion ~loc k dt = match k with + | Coercion.CRCleaf ls -> + let (_, dty) = specialize_ls ls in + let dt = + { dt_node = DTapp (ls, [dt]); dt_dty = dty; dt_loc = loc } in + { dt with dt_node = DTlabel (dt, slab_coercion) } + | Coercion.CRCcomp (k1, k2) -> + apply_coercion ~loc k2 (apply_coercion ~loc k1 dt) + +let dterm tuc ?loc node = + let rec dterm_expected dt dty = + let loc = dt.dt_loc in + match dt.dt_dty with + | Some dt_dty -> + begin try dty_unify dt_dty dty; dt with Exit -> + let ty1 = ty_of_dty ~strict:false dt_dty in + let ty2 = ty_of_dty ~strict:false dty in + try begin match ty1, ty2 with + | { ty_node = Tyapp (ts1, _) }, { ty_node = Tyapp (ts2, _) } -> + let open Theory in + let open Coercion in + let crc = find tuc.uc_crcmap ts1 ts2 in + dterm_node loc (apply_coercion ~loc crc.crc_kind dt).dt_node + | _ -> + raise Not_found + end with Not_found -> + Loc.errorm ?loc + "This term has type %a,@ but is expected to have type %a" + print_dty dt_dty print_dty dty + end + | None -> + try dty_unify dty_bool dty; dt with Exit -> + Loc.error ?loc TermExpected + + and dfmla_expected dt = match dt.dt_dty with + | Some dt_dty -> + begin try dty_unify dt_dty dty_bool; dt with Exit -> + let ty1 = ty_of_dty ~strict:false dt_dty in + try begin match ty1 with + | { ty_node = Tyapp (ts1, _) } -> + let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts_bool in + let dt = apply_coercion ~loc crc.Coercion.crc_kind dt in + dterm_node loc dt.dt_node + | _ -> + raise Not_found + end with Not_found -> + Loc.error ?loc:dt.dt_loc FmlaExpected end + | None -> dt + + and dterm_node loc node = + let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in + match node with | DTvar (_,dty) -> - Some dty + mk_dty (Some dty) | DTgvar vs -> - Some (dty_of_ty vs.vs_ty) + mk_dty (Some (dty_of_ty vs.vs_ty)) | DTconst (Number.ConstInt _) -> - Some dty_int + mk_dty (Some dty_int) | DTconst (Number.ConstReal _) -> - Some dty_real - | DTapp (ls,dtl) -> - let dtyl, dty = specialize_ls ls in - dty_unify_app ls dterm_expected_type dtl dtyl; - dty + mk_dty (Some dty_real) + | DTapp (ls, dtl) -> + let dtyl, dty = specialize_ls ls in + { dt_node = DTapp (ls, dty_unify_app_map ls dterm_expected dtl dtyl); + dt_dty = dty; + dt_loc = loc } | DTfapp ({dt_dty = Some res} as dt1,dt2) -> - let rec not_arrow = function - | Dvar {contents = Dval dty} -> not_arrow dty - | Duty {ty_node = Tyapp (ts,_)} - | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func) - | Dvar _ -> false | _ -> true in - if not_arrow res then Loc.errorm ?loc:dt1.dt_loc - "This term has type %a,@ it cannot be applied" print_dty res; - let dtyl, dty = specialize_ls fs_func_app in - dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl; - dty + let rec not_arrow = function + | Dvar {contents = Dval dty} -> not_arrow dty + | Duty {ty_node = Tyapp (ts,_)} + | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func) + | Dvar _ -> false | _ -> true in + if not_arrow res then Loc.errorm ?loc:dt1.dt_loc + "This term has type %a,@ it cannot be applied" print_dty res; + let dtyl, dty = specialize_ls fs_func_app in + dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl; + mk_dty dty | DTfapp ({dt_dty = None; dt_loc = loc},_) -> - Loc.errorm ?loc "This term has type bool,@ it cannot be applied" + Loc.errorm ?loc "This term has type bool,@ it cannot be applied" | DTif (df,dt1,dt2) -> - dfmla_expected_type df; - dexpr_expected_type dt2 dt1.dt_dty; - if dt2.dt_dty = None then None else dt1.dt_dty + let df = dfmla_expected df in + dexpr_expected_type dt2 dt1.dt_dty; + { dt_node = DTif (df, dt1, dt2); + dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty; + dt_loc = loc } | DTlet (dt,_,df) -> - ignore (dty_of_dterm dt); - df.dt_dty + ignore (dty_of_dterm dt); + mk_dty df.dt_dty | DTcase (_,[]) -> - raise EmptyCase + raise EmptyCase | DTcase (dt,(dp1,df1)::bl) -> dterm_expected_type dt dp1.dp_dty; let check (dp,df) = @@ -333,39 +392,37 @@ let dterm ?loc node = dexpr_expected_type df df1.dt_dty in List.iter check bl; let is_fmla (_,df) = df.dt_dty = None in - if List.exists is_fmla bl then None else df1.dt_dty + if List.exists is_fmla bl then mk_dty None else mk_dty df1.dt_dty | DTeps (_,dty,df) -> - dfmla_expected_type df; - Some dty + dfmla_expected_type df; + mk_dty (Some dty) | DTquant (DTlambda,vl,_,df) -> - let res = Opt.get_def dty_bool df.dt_dty in - let app (_,l,_) r = Dapp (ts_func,[l;r]) in - Some (List.fold_right app vl res) + let res = Opt.get_def dty_bool df.dt_dty in + let app (_,l,_) r = Dapp (ts_func,[l;r]) in + mk_dty (Some (List.fold_right app vl res)) | DTquant ((DTforall|DTexists),_,_,df) -> - dfmla_expected_type df; - None + dfmla_expected_type df; + mk_dty None | DTbinop (_,df1,df2) -> dfmla_expected_type df1; dfmla_expected_type df2; - None + mk_dty None | DTnot df -> dfmla_expected_type df; - None + mk_dty None | DTtrue | DTfalse -> (* we put here [Some dty_bool] instead of [None] because we can always replace [true] by [True] and [false] by [False], so that there is no need to count these constructs as "formulas" which require explicit if-then-else conversion to bool *) - Some dty_bool + mk_dty (Some dty_bool) | DTcast (dt,ty) -> - let dty = dty_of_ty ty in - dterm_expected_type dt dty; - Some dty + let dty = dty_of_ty ty in + dterm_expected dt dty | DTuloc (dt,_) | DTlabel (dt,_) -> - dt.dt_dty in - let dty = Loc.try1 ?loc get_dty node in - { dt_node = node; dt_dty = dty; dt_loc = loc } + mk_dty (dt.dt_dty) + in Loc.try1 ?loc (dterm_node loc) node (** Final stage *) diff --git a/src/core/dterm.mli b/src/core/dterm.mli index 6b4b2cc43bfc6662718d76cafc408f5aa4cf6e9a..59dcca3df8a62da56b5606508953da4c2970d2b1 100644 --- a/src/core/dterm.mli +++ b/src/core/dterm.mli @@ -99,7 +99,7 @@ val denv_get_opt : denv -> string -> dterm_node option val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern -val dterm : ?loc:Loc.position -> dterm_node -> dterm +val dterm : Theory.theory_uc -> ?loc:Loc.position -> dterm_node -> dterm (** Final stage *) diff --git a/src/core/pretty.ml b/src/core/pretty.ml index 9cfd3733481f0ec384a22c4b9c48cb477df536f2..0cb04b06b0d63d0b6e618ce02548a4e83e53fda6 100644 --- a/src/core/pretty.ml +++ b/src/core/pretty.ml @@ -26,6 +26,9 @@ let debug_print_labels = Debug.register_info_flag "print_labels" let debug_print_locs = Debug.register_info_flag "print_locs" ~desc:"Print@ locations@ of@ identifiers@ and@ expressions." +let debug_print_coercions = Debug.register_info_flag "print_coercions" + ~desc:"Print@ coercions@ in@ logical@ formulas." + let iprinter,aprinter,tprinter,pprinter = let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive"; "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta"; @@ -48,6 +51,8 @@ let forget_all () = forget_all tprinter; forget_all pprinter +let label_coercion = create_label "coercion" + let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string let print_labels = print_iter1 Slab.iter space print_label @@ -258,6 +263,9 @@ and print_tnode pri fmt t = match t.t_node with print_vs fmt v | Tconst c -> print_const fmt c + | Tapp (_, [t1]) when Slab.mem label_coercion t.t_label && + Debug.test_noflag debug_print_coercions -> + print_lterm pri fmt (t_label t1.t_label t1) | Tapp (fs, tl) when is_fs_tuple fs -> fprintf fmt "(%a)" (print_list comma print_term) tl | Tapp (fs, tl) when unambig_fs fs -> diff --git a/src/core/pretty.mli b/src/core/pretty.mli index a3fa03ebb8ba5af9e1002806218376f25ab1f09f..02ff9770b0226db163d78ec450fb662ed26e0f61 100644 --- a/src/core/pretty.mli +++ b/src/core/pretty.mli @@ -17,6 +17,8 @@ open Decl open Theory open Task +val label_coercion: label + val forget_all : unit -> unit (* flush id_unique *) val forget_tvs : unit -> unit (* flush id_unique for type vars *) val forget_var : vsymbol -> unit (* flush id_unique for a variable *) diff --git a/src/core/theory.ml b/src/core/theory.ml index 262b8585c8a032e02ee751ae2f58c714eb968960..3af56eac6cbe56d1517171a6bd18b2074de23378 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -150,13 +150,14 @@ let list_metas () = Hstr.fold (fun _ v acc -> v::acc) meta_table [] (** Theory *) type theory = { - th_name : ident; (* theory name *) - th_path : string list;(* environment qualifiers *) - th_decls : tdecl list; (* theory declarations *) - th_export : namespace; (* exported namespace *) - th_known : known_map; (* known identifiers *) - th_local : Sid.t; (* locally declared idents *) - th_used : Sid.t; (* used theories *) + th_name : ident; (* theory name *) + th_path : string list; (* environment qualifiers *) + th_decls : tdecl list; (* theory declarations *) + th_export : namespace; (* exported namespace *) + th_known : known_map; (* known identifiers *) + th_local : Sid.t; (* locally declared idents *) + th_used : Sid.t; (* used theories *) + th_crcmap : Coercion.t; (* coercions *) } and tdecl = { @@ -262,6 +263,7 @@ type theory_uc = { uc_known : known_map; uc_local : Sid.t; uc_used : Sid.t; + uc_crcmap : Coercion.t; } exception CloseTheory @@ -277,17 +279,19 @@ let empty_theory n p = { uc_known = Mid.empty; uc_local = Sid.empty; uc_used = Sid.empty; + uc_crcmap = Coercion.empty; } let close_theory uc = match uc.uc_export with - | [e] -> { - th_name = uc.uc_name; + | [e] -> + { th_name = uc.uc_name; th_path = uc.uc_path; th_decls = List.rev uc.uc_decls; th_export = e; th_known = uc.uc_known; th_local = uc.uc_local; - th_used = uc.uc_used } + th_used = uc.uc_used; + th_crcmap = uc.uc_crcmap } | _ -> raise CloseTheory let get_namespace uc = List.hd uc.uc_import @@ -331,6 +335,8 @@ let known_meta kn al = in List.iter check al +let meta_coercion = register_meta ~desc:"coercion" "coercion" [MTlsymbol] + let add_tdecl uc td = match td.td_node with | Decl d -> { uc with uc_decls = td :: uc.uc_decls; @@ -343,6 +349,9 @@ let add_tdecl uc td = match td.td_node with uc_used = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) } | Clone (_,sm) -> known_clone uc.uc_known sm; { uc with uc_decls = td :: uc.uc_decls } + | Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion -> + known_meta uc.uc_known al; + { uc with uc_crcmap = Coercion.add uc.uc_crcmap ls } | Meta (_,al) -> known_meta uc.uc_known al; { uc with uc_decls = td :: uc.uc_decls } @@ -452,7 +461,8 @@ let use_export uc th = match uc.uc_import, uc.uc_export with | i0 :: sti, e0 :: ste -> { uc with uc_import = merge_ns false th.th_export i0 :: sti; - uc_export = merge_ns true th.th_export e0 :: ste } + uc_export = merge_ns true th.th_export e0 :: ste; + uc_crcmap = Coercion.union uc.uc_crcmap th.th_crcmap } | _ -> assert false (** Clone *) diff --git a/src/core/theory.mli b/src/core/theory.mli index 71e6a5e1c6654555913f30de3aa4bde66cbd09bd..018f67a5eb4f01a4a639bad2ec0d2c5a9163f5e2 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -81,13 +81,14 @@ val list_metas : unit -> meta list (** {2 Theories} *) type theory = private { - th_name : ident; (* theory name *) - th_path : string list;(* environment qualifiers *) - th_decls : tdecl list; (* theory declarations *) - th_export : namespace; (* exported namespace *) - th_known : known_map; (* known identifiers *) - th_local : Sid.t; (* locally declared idents *) - th_used : Sid.t; (* used theories *) + th_name : ident; (* theory name *) + th_path : string list; (* environment qualifiers *) + th_decls : tdecl list; (* theory declarations *) + th_export : namespace; (* exported namespace *) + th_known : known_map; (* known identifiers *) + th_local : Sid.t; (* locally declared idents *) + th_used : Sid.t; (* used theories *) + th_crcmap : Coercion.t (* coercions *) } and tdecl = private { @@ -127,6 +128,8 @@ type theory_uc = private { uc_known : known_map; uc_local : Sid.t; uc_used : Sid.t; + uc_crcmap : Coercion.t; + } val create_theory : ?path:string list -> preid -> theory_uc @@ -225,4 +228,3 @@ exception KnownMeta of meta exception UnknownMeta of string exception BadMetaArity of meta * int exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type - diff --git a/src/core/ty.ml b/src/core/ty.ml index f995fad9aeceb35859e61cff314336e5430d4f52..035c33e695b5dceb3fe7f8dcc6833506db53c566 100644 --- a/src/core/ty.ml +++ b/src/core/ty.ml @@ -265,4 +265,3 @@ let oty_cons = Opt.fold (fun tl t -> t::tl) let ty_equal_check ty1 ty2 = if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2)) - diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 631c0fb67931120587948dc5ddb64f2aa5f4bf48..af84f35ea415a1db5e8470718b02761e34a14e03 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -40,6 +40,7 @@ type t = mutable default_editor : string; mutable intro_premises : bool; mutable show_labels : bool; + mutable show_coercions : bool; mutable show_locs : bool; mutable show_time_limit : bool; mutable max_boxes : int; @@ -74,6 +75,7 @@ type ide = { ide_verbose : int; ide_intro_premises : bool; ide_show_labels : bool; + ide_show_coercions : bool; ide_show_locs : bool; ide_show_time_limit : bool; ide_max_boxes : int; @@ -98,6 +100,7 @@ let default_ide = ide_verbose = 0; ide_intro_premises = true; ide_show_labels = false; + ide_show_coercions = true; ide_show_locs = false; ide_show_time_limit = false; ide_max_boxes = 16; @@ -132,6 +135,8 @@ let load_ide section = "intro_premises"; ide_show_labels = get_bool section ~default:default_ide.ide_show_labels "print_labels"; + ide_show_coercions = + get_bool section ~default:default_ide.ide_show_labels "print_coercions"; ide_show_locs = get_bool section ~default:default_ide.ide_show_locs "print_locs"; ide_show_time_limit = @@ -172,6 +177,11 @@ let set_labels_flag = fun b -> (if b then Debug.set_flag else Debug.unset_flag) fl +let set_coercions_flag = + let fl = Debug.lookup_flag "print_coercions" in + fun b -> + (if b then Debug.set_flag else Debug.unset_flag) fl + let set_locs_flag = let fl = Debug.lookup_flag "print_locs" in fun b -> @@ -184,6 +194,7 @@ let load_config config original_config env = | Some s -> load_ide s in set_labels_flag ide.ide_show_labels; + set_coercions_flag ide.ide_show_coercions; set_locs_flag ide.ide_show_locs; { window_height = ide.ide_window_height; window_width = ide.ide_window_width; @@ -193,6 +204,7 @@ let load_config config original_config env = verbose = ide.ide_verbose; intro_premises= ide.ide_intro_premises ; show_labels = ide.ide_show_labels ; + show_coercions = ide.ide_show_coercions ; show_locs = ide.ide_show_locs ; show_time_limit = ide.ide_show_time_limit; max_boxes = ide.ide_max_boxes; @@ -241,6 +253,7 @@ let save_config t = let ide = set_int ide "verbose" t.verbose in let ide = set_bool ide "intro_premises" t.intro_premises in let ide = set_bool ide "print_labels" t.show_labels in + let ide = set_bool ide "print_coercions" t.show_coercions in let ide = set_bool ide "print_locs" t.show_locs in let ide = set_bool ide "print_time_limit" t.show_time_limit in let ide = set_int ide "max_boxes" t.max_boxes in @@ -747,6 +760,18 @@ let appearance_settings (c : t) (notebook:GPack.notebook) = c.show_labels <- not c.show_labels; set_labels_flag c.show_labels) in + let showcoercions = + GButton.check_button + ~label:"show coercions in formulas" + ~packing:display_options_box#add () + ~active:c.show_coercions + in + let (_ : GtkSignal.id) = + showcoercions#connect#toggled ~callback: + (fun () -> + c.show_coercions <- not c.show_coercions; + set_coercions_flag c.show_coercions) + in let showlocs = GButton.check_button ~label:"show source locations in formulas" diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index 1ab306a43ac302503bdb1c5c6a1e57fd96188f1b..9aea707014ebc302e12fd1717c5855aff9984dd4 100644 --- a/src/ide/gconfig.mli +++ b/src/ide/gconfig.mli @@ -22,6 +22,7 @@ type t = mutable default_editor : string; mutable intro_premises : bool; mutable show_labels : bool; + mutable show_coercions : bool; mutable show_locs : bool; mutable show_time_limit : bool; mutable max_boxes : int; diff --git a/src/parser/typing.ml b/src/parser/typing.ml index e9310ef9068dc4e4f18d3122743182e0ade7779e..bb840457bac62f4df2bbcc1a18d9f3c38dce717b 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -210,17 +210,17 @@ let is_reusable dt = match dt.dt_node with | DTapp (_,[]) -> true | _ -> false -let mk_var n dt = +let mk_var tuc n dt = let dty = match dt.dt_dty with | None -> dty_of_ty ty_bool | Some dty -> dty in - Dterm.dterm ?loc:dt.dt_loc (DTvar (n, dty)) + Dterm.dterm tuc ?loc:dt.dt_loc (DTvar (n, dty)) -let mk_let ~loc n dt node = - DTlet (dt, id_user n loc, Dterm.dterm ~loc node) +let mk_let tuc ~loc n dt node = + DTlet (dt, id_user n loc, Dterm.dterm tuc ~loc node) -let mk_closure loc ls = - let mk dt = Dterm.dterm ~loc dt in +let mk_closure tuc loc ls = + let mk dt = Dterm.dterm tuc ~loc dt in let mk_v i _ = Some (id_user ("y" ^ string_of_int i) loc), dty_fresh (), None in let mk_t (id, dty, _) = mk (DTvar ((Opt.get id).pre_name, dty)) in @@ -230,12 +230,12 @@ let mk_closure loc ls = let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = let func_app e el = List.fold_left (fun e1 (loc, e2) -> - DTfapp (Dterm.dterm ~loc e1, e2)) e el + DTfapp (Dterm.dterm tuc ~loc e1, e2)) e el in let rec apply_ls loc ls al l el = match l, el with | (_::l), (e::el) -> apply_ls loc ls (e::al) l el | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el - | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el) + | _, [] -> func_app (mk_closure tuc loc ls) (List.rev_append al el) in let qualid_app q el = match gvars at q with | Some v -> func_app (DTgvar v.pv_vs) el @@ -259,7 +259,7 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = | _ -> func_app (DTfapp (dterm tuc gvars at denv e1, e2)) el in - Dterm.dterm ~loc (match desc with + Dterm.dterm tuc ~loc (match desc with | Ptree.Tident q -> qualid_app q [] | Ptree.Tidapp (q, tl) -> @@ -276,15 +276,15 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = if op.id_str = "infix <>" then let op = { op with id_str = "infix =" } in let ls = find_lsymbol tuc (Qident op) in - DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2]))) + DTnot (Dterm.dterm tuc ~loc (DTapp (ls, [de1;de2]))) else DTapp (find_lsymbol tuc (Qident op), [de1;de2]) in let rec chain loc de1 op1 = function | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } -> let de2 = dterm tuc gvars at denv e2 in let loc12 = loc_cutoff loc loc23 e2.term_loc in - let de12 = Dterm.dterm ~loc:loc12 (apply loc12 de1 op1 de2) in - let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 op2 e3) in + let de12 = Dterm.dterm tuc ~loc:loc12 (apply loc12 de1 op1 de2) in + let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 op2 e3) in DTbinop (DTand, de12, de23) | e23 -> apply loc de1 op1 (dterm tuc gvars at denv e23) in @@ -321,8 +321,8 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = | { term_desc = Ptree.Tbinop (e2, DTiff, e3); term_loc = loc23 } -> let de2 = dterm tuc gvars at denv e2 in let loc12 = loc_cutoff loc loc23 e2.term_loc in - let de12 = Dterm.dterm ~loc:loc12 (DTbinop (DTiff, de1, de2)) in - let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 e3) in + let de12 = Dterm.dterm tuc ~loc:loc12 (DTbinop (DTiff, de1, de2)) in + let de23 = Dterm.dterm tuc ~loc:loc23 (chain loc23 de2 e3) in DTbinop (DTand, de12, de23) | { term_desc = Ptree.Tbinop (_, DTimplies, _); term_loc = loc23 } -> Loc.errorm ~loc:loc23 "An unparenthesized implication cannot be \ @@ -351,13 +351,13 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = | Ptree.Tupdate (e1, fl) -> let e1 = dterm tuc gvars at denv e1 in let re = is_reusable e1 in - let v = if re then e1 else mk_var "q " e1 in + let v = if re then e1 else mk_var tuc "q " e1 in let get_val _ pj = function | Some e -> dterm tuc gvars at denv e - | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in + | None -> Dterm.dterm tuc ~loc (DTapp (pj,[v])) in let cs, fl = parse_record ~loc tuc get_val fl in let d = DTapp (cs, fl) in - if re then d else mk_let ~loc "q " e1 d + if re then d else mk_let tuc ~loc "q " e1 d | Ptree.Tat (e1, l) -> DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty) | Ptree.Tnamed (Lpos uloc, e1) ->