matita/components/ng_kernel/nCicEnvironment.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 module C = NCic
  15 module Ref = NReference
  16
  17 exception CircularDependency of string Lazy.t;;
  18 exception ObjectNotFound of string Lazy.t;;
  19 exception BadDependency of string Lazy.t * exn;;
  20 exception BadConstraint of string Lazy.t;;
  21 exception AlreadyDefined of string Lazy.t;;
  22
  23 let cache = NUri.UriHash.create 313;;
  24 let history = ref [];;
  25 let frozen_list = ref [];;
  26
  27 let get_obj = ref (fun _ _ -> assert false);;
  28 let set_get_obj = (:=) get_obj;;
  29
  30 module F = Format
  31
  32 let rec ppsort f = function
  33   | C.Prop -> F.fprintf f "Prop"
  34   | (C.Type []) -> F.fprintf f "Type0"
  35   | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
  36   | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
  37   | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
  38   | (C.Type l) ->
  39       F.fprintf f "Max(";
  40       ppsort f ((C.Type [List.hd l]));
  41       List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
  42       F.fprintf f ")"
  43 ;;
  44
  45 let string_of_univ u =
  46   let b = Buffer.create 100 in
  47   let f = Format.formatter_of_buffer b in
  48   ppsort f (NCic.Type u);
  49   Format.fprintf f "@?";
  50   Buffer.contents b
  51 ;;
  52
  53 let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
  54
  55 let max (l1:NCic.universe) (l2:NCic.universe) =
  56  match l2 with
  57  | x::tl ->
  58     let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
  59     x :: HExtlib.list_uniq ~eq:eq_univ
  60       (List.sort (fun (b1,u1) (b2,u2) ->
  61          let res = compare b1 b2 in
  62          if res = 0 then NUri.compare u1 u2 else res)
  63       rest)
  64  | [] ->
  65      match l1 with
  66      | [] -> []
  67      | ((`Type|`Succ), _)::_ -> l1
  68      | (`CProp, u)::tl -> (`Type, u)::tl
  69 ;;
  70
  71 let lt_constraints = ref [] (* a,b := a < b *)
  72
  73 let rec lt_path_uri avoid a b =
  74  List.exists
  75   (fun (x,y) ->
  76       NUri.eq y b &&
  77      (NUri.eq a x ||
  78         (not (List.exists (NUri.eq x) avoid) &&
  79         lt_path_uri (x::avoid) a x))
  80   ) !lt_constraints
  81 ;;
  82
  83 let lt_path a b = lt_path_uri [b] a b;;
  84
  85 let universe_eq a b =
  86   match a,b with
  87   | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] ->
  88          b1 = b2 && NUri.eq u1 u2
  89   | _, [(`Type|`CProp),_]
  90   | [(`Type|`CProp),_],_ -> false
  91   | _ ->
  92      raise (BadConstraint
  93       (lazy "trying to check if two inferred universes are equal"))
  94 ;;
  95
  96 let universe_leq a b =
  97   match a, b with
  98   | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
  99   | l, [((`Type|`CProp),b)] ->
 100        List.for_all
 101          (function
 102          | `Succ,a -> lt_path a b
 103          | _, a -> NUri.eq a b || lt_path a b) l
 104   | _, ([] | [`Succ,_] | _::_::_) ->
 105      raise (BadConstraint (lazy (
 106        "trying to check if "^string_of_univ a^
 107        " is leq than the inferred universe " ^ string_of_univ b)))
 108 ;;
 109
 110 let are_sorts_convertible ~test_eq_only s1 s2 =
 111    match s1,s2 with
 112    | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
 113    | C.Type a, C.Type b -> universe_eq a b
 114    | C.Prop,C.Type _ -> (not test_eq_only)
 115    | C.Prop, C.Prop -> true
 116    | _ -> false
 117 ;;
 118
 119 let pp_constraint x y =
 120   NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
 121 ;;
 122
 123 let pp_constraints () =
 124   String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
 125 ;;
 126
 127 let universes = ref [];;
 128
 129 let get_universes () =
 130   List.map (fun x -> [`Type,x]) !universes @
 131   List.map (fun x -> [`CProp,x]) !universes
 132 ;;
 133
 134 let is_declared u =
 135  match u with
 136  | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
 137  | _ -> assert false
 138 ;;
 139
 140 exception UntypableSort of string Lazy.t
 141 exception AssertFailure of string Lazy.t
 142
 143 let typeof_sort = function
 144   | C.Type ([(`Type|`CProp),u] as univ) ->
 145      if is_declared univ then (C.Type [`Succ, u])
 146      else
 147       let universes = !universes in
 148        raise (UntypableSort (lazy ("undeclared universe " ^
 149          NUri.string_of_uri u ^ "\ndeclared ones are: " ^
 150          String.concat ", " (List.map NUri.string_of_uri universes)
 151      )))
 152   | C.Type t ->
 153       raise (AssertFailure (lazy (
 154               "Cannot type an inferred type: "^ string_of_univ t)))
 155   | C.Prop -> (C.Type [])
 156 ;;
 157
 158 let add_lt_constraint a b =
 159   match a,b with
 160   | [`Type,a2],[`Type,b2] ->
 161       if not (lt_path_uri [] a2 b2) then (
 162         if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
 163          (raise(BadConstraint(lazy("universe inconsistency adding "^
 164                     pp_constraint a2 b2
 165            ^ " to:\n" ^ pp_constraints ()))));
 166         universes := a2 :: b2 ::
 167           List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
 168         lt_constraints := (a2,b2) :: !lt_constraints);
 169       history := (`Constr (a,b))::!history;
 170   | _ -> raise (BadConstraint
 171           (lazy "trying to add a constraint on an inferred universe"))
 172 ;;
 173
 174 let family_of = function (`CProp,_)::_ -> `CProp | _ -> `Type ;;
 175
 176 let sup fam l =
 177   match l with
 178   | [(`Type|`CProp),_] -> Some l
 179   | l ->
 180    let bigger_than acc (s1,n1) =
 181     List.filter
 182      (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc
 183    in
 184    let solutions = List.fold_left bigger_than !universes l in
 185    let rec aux = function
 186      | [] -> None
 187      | u :: tl ->
 188          if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
 189          else Some [fam,u]
 190    in
 191     aux solutions
 192 ;;
 193
 194 let sup l = sup (family_of l) l;;
 195
 196 let inf ~strict fam l =
 197   match l with
 198   | [(`Type|`CProp),_] -> Some l
 199   | [] -> None
 200   | l ->
 201    let smaller_than acc (_s1,n1) =
 202     List.filter
 203      (fun x -> lt_path_uri [] x n1 || (not strict && NUri.eq n1 x)) acc
 204    in
 205    let solutions = List.fold_left smaller_than !universes l in
 206    let rec aux = function
 207      | [] -> None
 208      | u :: tl ->
 209          if List.exists (lt_path_uri [] u) solutions then aux tl
 210          else Some [fam,u]
 211    in
 212     aux solutions
 213 ;;
 214
 215 let inf ~strict l = inf ~strict (family_of l) l;;
 216
 217 let rec universe_lt a b =
 218   match a, b with
 219   | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
 220   | l, ([((`Type|`CProp),b)] as orig_b) ->
 221        List.for_all
 222          (function
 223          | `Succ,_ as a ->
 224              (match sup [a] with
 225              | None -> false
 226              | Some x -> universe_lt x orig_b)
 227          | _, a -> lt_path a b) l
 228   | _, ([] | [`Succ,_] | _::_::_) ->
 229      raise (BadConstraint (lazy (
 230        "trying to check if "^string_of_univ a^
 231        " is lt than the inferred universe " ^ string_of_univ b)))
 232 ;;
 233
 234
 235 let allowed_sort_elimination s1 s2 =
 236   match s1, s2 with
 237   | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])
 238   | C.Type _, C.Type ((`CProp,_)::_)
 239   | C.Type _, C.Prop
 240   | C.Prop, C.Prop -> `Yes
 241
 242   | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
 243   | C.Prop, C.Type _ -> `UnitOnly
 244 ;;
 245
 246 let typecheck_obj,already_set = ref (fun _ _ -> assert false), ref false;;
 247 let set_typecheck_obj f =
 248  if !already_set then
 249   assert false
 250  else
 251   begin
 252    typecheck_obj := f;
 253    already_set := true
 254   end
 255 ;;
 256
 257 (* CSC: old code that performs recursive invalidation; to be removed
 258  * once we understand what we really want. Once we removed it, we can
 259  * also remove the !history
 260 let invalidate_item item =
 261  let item_eq a b =
 262    match a, b with
 263    | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2
 264    | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *)
 265    | _ -> false
 266  in
 267  let rec aux to_be_deleted =
 268   function
 269      [] -> assert false
 270    | item'::tl when item_eq item item' -> item'::to_be_deleted,tl
 271    | item'::tl -> aux (item'::to_be_deleted) tl
 272  in
 273   let to_be_deleted,h = aux [] !history in
 274    history := h;
 275    List.iter
 276      (function
 277      | `Obj (uri,_) -> NUri.UriHash.remove cache uri
 278      | `Constr ([_,u1],[_,u2]) as c ->
 279           let w = u1,u2 in
 280           if not(List.mem c !history) then
 281            lt_constraints := List.filter ((<>) w) !lt_constraints;
 282      | `Constr _ -> assert false
 283      ) to_be_deleted
 284 ;;
 285 *)
 286
 287 let invalidate_item =
 288  function
 289     `Obj (uri,_) -> NUri.UriHash.remove cache uri
 290   | `Constr ([_,u1],[_,u2]) ->
 291       let w = u1,u2 in
 292       lt_constraints := List.filter ((<>) w) !lt_constraints;
 293   | `Constr _ -> assert false
 294 ;;
 295
 296 exception Propagate of NUri.uri * exn;;
 297
 298 let to_exn f x =
 299  match f x with
 300     `WellTyped o -> o
 301   | `Exn e -> raise e
 302 ;;
 303
 304 let check_and_add_obj (status:#NCic.status) ((u,_,_,_,_) as obj) =
 305  let saved_frozen_list = !frozen_list in
 306  try
 307    frozen_list := (u,obj)::saved_frozen_list;
 308    HLog.warn ("Typechecking of " ^ NUri.string_of_uri u);
 309    !typecheck_obj (status :> NCic.status) obj;
 310    frozen_list := saved_frozen_list;
 311    let obj' = `WellTyped obj in
 312    NUri.UriHash.add cache u obj';
 313    history := (`Obj (u,obj))::!history;
 314    obj'
 315  with
 316     Sys.Break as e ->
 317      frozen_list := saved_frozen_list;
 318      raise e
 319   | Propagate (u',old_exn) as e' ->
 320      frozen_list := saved_frozen_list;
 321      let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
 322        " depends (recursively) on " ^ NUri.string_of_uri u' ^
 323        " which is not well-typed"),
 324        match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
 325      NUri.UriHash.add cache u exn;
 326      history := (`Obj (u,obj))::!history;
 327      if saved_frozen_list = [] then
 328       exn
 329      else
 330       raise e'
 331   | e ->
 332      frozen_list := saved_frozen_list;
 333      let exn = `Exn e in
 334      NUri.UriHash.add cache u exn;
 335      history := (`Obj (u,obj))::!history;
 336      if saved_frozen_list = [] then
 337       exn
 338      else
 339       raise (Propagate (u,e))
 340 ;;
 341
 342 let get_checked_obj status u =
 343  if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
 344  then
 345   raise (CircularDependency (lazy (NUri.string_of_uri u)))
 346  else
 347   try NUri.UriHash.find cache u
 348   with Not_found -> check_and_add_obj status (!get_obj (status :> NCic.status) u)
 349 ;;
 350
 351 let get_checked_obj (status:#NCic.status) u = to_exn (get_checked_obj status) u;;
 352
 353 let check_and_add_obj status ((u,_,_,_,_) as obj) =
 354  if NUri.UriHash.mem cache u then
 355   raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
 356  else
 357   ignore (to_exn (check_and_add_obj status) obj)
 358 ;;
 359
 360 let get_checked_decl status = function
 361   | Ref.Ref (uri, Ref.Decl) ->
 362       (match get_checked_obj status uri with
 363       | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
 364           rlv,name,ty,att,height
 365       | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
 366           prerr_endline "get_checked_decl on a definition"; assert false
 367       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
 368   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
 369 ;;
 370
 371 let get_checked_def status = function
 372   | Ref.Ref (uri, Ref.Def _) ->
 373       (match get_checked_obj status uri with
 374       | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
 375           rlv,name,bo,ty,att,height
 376       | _,_,_,_, C.Constant (_,_,None,_,_) ->
 377           prerr_endline "get_checked_def on an axiom"; assert false
 378       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
 379   | _ -> prerr_endline "get_checked_def on a non def"; assert false
 380 ;;
 381
 382 let get_checked_indtys status = function
 383   | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
 384       (match get_checked_obj status uri with
 385       | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
 386         inductive,leftno,tys,att,n
 387       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
 388   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 389 ;;
 390
 391 let get_checked_fixes_or_cofixes status = function
 392   | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
 393       (match get_checked_obj status uri with
 394       | _,height,_,_, C.Fixpoint (_,funcs,att) ->
 395          funcs, att, height
 396       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
 397   | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
 398 ;;
 399
 400 let get_relevance status (Ref.Ref (_, infos) as r) =
 401   match infos with
 402      Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def status r in res
 403    | Ref.Decl -> let res,_,_,_,_ = get_checked_decl status r in res
 404    | Ref.Ind _ ->
 405        let _,_,tl,_,n = get_checked_indtys status r in
 406        let res,_,_,_ = List.nth tl n in
 407          res
 408     | Ref.Con (_,i,_) ->
 409        let _,_,tl,_,n = get_checked_indtys status r in
 410        let _,_,_,cl = List.nth tl n in
 411        let res,_,_ = List.nth cl (i - 1) in
 412          res
 413     | Ref.Fix (fixno,_,_)
 414     | Ref.CoFix fixno ->
 415         let fl,_,_ = get_checked_fixes_or_cofixes status r in
 416         let res,_,_,_,_ = List.nth fl fixno in
 417           res
 418 ;;
 419
 420
 421 let invalidate _ =
 422   assert (!frozen_list = []);
 423   NUri.UriHash.clear cache
 424 ;;