--- /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 NotWellTyped of string;;
+exception WrongUriToConstant of string;;
+exception WrongUriToVariable of string;;
+exception WrongUriToMutualInductiveDefinitions of string;;
+exception ListTooShort;;
+exception RelToHiddenHypothesis;;
+
+type types = {synthesized : Cic.term ; expected : Cic.term};;
+
+let rec split l n =
+ match (l,n) with
+ (l,0) -> ([], l)
+ | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
+ | (_,_) -> raise ListTooShort
+;;
+
+let cooked_type_of_constant uri cookingsno =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ let cobj =
+ match CicEnvironment.is_type_checked uri cookingsno with
+ CicEnvironment.CheckedObj cobj -> cobj
+ | CicEnvironment.UncheckedObj uobj ->
+ raise (NotWellTyped "Reference to an unchecked constant")
+ in
+ match cobj with
+ C.Definition (_,_,ty,_) -> ty
+ | C.Axiom (_,ty,_) -> ty
+ | C.CurrentProof (_,_,_,ty) -> ty
+ | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+;;
+
+let type_of_variable uri =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ (* 0 because a variable is never cooked => no partial cooking at one level *)
+ match CicEnvironment.is_type_checked uri 0 with
+ CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
+ | CicEnvironment.UncheckedObj (C.Variable _) ->
+ raise (NotWellTyped "Reference to an unchecked variable")
+ | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+;;
+
+let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ let cobj =
+ match CicEnvironment.is_type_checked uri cookingsno with
+ CicEnvironment.CheckedObj cobj -> cobj
+ | CicEnvironment.UncheckedObj uobj ->
+ raise (NotWellTyped "Reference to an unchecked inductive type")
+ in
+ match cobj with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity
+ | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+;;
+
+let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ let cobj =
+ match CicEnvironment.is_type_checked uri cookingsno with
+ CicEnvironment.CheckedObj cobj -> cobj
+ | CicEnvironment.UncheckedObj uobj ->
+ raise (NotWellTyped "Reference to an unchecked constructor")
+ in
+ match cobj 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))
+;;
+
+module CicHash =
+ Hashtbl.Make
+ (struct
+ type t = Cic.term
+ let equal = (==)
+ let hash = Hashtbl.hash
+ end)
+;;
+
+(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+let rec type_of_aux' subterms_to_types metasenv context t =
+ (* Coscoy's double type-inference algorithm *)
+ (* It computes the inner-types of every subterm of [t], *)
+ (* even when they are not needed to compute the types *)
+ (* of other terms. *)
+ let rec type_of_aux context t =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution in
+ let module U = UriManager in
+ let synthesized =
+ match t with
+ C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Decl t) -> S.lift n t
+ | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
+ | None -> raise RelToHiddenHypothesis
+ with
+ _ -> raise (NotWellTyped "Not a close term")
+ )
+ | C.Var uri -> type_of_variable uri
+ | C.Meta (n,l) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let _ =
+ List.iter
+ (function None -> () | Some t -> ignore (type_of_aux context t)) l
+ in
+ let (_,canonical_context,ty) =
+ List.find (function (m,_,_) -> n = m) metasenv
+ in
+ (* Checks suppressed *)
+ CicSubstitution.lift_meta l ty
+ | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+ | C.Implicit -> raise (Impossible 21)
+ | C.Cast (te,ty) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let _ = type_of_aux context te in
+ let _ = type_of_aux context ty in
+ (* Checks suppressed *)
+ ty
+ | C.Prod (name,s,t) ->
+ let sort1 = type_of_aux context s
+ and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+ sort_of_prod context (name,s) (sort1,sort2)
+ | C.Lambda (n,s,t) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let _ = type_of_aux context s in
+ let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
+ (* Checks suppressed *)
+ C.Prod (n,s,type2)
+ | C.LetIn (n,s,t) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let _ = type_of_aux context s in
+ (* Checks suppressed *)
+ C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+ | C.Appl (he::tl) when List.length tl > 0 ->
+ let hetype = type_of_aux context he
+ and tlbody_and_type =
+ List.map (fun x -> (x, type_of_aux context x)) tl
+ in
+ eat_prods context hetype tlbody_and_type
+ | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
+ | C.Const (uri,cookingsno) ->
+ cooked_type_of_constant uri cookingsno
+ | C.Abst _ -> raise (Impossible 22)
+ | C.MutInd (uri,cookingsno,i) ->
+ cooked_type_of_mutual_inductive_defs uri cookingsno i
+ | C.MutConstruct (uri,cookingsno,i,j) ->
+ let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
+ cty
+ | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let _ = List.map (type_of_aux context) pl in
+ let outsort = type_of_aux context outtype in
+ let (need_dummy, k) =
+ let rec guess_args context t =
+ match CicReduction.whd context t with
+ C.Sort _ -> (true, 0)
+ | C.Prod (name, s, t) ->
+ let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
+ if n = 0 then
+ (* last prod before sort *)
+ match CicReduction.whd context s with
+ (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
+ C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
+ (false, 1)
+ | C.Appl ((C.MutInd (uri',_,i')) :: _)
+ when U.eq uri' uri && i' = i -> (false, 1)
+ | _ -> (true, 1)
+ else
+ (b, n + 1)
+ | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
+ in
+ (*CSC whd non serve dopo type_of_aux ? *)
+ let (b, k) = guess_args context outsort in
+ if not b then (b, k - 1) else (b, k)
+ in
+ let (_, arguments) =
+ match R.whd context (type_of_aux context term) with
+ (*CSC manca il caso dei CAST *)
+ C.MutInd (uri',_,i') ->
+ (* Checks suppressed *)
+ [],[]
+ | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+ split tl (List.length tl - k)
+ | _ ->
+ raise (NotWellTyped "MutCase: the term is not an inductive one")
+ in
+ (* Checks suppressed *)
+ if not need_dummy then
+ C.Appl ((outtype::arguments)@[term])
+ else if arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments)
+ | C.Fix (i,fl) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let context' =
+ List.rev
+ (List.map
+ (fun (n,_,ty,_) ->
+ let _ = type_of_aux context ty in
+ (Some (C.Name n,(C.Decl ty)))
+ ) fl
+ ) @
+ context
+ in
+ let _ =
+ List.iter
+ (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+ in
+ (* Checks suppressed *)
+ let (_,_,ty,_) = List.nth fl i in
+ ty
+ | C.CoFix (i,fl) ->
+ (* Let's visit all the subterms that will not be visited later *)
+ let context' =
+ List.rev
+ (List.map
+ (fun (n,ty,_) ->
+ let _ = type_of_aux context ty in
+ (Some (C.Name n,(C.Decl ty)))
+ ) fl
+ ) @
+ context
+ in
+ let _ =
+ List.iter
+ (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+ in
+ (* Checks suppressed *)
+ let (_,ty,_) = List.nth fl i in
+ ty
+ in
+ (*CSC: Is whd the right thing to do? Or should full beta *)
+ (*CSC: reduction be more appropriate? *)
+(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
+(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
+ let synthesized' = CicReduction.whd context synthesized in
+ CicHash.add subterms_to_types t
+ {synthesized = synthesized' ; expected = Cic.Implicit} ;
+ synthesized'
+
+ and sort_of_prod context (name,s) (t1, t2) =
+ let module C = Cic 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
+ | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+ | (_,_) ->
+ raise
+ (NotWellTyped
+ ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
+
+ and eat_prods context hetype =
+ (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
+ (*CSC: cucinati *)
+ function
+ [] -> hetype
+ | (hete, hety)::tl ->
+ (match (CicReduction.whd context hetype) with
+ Cic.Prod (n,s,t) ->
+ (* Checks suppressed *)
+ eat_prods context (CicSubstitution.subst hete t) tl
+ | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
+ )
+
+ in
+ type_of_aux context t
+;;
+
+let double_type_of metasenv context t =
+ let subterms_to_types = CicHash.create 503 in
+ ignore (type_of_aux' subterms_to_types metasenv context t) ;
+ subterms_to_types
+;;
projects / helm.git / commitdiff