(NCicPp.ppterm t1) (NCicPp.ppterm t2))))
;;
+let eat_prods ~subst ~metasenv context ty_he args_with_ty =
+ let rec aux ty_he = function
+ | [] -> ty_he
+ | (arg, ty_arg)::tl ->
+ (match R.whd ~subst context ty_he with
+ | C.Prod (n,s,t) ->
+ if R.are_convertible ~subst ~metasenv context ty_arg s then
+ aux (S.subst ~avoid_beta_redexes:true arg t) tl
+ else
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Appl: wrong parameter-type, expected %s, found %s")
+ (NCicPp.ppterm ty_arg) (NCicPp.ppterm s))))
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy "Appl: this is not a function, it cannot be applied")))
+ in
+ aux ty_he args_with_ty
+;;
+
let typeof ~subst ~metasenv context term =
- let rec aux context = function
+ let rec typeof_aux context = function
| C.Rel n ->
(try
match List.nth context (n - 1) with
| 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
+ let sort1 = typeof_aux context s in
+ let sort2 = typeof_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
+ let sort1 = typeof_aux context s in
(match R.whd ~subst context sort1 with
| C.Meta _ | C.Sort _ -> ()
| _ ->
"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
+ typeof_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
+ let ty_t = typeof_aux context t in
if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
raise
(TypeCheckerFailure
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
+ let ty_bo = typeof_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
+ | C.Appl (he::(_::_ as args)) ->
+ let ty_he = typeof_aux context he in
+ let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
+ eat_prods ~subst ~metasenv context ty_he args_with_ty
+ | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
+ | C.Meta (n,l) ->
+ (try
+ let _,canonical_context,term,ty = NCicUtils.lookup_subst n subst in
+ check_metasenv_consistency context canonical_context l;
+ (* assuming subst is well typed !!!!! *)
+ S.subst_meta l ty
+ with NCicUtils.Subst_not_found _ ->
+ let _,_,canonical_context,ty = NCicUtils.lookup_meta n metasenv in
+ check_metasenv_consistency context canonical_context l;
+ S.subst_meta l ty)
+ | C.Match (r,outtype,term,pl) ->
+ let outsort = typeof_aux context outtype in
+assert false (* FINQUI
let (need_dummy, k) =
let rec guess_args context t =
- let outtype = CicReduction.whd ~subst context t in
+ let outtype = R.whd ~subst context t in
match outtype with
C.Sort _ -> (true, 0)
| C.Prod (name, s, t) ->
else CicReduction.head_beta_reduce (C.Appl arguments')
in
outtype,ugraph5
+ *)
+ and check_metasenv_consistency context canonical_context l =
+ let lifted_canonical_context =
+ let rec lift_metas i = function
+ | [] -> []
+ | (n,C.Decl t)::tl ->
+ (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
+ | (n,C.Def (t,ty))::tl ->
+ (n,C.Def ((S.subst_meta l (S.lift i t)),
+ S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
+ in
+ lift_metas 1 canonical_context
+ in
+ (* we could optimize when l is an NCic.Irl *)
+ let l =
+ let shift, lc_kind = l in
+ List.map (S.lift shift) (NCicUtils.expand_local_context lc_kind)
+ in
+ List.iter2
+ (fun t ct ->
+ match (t,ct) with
+ | t, (_,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
+ | C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ | (_,C.Def (te,_)) -> S.lift n te
+ | _ -> t
+ with Failure _ -> t)
+ | _ -> t
+ in
+ if not (R.are_convertible ~subst ~metasenv context optimized_t ct)then
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context: " ^^
+ "expected a term convertible with %s, found %s")
+ (NCicPp.ppterm ct) (NCicPp.ppterm t))))
+ | t, (_,C.Decl ct) ->
+ let type_t = typeof_aux context t in
+ if not (R.are_convertible ~subst ~metasenv context type_t ct) then
+ raise (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context: "^^
+ "expected a term of type %s, found %s of type %s")
+ (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+ ) l lifted_canonical_context
+ in
+ typeof_aux context term
+(*
+ | 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.Fix (i,fl) ->
let types,kl,ugraph1,len =
List.fold_left
projects / helm.git / commitdiff