From: Enrico Tassi Date: Tue, 19 Feb 2008 11:13:39 +0000 (+0000) Subject: initial steps of convertibility X-Git-Tag: make_still_working~5599 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=3fb743f1c1fd5f5e49df2c5322e8c96a1a6ede67;hp=0ec61cd3d3fe2bf43b75fc94800af0c23cfa8c3b;p=helm.git initial steps of convertibility --- diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 37472875e..5bb6260ca 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -1,27 +1,12 @@ -(* 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/. - *) +(* ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) (* $Id$ *) @@ -82,8 +67,27 @@ module type Strategy = end ;; -(* -module CallByValueByNameForUnwind = +module CallByValueByNameForUnwind' = + struct + type config = int * env_term list * NCic.term * stack_term list + and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) + and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) + let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let from_stack (c,_) = Lazy.force c + let from_stack_list_for_unwind ~unwind:_ l = + List.map (function (_,c) -> Lazy.force c) l + let from_env (c,_) = Lazy.force c + let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c + let stack_to_env ~reduce:_ ~unwind:_ config = config + let compute_to_env ~reduce ~unwind k e t = + lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[])) + let compute_to_stack ~reduce ~unwind config = + lazy (reduce config), lazy (unwind config) + end +;; + + +(* {{{ module CallByValueByNameForUnwind = struct type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list and stack_term = config @@ -103,29 +107,9 @@ module CallByValueByNameForUnwind = let compute_to_stack ~reduce ~unwind config = config end ;; -*) - -module CallByValueByNameForUnwind' = - struct - type config = int * env_term list * NCic.term * stack_term list - and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) - and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) - let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) - let from_stack (c,_) = Lazy.force c - let from_stack_list_for_unwind ~unwind:_ l = - List.map (function (_,c) -> Lazy.force c) l - let from_env (c,_) = Lazy.force c - let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c - let stack_to_env ~reduce:_ ~unwind:_ config = config - let compute_to_env ~reduce ~unwind k e t = - lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[])) - let compute_to_stack ~reduce ~unwind config = - lazy (reduce config), lazy (unwind config) - end -;; -(* Old Machine +(* Old Machine *) module CallByNameStrategy = struct type stack_term = Cic.term @@ -375,7 +359,7 @@ module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy = end ;; -*) +}}} *) module Reduction(RS : Strategy) = struct @@ -431,7 +415,8 @@ module Reduction(RS : Strategy) = List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl in aux (k, e, he, tl' @ s) - | (_, _, NCic.Const(NReference.Ref (_,_,NReference.Def) as refer), s) as config -> + | (_, _, NCic.Const + (NReference.Ref (_,_,NReference.Def) as refer), s) as config -> let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in if delta >= height then config else aux (0, [], body, s) | (_, _, NCic.Const (NReference.Ref @@ -480,7 +465,7 @@ module Reduction(RS : Strategy) = ;; -(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione +(* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione senza ridurre la testa module R = Reduction CallByNameStrategy;; OK 56.368s module R = Reduction CallByValueStrategy;; ROTTO @@ -495,18 +480,15 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s -*) -(*module R = Reduction(CallByValueByNameForUnwind);;*) +module R = Reduction(CallByValueByNameForUnwind);; +module R = Reduction(CallByNameStrategy);; +module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *) module RS = CallByValueByNameForUnwind';; -(*module R = Reduction(CallByNameStrategy);;*) -(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) -(* module R = Reduction(RS);; module U = UriManager;; let whd = R.whd -*) (* let whd = @@ -517,40 +499,36 @@ let whd = (* - (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then - * fallbacks to structural equality *) -let (===) x y = - Pervasives.compare x y = 0 + (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then + * fallbacks to structural equality *) +let (===) x y = Pervasives.compare x y = 0 ;; + +module C = NCic (* t1, t2 must be well-typed *) let are_convertible whd ?(subst=[]) ?(metasenv=[]) = let heuristic = ref true in - let rec aux test_equality_only context t1 t2 ugraph = - let rec aux2 test_equality_only t1 t2 ugraph = - - (* this trivial euristic cuts down the total time of about five times ;-) *) - (* this because most of the time t1 and t2 are "sintactically" the same *) - if t1 === t2 then - true,ugraph - else - begin - let module C = Cic in + let rec aux test_equality_only context t1 t2 = + let rec aux2 test_equality_only t1 t2 = + if t1 === t2 then + true + else match (t1,t2) with - (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph - | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) -> - if U.eq uri1 uri2 then - (try - List.fold_right2 - (fun (uri1,x) (uri2,y) (b,ugraph) -> - let b',ugraph' = aux test_equality_only context x y ugraph in - (U.eq uri1 uri2 && b' && b),ugraph' - ) exp_named_subst1 exp_named_subst2 (true,ugraph) - with - Invalid_argument _ -> false,ugraph - ) - else - false,ugraph - | (C.Meta (n1,l1), C.Meta (n2,l2)) -> + | (C.Rel n1, C.Rel n2) -> n1 = n2 + + | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b + | (C.Sort (C.Type a), C.Sort (C.Type b)) when test_equality_only -> a=b + | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only) + | (C.Sort s1, C.Sort s2) -> s1 = s2 + + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + aux true context s1 s2 && + aux test_equality_only ((name1, C.Decl s1)::context) t1 t2 + | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> + aux test_equality_only context s1 s2 && (* sure?! *) + aux test_equality_only ((name1, C.Decl s1)::context) t1 t2 + + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> if n1 = n2 then let b2, ugraph1 = let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in @@ -574,47 +552,14 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = (try let _,term,_ = NCicUtils.lookup_subst n1 subst in let term' = CicSubstitution.subst_meta l1 term in -(* -prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); -prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2); -*) aux test_equality_only context term' t2 ugraph with CicUtil.Subst_not_found _ -> false,ugraph) | _, C.Meta (n2,l2) -> (try let _,term,_ = CicUtil.lookup_subst n2 subst in let term' = CicSubstitution.subst_meta l2 term in -(* -prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); -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) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (try - true,(CicUniv.add_ge t2 t1 ugraph) - with CicUniv.UniverseInconsistency _ -> false,ugraph) - | (C.Sort s1, C.Sort (C.Type _)) -> (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 - if b' then - aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph - | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only 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)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then @@ -755,7 +700,6 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false,ugraph - end in let res = if !heuristic then @@ -819,7 +763,7 @@ end ;; *) -(* DEBUGGING ONLY +(* {{{ DEBUGGING ONLY let whd ?(delta=true) ?(subst=[]) context t = let res = whd ~delta ~subst context t in let rescsc = CicReductionNaif.whd ~delta ~subst context t in @@ -838,25 +782,19 @@ let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv. else res ;; -*) - -(* -let are_convertible = are_convertible whd + }}} *) -let whd = R.whd -*) +(*let are_convertible = are_convertible whd*) -(* -let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd" +(* {{{ let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd" let whd ?(delta=true) ?(subst=[]) context t = let foo () = whd ~delta ~subst context t in profiler_other_whd.HExtlib.profile foo () -*) + }}} *) -(* -let rec normalize ?(delta=true) ?(subst=[]) ctx term = +(* {{{ let rec normalize ?(delta=true) ?(subst=[]) ctx term = let module C = Cic in let t = whd ~delta ~subst ctx term in let aux = normalize ~delta ~subst in @@ -893,17 +831,15 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = (*CSC: to be completed, I suppose *) | C.Fix _ -> t | C.CoFix _ -> t -*) -(* let normalize ?delta ?subst ctx term = (* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *) let t = normalize ?delta ?subst ctx term in (* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *) t -*) + }}} *) -(* performs an head beta/cast reduction +(* {{{ performs an head beta/cast reduction let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = match upto with 0 -> t @@ -947,8 +883,9 @@ let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = | Some bo -> head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo)) | t -> t -*) -(* + }}} *) + +(* {{{ let are_convertible ?subst ?metasenv context t1 t2 ugraph = let before = Unix.gettimeofday () in let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in @@ -961,4 +898,6 @@ let are_convertible ?subst ?metasenv context t1 t2 ugraph = ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc); end; res -*) + }}} *) + +(* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 328924c79..3677944bd 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -31,11 +31,14 @@ exception ReferenceToInductiveDefinition (* val fdebug : int ref val whd : - ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term + ?delta:bool -> ?subst:NCic.substitution -> + NCic.context -> NCic.term -> + NCic.term + val are_convertible : - ?subst:Cic.substitution -> ?metasenv:Cic.metasenv -> - Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> - bool * CicUniv.universe_graph + ?subst:NCic.substitution -> ?metasenv:NCic.metasenv -> + NCic.context -> NCic.term -> NCic.term -> + bool val normalize: ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term