From c3be2411bf115cfa1305777b0b2ee3b7d3dab761 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 19 Nov 2019 19:41:21 -0600 Subject: [PATCH] wip: th data --- src/th-data/types.ml | 50 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 src/th-data/types.ml diff --git a/src/th-data/types.ml b/src/th-data/types.ml new file mode 100644 index 00000000..ba4085e3 --- /dev/null +++ b/src/th-data/types.ml @@ -0,0 +1,50 @@ + +and datatype = { + data_cstors: data_cstor ID.Map.t lazy_t; +} + +(* TODO: in cstor, add: + - for each selector, a special "magic" term for undefined, in + case the selector is ill-applied (Collapse 2) *) + +(* a constructor *) +and data_cstor = { + cstor_ty: ty; + cstor_args: ty IArray.t; (* argument types *) + cstor_proj: cst IArray.t lazy_t; (* projectors *) + cstor_test: cst lazy_t; (* tester *) + cstor_cst: cst; (* the cstor itself *) + cstor_card: ty_card; (* cardinality of the constructor('s args) *) +} + +val make_cstor : ID.t -> Ty.t -> data_cstor lazy_t -> t +val make_proj : ID.t -> Ty.t -> data_cstor lazy_t -> int -> t +val make_tester : ID.t -> Ty.t -> data_cstor lazy_t -> t +val make_defined : ID.t -> Ty.t -> term lazy_t -> cst_defined_info -> t +val make_undef : ID.t -> Ty.t -> t + +let make_cstor id ty cstor = + let _, ret = Ty.unfold ty in + assert (Ty.is_data ret); + make id (Cst_cstor cstor) +let make_proj id ty cstor i = + make id (Cst_proj (ty, cstor, i)) +let make_tester id ty cstor = + make id (Cst_test (ty, cstor)) + +val cstor_test : data_cstor -> term -> t +val cstor_proj : data_cstor -> int -> term -> t +val case : term -> term ID.Map.t -> t + +let case u m = Case (u,m) +let if_ a b c = + assert (Ty.equal b.term_ty c.term_ty); + If (a,b,c) + +let cstor_test cstor t = + app_cst (Lazy.force cstor.cstor_test) (IArray.singleton t) + +let cstor_proj cstor i t = + let p = IArray.get (Lazy.force cstor.cstor_proj) i in + app_cst p (IArray.singleton t) +