diff options
| author | Pierre-Marie Pédrot | 2019-05-31 14:27:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-04 11:16:17 +0200 |
| commit | e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d (patch) | |
| tree | f3b9bc7307d04f2757b3d00504100023bc9f2d9a /checker/values.ml | |
| parent | 589aaf4f97d5cfcdabfda285739228f5ee52261f (diff) | |
Do not substitute opaque constants when discharging.
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 031f05dd6b..6dbf281f49 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) - [|Fail "Var"|]; (* Var *) + [|v_id|]; (* Var *) [|Fail "Meta"|]; (* Meta *) [|Fail "Evar"|]; (* Evar *) [|v_sort|]; (* Sort *) @@ -383,6 +383,22 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_opaques = Array (Opt v_constr) +let v_ndecl = v_sum "named_declaration" 0 + [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *) + [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *) + +let v_nctxt = List v_ndecl + +let v_work_list = + let v_abstr = v_pair v_instance (Array v_id) in + Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|]) + +let v_abstract = + Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |]) + +let v_cooking_info = + Tuple ("cooking_info", [|v_work_list; v_abstract|]) + +let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |]))) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |