From: Enrico Tassi Date: Wed, 24 Sep 2008 14:48:23 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4748 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0bd584a839bae570f44c4a5f8a06cdbc55fe0726;p=helm.git ... --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 0e324483a..b3fbf55f3 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -8,6 +8,7 @@ nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicPp.cmi: nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nCic.cmo +nCicUntrusted.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -24,10 +25,8 @@ oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmo \ oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.cmi -nCic2OCic.cmo: nUri.cmi nReference.cmi nCicEnvironment.cmi nCic.cmo \ - nCic2OCic.cmi -nCic2OCic.cmx: nUri.cmx nReference.cmx nCicEnvironment.cmx nCic.cmx \ - nCic2OCic.cmi +nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi +nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \ @@ -46,3 +45,5 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi +nCicUntrusted.cmo: nReference.cmi nCic.cmo nCicUntrusted.cmi +nCicUntrusted.cmx: nReference.cmx nCic.cmx nCicUntrusted.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 8b8fee22f..a4affb50b 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -8,16 +8,19 @@ nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicPp.cmi: nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nCic.cmx +nCicUntrusted.cmi: nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi nUri.cmx: nUri.cmi nReference.cmo: nUri.cmi nReference.cmi nReference.cmx: nUri.cmx nReference.cmi -nCicUtils.cmo: nCic.cmx nCicUtils.cmi -nCicUtils.cmx: nCic.cmx nCicUtils.cmi -nCicSubstitution.cmo: nCicUtils.cmi nCic.cmx nCicSubstitution.cmi -nCicSubstitution.cmx: nCicUtils.cmx nCic.cmx nCicSubstitution.cmi +nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi +nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi +nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \ + nCicSubstitution.cmi +nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ + nCicSubstitution.cmi oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmx \ oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ @@ -42,3 +45,5 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi +nCicUntrusted.cmo: nReference.cmi nCic.cmx nCicUntrusted.cmi +nCicUntrusted.cmx: nReference.cmx nCic.cmx nCicUntrusted.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index f4ef9a8bf..670429b99 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -12,7 +12,8 @@ INTERFACE_FILES = \ nCicEnvironment.mli \ nCicPp.mli \ nCicReduction.mli \ - nCicTypeChecker.mli + nCicTypeChecker.mli \ + nCicUntrusted.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 59443bb1a..cc4d99e05 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -177,6 +177,7 @@ let prof = HExtlib.profiling_enabled := true;HExtlib.profile "cache failures";; let prof2 = HExtlib.profiling_enabled := true;HExtlib.profile "dancing sorts";; (* t1, t2 must be well-typed *) let are_convertible ?(subst=[]) get_relevance = +(* let get_relevance_p ~subst context t args = (match prof with {HExtlib.profile = p} -> p) (fun (a,b,c,d) -> get_relevance ~subst:a b c d) @@ -184,8 +185,9 @@ let are_convertible ?(subst=[]) get_relevance = in let dance () = (match prof2 with {HExtlib.profile = p} -> p) (fun () -> ()) () in +*) let rec aux test_eq_only context t1 t2 = - let rec alpha_eq test_eq_only t1 t2 = + let alpha_eq test_eq_only t1 t2 = if t1 === t2 then true else diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index 07781350c..1c3080826 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -32,3 +32,8 @@ val typeof: subst:NCic.substitution -> metasenv:NCic.metasenv -> NCic.context -> NCic.term -> NCic.term + +val get_relevance : + subst:NCic.substitution -> + NCic.context -> NCic.term -> NCic.term list -> bool list + diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml new file mode 100644 index 000000000..655c8f17a --- /dev/null +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -0,0 +1,73 @@ +(* + ||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$ *) + +module C = NCic +module Ref = NReference + +let map_term_fold_a g k f a = function + | C.Meta _ -> assert false + | C.Implicit _ + | C.Sort _ + | C.Const _ + | C.Rel _ as t -> a,t + | C.Appl [] | C.Appl [_] -> assert false + | C.Appl l as orig -> + let a,l = + (* sharing fold? *) + List.fold_right (fun t (a,l) -> let a,t = f k a t in a, t :: l) l (a,[]) + in + a, (match l with + | C.Appl l :: tl -> C.Appl (l@tl) + | l1 when l == l1 -> orig + | l1 -> C.Appl l1) + | C.Prod (n,s,t) as orig -> + let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in + a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) + | C.Lambda (n,s,t) as orig -> + let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in + a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1) + | C.LetIn (n,ty,t,b) as orig -> + let a,ty1 = f k a ty in let a,t1 = f k a t in + let a,b1 = f (g (n,C.Def (t,ty)) k) a b in + a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1) + | C.Match (r,oty,t,pl) as orig -> + let a,oty1 = f k a oty in let a,t1 = f k a t in + let a,pl1 = + (* sharing fold? *) + List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[]) + in + a, if oty1 == oty && t1 == t && pl1 == pl then orig + else C.Match(r,oty1,t1,pl1) +;; + +let metas_of_term subst context term = + let rec aux ctx acc = function + | NCic.Rel i -> + (match HExtlib.list_skip (i-1) ctx with + | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo + | _ -> acc) + | NCic.Meta(i,l) -> + (try + let _,_,bo,_ = NCicUtils.lookup_subst i subst in + let bo = NCicSubstitution.subst_meta l bo in + aux ctx acc bo + with NCicUtils.Subst_not_found _ -> + let shift, lc = l in + let lc = NCicUtils.expand_local_context lc in + let l = List.map (NCicSubstitution.lift shift) lc in + List.fold_left (aux ctx) (i::acc) l) + | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t + in + HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term)) +;; + diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli new file mode 100644 index 000000000..72e512784 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -0,0 +1,19 @@ +(* + ||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$ *) + +val map_term_fold_a: + (NCic.hypothesis -> 'k -> 'k) -> 'k -> + ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term + +val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list + diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index 74d1a7834..f4f77a367 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -80,39 +80,3 @@ let map g k f = function if oty1 == oty && t1 == t && pl1 == pl then orig else C.Match(r,oty1,t1,pl1) ;; - -let map_term_fold_a g k f a = function - | C.Meta _ -> assert false - | C.Implicit _ - | C.Sort _ - | C.Const _ - | C.Rel _ as t -> a,t - | C.Appl [] | C.Appl [_] -> assert false - | C.Appl l as orig -> - let a,l = - (* sharing fold? *) - List.fold_right (fun t (a,l) -> let a,t = f k a t in a, t :: l) l (a,[]) - in - a, (match l with - | C.Appl l :: tl -> C.Appl (l@tl) - | l1 when l == l1 -> orig - | l1 -> C.Appl l1) - | C.Prod (n,s,t) as orig -> - let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in - a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) - | C.Lambda (n,s,t) as orig -> - let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in - a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1) - | C.LetIn (n,ty,t,b) as orig -> - let a,ty1 = f k a ty in let a,t1 = f k a t in - let a,b1 = f (g (n,C.Def (t,ty)) k) a b in - a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1) - | C.Match (r,oty,t,pl) as orig -> - let a,oty1 = f k a oty in let a,t1 = f k a t in - let a,pl1 = - (* sharing fold? *) - List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[]) - in - a, if oty1 == oty && t1 == t && pl1 == pl then orig - else C.Match(r,oty1,t1,pl1) -;; diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index 1560094dc..c87dd6638 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -27,6 +27,3 @@ val fold: val map: (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term -val map_term_fold_a: - (NCic.hypothesis -> 'k -> 'k) -> 'k -> - ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term