- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let lifted_canonical_context =
- let rec aux i =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,ty)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
- in
- aux 1 canonical_context
- in
- List.fold_left2
- (fun ugraph t ct ->
- match (t,ct) with
- | _,None -> ugraph
- | Some t,Some (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly expensive
- reduction that can be easily avoided and that is quite
- frequent. However, this is better handled using levels to
- control reduction *)
- let optimized_t =
- match t with
- Cic.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with
- Failure _ -> t)
- | _ -> t
- in
-(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
-else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
- let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context optimized_t ct ugraph
- in
- if not b then
- raise
- (TypeCheckerFailure
- (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))))
- else
- ugraph1
- | Some t,Some (_,C.Decl ct) ->
- let type_t,ugraph1 =
- type_of_aux' ~logger ~subst metasenv context t ugraph
- in
- let b,ugraph2 =
- R.are_convertible ~subst ~metasenv context type_t ct ugraph1
- in
- if not b then
- raise (TypeCheckerFailure
- (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
- (CicPp.ppterm ct) (CicPp.ppterm t)
- (CicPp.ppterm type_t))))
- else
- ugraph2
- | None, _ ->
- raise (TypeCheckerFailure
- (lazy ("Not well typed metavariable local context: "^
- "an hypothesis, that is not hidden, is not instantiated")))
- ) ugraph l lifted_canonical_context
-
-
-(*
- type_of_aux' is just another name (with a different scope)
- for type_of_aux
-*)
-
-and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
- let rec type_of_aux ~logger context t ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let module U = UriManager in
- match t with
- C.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Decl t) -> S.lift n t,ugraph
- | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
- | None -> raise
- (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
- with
- Failure _ ->
- raise (TypeCheckerFailure (lazy "unbound variable"))
- )
- | C.Var (uri,exp_named_subst) ->
- incr fdebug ;
- let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
- in
- let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
- let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
- decr fdebug ;
- ty1,ugraph2
- | 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))
- (* TASSI: CONSTRAINTS *)
- | C.Sort (C.Type t) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt t' t ugraph in
- (C.Sort (C.Type t')),ugraph1
- with
- CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
- | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
- | C.Cast (te,ty) as t ->
- let _,ugraph1 = type_of_aux ~logger context ty ugraph in
- let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
- let b,ugraph3 =
- R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
- in
- if b then
- ty,ugraph3
- else
- raise (TypeCheckerFailure
- (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t))))
- | C.Prod (name,s,t) ->
- let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
- let sort2,ugraph2 =
- type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1
- in
- sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
- | C.Lambda (n,s,t) ->
- let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
- (match R.whd ~subst context sort1 with
- C.Meta _
- | C.Sort _ -> ()
- | _ ->
- raise
- (TypeCheckerFailure (lazy (sprintf
- "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
- (CicPp.ppterm sort1))))
- ) ;
- let type2,ugraph2 =
- type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
- in
- (C.Prod (n,s,type2)),ugraph2
- | C.LetIn (n,s,ty,t) ->
- (* only to check if s is well-typed *)
- let ty',ugraph1 = type_of_aux ~logger context s ugraph in
- let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context ty ty' ugraph1
- in
- if not b then
- raise
- (TypeCheckerFailure
- (lazy (sprintf
- "The type of %s is %s but it is expected to be %s"
- (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
- else
- (* The type of a LetIn is a LetIn. Extremely slow since the computed
- LetIn is later reduced and maybe also re-checked.
- (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
- *)
- (* 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.
- (CicReduction.whd ~subst context
- (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
- *)
- (* One-step LetIn reduction. Even faster than the previous solution.
- Moreover the inferred type is closer to the expected one. *)
- let ty1,ugraph2 =
- type_of_aux ~logger
- ((Some (n,(C.Def (s,ty))))::context) t ugraph1
- in
- (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
- | 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)