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