Skip to content

Commit

Permalink
Merge pull request #3322 from mtzguido/misc
Browse files Browse the repository at this point in the history 
Add an interface for FStar.Reflection.V2.TermEq, and mark it a plugin
  • Loading branch information
@mtzguido
mtzguido authored Jun 20, 2024
2 parents c383918 + 675dbe6 commit af7e317
Show file tree
Hide file tree
Showing 3 changed files with 289 additions and 154 deletions.
144 changes: 130 additions & 14 deletions ocaml/fstar-lib/generated/FStar_Reflection_V2_TermEq.ml
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

141 changes: 1 addition & 140 deletions ulib/FStar.Reflection.V2.TermEq.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,26 +17,6 @@ In fact many auxiliary lemmas should be removed as they should become
obvious. Lines marked with *** should not be needed.
*)

let rec allP0 #a (pred : a -> Type0) (l : list a) : Type0 =
match l with
| [] -> True
| x::xs -> pred x /\ allP0 pred xs

let rec allP #a #b (top:b) (pred : (x:a{x << top}) -> Type0) (l : list a{l << top \/ l === top}) : Type0 =
match l with
| [] -> True
| x::xs -> pred x /\ allP top pred xs

let optP0 #a (pred : a -> Type0) (o : option a) : Type0 =
match o with
| None -> True
| Some x -> pred x

let optP #a #b (top:b) (pred : (x:a{x << top}) -> Type0) (o : option a{o << top}) : Type0 =
match o with
| None -> True
| Some x -> pred x

let rec memP_allP #a #b (top:b) (pred : (x:a{x << top}) -> Type) (x : a) (l : list a{l << top})
: Lemma (requires allP top pred l /\ L.memP x l)
(ensures x << top /\ pred x)
Expand Down Expand Up @@ -399,19 +379,6 @@ let rec defined_list_dec #a #b (t1 t2 : b) (f : comparator_for a)
| x::xs, y::ys -> defined_list_dec t1 t2 f xs ys
| _ -> ()

val faithful_univ : universe -> Type0
let rec faithful_univ (u : universe) =
match inspect_universe u with
| Uv_Unif _ -> False (* We just forbid this *)

| Uv_Unk
| Uv_Zero
| Uv_BVar _
| Uv_Name _ -> True

| Uv_Succ u -> faithful_univ u
| Uv_Max us -> allP u faithful_univ us

let faithful_univ_UvMax (u : universe) (us : list universe)
: Lemma (requires inspect_universe u == Uv_Max us /\ faithful_univ u)
(ensures allP u faithful_univ us)
Expand Down Expand Up @@ -454,106 +421,6 @@ and univ_faithful_lemma_list #b (u1 u2 : b) (us1 : list universe{us1 << u1}) (us
defined_list_dec u1 u2 univ_cmp us1 us2

(* Just a placeholder for now *)
val faithful_const : vconst -> Type0
let faithful_const c = True

val faithful : term -> Type0
let rec faithful t =
match inspect_ln t with
| Tv_Var _
| Tv_BVar _
| Tv_FVar _
| Tv_Unknown ->
True

| Tv_Const c ->
faithful_const c

| Tv_UInst f us ->
allP t faithful_univ us

| Tv_Unsupp -> False
| Tv_App h a ->
faithful h /\ faithful_arg a
| Tv_Abs b t ->
faithful_binder b /\ faithful t
| Tv_Arrow b c ->
faithful_binder b /\ faithful_comp c
| Tv_Type u ->
faithful_univ u
| Tv_Refine b phi ->
faithful_binder b
/\ faithful phi

| Tv_Uvar n u -> False
| Tv_Let r ats x e b ->
faithful_attrs ats
/\ faithful_binder x
/\ faithful e
/\ faithful b

| Tv_Match sc o brs ->
faithful sc
/\ None? o // stopgap
/\ allP t faithful_branch brs

| Tv_AscribedT e ta tacopt eq ->
faithful e
/\ faithful ta
/\ optP t faithful tacopt

| Tv_AscribedC e c tacopt eq ->
faithful e
/\ faithful_comp c
/\ optP t faithful tacopt

and faithful_arg (a : argv) : Type0 =
faithful (fst a) /\ faithful_qual (snd a)

and faithful_qual (q:aqualv) : Type0 =
match q with
| Q_Implicit -> True
| Q_Explicit -> True
| Q_Meta m -> faithful m

and faithful_binder (b:binder) : Type0 =
match inspect_binder b with
| {sort=sort; qual=q; attrs=attrs} ->
faithful sort /\ faithful_qual q /\ faithful_attrs attrs

and faithful_branch (b : branch) : Type0 =
let (p, t) = b in
faithful_pattern p /\ faithful t

and faithful_pattern (p : pattern) : Type0 =
match p with
| Pat_Constant c -> faithful_const c
| Pat_Cons head univs subpats ->
optP p (allP p faithful_univ) univs
/\ allP p faithful_pattern_arg subpats

(* non-binding bvs are always OK *)
| Pat_Var _ _ -> True
| Pat_Dot_Term None -> True
| Pat_Dot_Term (Some t) -> faithful t

and faithful_pattern_arg (pb : pattern & bool) : Type0 =
faithful_pattern (fst pb)

and faithful_attrs ats : Type0 =
allP ats faithful ats

and faithful_comp c =
match inspect_comp c with
| C_Total t -> faithful t
| C_GTotal t -> faithful t
| C_Lemma pre post pats -> faithful pre /\ faithful post /\ faithful pats
| C_Eff us ef r args decs ->
allP c faithful_univ us
/\ faithful r
/\ allP c faithful_arg args
/\ allP c faithful decs

val faithful_lemma (t1:term) (t2:term) : Lemma (requires faithful t1 /\ faithful t2) (ensures defined (term_cmp t1 t2))

#push-options "--z3rlimit 40"
Expand Down Expand Up @@ -820,22 +687,16 @@ and faithful_lemma_comp (c1 c2 : comp) : Lemma (requires faithful_comp c1 /\ fai
#pop-options


let faithful_term = t:term{faithful t}

(* A conservative version: works on all terms, returns `true` if they
are guaranteed to be equal. *)
let term_eq (t1 t2 : term) : (b:bool{b ==> t1 == t2}) =
Eq? (term_cmp t1 t2)

(* A fully decidable version, for faithful terms. *)
let term_eq_dec (t1 t2 : faithful_term) : (b:bool{b <==> t1 == t2}) =
faithful_lemma t1 t2;
Eq? (term_cmp t1 t2)

(* Idem for universes *)
let faithful_universe = t:universe{faithful_univ t}
let univ_eq (u1 u2 : universe) : (b:bool{b ==> u1 == u2}) =
Eq? (univ_cmp u1 u2)

let univ_eq_dec (u1 u2 : faithful_universe) : (b:bool{b <==> u1 == u2}) =
univ_faithful_lemma u1 u2;
Eq? (univ_cmp u1 u2)
Loading

0 comments on commit af7e317

Please sign in to comment.