From 54f3a0239cb6cee6176a475070cc70f309a82819 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 09:57:58 +0000 Subject: [PATCH 1/1] type_of_branch ported and optimized to not lift the outty every Prod, keep the number of passes binders and lift it just once --- .../components/ng_kernel/nCicTypeChecker.ml | 48 +++++++------------ 1 file changed, 18 insertions(+), 30 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 1760c57e4..920a2078e 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -517,33 +517,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = args coInductiveTypeURI ) fl true -and type_of_branch ~subst context argsno need_dummy outtype term constype = - let module C = Cic in - let module R = CicReduction in - match R.whd ~subst 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 (name,so,type_of_branch ~subst - ((Some (name,(C.Decl so)))::context) argsno need_dummy - (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (AssertFailure (lazy "20")) - and returns_a_coinductive ~subst context ty = let module C = Cic in match CicReduction.whd ~subst context ty with @@ -830,7 +803,7 @@ let rec typeof ~subst ~metasenv context term = let ty_p = typeof_aux context p in let ty_cons = typeof_aux context cons in let ty_branch = - type_of_branch ~subst context leftno outtype cons ty_cons in + type_of_branch ~subst context leftno outtype cons ty_cons 0 in j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch else j,false @@ -846,7 +819,22 @@ let rec typeof ~subst ~metasenv context term = R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false - and type_of_branch ~subst context leftno outty cons tycons = assert false + and type_of_branch ~subst context leftno outty cons tycons liftno = + match R.whd ~subst context tycons with + | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons] + | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) -> + let _,arguments = HExtlib.split_nth leftno tl in + C.Appl (S.lift liftno outty::arguments@[cons]) + | C.Prod (name,so,de) -> + let cons = + match S.lift 1 cons with + | C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1] + in + C.Prod (name,so, + type_of_branch ~subst ((name,(C.Decl so))::context) + leftno outty cons de (liftno+1)) + | _ -> raise (AssertFailure (lazy "type_of_branch")) (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -1107,7 +1095,6 @@ and split_prods ~subst context n te = split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta | _ -> raise (AssertFailure (lazy "split_prods")) -(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and is_really_smaller ~subst (context, recfuns, x, safes as k) te = match R.whd ~subst context te with | C.Rel m when List.mem m safes -> true @@ -1120,6 +1107,7 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te = | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) + (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*) is_really_smaller ~subst k he | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false -- 2.39.2