X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=2d5f03945f8d1fa69ae85444c2fdf58fbb842a57;hb=bbbf8a74bd5a272673c8687fdf2fc5eb9867853b;hp=57f130546d9ed4c5a663e88119fba719d6df2e7f;hpb=d3ce67da8c0fc8dc010cb99fb4700e5b803a7c89;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 57f130546..2d5f03945 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -16,11 +16,20 @@ module Ref = NReference exception CircularDependency of string Lazy.t;; exception ObjectNotFound of string Lazy.t;; -exception BadDependency of string Lazy.t;; +exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; +let get_obj = ref (fun _ -> assert false);; +let set_get_obj f = get_obj := f;; + let type0 = [] +let max l1 l2 = + HExtlib.list_uniq ~eq:(fun (b1,u1) (b2,u2) -> b1=b2 && NUri.eq u1 u2) + (List.sort (fun (b1,u1) (b2,u2) -> + let res = compare b1 b2 in if res = 0 then NUri.compare u1 u2 else res) + (l1 @ l2)) + let le_constraints = ref [] (* strict,a,b *) let rec le_path_uri avoid strict a b = @@ -41,19 +50,57 @@ let universe_leq a b = raise (BadConstraint (lazy "trying to check if a universe is less or equal than an inferred universe")) -let universe_eq a b = universe_leq b a && universe_leq a b +let universe_eq a b = + match a,b with + | [(false,_)], [(false,_)] -> universe_leq b a && universe_leq a b + | _, [(false,_)] + | [(false,_)],_ -> false + | _ -> + raise (BadConstraint + (lazy "trying to check if two inferred universes are equal")) +;; + +let pp_constraint b x y = + NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y +;; + +let pp_constraints () = + String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints) +;; + +let universes = ref [];; let add_constraint strict a b = match a,b with | [false,a2],[false,b2] -> if not (le_path_uri [] strict a2 b2) then ( if le_path_uri [] (not strict) b2 a2 then - (raise (BadConstraint (lazy "universe inconsistency"))); + (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2 + ^ " to:\n" ^ pp_constraints ())))); + universes := a2 :: b2 :: + List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes; le_constraints := (strict,a2,b2) :: !le_constraints) | _ -> raise (BadConstraint (lazy "trying to add a constraint on an inferred universe")) ;; +let sup l = + match l with + | [false,_] -> Some l + | l -> + let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in + let solutions = List.fold_left bigger_than !universes l in + let rec aux = function + | [] -> None + | u :: tl -> + if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl + else Some [false,u] + in + aux solutions +;; + + + let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;; let set_typecheck_obj f = if !already_set then @@ -66,60 +113,79 @@ let set_typecheck_obj f = ;; let cache = NUri.UriHash.create 313;; +let history = ref [];; let frozen_list = ref [];; +let invalidate_obj uri = + let rec aux to_be_deleted = + function + [] -> assert false + | uri'::tl when NUri.eq uri uri' -> uri'::to_be_deleted,tl + | uri'::tl -> aux (uri'::to_be_deleted) tl + in + let to_be_deleted,h = aux [] !history in + history := h; + List.iter (fun uri -> NUri.UriHash.remove cache uri) to_be_deleted +;; + exception Propagate of NUri.uri * exn;; +let to_exn f x = + match f x with + `WellTyped o -> o + | `Exn e -> raise e +;; + +let check_and_add_obj ((u,_,_,_,_) as obj) = + let saved_frozen_list = !frozen_list in + try + frozen_list := (u,obj)::saved_frozen_list; + !typecheck_obj obj; + frozen_list := saved_frozen_list; + let obj = `WellTyped obj in + NUri.UriHash.add cache u obj; + history := u::!history; + obj + with + Sys.Break as e -> + frozen_list := saved_frozen_list; + raise e + | Propagate (u',old_exn) as e' -> + frozen_list := saved_frozen_list; + let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^ + " depends (recursively) on " ^ NUri.string_of_uri u' ^ + " which is not well-typed"), + match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in + NUri.UriHash.add cache u exn; + history := u::!history; + if saved_frozen_list = [] then + exn + else + raise e' + | e -> + frozen_list := saved_frozen_list; + let exn = `Exn e in + NUri.UriHash.add cache u exn; + history := u::!history; + if saved_frozen_list = [] then + exn + else + raise (Propagate (u,e)) +;; + let get_checked_obj u = if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list then raise (CircularDependency (lazy (NUri.string_of_uri u))) else - let obj = - try NUri.UriHash.find cache u - with - Not_found -> - let saved_frozen_list = !frozen_list in - try - let obj = - try NCicLibrary.get_obj u - with - NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m) - in - frozen_list := (u,obj)::saved_frozen_list; - !typecheck_obj obj; - frozen_list := saved_frozen_list; - let obj = `WellTyped obj in - NUri.UriHash.add cache u obj; - obj - with - Sys.Break as e -> - frozen_list := saved_frozen_list; - raise e - | Propagate (u',_) as e' -> - frozen_list := saved_frozen_list; - let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^ - " depends (recursively) on " ^ NUri.string_of_uri u' ^ - " which is not well-typed"))) in - NUri.UriHash.add cache u exn; - if saved_frozen_list = [] then - exn - else - raise e' - | e -> - frozen_list := saved_frozen_list; - let exn = `Exn e in - NUri.UriHash.add cache u exn; - if saved_frozen_list = [] then - exn - else - raise (Propagate (u,e)) - in - match obj with - `WellTyped o -> o - | `Exn e -> raise e + try NUri.UriHash.find cache u + with Not_found -> check_and_add_obj (!get_obj u) ;; +let get_checked_obj u = to_exn get_checked_obj u;; + +let check_and_add_obj obj = ignore (to_exn check_and_add_obj obj);; + let get_checked_decl = function | Ref.Ref (uri, Ref.Decl) -> (match get_checked_obj uri with