+let type_of_aux' ?localization_tbl metasenv context term ugraph =
+ try
+ type_of_aux' ?localization_tbl metasenv context term ugraph
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
+
+let undebrujin uri typesno tys t =
+ snd
+ (List.fold_right
+ (fun (name,_,_,_) (i,t) ->
+ (* here the explicit_named_substituion is assumed to be *)
+ (* of length 0 *)
+ let t' = Cic.MutInd (uri,i,[]) in
+ let t = CicSubstitution.subst t' t in
+ i - 1,t
+ ) tys (typesno - 1,t))
+
+let map_first_n n start f g l =
+ let rec aux acc k l =
+ if k < n then
+ match l with
+ | [] -> raise (Invalid_argument "map_first_n")
+ | hd :: tl -> f hd k (aux acc (k+1) tl)
+ else
+ g acc l
+ in
+ aux start 0 l
+
+(*CSC: this is a very rough approximation; to be finished *)
+let are_all_occurrences_positive metasenv ugraph uri tys leftno =
+ let subst,metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
+ let subst,metasenv,ugraph,cl =
+ List.fold_right
+ (fun (name,ty) (subst,metasenv,ugraph,acc) ->
+ let rec aux ctx k subst = function
+ | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
+ let subst,metasenv,ugraph,tl =
+ map_first_n leftno
+ (subst,metasenv,ugraph,[])
+ (fun t n (subst,metasenv,ugraph,acc) ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst
+ subst ctx metasenv t (Cic.Rel (k-n)) ugraph
+ in
+ subst,metasenv,ugraph,(t::acc))
+ (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
+ tl
+ in
+ subst,metasenv,ugraph,(Cic.Appl (hd::tl))
+ | Cic.MutInd(uri',_,_) as t when uri = uri'->
+ subst,metasenv,ugraph,t
+ | Cic.Prod (name,s,t) ->
+ let ctx = (Some (name,Cic.Decl s))::ctx in
+ let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
+ subst,metasenv,ugraph,Cic.Prod (name,s,t)
+ | _ ->
+ raise
+ (RefineFailure
+ (lazy "not well formed constructor type"))
+ in
+ let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
+ subst,metasenv,ugraph,(name,ty) :: acc)
+ cl (subst,metasenv,ugraph,[])
+ in
+ subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
+ tys ([],metasenv,ugraph,[])
+ in
+ let substituted_tys =
+ List.map
+ (fun (name,ind,arity,cl) ->
+ let cl =
+ List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
+ in
+ name,ind,CicMetaSubst.apply_subst subst arity,cl)
+ tys
+ in
+ metasenv,ugraph,substituted_tys
+
+let typecheck metasenv uri obj ~localization_tbl =
+ let ugraph = CicUniv.empty_ugraph in
+ match obj with
+ Cic.Constant (name,Some bo,ty,args,attrs) ->
+ let bo',boty,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] bo ugraph in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph in
+ let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+ let bo' = CicMetaSubst.apply_subst subst bo' in
+ let ty' = CicMetaSubst.apply_subst subst ty' in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
+ | Cic.Constant (name,None,ty,args,attrs) ->
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph
+ in
+ Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
+ assert (metasenv' = metasenv);
+ (* Here we do not check the metasenv for correctness *)
+ let bo',boty,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] bo ugraph in
+ let ty',sort,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph in
+ begin
+ match sort with
+ Cic.Sort _
+ (* instead of raising Uncertain, let's hope that the meta will become
+ a sort *)
+ | Cic.Meta _ -> ()
+ | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
+ end;
+ let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+ let bo' = CicMetaSubst.apply_subst subst bo' in
+ let ty' = CicMetaSubst.apply_subst subst ty' in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
+ | Cic.Variable _ -> assert false (* not implemented *)
+ | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
+ (*CSC: this code is greately simplified and many many checks are missing *)
+ (*CSC: e.g. the constructors are not required to build their own types, *)
+ (*CSC: the arities are not required to have as type a sort, etc. *)
+ let uri = match uri with Some uri -> uri | None -> assert false in
+ let typesno = List.length tys in
+ (* first phase: we fix only the types *)
+ let metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv [] ty ugraph
+ in
+ metasenv,ugraph,(name,b,ty',cl)::res
+ ) tys (metasenv,ugraph,[]) in
+ let con_context =
+ List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
+ (* second phase: we fix only the constructors *)
+ let metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+ let metasenv,ugraph,cl' =
+ List.fold_right
+ (fun (name,ty) (metasenv,ugraph,res) ->
+ let ty =
+ CicTypeChecker.debrujin_constructor
+ ~cb:(relocalize localization_tbl) uri typesno ty in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
+ let ty' = undebrujin uri typesno tys ty' in
+ metasenv,ugraph,(name,ty')::res
+ ) cl (metasenv,ugraph,[])
+ in
+ metasenv,ugraph,(name,b,ty,cl')::res
+ ) tys (metasenv,ugraph,[]) in
+ (* third phase: we check the positivity condition *)
+ let metasenv,ugraph,tys =
+ are_all_occurrences_positive metasenv ugraph uri tys paramsno
+ in
+ Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+