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
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 \
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
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 \
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
nCicEnvironment.mli \
nCicPp.mli \
nCicReduction.mli \
- nCicTypeChecker.mli
+ nCicTypeChecker.mli \
+ nCicUntrusted.mli
IMPLEMENTATION_FILES = \
nCic.ml $(INTERFACE_FILES:%.mli=%.ml)
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)
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
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
+
--- /dev/null
+(*
+ ||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))
+;;
+
--- /dev/null
+(*
+ ||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
+
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)
-;;
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
projects / helm.git / commitdiff