--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception Impossible of int;;
+exception NotRefinable of string;;
+exception WrongUriToConstant of string;;
+exception WrongUriToVariable of string;;
+exception WrongUriToMutualInductiveDefinitions of string;;
+exception RelToHiddenHypothesis;;
+exception MetasenvInconsistency;;
+exception MutCaseFixAndCofixRefineNotImplemented;;
+exception FreeMetaFound of int;;
+
+let fdebug = ref 0;;
+let debug t context =
+ let rec debug_aux t i =
+ let module C = Cic in
+ let module U = UriManager in
+ CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+ in
+ if !fdebug = 0 then
+ raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
+ (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
+;;
+
+let rec type_of_constant uri =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ match CicEnvironment.get_cooked_obj uri with
+ C.Constant (_,_,ty,_) -> ty
+ | C.CurrentProof (_,_,_,ty,_) -> ty
+ | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+
+and type_of_variable uri =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ match CicEnvironment.get_cooked_obj uri with
+ C.Variable (_,_,ty,_) -> ty
+ | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+
+and type_of_mutual_inductive_defs uri i =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ match CicEnvironment.get_cooked_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity
+ | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+
+and type_of_mutual_inductive_constr uri i j =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ match CicEnvironment.get_cooked_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,_,cl) = List.nth dl i in
+ let (_,ty) = List.nth cl (j-1) in
+ ty
+ | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+
+(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+and type_of_aux' metasenv context t =
+ let rec type_of_aux subst metasenv context =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module U = UriManager in
+ let module Un = CicUnification in
+ function
+ C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Decl t) -> S.lift n t,subst,metasenv
+ | Some (_,C.Def bo) ->
+ type_of_aux subst metasenv context (S.lift n bo)
+ | None -> raise RelToHiddenHypothesis
+ with
+ _ -> raise (NotRefinable "Not a close term")
+ )
+ | C.Var (uri,exp_named_subst) ->
+ incr fdebug ;
+ let subst',metasenv' =
+ check_exp_named_subst subst metasenv context exp_named_subst in
+ let ty =
+ CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
+ in
+ decr fdebug ;
+ ty,subst',metasenv'
+ | C.Meta (n,l) ->
+ let (_,canonical_context,ty) =
+ try
+ List.find (function (m,_,_) -> n = m) metasenv
+ with
+ Not_found -> raise (FreeMetaFound n)
+ in
+ let subst',metasenv' =
+ check_metasenv_consistency subst metasenv context canonical_context l
+ in
+ CicSubstitution.lift_meta l ty, subst', metasenv'
+ | C.Sort s ->
+ C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
+ subst,metasenv
+ | C.Implicit -> raise (Impossible 21)
+ | C.Cast (te,ty) ->
+ let _,subst',metasenv' =
+ type_of_aux subst metasenv context ty in
+ let inferredty,subst'',metasenv'' =
+ type_of_aux subst' metasenv' context ty
+ in
+ (try
+ let subst''',metasenv''' =
+ Un.fo_unif_subst subst'' context metasenv'' inferredty ty
+ in
+ ty,subst''',metasenv'''
+ with
+ _ -> raise (NotRefinable "Cast"))
+ | C.Prod (name,s,t) ->
+ let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+ let sort2,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
+ in
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
+ | C.Lambda (n,s,t) ->
+ let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+ let type2,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
+ in
+ let sort2,subst''',metasenv''' =
+ type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
+ in
+ (* only to check if the product is well-typed *)
+ let _,subst'''',metasenv'''' =
+ sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
+ in
+ C.Prod (n,s,type2),subst'''',metasenv''''
+ | C.LetIn (n,s,t) ->
+ (* only to check if s is well-typed *)
+ let _,subst',metasenv' = type_of_aux subst metasenv context s in
+ let inferredty,subst'',metasenv'' =
+ type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::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::tl) when List.length tl > 0 ->
+ 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 (NotRefinable "Appl: no arguments")
+ | C.Const (uri,exp_named_subst) ->
+ incr fdebug ;
+ 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
+ decr fdebug ;
+ cty,subst',metasenv'
+ | C.MutInd (uri,i,exp_named_subst) ->
+ incr fdebug ;
+ 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
+ decr fdebug ;
+ 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 _
+ | C.Fix _
+ | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+
+ (* 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 subst metasenv context canonical_context l =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
+ let lifted_canonical_context =
+ let rec aux i =
+ function
+ [] -> []
+ | (Some (n,C.Decl t))::tl ->
+ (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def t))::tl ->
+ (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | None::tl -> None::(aux (i+1) tl)
+ in
+ aux 1 canonical_context
+ in
+ List.fold_left2
+ (fun (subst,metasenv) t ct ->
+ match (t,ct) with
+ _,None -> subst,metasenv
+ | Some t,Some (_,C.Def ct) ->
+ (try
+ CicUnification.fo_unif_subst subst context metasenv t ct
+ with _ -> raise MetasenvInconsistency)
+ | Some t,Some (_,C.Decl ct) ->
+ let inferredty,subst',metasenv' =
+ type_of_aux subst metasenv context t
+ in
+ (try
+ CicUnification.fo_unif_subst subst context metasenv inferredty ct
+ with _ -> raise MetasenvInconsistency)
+ | _, _ -> raise MetasenvInconsistency
+ ) (subst,metasenv) l lifted_canonical_context
+
+ and check_exp_named_subst metasubst metasenv context =
+ let rec check_exp_named_subst_aux metasubst metasenv substs =
+ function
+ [] -> metasubst,metasenv
+ | ((uri,t) as subst)::tl ->
+ let typeofvar =
+ CicSubstitution.subst_vars substs (type_of_variable uri) in
+ (match CicEnvironment.get_cooked_obj ~trust:false uri with
+ Cic.Variable (_,Some bo,_,_) ->
+ raise
+ (NotRefinable
+ "A variable with a body can not be explicit substituted")
+ | Cic.Variable (_,None,_,_) -> ()
+ | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ ) ;
+ let typeoft,metasubst',metasenv' =
+ type_of_aux metasubst metasenv context t
+ in
+ try
+ let metasubst'',metasenv'' =
+ CicUnification.fo_unif_subst
+ metasubst' context metasenv' typeoft typeofvar
+ in
+ check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
+ with _ ->
+ raise (NotRefinable "Wrong Explicit Named Substitution")
+ in
+ check_exp_named_subst_aux metasubst metasenv []
+
+ and sort_of_prod subst metasenv context (name,s) (t1, t2) =
+ let module C = Cic in
+ (* ti could be a metavariable in the domain of the substitution *)
+ let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
+ let t1' = CicUnification.apply_subst subst' t1 in
+ let t2' = CicUnification.apply_subst subst' t2 in
+ let t1'' = CicReduction.whd context t1' in
+ let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
+ match (t1'', t2'') with
+ (C.Sort s1, C.Sort s2)
+ when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+ C.Sort s2,subst',metasenv'
+ | (C.Sort s1, C.Sort s2) ->
+ (*CSC manca la gestione degli universi!!! *)
+ C.Sort C.Type,subst',metasenv'
+ | (_,_) ->
+ raise
+ (NotRefinable
+ ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
+
+ and eat_prods subst metasenv context hetype =
+ function
+ [] -> hetype,subst,metasenv
+ | (hete, hety)::tl ->
+ (match (CicReduction.whd context hetype) with
+ Cic.Prod (n,s,t) ->
+ let subst',metasenv' =
+ try
+ CicUnification.fo_unif_subst subst context metasenv s hety
+ with _ ->
+ raise (NotRefinable "Appl: wrong parameter-type")
+ in
+ CicReduction.fdebug := -1 ;
+ eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
+ | _ -> raise (NotRefinable "Appl: wrong Prod-type")
+ )
+ in
+ let ty,subst',metasenv' =
+ type_of_aux [] metasenv context t
+ in
+ let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
+ (* we get rid of the metavariables that have been instantiated *)
+ let metasenv''' =
+ List.filter
+ (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
+ metasenv''
+ in
+ CicUnification.apply_subst subst'' t,
+ CicUnification.apply_subst subst'' ty,
+ subst'', metasenv'''
+;;
+
+(* DEBUGGING ONLY *)
+let type_of_aux' metasenv context term =
+ try
+ let (t,ty,s,m) =
+ type_of_aux' metasenv context term
+ in
+ List.iter
+ (function (i,t) ->
+ prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
+ List.iter
+ (function (i,_,t) ->
+ prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
+ prerr_endline
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
+ (t,ty,s,m)
+ with
+ e ->
+ List.iter
+ (function (i,_,t) ->
+ prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
+ metasenv ;
+ prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
+ raise e
+;;
projects / helm.git / commitdiff