+and type_of_aux' metasenv context t ugraph =
+ 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
+ match t with
+ (* function *)
+ C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Decl t) -> S.lift n t,subst,metasenv, ugraph
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv, ugraph
+ | Some (_,C.Def (bo,None)) ->
+ type_of_aux subst metasenv context (S.lift n bo) ugraph
+ | None -> raise (RefineFailure "Rel to hidden hypothesis")
+ with
+ _ -> raise (RefineFailure "Not a close term")
+ )
+ | C.Var (uri,exp_named_subst) ->
+ let 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
+ ty,subst',metasenv',ugraph1
+ | C.Meta (n,l) ->
+ (try
+ let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in
+ let subst,metasenv,ugraph1 =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l ugraph
+ in
+ (* trust or check ??? *)
+ CicSubstitution.lift_meta l ty, subst, metasenv, ugraph1
+ (* type_of_aux subst metasenv
+ context (CicSubstitution.lift_meta l term) *)
+ with CicUtil.Subst_not_found _ ->
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+ let subst,metasenv, ugraph1 =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l ugraph
+ in
+ CicSubstitution.lift_meta l ty, subst, metasenv,ugraph1)
+ (* TASSI: CONSTRAINT *)
+ | C.Sort (C.Type t) ->
+ let t' = CicUniv.fresh() in
+ let ugraph1 = CicUniv.add_gt t' t ugraph in
+ (C.Sort (C.Type t')),subst,metasenv,ugraph1
+ (* TASSI: CONSTRAINT *)
+ | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
+ | C.Implicit _ -> raise (AssertFailure "21")
+ | C.Cast (te,ty) ->
+ let _,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph in
+ let inferredty,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' context te ugraph1
+ in
+ (try
+ let subst''',metasenv''',ugraph3 =
+ fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2
+ in
+ ty,subst''',metasenv''',ugraph3
+ with
+ _ -> raise (RefineFailure "Cast"))
+ | C.Prod (name,s,t) ->
+ let sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in
+ let sort2,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t ugraph1
+ in
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) ugraph2
+ | C.Lambda (n,s,t) ->
+ let sort1,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph
+ in
+ (match CicReduction.whd ~subst:subst' context sort1 with
+ C.Meta _
+ | C.Sort _ -> ()
+ | _ ->
+ raise (RefineFailure (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,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t ugraph1
+ in
+ C.Prod (n,s,type2),subst'',metasenv'',ugraph2
+ | C.LetIn (n,s,t) ->
+ (* only to check if s is well-typed *)
+ let ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph
+ in
+ let inferredty,subst'',metasenv'',ugraph2 =
+ type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
+ 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',ugraph2
+ | C.Appl (he::((_::_) as tl)) ->
+ let hetype,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context he ugraph
+ in
+ let tlbody_and_type,subst'',metasenv'',ugraph2 =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x, ty)::res,subst',metasenv',ugraph1
+ ) tl ([],subst',metasenv',ugraph1)
+ in
+ eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2
+ | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
+ | C.Const (uri,exp_named_subst) ->
+ let 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
+ cty,subst',metasenv',ugraph2
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let 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
+ cty,subst',metasenv',ugraph2
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let 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
+ 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 obj =
+ try
+ CicEnvironment.get_cooked_obj ~trust:true uri
+ with Not_found -> assert false
+ in
+ *)
+ let obj,u = CicEnvironment.get_obj uri ugraph in
+ match obj with
+ C.InductiveDefinition (l,expl_params,parsno) ->
+ List.nth l i , expl_params, parsno, u
+ | _ ->
+ 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,ugraph1 =
+ type_of_aux subst metasenv context term ugraph in
+ let _, 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 =
+ fo_unif_subst subst context metasenv expected_type actual_type ugraph2
+ in
+ (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+ let (_,outtypeinstances,subst,metasenv,ugraph4) =
+ List.fold_left
+ (fun (j,outtypeinstances,subst,metasenv,ugraph) p ->
+ 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 actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context p ugraph in
+ let expected_type, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context constructor ugraph1 in
+ let outtypeinstance,subst,metasenv,ugraph3 =
+ check_branch
+ 0 context metasenv subst
+ no_left_params actual_type constructor expected_type ugraph2 in
+ (j+1,outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
+ (1,[],subst,metasenv,ugraph3) pl 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 *)
+
+ (* easy case *)
+ let _, subst, metasenv,ugraph5 =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term])) ugraph4
+ in
+ let (subst,metasenv,ugraph6) =
+ List.fold_left
+ (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+ (*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv,ugraph1) =
+ type_of_aux subst metasenv context appl ugraph
+ in
+ *)
+ (* DEBUG
+ let prova1 = CicMetaSubst.whd subst context appl in
+ let prova2 = CicReduction.whd ~subst context appl in
+ if not (prova1 = prova2) then
+ begin
+ prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
+ prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
+ end;
+ *)
+ (* CicMetaSubst.whd subst context appl *)
+ CicReduction.whd ~subst context appl
+ in
+ fo_unif_subst subst context metasenv instance instance' ugraph)
+ (subst,metasenv,ugraph5) outtypeinstances in
+ CicReduction.whd ~subst
+ context (C.Appl(outtype::right_args@[term])),subst,metasenv,ugraph6
+ | C.Fix (i,fl) ->
+ let subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (fun (subst,metasenv,types,ugraph) (n,_,ty,_) ->
+ let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph
+ ) (subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv,ugraph2 =
+ List.fold_left
+ (fun (subst,metasenv,ugraph) (name,x,ty,bo) ->
+ let ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ) (subst,metasenv,ugraph1) fl in
+ let (_,_,ty,_) = List.nth fl i in
+ ty,subst,metasenv,ugraph2
+ | C.CoFix (i,fl) ->
+ let subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (fun (subst,metasenv,types,ugraph) (n,ty,_) ->
+ let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph1
+ ) (subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv,ugraph2 =
+ List.fold_left
+ (fun (subst,metasenv,ugraph) (name,ty,bo) ->
+ let ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ) (subst,metasenv,ugraph1) fl in
+
+ let (_,ty,_) = List.nth fl i in
+ ty,subst,metasenv,ugraph2
+
+ (* check_metasenv_consistency checks that the "canonical" context of a
+ metavariable is consitent - up to relocation via the relocation list l -
+ with the actual context *)
+ and check_metasenv_consistency
+ metano subst metasenv context canonical_context l ugraph
+ =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in