From 4767ed3aba79ed1d06c6d4e2d195b77e5bd26db5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 20 Jul 2004 13:26:56 +0000 Subject: [PATCH] The type substitution has been moved into Cic. --- helm/ocaml/cic/cic.ml | 3 +++ helm/ocaml/cic/cicUtil.ml | 28 ++++++++++++++++++++++++++++ helm/ocaml/cic/cicUtil.mli | 5 +++++ 3 files changed, 36 insertions(+) diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index e310b6a9f..7dc86114d 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -110,6 +110,9 @@ and coInductiveFun = (* depend on new ones. *) and conjecture = int * context * term and metasenv = conjecture list +and substitution = (int * (context * term)) list + + (* a metasenv is a list of declarations of metas in declarations *) (* order (i.e. [oldest ; ... ; newest]). Older variables can not *) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 55a70822e..ad01110c4 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -24,14 +24,42 @@ *) exception Meta_not_found of int +exception Subst_not_found of int + let lookup_meta index metasenv = try List.find (fun (index', _, _) -> index = index') metasenv with Not_found -> raise (Meta_not_found index) +let lookup_subst n subst = + try + List.assoc n subst + with Not_found -> raise (Subst_not_found n) + let exists_meta index = List.exists (fun (index', _, _) -> (index = index')) +(* clean_up_meta take a substitution, a metasenv a meta_inex and a local +context l and clean up l with respect to the hidden hipothesis in the +canonical context *) + +let clean_up_local_context subst metasenv n l = + let cc = + (try + let (cc,_) = lookup_subst n subst in cc + with Subst_not_found _ -> + try + let (_,cc,_) = lookup_meta n metasenv in cc + with Meta_not_found _ -> assert false) in + (try + List.map2 + (fun t1 t2 -> + match t1,t2 with + None , _ -> None + | _ , t -> t) cc l + with + Invalid_argument _ -> assert false) + let is_closed = let module C = Cic in let rec is_closed k = diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 9069c24fb..c03783b86 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -24,9 +24,14 @@ *) exception Meta_not_found of int +exception Subst_not_found of int val lookup_meta: int -> Cic.metasenv -> Cic.conjecture +val lookup_subst: int -> Cic.substitution -> Cic.context * Cic.term val exists_meta: int -> Cic.metasenv -> bool +val clean_up_local_context : + Cic.substitution -> Cic.metasenv -> int -> (Cic.term option) list + -> (Cic.term option) list val is_closed : Cic.term -> bool -- 2.39.2