diff options
| author | Maxime Dénès | 2019-06-06 17:33:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-06 17:33:53 +0200 |
| commit | 281faca10d471be5fd2bca864ffd382d69f7a110 (patch) | |
| tree | 8ceda4c0c13c1d8103713aac84b4f7439fe1245a /checker/values.ml | |
| parent | 90c1084ba489415f8df588c43e088491bc6be450 (diff) | |
| parent | 1cdfb1f9270e399a784b346c3f8d6abbc4477552 (diff) | |
Merge PR #10299: Lazy substitution of section contexts in opaque proofs
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
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..4a4c8d803c 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 (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |