- let rec type_of_aux subst metasenv context t ugraph =
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
- let (t',_,_,_,_) as res =
- match t with
- (* function *)
- C.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Decl ty) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,ty)) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | None ->
- enrich localization_tbl t
- (RefineFailure (lazy "Rel to hidden hypothesis"))
- with
- Failure _ ->
- enrich localization_tbl t
- (RefineFailure (lazy "Not a closed term")))
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst
- subst metasenv context exp_named_subst ugraph
- in
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let ty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
- | C.Meta (n,l) ->
- (try
- let (canonical_context, term,ty) =
- CicUtil.lookup_subst n subst
- in
- let l',subst',metasenv',ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- (* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv', ugraph1
- (* type_of_aux subst metasenv
- context (CicSubstitution.subst_meta l term) *)
- with CicUtil.Subst_not_found _ ->
- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let l',subst',metasenv', ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv',ugraph1)
- | C.Sort (C.Type tno) ->
- let tno' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | C.Sort (C.CProp tno) ->
- let tno' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | C.Sort (C.Prop|C.Set) ->
- t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
- | C.Implicit infos ->
- let metasenv',t' = exp_impl metasenv subst context infos in
- type_of_aux subst metasenv' context t' ugraph
- | C.Cast (te,ty) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- let te',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' context te ugraph1
- in
- let (te', ty'), subst''',metasenv''',ugraph3 =
- coerce_to_something true localization_tbl te' inferredty ty'
- subst'' metasenv'' context ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- | C.Prod (name,s,t) ->
- let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let s',sort1,subst', metasenv',ugraph1 =
- coerce_to_sort localization_tbl
- s' sort1 subst' context metasenv' ugraph1
- in
- let context_for_t = ((Some (name,(C.Decl s')))::context) in
- let t',sort2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- let t',sort2,subst'',metasenv'',ugraph2 =
- coerce_to_sort localization_tbl
- t' sort2 subst'' context_for_t metasenv'' ugraph2
- in
- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod localization_tbl subst'' metasenv''
- context (name,s') t' (sort1,sort2) ugraph2
- in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
- | C.Lambda (n,s,t) ->
- let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let s',sort1,subst',metasenv',ugraph1 =
- coerce_to_sort localization_tbl
- s' sort1 subst' context metasenv' ugraph1
- in
- let context_for_t = ((Some (n,(C.Decl s')))::context) in
- let t',type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' context_for_t t ugraph1
- in
- C.Lambda (n,s',t'),C.Prod (n,s',type2),
- subst'',metasenv'',ugraph2
- | C.LetIn (n,s,ty,t) ->
- (* only to check if s is well-typed *)
- let s',ty',subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
- let ty,_,subst',metasenv',ugraph1 =
- type_of_aux subst' metasenv' context ty ugraph1 in
- let subst',metasenv',ugraph1 =
- try
- fo_unif_subst subst' context metasenv'
- ty ty' ugraph1
- with
- exn ->
- enrich localization_tbl s' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
- context))
- in
- let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
-
- let t',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- (* One-step LetIn reduction.
- * Even faster than the previous solution.
- * Moreover the inferred type is closer to the expected one.
- *)
- C.LetIn (n,s',ty,t'),
- CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
- subst'',metasenv'',ugraph2
- | C.Appl (he::((_::_) as tl)) ->
- let he',hetype,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context he ugraph
- in
- let tlbody_and_type,subst'',metasenv'',ugraph2 =
- typeof_list subst' metasenv' context ugraph1 tl
- in
- let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
- eat_prods true subst'' metasenv'' context
- he' hetype tlbody_and_type ugraph2
- in
- let newappl = (C.Appl (coerced_he::coerced_args)) in
- avoid_double_coercion
- context subst''' metasenv''' ugraph3 newappl applty
- | C.Appl _ -> assert false
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph in
- let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutInd (uri,i,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri in
- C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 =
- type_of_mutual_inductive_constr uri i j ugraph1
- in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
- metasenv',ugraph2
- | 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,ugraph =
- let _ = CicTypeChecker.typecheck uri in
- let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
- match obj with
- C.InductiveDefinition (l,expl_params,parsno,_) ->
- List.nth l i , expl_params, parsno, u
- | _ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("Unkown mutual inductive definition " ^
- U.string_of_uri uri)))
- in
- if List.length constructors <> List.length pl then
- enrich localization_tbl t
- (RefineFailure
- (lazy "Wrong number of cases")) ;
- 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 term',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context term ugraph in
- let expected_type',_, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context expected_type ugraph1
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv,ugraph3 =
- try
- fo_unif_subst subst context metasenv
- expected_type' actual_type ugraph2
- with
- exn ->
- enrich localization_tbl term' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst term'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
- context))
- in
- let rec instantiate_prod t =
- function
- [] -> t
- | he::tl ->
- match CicReduction.whd ~subst context t with
- C.Prod (_,_,t') ->
- instantiate_prod (CicSubstitution.subst he t') tl
- | _ -> assert false
- in
- let arity_instantiated_with_left_args =
- instantiate_prod arity left_args in
- (* TODO: check if the sort elimination
- * is allowed: [(I q1 ... qr)|B] *)
- let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- List.fold_right
- (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
- let constructor =
- if left_args = [] then
- (C.MutConstruct (uri,i,j,exp_named_subst))
- else
- (C.Appl
- (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
- in
- let p',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context p ugraph
- in
- let constructor',expected_type, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context constructor ugraph1
- in
- let outtypeinstance,subst,metasenv,ugraph3 =
- try
- check_branch 0 context metasenv subst
- no_left_params actual_type constructor' expected_type
- ugraph2
- with
- exn ->
- enrich localization_tbl constructor'
- ~f:(fun _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context metasenv subst p'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context metasenv subst actual_type
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context metasenv subst expected_type
- context)) exn
- in
- (p'::pl,j-1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- pl ([],List.length pl,[],subst,metasenv,ugraph3)
- in
-
- (* we are left to check that the outype matches his instances.
- The easy case is when the outype is specified, that amount
- to a trivial check. Otherwise, we should guess a type from
- its instances
- *)
-
- let outtype,outtypety, subst, metasenv,ugraph4 =
- type_of_aux subst metasenv context outtype ugraph4 in
- (match outtype with
- | C.Meta (n,l) ->
- (let candidate,ugraph5,metasenv,subst =
- let exp_name_subst, metasenv =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
- in
- let uris = CicUtil.params_of_obj o in
- List.fold_right (
- fun uri (acc,metasenv) ->
- let metasenv',new_meta =
- CicMkImplicit.mk_implicit metasenv subst context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- context
- in
- (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
- ) uris ([],metasenv)
- in
- let ty =
- match left_args,right_args with
- [],[] -> Cic.MutInd(uri, i, exp_name_subst)
- | _,_ ->
- let rec mk_right_args =
- function
- 0 -> []
- | n -> (Cic.Rel n)::(mk_right_args (n - 1))
- in
- let right_args_no = List.length right_args in
- let lifted_left_args =
- List.map (CicSubstitution.lift right_args_no) left_args
- in
- Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
- (lifted_left_args @ mk_right_args right_args_no))
- in
- let fresh_name =
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- context Cic.Anonymous ~typ:ty
- in
- match outtypeinstances with
- | [] ->
- let extended_context =
- let rec add_right_args =
- function
- Cic.Prod (name,ty,t) ->
- Some (name,Cic.Decl ty)::(add_right_args t)
- | _ -> []
- in
- (Some (fresh_name,Cic.Decl ty))::
- (List.rev
- (add_right_args arity_instantiated_with_left_args))@
- context
- in
- let metasenv,new_meta =
- CicMkImplicit.mk_implicit metasenv subst extended_context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- extended_context
- in
- let rec add_lambdas b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas b t))
- | _ -> Cic.Lambda (fresh_name, ty, b)
- in
- let candidate =
- add_lambdas (Cic.Meta (new_meta,irl))
- arity_instantiated_with_left_args
- in
- (Some candidate),ugraph4,metasenv,subst
- | (constructor_args_no,_,instance,_)::tl ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let candidate,ugraph,metasenv,subst =
- List.fold_left (
- fun (candidate_oty,ugraph,metasenv,subst)
- (constructor_args_no,_,instance,_) ->
- match candidate_oty with
- | None -> None,ugraph,metasenv,subst
- | Some ty ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv
- instance' ty ugraph
- in
- candidate_oty,ugraph,metasenv,subst
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | RefineFailure _ | Uncertain _ ->
- None,ugraph,metasenv,subst
- ) (Some instance',ugraph4,metasenv,subst) tl
- in
- match candidate with
- | None -> None, ugraph,metasenv,subst
- | Some t ->
- let rec add_lambdas n b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
- | _ ->
- Cic.Lambda (fresh_name, ty,
- CicSubstitution.lift (n + 1) t)
- in
- Some
- (add_lambdas 0 t arity_instantiated_with_left_args),
- ugraph,metasenv,subst
- with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- None,ugraph4,metasenv,subst
- in
- match candidate with
- | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
- | Some candidate ->
- let subst,metasenv,ugraph =
- try
- fo_unif_subst subst context metasenv
- candidate outtype ugraph5
- with
- exn -> assert false(* unification against a metavariable *)
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (Cic.Appl (outtype::right_args@[term']))),
- subst,metasenv,ugraph)
- | _ -> (* easy case *)
- let tlbody_and_type,subst,metasenv,ugraph4 =
- typeof_list subst metasenv context ugraph4 (right_args @ [term'])
- in
- let _,_,_,subst,metasenv,ugraph4 =
- eat_prods false subst metasenv context
- outtype outtypety tlbody_and_type ugraph4
- in
- let _,_, subst, metasenv,ugraph5 =
- type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
- in
- let (subst,metasenv,ugraph6) =
- List.fold_left2
- (fun (subst,metasenv,ugraph)
- p (constructor_args_no,context,instance,args)
- ->
- let instance' =
- let appl =
- let outtype' =
- CicSubstitution.lift constructor_args_no outtype
- in
- C.Appl (outtype'::args)
- in
- CicReduction.head_beta_reduce ~delta:false
- ~upto:(List.length args) appl
- in
- try
- fo_unif_subst subst context metasenv instance instance'
- ugraph
- with
- exn ->
- enrich localization_tbl p exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst p
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance
- context)))
- (subst,metasenv,ugraph5) pl' outtypeinstances
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (C.Appl(outtype::right_args@[term']))),
- subst,metasenv,ugraph6)
- | C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
- :: types, ugraph, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context'))
- in
- fl @ [bo'] , subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.Fix (i,fl''),ty,subst,metasenv,ugraph2
- | C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
- types, ugraph1, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context))
- in
- fl @ [bo'],subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.CoFix (i,fl''),ty,subst,metasenv,ugraph2