-(* 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$ *)
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
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
end
;;
-*)
+}}} *)
module Reduction(RS : Strategy) =
struct
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
;;
-(* 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
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 =
(*
- (* 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
(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
| 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
;;
*)
-(* 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
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
(*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
| 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
("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
end;
res
-*)
+ }}} *)
+
+(* vim:set foldmethod=marker: *)
projects / helm.git / commitdiff