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 exception CircularDependency of string Lazy.t;;
  15 exception ObjectNotFound of string Lazy.t;;
  16 exception BadDependency of string Lazy.t;;
  17
  18 let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
  19
  20 let u_eq (a1,a2) (b1,b2) = a1=b1 && NUri.eq a2 b2
  21
  22 let u_lt a b =
  23   match a,b with
  24   | (false,a2), (true,b2) -> NUri.eq a2 b2
  25   | _ -> false
  26 ;;
  27
  28 let leq_constraints = ref []
  29
  30 let rec path a b =
  31   List.exists (fun (x,y) -> u_eq y b && (u_eq a x || u_lt a x || path a x))
  32     !leq_constraints
  33
  34 let universe_leq a b =
  35   match a, b with
  36   | a,[b] -> List.for_all (fun a -> path a b) a
  37   | _ -> assert false
  38
  39 let universe_eq a b = universe_leq b a || universe_leq a b
  40
  41 let add_lt_constraint a b =
  42   match a,b with
  43   | [false,a2 as a],[false,_ as b] ->
  44       if path b a then (raise (Failure "universe inconsistency"));
  45       leq_constraints := ((true,a2),b) :: !leq_constraints
  46   | _ -> assert false
  47 ;;
  48
  49 let add_leq_constraint a b =
  50   match a,b with
  51   | [false,_ as a],[false,b2 as b] ->
  52       if path (true,b2) a then (raise (Failure "universe inconsistency"));
  53       leq_constraints := (a,b) :: !leq_constraints
  54   | _ -> assert false
  55 ;;
  56
  57
  58
  59 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
  60 let set_typecheck_obj f =
  61  if !already_set then
  62   assert false
  63  else
  64   begin
  65    typecheck_obj := f;
  66    already_set := true
  67   end
  68 ;;
  69
  70 let cache = NUri.UriHash.create 313;;
  71 let frozen_list = ref [];;
  72
  73 exception Propagate of NUri.uri * exn;;
  74
  75 let get_checked_obj u =
  76  if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
  77  then
  78   raise (CircularDependency (lazy (NUri.string_of_uri u)))
  79  else
  80   let obj =
  81    try NUri.UriHash.find cache u
  82    with
  83     Not_found ->
  84      let saved_frozen_list = !frozen_list in
  85      try
  86       let obj =
  87        try NCicLibrary.get_obj u
  88        with
  89         NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
  90       in
  91         frozen_list := (u,obj)::saved_frozen_list;
  92         !typecheck_obj obj;
  93         frozen_list := saved_frozen_list;
  94         let obj = `WellTyped obj in
  95         NUri.UriHash.add cache u obj;
  96         obj
  97      with
  98         Sys.Break as e ->
  99          frozen_list := saved_frozen_list;
 100          raise e
 101       | Propagate (u',_) as e' ->
 102          frozen_list := saved_frozen_list;
 103          let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
 104            " depends (recursively) on " ^ NUri.string_of_uri u' ^
 105            " which is not well-typed"))) in
 106          NUri.UriHash.add cache u exn;
 107          if saved_frozen_list = [] then
 108           exn
 109          else
 110           raise e'
 111       | e ->
 112          frozen_list := saved_frozen_list;
 113          let exn = `Exn e in
 114          NUri.UriHash.add cache u exn;
 115          if saved_frozen_list = [] then
 116           exn
 117          else
 118           raise (Propagate (u,e))
 119   in
 120    match obj with
 121       `WellTyped o -> o
 122     | `Exn e -> raise e
 123 ;;
 124
 125 let get_checked_decl = function
 126   | NReference.Ref (uri, NReference.Decl) ->
 127       (match get_checked_obj uri with
 128       | _,height,_,_, NCic.Constant (rlv,name,None,ty,att) ->
 129           rlv,name,ty,att,height
 130       | _,_,_,_, NCic.Constant (_,_,Some _,_,_) ->
 131           prerr_endline "get_checked_decl on a definition"; assert false
 132       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
 133   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
 134 ;;
 135
 136 let get_checked_def = function
 137   | NReference.Ref (uri, NReference.Def _) ->
 138       (match get_checked_obj uri with
 139       | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
 140           rlv,name,bo,ty,att,height
 141       | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
 142           prerr_endline "get_checked_def on an axiom"; assert false
 143       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
 144   | _ -> prerr_endline "get_checked_def on a non def"; assert false
 145 ;;
 146
 147 let get_checked_indtys = function
 148   | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
 149       (match get_checked_obj uri with
 150       | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
 151         inductive,leftno,tys,att,n
 152       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
 153   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 154 ;;
 155
 156 let get_checked_fixes_or_cofixes = function
 157   | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))->
 158       (match get_checked_obj uri with
 159       | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
 160          funcs, att, height
 161       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
 162   | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
 163 ;;
 164
 165 let get_indty_leftno = function
 166   | NReference.Ref (uri, NReference.Ind _)
 167   | NReference.Ref (uri, NReference.Con _) ->
 168       (match get_checked_obj uri with
 169       | _,_,_,_, NCic.Inductive (_,left,_,_) -> left
 170       | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
 171   | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
 172 ;;
 173
 174 let get_relevance (NReference.Ref (_, infos) as r) =
 175   match infos with
 176      NReference.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
 177    | NReference.Decl -> let res,_,_,_,_ = get_checked_decl r in res
 178    | NReference.Ind _ ->
 179        let _,_,tl,_,n = get_checked_indtys r in
 180        let res,_,_,_ = List.nth tl n in
 181          res
 182     | NReference.Con (_,i) ->
 183        let _,_,tl,_,n = get_checked_indtys r in
 184        let _,_,_,cl = List.nth tl n in
 185        let res,_,_ = List.nth cl (i - 1) in
 186          res
 187     | NReference.Fix (fixno,_,_)
 188     | NReference.CoFix fixno ->
 189         let fl,_,_ = get_checked_fixes_or_cofixes r in
 190         let res,_,_,_,_ = List.nth fl fixno in
 191           res
 192 ;;
 193
 194
 195 let invalidate _ =
 196   assert (!frozen_list = []);
 197   NUri.UriHash.clear cache
 198 ;;