helm/software/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 f = get_obj := f;;
  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 let invalidate_item item =
 258  let item_eq a b =
 259    match a, b with
 260    | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2
 261    | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *)
 262    | _ -> false
 263  in
 264  let rec aux to_be_deleted =
 265   function
 266      [] -> assert false
 267    | item'::tl when item_eq item item' -> item'::to_be_deleted,tl
 268    | item'::tl -> aux (item'::to_be_deleted) tl
 269  in
 270   let to_be_deleted,h = aux [] !history in
 271    history := h;
 272    List.iter
 273      (function
 274      | `Obj (uri,_) -> NUri.UriHash.remove cache uri
 275      | `Constr ([_,u1],[_,u2]) as c ->
 276           let w = u1,u2 in
 277           if not(List.mem c !history) then
 278            lt_constraints := List.filter ((<>) w) !lt_constraints;
 279      | `Constr _ -> assert false
 280      ) to_be_deleted
 281 ;;
 282
 283 exception Propagate of NUri.uri * exn;;
 284
 285 let to_exn f x =
 286  match f x with
 287     `WellTyped o -> o
 288   | `Exn e -> raise e
 289 ;;
 290
 291 let check_and_add_obj ((u,_,_,_,_) as obj) =
 292  let saved_frozen_list = !frozen_list in
 293  try
 294    frozen_list := (u,obj)::saved_frozen_list;
 295    !typecheck_obj obj;
 296    frozen_list := saved_frozen_list;
 297    let obj' = `WellTyped obj in
 298    NUri.UriHash.add cache u obj';
 299    history := (`Obj (u,obj))::!history;
 300    obj'
 301  with
 302     Sys.Break as e ->
 303      frozen_list := saved_frozen_list;
 304      raise e
 305   | Propagate (u',old_exn) as e' ->
 306      frozen_list := saved_frozen_list;
 307      let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
 308        " depends (recursively) on " ^ NUri.string_of_uri u' ^
 309        " which is not well-typed"),
 310        match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
 311      NUri.UriHash.add cache u exn;
 312      history := (`Obj (u,obj))::!history;
 313      if saved_frozen_list = [] then
 314       exn
 315      else
 316       raise e'
 317   | e ->
 318      frozen_list := saved_frozen_list;
 319      let exn = `Exn e in
 320      NUri.UriHash.add cache u exn;
 321      history := (`Obj (u,obj))::!history;
 322      if saved_frozen_list = [] then
 323       exn
 324      else
 325       raise (Propagate (u,e))
 326 ;;
 327
 328 let get_checked_obj u =
 329  if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
 330  then
 331   raise (CircularDependency (lazy (NUri.string_of_uri u)))
 332  else
 333   try NUri.UriHash.find cache u
 334   with Not_found -> check_and_add_obj (!get_obj u)
 335 ;;
 336
 337 let get_checked_obj u = to_exn get_checked_obj u;;
 338
 339 let check_and_add_obj ((u,_,_,_,_) as obj) =
 340  if NUri.UriHash.mem cache u then
 341   raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
 342  else
 343   ignore (to_exn check_and_add_obj obj)
 344 ;;
 345
 346 let get_checked_decl = function
 347   | Ref.Ref (uri, Ref.Decl) ->
 348       (match get_checked_obj uri with
 349       | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
 350           rlv,name,ty,att,height
 351       | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
 352           prerr_endline "get_checked_decl on a definition"; assert false
 353       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
 354   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
 355 ;;
 356
 357 let get_checked_def = function
 358   | Ref.Ref (uri, Ref.Def _) ->
 359       (match get_checked_obj uri with
 360       | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
 361           rlv,name,bo,ty,att,height
 362       | _,_,_,_, C.Constant (_,_,None,_,_) ->
 363           prerr_endline "get_checked_def on an axiom"; assert false
 364       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
 365   | _ -> prerr_endline "get_checked_def on a non def"; assert false
 366 ;;
 367
 368 let get_checked_indtys = function
 369   | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
 370       (match get_checked_obj uri with
 371       | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
 372         inductive,leftno,tys,att,n
 373       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
 374   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 375 ;;
 376
 377 let get_checked_fixes_or_cofixes = function
 378   | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
 379       (match get_checked_obj uri with
 380       | _,height,_,_, C.Fixpoint (_,funcs,att) ->
 381          funcs, att, height
 382       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
 383   | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
 384 ;;
 385
 386 let get_relevance (Ref.Ref (_, infos) as r) =
 387   match infos with
 388      Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
 389    | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
 390    | Ref.Ind _ ->
 391        let _,_,tl,_,n = get_checked_indtys r in
 392        let res,_,_,_ = List.nth tl n in
 393          res
 394     | Ref.Con (_,i,_) ->
 395        let _,_,tl,_,n = get_checked_indtys r in
 396        let _,_,_,cl = List.nth tl n in
 397        let res,_,_ = List.nth cl (i - 1) in
 398          res
 399     | Ref.Fix (fixno,_,_)
 400     | Ref.CoFix fixno ->
 401         let fl,_,_ = get_checked_fixes_or_cofixes r in
 402         let res,_,_,_,_ = List.nth fl fixno in
 403           res
 404 ;;
 405
 406
 407 let invalidate _ =
 408   assert (!frozen_list = []);
 409   NUri.UriHash.clear cache
 410 ;;