simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix emission of reference terms

Browse source
This commit is contained in:
Simon Cruanes 2021-10-29 22:35:19 -04:00
parent 6b1b1eb587
commit 72d79d7c0a
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
3 changed files with 8 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/base/Proof_quip.ml
View file

@ -158,7 +158,7 @@ end = struct
let name = name_term lid in let name = name_term lid in
let step = lazy (P.S_define_t_name (name, !!t)) in let step = lazy (P.S_define_t_name (name, !!t)) in
add_top_step step; add_top_step step;
L_terms.add lid (lazy (P.T.ref id)) L_terms.add lid (lazy (P.T.ref name))
) else ( ) else (
L_terms.add lid t L_terms.add lid t
) )

12
src/quip/Proof.ml
View file

@ -8,7 +8,7 @@ module Ty = struct
| Bool | Bool
| Arrow of t array * t | Arrow of t array * t
| App of string * t array | App of string * t array
| Ref of id | Ref of string
let equal : t -> t -> bool = (=) let equal : t -> t -> bool = (=)
let hash : t -> int = CCHash.poly let hash : t -> int = CCHash.poly
@ -22,7 +22,7 @@ module Ty = struct
| App (c, [||]) -> Fmt.string out c | App (c, [||]) -> Fmt.string out c
| App (c, args) -> | App (c, args) ->
Fmt.fprintf out "(@[%s@ %a@])" c (Util.pp_array pp) args Fmt.fprintf out "(@[%s@ %a@])" c (Util.pp_array pp) args
| Ref id -> Fmt.fprintf out "@@%d" id | Ref name -> Fmt.fprintf out "(@@ %s)" name
end end
module Fun = struct module Fun = struct
@ -43,7 +43,7 @@ module T = struct
| Ite of t * t * t | Ite of t * t * t
| Not of t | Not of t
| Eq of t * t | Eq of t * t
| Ref of id | Ref of string
let[@inline] view (self:t) : t = self let[@inline] view (self:t) : t = self
let equal : t -> t -> bool = (=) let equal : t -> t -> bool = (=)
@ -54,7 +54,7 @@ module T = struct
let bool b = Bool b let bool b = Bool b
let not_ = function Not x -> x | x -> Not x let not_ = function Not x -> x | x -> Not x
let eq a b : t = Eq (a,b) let eq a b : t = Eq (a,b)
let ref id : t = Ref id let ref name : t = Ref name
let app_fun f args : t = App_fun (f, args) let app_fun f args : t = App_fun (f, args)
let const c = app_fun c [||] let const c = app_fun c [||]
let app_ho a b : t = App_ho (a,b) let app_ho a b : t = App_ho (a,b)
@ -69,7 +69,7 @@ module T = struct
| App_ho (f,a) -> Fmt.fprintf out "(@[%a@ %a@])" pp f pp a | App_ho (f,a) -> Fmt.fprintf out "(@[%a@ %a@])" pp f pp a
| Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a | Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a
| Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b
| Ref id -> Fmt.fprintf out "@@%d" id | Ref name -> Fmt.fprintf out "(@@ %s)" name
end end
type term = T.t type term = T.t
@ -112,7 +112,6 @@ type t =
| CC_lemma of clause | CC_lemma of clause
| Assertion of term | Assertion of term
| Assertion_c of clause | Assertion_c of clause
| Drup_res of clause
| Hres of t * hres_step list | Hres of t * hres_step list
| Res of term * t * t | Res of term * t * t
| Res1 of t * t | Res1 of t * t
@ -208,7 +207,6 @@ let bool_eq a b : t = Bool_eq (a,b)
let bool_c name c : t = Bool_c (name, c) let bool_c name c : t = Bool_c (name, c)
let nn c : t = Nn c let nn c : t = Nn c
let drup_res c : t = Drup_res c
let hres_l p l : t = let hres_l p l : t =
let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
if l=[] then p else Hres (p,l) if l=[] then p else Hres (p,l)

5
src/quip/Sidekick_quip.ml
View file

@ -28,7 +28,7 @@ module Make_printer(Out : OUT) = struct
| T.App_fun (c, [||]) -> a c | T.App_fun (c, [||]) -> a c
| T.App_fun (c, args) -> | T.App_fun (c, args) ->
l(a c :: Util.array_to_list_map pp_t args) l(a c :: Util.array_to_list_map pp_t args)
| T.Ref i -> l[a"@"; a(string_of_int i)] | T.Ref name -> l[a"@"; a name]
| T.App_ho(f,a) -> l[pp_t f;pp_t a] | T.App_ho(f,a) -> l[pp_t f;pp_t a]
| T.Eq (t,u) -> l[a"=";pp_t t;pp_t u] | T.Eq (t,u) -> l[a"=";pp_t t;pp_t u]
| T.Not u -> l[a"not";pp_t u] | T.Not u -> l[a"not";pp_t u]
@ -54,7 +54,7 @@ module Make_printer(Out : OUT) = struct
a c a c
| Ty.App (c,args) -> | Ty.App (c,args) ->
l(a c::Util.array_to_list_map pp_ty args) l(a c::Util.array_to_list_map pp_ty args)
| Ty.Ref i -> l[a "@"; a (string_of_int i)] | Ty.Ref name -> l[a "@"; a name]
| Ty.Arrow (args,b) -> | Ty.Arrow (args,b) ->
l (a "->" :: Util.array_to_list_map pp_ty args @ [pp_ty b]) l (a "->" :: Util.array_to_list_map pp_ty args @ [pp_ty b])
@ -83,7 +83,6 @@ module Make_printer(Out : OUT) = struct
| Nn p -> l[a"nn";pp_rec p] | Nn p -> l[a"nn";pp_rec p]
| Assertion t -> l[a"assert";pp_t t] | Assertion t -> l[a"assert";pp_t t]
| Assertion_c c -> l[a"assert-c";pp_cl c] | Assertion_c c -> l[a"assert-c";pp_cl c]
| Drup_res c -> l[a"drup";pp_cl c]
| Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)] | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)]
| Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2] | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
| Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2] | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]