X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb;hb=5e5d161f094982275ce39dbb4780c106e4475b37;hp=7f1ec58359b728857fb4536258e7f33de7b934f1;hpb=72206bee39e35bcc5cf8a7074ade13a4a81c0c08;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 7f1ec5835..ff19dff19 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -451,7 +451,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t) | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = @@ -522,31 +523,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst params exp_named_subst' m = - (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params - let ens' = - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) - List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens - in - let rec filter_and_lift = - function - [] -> [] - | uri::tl -> - let r = filter_and_lift tl in - (try - (uri,(List.assq uri ens'))::r - with - Not_found -> r - ) - in - filter_and_lift params - *) - - (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) - (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) - - (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) - (*CSC: codice altamente inefficiente *) + (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) let rec filter_and_lift already_instantiated = function [] -> [] @@ -561,18 +538,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) :: (filter_and_lift (uri::already_instantiated) tl) | _::tl -> filter_and_lift already_instantiated tl -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (filter_and_lift [] (List.rev ens)) + let res = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in unwind_aux m t @@ -596,19 +579,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function (k, e, _, C.Rel n, s) as config -> let config' = - try - Some (RS.from_env (List.nth e (n-1))) - with - Failure _ -> - try - begin - match List.nth context (n - 1 - k) with - None -> assert false - | Some (_,C.Decl _) -> None - | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) - end - with - Failure _ -> None + if not delta then None + else + try + Some (RS.from_env (List.nth e (n-1))) + with + Failure _ -> + try + begin + match List.nth context (n - 1 - k) with + None -> assert false + | Some (_,C.Decl _) -> None + | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) + end + with + Failure _ -> None in (match config' with Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s) @@ -643,7 +628,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (_, _, _, C.Lambda _, []) as config -> config | (k, e, ens, C.Lambda (_,_,t), p::s) -> reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s) - | (k, e, ens, C.LetIn (_,m,t), s) -> + | (k, e, ens, C.LetIn (_,m,_,t), s) -> let m' = RS.compute_to_env ~reduce ~unwind k e ens m in reduce (k+1, m'::e, ens, t, s) | (_, _, _, C.Appl [], _) -> assert false @@ -884,19 +869,16 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); *) aux test_equality_only context t1 term' ugraph with CicUtil.Subst_not_found _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - (try - true,(CicUniv.add_eq t2 t1 ugraph) - with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (try - true,(CicUniv.add_ge t2 t1 ugraph) - with CicUniv.UniverseInconsistency _ -> false,ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when test_equality_only -> + (try true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when not test_equality_only -> + (try true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) + | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> let b',ugraph' = aux true context s1 s2 ugraph in @@ -906,17 +888,21 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + let b',ugraph' = aux true context s1 s2 ugraph in if b' then aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 ugraph' else false,ugraph - | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only - ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' + let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in + if b' then + aux test_equality_only + ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph' + else + false,ugraph else false,ugraph | (C.Appl l1, C.Appl l2) -> @@ -1169,7 +1155,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = | C.Lambda (n,s,t) -> let s' = aux ctx s in C.Lambda (n, s', aux ((decl n s')::ctx) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,_,t) -> (* the term is already in weak head normal form *) assert false | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))