*)
+module C = NCic
+module R = NCicReduction
+module S = NCicSubstitution
+module U = NCicUtils
+
+
+let sort_of_prod ~subst context (name,s) (t1, t2) =
+ let t1 = R.whd ~subst context t1 in
+ let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
+ match t1, t2 with
+ | C.Sort s1, C.Sort s2
+ (* different from Coq manual, Impredicative Set! *)
+ when (s2 = C.Prop || s2 = C.Set || s2 = C.CProp) -> C.Sort s2
+ | C.Sort (C.Type t1), C.Sort (C.Type t2) -> C.Sort (C.Type (max t1 t2))
+ | C.Sort _,C.Sort (C.Type t1) -> C.Sort (C.Type t1)
+ | C.Meta _, C.Sort _ -> t2
+ | C.Meta _, ((C.Meta _) as t)
+ | C.Sort _, ((C.Meta _) as t) when U.is_closed t -> t2
+ | _ ->
+ raise (TypeCheckerFailure (lazy (Printf.sprintf
+ "Prod: expected two sorts, found = %s, %s"
+ (NCicPp.ppterm t1) (NCicPp.ppterm t2))))
+;;
+
+
+let typeof ~subst ~metasenv context term =
+ let rec aux context = function
+ | C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ | (_,C.Decl ty) -> S.lift n ty
+ | (_,C.Def (_,ty)) -> S.lift n ty
+ with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")))
+ | C.Sort (C.Type i) -> C.Sort (C.Type (i+1))
+ | C.Sort s -> C.Sort (C.Type 0)
+ | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
+ | C.Prod (name,s,t) ->
+ let sort1 = aux context s in
+ let sort2 = aux ((name,(C.Decl s))::context) t in
+ sort_of_prod ~subst context (name,s) (sort1,sort2)
+ | C.Lambda (n,s,t) ->
+ let sort1 = aux context s in
+ (match R.whd ~subst context sort1 with
+ | C.Meta _ | C.Sort _ -> ()
+ | _ ->
+ raise
+ (TypeCheckerFailure (lazy (Printf.sprintf
+ ("Not well-typed lambda-abstraction: " ^^
+ "the source %s should be a type; instead it is a term " ^^
+ "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort1)))));
+ let type2 =
+ aux ((n,(C.Decl s))::context) t
+ in
+ C.Prod (n,s,type2)
+ | C.LetIn (n,ty,t,bo) ->
+ let ty_t = aux context t in
+ if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ "The type of %s is %s but it is expected to be %s"
+ (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty))))
+ else
+ (* Alternatives:
+ 1) The type of a LetIn is a LetIn, extremely slow since the computed
+ LetIn may be later reduced.
+ 2) The type of the LetIn is reduced, much faster than the previous
+ solution, moreover the inferred type is probably very different
+ from the expected one.
+ 3) One-step LetIn reduction, even faster than the previous solution,
+ moreover the inferred type is closer to the expected one. *)
+ let ty_bo = aux ((n,C.Def (t,ty))::context) bo in
+ S.subst ~avoid_beta_redexes:true t ty_bo
+ in
+ aux context term
+(*
+ | C.Meta (n,l) ->
+ (try
+ let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+ let ugraph1 =
+ check_metasenv_consistency ~logger
+ ~subst metasenv context canonical_context l ugraph
+ in
+ (* assuming subst is well typed !!!!! *)
+ ((CicSubstitution.subst_meta l ty), ugraph1)
+ (* type_of_aux context (CicSubstitution.subst_meta l term) *)
+ with CicUtil.Subst_not_found _ ->
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+ let ugraph1 =
+ check_metasenv_consistency ~logger
+ ~subst metasenv context canonical_context l ugraph
+ in
+ ((CicSubstitution.subst_meta l ty),ugraph1))
+ | C.Appl (he::tl) when List.length tl > 0 ->
+ let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
+ let tlbody_and_type,ugraph2 =
+ List.fold_right (
+ fun x (l,ugraph) ->
+ let ty,ugraph1 = type_of_aux ~logger context x ugraph in
+ (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*)
+ ((x,ty)::l,ugraph1))
+ tl ([],ugraph1)
+ in
+ (* TASSI: questa c'era nel mio... ma non nel CVS... *)
+ (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
+ eat_prods ~subst context hetype tlbody_and_type ugraph2
+ | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments"))
+ | C.Const (uri,exp_named_subst) ->
+ incr fdebug ;
+ let ugraph1 =
+ check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ in
+ let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
+ let cty1 =
+ CicSubstitution.subst_vars exp_named_subst cty
+ in
+ decr fdebug ;
+ cty1,ugraph2
+ | C.MutInd (uri,i,exp_named_subst) ->
+ incr fdebug ;
+ let ugraph1 =
+ check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ in
+ (* TASSI: da me c'era anche questa, ma in CVS no *)
+ let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
+ (* fine parte dubbia *)
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst mty
+ in
+ decr fdebug ;
+ cty,ugraph2
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let ugraph1 =
+ check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
+ in
+ (* TASSI: idem come sopra *)
+ let mty,ugraph2 =
+ type_of_mutual_inductive_constr ~logger uri i j ugraph1
+ in
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst mty
+ in
+ cty,ugraph2
+ | C.MutCase (uri,i,outtype,term,pl) ->
+ let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
+ let (need_dummy, k) =
+ let rec guess_args context t =
+ let outtype = CicReduction.whd ~subst context t in
+ match outtype with
+ C.Sort _ -> (true, 0)
+ | C.Prod (name, s, t) ->
+ let (b, n) =
+ guess_args ((Some (name,(C.Decl s)))::context) t in
+ if n = 0 then
+ (* last prod before sort *)
+ match CicReduction.whd ~subst context s with
+(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
+ C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
+ (false, 1)
+(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
+ | C.Appl ((C.MutInd (uri',i',_)) :: _)
+ when U.eq uri' uri && i' = i -> (false, 1)
+ | _ -> (true, 1)
+ else
+ (b, n + 1)
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ "Malformed case analasys' output type %s"
+ (CicPp.ppterm outtype))))
+ in
+(*
+ let (parameters, arguments, exp_named_subst),ugraph2 =
+ let ty,ugraph2 = type_of_aux context term ugraph1 in
+ match R.whd ~subst context ty with
+ (*CSC manca il caso dei CAST *)
+(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
+(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
+(*CSC: Hint: nella DTD servono per gli stylesheet. *)
+ C.MutInd (uri',i',exp_named_subst) as typ ->
+ if U.eq uri uri' && i = i' then
+ ([],[],exp_named_subst),ugraph2
+ else
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
+ (CicPp.ppterm typ) (U.string_of_uri uri) i)))
+ | C.Appl
+ ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+ if U.eq uri uri' && i = i' then
+ let params,args =
+ split tl (List.length tl - k)
+ in (params,args,exp_named_subst),ugraph2
+ else
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ ("Case analysys: analysed term type is %s, "^
+ "but is expected to be (an application of) "^
+ "%s#1/%d{_}")
+ (CicPp.ppterm typ') (U.string_of_uri uri) i)))
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ ("Case analysis: "^
+ "analysed term %s is not an inductive one")
+ (CicPp.ppterm term))))
+*)
+ let (b, k) = guess_args context outsort in
+ if not b then (b, k - 1) else (b, k) in
+ let (parameters, arguments, exp_named_subst),ugraph2 =
+ let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
+ match R.whd ~subst context ty with
+ C.MutInd (uri',i',exp_named_subst) as typ ->
+ if U.eq uri uri' && i = i' then
+ ([],[],exp_named_subst),ugraph2
+ else raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+ (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
+ | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
+ if U.eq uri uri' && i = i' then
+ let params,args =
+ split tl (List.length tl - k)
+ in (params,args,exp_named_subst),ugraph2
+ else raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+ (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy (sprintf
+ "Case analysis: analysed term %s is not an inductive one"
+ (CicPp.ppterm term))))
+ in
+ (*
+ let's control if the sort elimination is allowed:
+ [(I q1 ... qr)|B]
+ *)
+ let sort_of_ind_type =
+ if parameters = [] then
+ C.MutInd (uri,i,exp_named_subst)
+ else
+ C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
+ in
+ let type_of_sort_of_ind_ty,ugraph3 =
+ type_of_aux ~logger context sort_of_ind_type ugraph2 in
+ let b,ugraph4 =
+ check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+ need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
+ in
+ if not b then
+ raise
+ (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
+ (* let's check if the type of branches are right *)
+ let parsno,constructorsno =
+ let obj,_ =
+ try
+ CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.InductiveDefinition (il,_,parsno,_) ->
+ let _,_,_,cl =
+ try List.nth il i with Failure _ -> assert false
+ in
+ parsno, List.length cl
+ | _ ->
+ raise (TypeCheckerFailure
+ (lazy ("Unknown mutual inductive definition:" ^
+ UriManager.string_of_uri uri)))
+ in
+ if List.length pl <> constructorsno then
+ raise (TypeCheckerFailure
+ (lazy ("Wrong number of cases in case analysis"))) ;
+ let (_,branches_ok,ugraph5) =
+ List.fold_left
+ (fun (j,b,ugraph) p ->
+ if b then
+ let cons =
+ if parameters = [] then
+ (C.MutConstruct (uri,i,j,exp_named_subst))
+ else
+ (C.Appl
+ (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
+ in
+ let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
+ let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
+ (* 2 is skipped *)
+ let ty_branch =
+ type_of_branch ~subst context parsno need_dummy outtype cons
+ ty_cons in
+ let b1,ugraph4 =
+ R.are_convertible
+ ~subst ~metasenv context ty_p ty_branch ugraph3
+ in
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
+ if not b1 then
+ debug_print (lazy
+ ("#### " ^ CicPp.ppterm ty_p ^
+ " <==> " ^ CicPp.ppterm ty_branch));
+ (j + 1,b1,ugraph4)
+ else
+ (j,false,ugraph)
+ ) (1,true,ugraph4) pl
+ in
+ if not branches_ok then
+ raise
+ (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
+ let arguments' =
+ if not need_dummy then outtype::arguments@[term]
+ else outtype::arguments in
+ let outtype =
+ if need_dummy && arguments = [] then outtype
+ else CicReduction.head_beta_reduce (C.Appl arguments')
+ in
+ outtype,ugraph5
+ | C.Fix (i,fl) ->
+ let types,kl,ugraph1,len =
+ List.fold_left
+ (fun (types,kl,ugraph,len) (n,k,ty,_) ->
+ let _,ugraph1 = type_of_aux ~logger context ty ugraph in
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ k::kl,ugraph1,len+1)
+ ) ([],[],ugraph,0) fl
+ in
+ let ugraph2 =
+ List.fold_left
+ (fun ugraph (name,x,ty,bo) ->
+ let ty_bo,ugraph1 =
+ type_of_aux ~logger (types@context) bo ugraph
+ in
+ let b,ugraph2 =
+ R.are_convertible ~subst ~metasenv (types@context)
+ ty_bo (CicSubstitution.lift len ty) ugraph1 in
+ if b then
+ begin
+ let (m, eaten, context') =
+ eat_lambdas ~subst (types @ context) (x + 1) bo
+ in
+ (*
+ let's control the guarded by
+ destructors conditions D{f,k,x,M}
+ *)
+ if not (guarded_by_destructors ~subst context' eaten
+ (len + eaten) kl 1 [] m) then
+ raise
+ (TypeCheckerFailure
+ (lazy ("Fix: not guarded by destructors")))
+ else
+ ugraph2
+ end
+ else
+ raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
+ ) ugraph1 fl in
+ (*CSC: controlli mancanti solo su D{f,k,x,M} *)
+ let (_,_,ty,_) = List.nth fl i in
+ ty,ugraph2
+ | C.CoFix (i,fl) ->
+ let types,ugraph1,len =
+ List.fold_left
+ (fun (l,ugraph,len) (n,ty,_) ->
+ let _,ugraph1 =
+ type_of_aux ~logger context ty ugraph in
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+ ugraph1,len+1)
+ ) ([],ugraph,0) fl
+ in
+ let ugraph2 =
+ List.fold_left
+ (fun ugraph (_,ty,bo) ->
+ let ty_bo,ugraph1 =
+ type_of_aux ~logger (types @ context) bo ugraph
+ in
+ let b,ugraph2 =
+ R.are_convertible ~subst ~metasenv (types @ context) ty_bo
+ (CicSubstitution.lift len ty) ugraph1
+ in
+ if b then
+ begin
+ (* let's control that the returned type is coinductive *)
+ match returns_a_coinductive ~subst context ty with
+ None ->
+ raise
+ (TypeCheckerFailure
+ (lazy "CoFix: does not return a coinductive type"))
+ | Some uri ->
+ (*
+ let's control the guarded by constructors
+ conditions C{f,M}
+ *)
+ if not (guarded_by_constructors ~subst
+ (types @ context) 0 len false bo [] uri) then
+ raise
+ (TypeCheckerFailure
+ (lazy "CoFix: not guarded by constructors"))
+ else
+ ugraph2
+ end
+ else
+ raise
+ (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
+ ) ugraph1 fl
+ in
+ let (_,ty,_) = List.nth fl i in
+ ty,ugraph2
+
+*)
+;;
+
(* typechecks the object, raising an exception if illtyped *)
let typecheck_obj obj = match obj with _ -> ()
projects / helm.git / commitdiff