X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcomplete_rg%2Fcrg.ml;h=5eb81e3e14641a0f3008ddfd0ae050170c85a794;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=5a394f4f8372f3411430137b45e3da9f9a61d827;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 5a394f4f8..5eb81e3e1 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -10,124 +10,134 @@ V_______________________________________________________________ *) (* kernel version: complete, relative, global *) -(* note : fragment of complete lambda-delta serving as abstract layer *) +(* note : fragment of complete \lambda\delta serving as abstract layer *) module C = Cps +module N = Layer module E = Entity -module N = Level type uri = E.uri type id = E.id -type attrs = E.attrs +type n_attrs = E.node_attrs +type a_attrs = E.appl_attrs +type b_attrs = E.bind_attrs -type bind = Abst of N.level * term list (* level, domains *) - | Abbr of term list (* bodies *) - | Void of int (* number of exclusions *) -and term = TSort of attrs * int (* attrs, hierarchy index *) - | TLRef of attrs * int * int (* attrs, position indexes *) - | TGRef of attrs * uri (* attrs, reference *) - | TCast of attrs * term * term (* attrs, domain, element *) - | TAppl of attrs * term list * term (* attrs, arguments, function *) - | TProj of attrs * lenv * term (* attrs, closure, member *) - | TBind of attrs * bind * term (* attrs, binder, scope *) +type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *) + | Abbr of term (* body *) + | Void (* *) -and lenv = ESort (* top *) - | EProj of lenv * attrs * lenv (* environment, attrs, closure *) - | EBind of lenv * attrs * bind (* environment, attrs, binder *) +and term = TSort of int (* hierarchy index *) + | TLRef of n_attrs * int (* attrs, position indexe *) + | TGRef of n_attrs * uri (* attrs, reference *) + | TCast of term * term (* domain, element *) + | TAppl of a_attrs * term * term (* attrs, argument, function *) + | TBind of b_attrs * bind * term (* attrs, binder, scope *) + | TProj of lenv * term (* closure, member *) + +and lenv = ESort (* top *) + | EBind of lenv * n_attrs * b_attrs * bind (* environment, attrs, binder *) + | EAppl of lenv * a_attrs * term (* environment, attrs, argument *) + | EProj of lenv * lenv (* environment, closure *) type entity = term E.entity (* helpers ******************************************************************) -let rec tshift t = function - | ESort -> t - | EBind (e, a, b) -> tshift (TBind (a, b, t)) e - | EProj (e, a, d) -> tshift (TProj (a, d, t)) e +let empty_lenv = ESort -let tshift c t = tshift t c +let push_bind f a y b lenv = f (EBind (lenv, a, y, b)) -let rec eshift f c = function - | ESort -> f c - | EBind (e, a, b) -> let f ee = f (EBind (ee, a, b)) in eshift f c e - | EProj (e, a, d) -> let f ee = f (EProj (ee, a, d)) in eshift f c e +let push_appl f a t lenv = f (EAppl (lenv, a, t)) -let empty_lenv = ESort +let push_proj f e lenv = f (EProj (lenv, e)) + +let add_bind f y b t = f (TBind (y, b, t)) + +let add_appl f a v t = f (TAppl (a, v, t)) + +let add_proj f e t = f (TProj (e, t)) + +let rec shift f c t = match c with + | ESort -> f t + | EBind (e, _, a, b) -> add_bind (shift f e) a b t + | EAppl (e, a, v) -> add_appl (shift f e) a v t + | EProj (e, d) -> add_proj (shift f e) d t + +let rec append f c = function + | ESort -> f c + | EBind (e, y, a, b) -> append (push_bind f y a b) c e + | EAppl (e, a, t) -> append (push_appl f a t) c e + | EProj (e, d) -> append (push_proj f d) c e -let push_bind f lenv a b = f (EBind (lenv, a, b)) - -let push_proj f lenv a e = f (EProj (lenv, a, e)) - -let push2 err f lenv ?attr ?t () = match lenv, attr, t with - | EBind (e, a, Abst (n, ws)), Some attr, Some t -> - f (EBind (e, (attr :: a), Abst (n, t :: ws))) - | EBind (e, a, Abst (n, ws)), None, Some t -> - f (EBind (e, a, Abst (n, t :: ws))) - | EBind (e, a, Abbr vs), Some attr, Some t -> - f (EBind (e, (attr :: a), Abbr (t :: vs))) - | EBind (e, a, Abbr vs), None, Some t -> - f (EBind (e, a, Abbr (t :: vs))) - | EBind (e, a, Void n), Some attr, None -> - f (EBind (e, (attr :: a), Void (succ n))) - | EBind (e, a, Void n), None, None -> - f (EBind (e, a, Void (succ n))) - | _ -> err () - -(* this id not tail recursive *) let resolve_lref err f id lenv = - let rec aux f i k = function - | ESort -> err () - | EBind (tl, _, Abst (_, [])) - | EBind (tl, _, Abbr []) - | EBind (tl, _, Void 0) -> aux f i k tl - | EBind (tl, a, b) -> - let err kk = aux f (succ i) (k + kk) tl in - let f j = f i j (k + j) in - E.resolve err f id a - | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) + let rec aux i = function + | ESort -> err () + | EAppl (tl, _, _) -> aux i tl + | EBind (tl, y, a, _) -> + let f id0 _ = if id0 = id then f y a i else aux (succ i) tl in + let err () = aux (succ i) tl in + E.name err f a + | EProj (tl, d) -> append (aux i) tl d in - aux f 0 0 lenv - -let rec get_name err f i j = function - | ESort -> err i - | EBind (tl, _, Abst (_, [])) - | EBind (tl, _, Abbr []) - | EBind (tl, _, Void 0) -> get_name err f i j tl - | EBind (_, a, _) when i = 0 -> + aux 0 lenv + +let rec get_name err f i = function + | ESort -> err i + | EAppl (tl, _, _) -> get_name err f i tl + | EBind (_, _, a, _) when i = 0 -> let err () = err i in - E.get_name err f j a - | EBind (tl, _, _) -> - get_name err f (pred i) j tl - | EProj (tl, _, e) -> - let err i = get_name err f i j tl in - get_name err f i j e - -let get_index err f i j lenv = - let rec aux f i k = function - | ESort -> err i - | EBind (tl, _, Abst (_, [])) - | EBind (tl, _, Abbr []) - | EBind (tl, _, Void 0) -> aux f i k tl - | EBind (_, a, _) when i = 0 -> - if E.count_names a > j then f (k + j) else err i - | EBind (tl, a, _) -> - aux f (pred i) (k + E.count_names a) tl - | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) + E.name err f a + | EBind (tl, _, _, _) -> get_name err f (pred i) tl + | EProj (tl, e) -> + let err i = get_name err f i tl in + get_name err f i e + +let rec get e i = match e with + | ESort -> ESort, E.empty_node, E.empty_bind, Void + | EBind (e, y, a, b) when i = 0 -> e, y, a, b + | EBind (e, _, _, _) -> get e (pred i) + | EAppl (e, _, _) -> get e i + | EProj (e, d) -> get (append C.start e d) i + +let rec sub_list_strict f e l = match e, l with + | _, [] -> f e + | EBind (e, _, _, Abst _), _ :: tl -> sub_list_strict f e tl + | _ -> assert false + +let rec fold_names f map x = function + | ESort -> f x + | EBind (e, _, {E.b_name = Some n}, Abst _) -> fold_names f map (map x n) e + | _ -> assert false + +let rec mem err f e a0 = match e with + | ESort -> err () + | EBind (e, _, a, _) -> + if a.E.b_name = a0.E.b_name then f () else mem err f e a0 + | EAppl (e, _, _) -> mem err f e a0 + | EProj (e, d) -> + let err () = mem err f e a0 in mem err f d a0 + +let set_layer f n0 e = + let rec aux f = function + | ESort -> f ESort + | EBind (e, y, a, Abst (r, n, w)) -> aux (push_bind f y a (Abst (r, n0, w))) e + | EBind (e, y, a, b) -> aux (push_bind f y a b) e + | EAppl (e, a, v) -> aux (push_appl f a v) e + | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d + in + aux f e + +let set_attrs f a0 e = + let rec aux f = function + | ESort -> f ESort + | EBind (e, y, a, b) -> + let a = E.compose a a0 in + aux (push_bind f y a b) e + | EAppl (e, a, v) -> + aux (push_appl f a v) e + | EProj (e, d) -> + let f d = aux (push_proj f d) e in + aux f d in - aux f i 0 lenv - -let rec names_of_lenv ns = function - | ESort -> ns - | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl - | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl - -let rec get i = function - | ESort -> ESort, [], Void 0 - | EBind (e, _, Abst (_, [])) - | EBind (e, _, Abbr []) - | EBind (e, _, Void 0) -> get i e - | EBind (e, a, b) when i = 0 -> e, a, b - | EBind (e, _, _) -> get (pred i) e - | EProj (e, _, d) -> get i (eshift C.start e d) - -let get e i = get i e + aux f e