]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nCicEnvironment.ml
removed spurious "
[helm.git] / 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
22 let type0 = []
23
24 let max l1 l2 =
25  HExtlib.list_uniq ~eq:(fun (b1,u1) (b2,u2) -> b1=b2 && NUri.eq u1 u2)
26   (List.sort (fun (b1,u1) (b2,u2) ->
27     let res = compare b1 b2 in if res = 0 then NUri.compare u1 u2 else res)
28       (l1 @ l2))
29
30 let le_constraints = ref [] (* strict,a,b *)
31
32 let rec le_path_uri avoid strict a b =
33  (not strict && NUri.eq a b) ||
34  List.exists
35   (fun (strict',x,y) ->
36      NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
37        le_path_uri (x::avoid) (strict && not strict') a x
38   ) !le_constraints
39 ;;
40
41 let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
42
43 let universe_leq a b = 
44   match a, b with
45   | a,[(false,b)] -> List.for_all (fun a -> leq_path a b) a
46   | _,_ ->
47      raise (BadConstraint
48       (lazy "trying to check if a universe is less or equal than an inferred universe"))
49
50 let universe_eq a b = 
51   match a,b with 
52   | [(false,_)], [(false,_)] -> universe_leq b a && universe_leq a b
53   | _, [(false,_)]
54   | [(false,_)],_ -> false
55   | _ ->
56      raise (BadConstraint
57       (lazy "trying to check if two inferred universes are equal"))
58 ;;
59
60 let pp_constraint b x y =  
61   NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y
62 ;;
63
64 let pp_constraints () =
65   String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
66 ;;
67
68 let universes = ref [];;
69
70 let add_constraint strict a b = 
71   match a,b with
72   | [false,a2],[false,b2] -> 
73       if not (le_path_uri [] strict a2 b2) then (
74         if le_path_uri [] (not strict) b2 a2 then
75          (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2
76            ^ " to:\n" ^ pp_constraints ()))));
77         universes := a2 :: b2 :: 
78           List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
79         le_constraints := (strict,a2,b2) :: !le_constraints)
80   | _ -> raise (BadConstraint
81           (lazy "trying to add a constraint on an inferred universe"))
82 ;;
83
84 let sup l =
85   match l with
86   | [false,_] -> Some l
87   | l ->
88    let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in
89    let solutions = List.fold_left bigger_than !universes l in
90    let rec aux = function
91      | [] -> None
92      | u :: tl ->
93          if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl
94          else Some [false,u]
95    in
96     aux solutions
97 ;;
98
99
100
101 let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
102 let set_typecheck_obj f =
103  if !already_set then
104   assert false
105  else
106   begin
107    typecheck_obj := f;
108    already_set := true
109   end
110 ;;
111
112 let cache = NUri.UriHash.create 313;;
113 let frozen_list = ref [];;
114
115 exception Propagate of NUri.uri * exn;;
116
117 let get_checked_obj u =
118  if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list
119  then
120   raise (CircularDependency (lazy (NUri.string_of_uri u)))
121  else
122   let obj =
123    try NUri.UriHash.find cache u
124    with
125     Not_found ->
126      let saved_frozen_list = !frozen_list in
127      try
128       let obj =
129        try NCicLibrary.get_obj u
130        with
131         NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
132       in
133         frozen_list := (u,obj)::saved_frozen_list;
134         !typecheck_obj obj;
135         frozen_list := saved_frozen_list;
136         let obj = `WellTyped obj in
137         NUri.UriHash.add cache u obj;
138         obj
139      with
140         Sys.Break as e ->
141          frozen_list := saved_frozen_list;
142          raise e
143       | Propagate (u',old_exn) as e' ->
144          frozen_list := saved_frozen_list;
145          let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^
146            " depends (recursively) on " ^ NUri.string_of_uri u' ^
147            " which is not well-typed"), 
148            match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
149          NUri.UriHash.add cache u exn;
150          if saved_frozen_list = [] then
151           exn
152          else
153           raise e'
154       | e ->
155          frozen_list := saved_frozen_list;
156          let exn = `Exn e in
157          NUri.UriHash.add cache u exn;
158          if saved_frozen_list = [] then
159           exn
160          else
161           raise (Propagate (u,e))
162   in
163    match obj with
164       `WellTyped o -> o
165     | `Exn e -> raise e
166 ;;
167
168 let get_checked_decl = function
169   | Ref.Ref (uri, Ref.Decl) ->
170       (match get_checked_obj uri with
171       | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
172           rlv,name,ty,att,height
173       | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
174           prerr_endline "get_checked_decl on a definition"; assert false
175       | _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
176   | _ -> prerr_endline "get_checked_decl on a non decl"; assert false
177 ;;
178
179 let get_checked_def = function
180   | Ref.Ref (uri, Ref.Def _) ->
181       (match get_checked_obj uri with
182       | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
183           rlv,name,bo,ty,att,height
184       | _,_,_,_, C.Constant (_,_,None,_,_) ->
185           prerr_endline "get_checked_def on an axiom"; assert false
186       | _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
187   | _ -> prerr_endline "get_checked_def on a non def"; assert false
188 ;;
189
190 let get_checked_indtys = function
191   | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
192       (match get_checked_obj uri with
193       | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
194         inductive,leftno,tys,att,n
195       | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
196   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
197 ;;
198
199 let get_checked_fixes_or_cofixes = function
200   | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
201       (match get_checked_obj uri with
202       | _,height,_,_, C.Fixpoint (_,funcs,att) ->
203          funcs, att, height
204       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
205   | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
206 ;;
207
208 let get_relevance (Ref.Ref (_, infos) as r) =
209   match infos with
210      Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
211    | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
212    | Ref.Ind _ ->
213        let _,_,tl,_,n = get_checked_indtys r in
214        let res,_,_,_ = List.nth tl n in
215          res
216     | Ref.Con (_,i,_) ->
217        let _,_,tl,_,n = get_checked_indtys r in
218        let _,_,_,cl = List.nth tl n in
219        let res,_,_ = List.nth cl (i - 1) in
220          res
221     | Ref.Fix (fixno,_,_)
222     | Ref.CoFix fixno ->
223         let fl,_,_ = get_checked_fixes_or_cofixes r in
224         let res,_,_,_,_ = List.nth fl fixno in
225           res
226 ;;
227
228
229 let invalidate _ = 
230   assert (!frozen_list = []);
231   NUri.UriHash.clear cache
232 ;;