- (CicPp.ppterm sort1)))
- ) ;
- let type2,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
- in
- C.Prod (n,s,type2),subst'',metasenv''
- | C.LetIn (n,s,t) ->
- (* only to check if s is well-typed *)
- let ty,subst',metasenv' = type_of_aux subst metasenv context s in
- let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
- in
- (* One-step LetIn reduction. Even faster than the previous solution.
- Moreover the inferred type is closer to the expected one. *)
- CicSubstitution.subst s inferredty,subst',metasenv'
- | C.Appl (he::((_::_) as tl)) ->
- let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
- let tlbody_and_type,subst'',metasenv'' =
- List.fold_right
- (fun x (res,subst,metasenv) ->
- let ty,subst',metasenv' =
- type_of_aux subst metasenv context x
- in
- (x, ty)::res,subst',metasenv'
- ) tl ([],subst',metasenv')
- in
- eat_prods subst'' metasenv'' context hetype tlbody_and_type
- | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
- | C.Const (uri,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
- let cty =
- CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
- in
- cty,subst',metasenv'
- | C.MutInd (uri,i,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
- let cty =
- CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_defs uri i)
- in
- cty,subst',metasenv'
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let subst',metasenv' =
- check_exp_named_subst subst metasenv context exp_named_subst in
- let cty =
- CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_constr uri i j)
- in
- cty,subst',metasenv'
- | C.MutCase (uri, i, outtype, term, pl) ->
- (* first, get the inductive type (and noparams) in the environment *)
- let (_,b,arity,constructors), expl_params, no_left_params =
- let obj =
- try
- CicEnvironment.get_cooked_obj ~trust:true uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (l,expl_params,parsno) ->
- List.nth l i , expl_params, parsno
- | _ ->
- raise
- (RefineFailure
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
- let rec count_prod t =
- match CicReduction.whd ~subst context t with
- C.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0 in
- let no_args = count_prod arity in
- (* now, create a "generic" MutInd *)
- let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
- let metasenv,right_args =
- let no_right_params = no_args - no_left_params in
- if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
- let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv subst context expl_params in
- let expected_type =
- if no_args = 0 then
- C.MutInd (uri,i,exp_named_subst)
- else
- C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
- in
- (* check consistency with the actual type of term *)
- let actual_type,subst,metasenv =
- type_of_aux subst metasenv context term in
- let _, subst, metasenv =
- type_of_aux subst metasenv context expected_type
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv =
- fo_unif_subst subst context metasenv expected_type actual_type
- in
- (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
- let (_,outtypeinstances,subst,metasenv) =
- List.fold_left
- (fun (j,outtypeinstances,subst,metasenv) p ->
- let constructor =
- if left_args = [] then
- (C.MutConstruct (uri,i,j,exp_named_subst))
+ (CicPp.ppterm sort1)))
+ ) ;
+ let type2,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
+ in
+ C.Prod (n,s,type2),subst'',metasenv''
+ | C.LetIn (n,s,t) ->
+ (* only to check if s is well-typed *)
+ let ty,subst',metasenv' = type_of_aux subst metasenv context s in
+ let inferredty,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
+ in
+ (* One-step LetIn reduction. Even faster than the previous solution.
+ Moreover the inferred type is closer to the expected one. *)
+ CicSubstitution.subst s inferredty,subst',metasenv'
+ | C.Appl (he::((_::_) as tl)) ->
+ let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
+ let tlbody_and_type,subst'',metasenv'' =
+ List.fold_right
+ (fun x (res,subst,metasenv) ->
+ let ty,subst',metasenv' =
+ type_of_aux subst metasenv context x
+ in
+ (x, ty)::res,subst',metasenv'
+ ) tl ([],subst',metasenv')
+ in
+ eat_prods subst'' metasenv'' context hetype tlbody_and_type
+ | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
+ | C.Const (uri,exp_named_subst) ->
+ let subst',metasenv' =
+ check_exp_named_subst subst metasenv context exp_named_subst in
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+ in
+ cty,subst',metasenv'
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst',metasenv' =
+ check_exp_named_subst subst metasenv context exp_named_subst in
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_defs uri i)
+ in
+ cty,subst',metasenv'
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst',metasenv' =
+ check_exp_named_subst subst metasenv context exp_named_subst in
+ let cty =
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_constr uri i j)
+ in
+ cty,subst',metasenv'
+ | C.MutCase (uri, i, outtype, term, pl) ->
+ (* first, get the inductive type (and noparams) in the environment *)
+ let (_,b,arity,constructors), expl_params, no_left_params =
+ (*
+ let obj =
+ try
+ CicEnvironment.get_cooked_obj ~trust:true uri
+ with Not_found -> assert false
+ in
+ *)
+ match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (l,expl_params,parsno) ->
+ List.nth l i , expl_params, parsno
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
+ let rec count_prod t =
+ match CicReduction.whd ~subst context t with
+ C.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0 in
+ let no_args = count_prod arity in
+ (* now, create a "generic" MutInd *)
+ let metasenv,left_args =
+ CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
+ let metasenv,right_args =
+ let no_right_params = no_args - no_left_params in
+ if no_right_params < 0 then assert false
+ else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
+ let metasenv,exp_named_subst =
+ CicMkImplicit.fresh_subst metasenv subst context expl_params in
+ let expected_type =
+ if no_args = 0 then
+ C.MutInd (uri,i,exp_named_subst)