exception ListTooShort;;
exception RelToHiddenHypothesis;;
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
+
+(*CSC: potrebbe creare applicazioni di applicazioni *)
+(*CSC: ora non e' piu' head, ma completa!!! *)
+let rec head_beta_reduce =
+ let module S = CicSubstitution in
+ let module C = Cic in
+ function
+ C.Rel _
+ | C.Var _ as t -> t
+ | C.Meta (n,l) ->
+ C.Meta (n,
+ List.map
+ (function None -> None | Some t -> Some (head_beta_reduce t)) l
+ )
+ | C.Sort _ as t -> t
+ | C.Implicit -> assert false
+ | C.Cast (te,ty) ->
+ C.Cast (head_beta_reduce te, head_beta_reduce ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
+ let he' = S.subst he t in
+ if tl = [] then
+ head_beta_reduce he'
+ else
+ head_beta_reduce (C.Appl (he'::tl))
+ | C.Appl l ->
+ C.Appl (List.map head_beta_reduce l)
+ | C.Const _ as t -> t
+ | C.MutInd _
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cno,i,outt,t,pl) ->
+ C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+ List.map head_beta_reduce pl)
+ | C.Fix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,i,ty,bo) ->
+ name,i,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.Fix (i,fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,ty,bo) ->
+ name,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.CoFix (i,fl')
+;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant), *)
+(* distinction between fake dependent products *)
+(* and non-dependent products, alfa-conversion *)
+(*CSC: must alfa-conversion be considered or not? *)
+let syntactic_equality t t' =
+ let module C = Cic in
+ let rec syntactic_equality t t' =
+ if t = t' then true
+ else
+ match t, t' with
+ C.Rel _, C.Rel _
+ | C.Var _, C.Var _
+ | C.Meta _, C.Meta _
+ | C.Sort _, C.Sort _
+ | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ | C.Cast (te,ty), C.Cast (te',ty') ->
+ syntactic_equality te te' &&
+ syntactic_equality ty ty'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Appl l, C.Appl l' ->
+ List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
+ | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
+ | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
+ UriManager.eq uri uri' && i = i'
+ | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+ UriManager.eq uri uri' && i = i' && j = j'
+ | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ UriManager.eq sp sp' && i = i' &&
+ syntactic_equality outt outt' &&
+ syntactic_equality t t' &&
+ List.fold_left2
+ (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+ | C.Fix (i,fl), C.Fix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+ b && i = i' &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | C.CoFix (i,fl), C.CoFix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,ty,bo) (_,ty',bo') ->
+ b &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | _,_ -> false
+ in
+ try
+ syntactic_equality t t'
+ with
+ _ -> false
+;;
let rec split l n =
match (l,n) with
;;
(* 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 =
+let rec type_of_aux' subterms_to_types metasenv context t expectedty =
(* 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 rec type_of_aux context t expectedty =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
(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)
+ | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
| None -> raise RelToHiddenHypothesis
with
_ -> raise (NotWellTyped "Not a close term")
(* 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
+ (function
+ None -> ()
+ | Some t -> ignore (type_of_aux context t None)
+ ) l
in
let (_,canonical_context,ty) =
List.find (function (m,_,_) -> n = m) metasenv
| 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
+ let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
+ let _ = type_of_aux context ty None 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
+ let sort1 = type_of_aux context s None
+ and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None 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)
+ let _ = type_of_aux context s None in
+ let expected_target_type =
+ match expectedty with
+ None -> None
+ | Some expectedty' ->
+ let ty =
+ match R.whd context expectedty' with
+ C.Prod (_,_,expected_target_type) ->
+ head_beta_reduce expected_target_type
+ | _ -> assert false
+ in
+ Some ty
+ in
+ let type2 =
+ type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
+ in
+ (* Checks suppressed *)
+ C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
+(*CSC: What are the right expected types for the source and *)
+(*CSC: target of a LetIn? None used. *)
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context s in
+ let _ = type_of_aux context s None in
(* Checks suppressed *)
- C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+ C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
| 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
+ let hetype = type_of_aux context he None in
+ let tlbody_and_type =
+ let rec aux =
+ function
+ _,[] -> []
+ | C.Prod (n,s,t),he::tl ->
+ (he, type_of_aux context he (Some (head_beta_reduce s)))::
+ (aux (R.whd context (S.subst he t), tl))
+ | _ -> assert false
+ in
+ aux (R.whd context hetype, 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)
+ let outsort = type_of_aux context outtype None 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
- 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")
+ let (b, k) = guess_args context outsort in
+ if not b then (b, k - 1) else (b, k)
+ in
+ let (parameters, arguments) =
+ let type_of_term =
+ CicTypeChecker.type_of_aux' metasenv context term
in
- (* Checks suppressed *)
- if not need_dummy then
- C.Appl ((outtype::arguments)@[term])
- else if arguments = [] then
- outtype
- else
- C.Appl (outtype::arguments)
+ match
+ R.whd context (type_of_aux context term
+ (Some (head_beta_reduce type_of_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 *)
+ (* Let's visit all the subterms that will not be visited later *)
+ let (cl,parsno) =
+ match CicEnvironment.get_cooked_obj uri cookingsno with
+ C.InductiveDefinition (tl,_,parsno) ->
+ let (_,_,_,cl) = List.nth tl i in (cl,parsno)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ in
+ let _ =
+ List.fold_left
+ (fun j (p,(_,c,_)) ->
+ let cons =
+ if parameters = [] then
+ (C.MutConstruct (uri,cookingsno,i,j))
+ else
+ (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
+ in
+ let expectedtype =
+ type_of_branch context parsno need_dummy outtype cons
+ (CicTypeChecker.type_of_aux' metasenv context cons)
+ in
+ ignore (type_of_aux context p
+ (Some (head_beta_reduce expectedtype))) ;
+ j+1
+ ) 1 (List.combine pl cl)
+ in
+ 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
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
in
(* Checks suppressed *)
let (_,_,ty,_) = List.nth fl i in
List.rev
(List.map
(fun (n,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
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'
+ let synthesized' = head_beta_reduce synthesized in
+ let types,res =
+ match expectedty with
+ None ->
+ (* No expected type *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some ty when syntactic_equality synthesized' ty ->
+ (* The expected type is synthactically equal to *)
+ (* the synthesized type. Let's forget it. *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some expectedty' ->
+prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
+prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
+ {synthesized = synthesized' ; expected = Some expectedty'},
+ expectedty'
+ in
+ CicHash.add subterms_to_types t types ;
+ res
and sort_of_prod context (name,s) (t1, t2) =
let module C = Cic in
| _ -> raise (NotWellTyped "Appl: wrong Prod-type")
)
+and type_of_branch context argsno need_dummy outtype term constype =
+ let module C = Cic in
+ let module R = CicReduction in
+ match R.whd context constype with
+ C.MutInd (_,_,_) ->
+ if need_dummy then
+ outtype
+ else
+ C.Appl [outtype ; term]
+ | C.Appl (C.MutInd (_,_,_)::tl) ->
+ let (_,arguments) = split tl argsno
+ in
+ if need_dummy && arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
+ | C.Prod (name,so,de) ->
+ let term' =
+ match CicSubstitution.lift 1 term with
+ C.Appl l -> C.Appl (l@[C.Rel 1])
+ | t -> C.Appl [t ; C.Rel 1]
+ in
+ C.Prod (C.Anonimous,so,type_of_branch
+ ((Some (name,(C.Decl so)))::context) argsno need_dummy
+ (CicSubstitution.lift 1 outtype) term' de)
+ | _ -> raise (Impossible 20)
+
in
- type_of_aux context t
+ type_of_aux context t expectedty
;;
-let double_type_of metasenv context t =
+let double_type_of metasenv context t expectedty =
let subterms_to_types = CicHash.create 503 in
- ignore (type_of_aux' subterms_to_types metasenv context t) ;
+ ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
subterms_to_types
;;
projects / helm.git / blobdiff