+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
exception NotImplemented;;
exception Impossible;;
exception NotWellTyped of string;;
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG",
+ CicPp.ppobj (C.Variable ("DEBUG", None,
C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
and type_of_variable uri =
let module C = Cic in
let module R = CicReduction in
+ let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
match CicCache.is_type_checked uri 0 with
- CicCache.CheckedObj (C.Variable (_,ty)) -> ty
- | CicCache.UncheckedObj (C.Variable (_,ty)) ->
+ CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty
+ | CicCache.UncheckedObj (C.Variable (_,bo,ty)) ->
(* only to check that ty is well-typed *)
let _ = type_of ty in
+ (match bo with
+ None -> ()
+ | Some bo ->
+ if not (R.are_convertible (type_of bo) ty) then
+ raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
+ ) ;
CicCache.set_type_checking_info uri ;
ty
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
| C.Lambda (_,so,dest) ->
does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+ | C.LetIn (_,so,dest) ->
+ does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n nn x) l true
| C.Const _
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
| C.Lambda _ -> raise Impossible (* due to type-checking *)
+ | C.LetIn _ -> raise NotImplemented
| C.Appl _ -> []
| C.Const _
| C.Abst _ -> raise Impossible
check_is_really_smaller_arg n nn kl x safes so &&
check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
(List.map (fun x -> x + 1) safes) ta
+ | C.LetIn (_,so,ta) ->
+ check_is_really_smaller_arg n nn kl x safes so &&
+ check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+ (List.map (fun x -> x + 1) safes) ta
| C.Appl (he::_) ->
(*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
(*CSC: solo perche' non abbiamo trovato controesempi *)
guarded_by_destructors n nn kl x safes so &&
guarded_by_destructors (n+1) (nn+1) kl (x+1)
(List.map (fun x -> x + 1) safes) ta
+ | C.LetIn (_,so,ta) ->
+ guarded_by_destructors n nn kl x safes so &&
+ guarded_by_destructors (n+1) (nn+1) kl (x+1)
+ (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
if not (List.length tl > k) then false
| C.Lambda (_,so,de) ->
does_not_occur n nn so &&
guarded_by_constructors (n + 1) (nn + 1) h de
+ | C.LetIn (_,so,de) ->
+ does_not_occur n nn so &&
+ guarded_by_constructors (n + 1) (nn + 1) h de
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h = 1 &&
List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
(* only to check if the product is well-typed *)
let _ = sort_of_prod (sort1,sort2) in
C.Prod (n,s,type2)
+ | C.LetIn (n,s,t) ->
+ let type1 = type_of_aux env s in
+ let type2 = type_of_aux (type1::env) t in
+ type2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype = type_of_aux env he
and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
debug (type_of te) [] ;
if not (R.are_convertible (type_of te) ty) then
raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
- | C.Variable (_,ty) ->
+ | C.Variable (_,bo,ty) ->
(* only to check that ty is well-typed *)
- (*CSC [] wrong *)
- let _ = type_of ty in ()
+ let _ = type_of ty in
+ (match bo with
+ None -> ()
+ | Some bo ->
+ if not (R.are_convertible (type_of bo) ty) then
+ raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
+ )
| C.InductiveDefinition _ ->
cooked_mutual_inductive_defs uri uobj
) ;
projects / helm.git / blobdiff