exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let debug_print = fun _ -> ()
+
let fdebug = ref 1;;
let debug t env s =
let rec debug_aux t i =
CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
- prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+ debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
;;
module type Strategy =
)
| C.Var (uri,exp_named_subst) ->
(*
-prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
*)
if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
else
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable (_,_,_,params,_) -> params
| C.Appl l -> C.Appl (List.map (unwind_aux m) l)
| C.Const (uri,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant (_,_,_,params,_) -> params
| C.Variable _ -> raise ReferenceToVariable
C.Const (uri,exp_named_subst')
| C.MutInd (uri,i,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
C.MutInd (uri,i,exp_named_subst')
| C.MutConstruct (uri,i,j,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| _::tl -> filter_and_lift already_instantiated tl
(*
| (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
+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
unwind' 0
;;
- let reduce ?(subst = []) context : config -> Cic.term =
+ let reduce ~delta ?(subst = []) context : config -> Cic.term =
let module C = Cic in
let module S = CicSubstitution in
let rec reduce =
reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
else
( let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
)
| (k, e, ens, (C.Meta (n,l) as t), s) ->
(try
- let (_, term,_) = CicUtil.lookup_subst n subst in
+ let (_, term,_) = CicUtil.lookup_subst n subst in
reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
- with CicUtil.Subst_not_found _ ->
+ with CicUtil.Subst_not_found _ ->
let t' = unwind k e ens t in
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
| (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
| (k, e, ens, C.Appl l, s) ->
C.Appl (List.append (List.map (unwind k e ens) l) s)
*)
+ | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
| (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
(let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- match o with
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ match o with
C.Constant (_,Some body,_,_,_) ->
let ens' = push_exp_named_subst k e ens exp_named_subst in
(* constants are closed *)
reduce (k, e, ens, (List.nth pl (j-1)), s)
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
- in
- match o with
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
+ in
+ match o with
C.InductiveDefinition (tl,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
in
(* ts are already unwinded because they are a sublist of tl *)
reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
- | C.Cast _ | C.Implicit _ ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let t' = unwind k e ens t in
(name,recindex,unwind k e ens typ,
unwind' leng k e ens body)
in
- List.map unwind_fl fl
+ List.map unwind_fl fl
in
let new_env =
let counter = ref 0 in
try
reduce context (0, [], [], t, [])
with Not_found ->
- prerr_endline (CicPp.ppterm t) ;
+ debug_print (lazy (CicPp.ppterm t)) ;
raise Not_found
;;
*)
- let rec whd ?(subst=[]) context t =
- reduce ~subst context (0, [], [], t, [])
+ let rec whd ?(delta=true) ?(subst=[]) context t =
+ reduce ~delta ~subst context (0, [], [], t, [])
;;
let rescsc = CicReductionNaif.whd context t in
if not (CicReductionNaif.are_convertible context res rescsc) then
begin
- prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
+ debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
flush stderr ;
- prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
+ debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
flush stderr ;
- prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
+ debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
flush stderr ;
CicReductionNaif.fdebug := 0 ;
let _ = CicReductionNaif.are_convertible context res rescsc in
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (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
- let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
- List.fold_left2
- (fun (b,ugraph) t1 t2 ->
- if b then
- match t1,t2 with
- None,_
- | _,None -> true,ugraph
- | Some t1',Some t2' ->
- aux test_equality_only context t1' t2' ugraph
- else
- false,ugraph
- ) (true,ugraph) l1 l2
- in
- if b2 then true,ugraph1 else false,ugraph
- else
- false,ugraph
+ if n1 = n2 then
+ let b2, ugraph1 =
+ let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+ let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+ List.fold_left2
+ (fun (b,ugraph) t1 t2 ->
+ if b then
+ match t1,t2 with
+ None,_
+ | _,None -> true,ugraph
+ | Some t1',Some t2' ->
+ aux test_equality_only context t1' t2' ugraph
+ else
+ false,ugraph
+ ) (true,ugraph) l1 l2
+ in
+ if b2 then true,ugraph1 else false,ugraph
+ else
+ false,ugraph
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+ true,(CicUniv.add_eq t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ true,(CicUniv.add_ge t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
(* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- true,(CicUniv.add_eq t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- true,(CicUniv.add_ge t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- (* TASSI: CONSTRAINTS *)
| (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
+ 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
+ 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
+ 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
+ if b' then
aux test_equality_only
((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
- else
- false,ugraph
+ else
+ false,ugraph
| (C.Appl l1, C.Appl l2) ->
(try
List.fold_right2
(fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph) l1 l2 (true,ugraph)
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph) l1 l2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
| (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
let b' = U.eq uri1 uri2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutInd (uri1,i1,exp_named_subst1),
C.MutInd (uri2,i2,exp_named_subst2)
) ->
let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
C.MutConstruct (uri2,i2,j2,exp_named_subst2)
) ->
let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutCase (uri1,i1,outtype1,term1,pl1),
C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
+ if b' then
let b'',ugraph''=aux test_equality_only context
- outtype1 outtype2 ugraph in
- if b'' then
- let b''',ugraph'''= aux test_equality_only context
- term1 term2 ugraph'' in
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph)
- pl1 pl2 (true,ugraph''')
- else
- false,ugraph
- else
- false,ugraph
+ outtype1 outtype2 ugraph in
+ if b'' then
+ let b''',ugraph'''= aux test_equality_only context
+ term1 term2 ugraph'' in
+ List.fold_right2
+ (fun x y (b,ugraph) ->
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph)
+ pl1 pl2 (b''',ugraph''')
+ else
+ false,ugraph
+ else
+ false,ugraph
| (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
let tys =
List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
List.fold_right2
(fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
if b && recindex1 = recindex2 then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
| (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
let tys =
List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
if i1 = i2 then
List.fold_right2
(fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
- if b then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
+ if b then
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
| (C.Cast _, _) | (_, C.Cast _)
| (C.Implicit _, _) | (_, C.Implicit _) ->
assert false
debug t1 [t2] "PREWHD";
(*
(match t1 with
- Cic.Meta _ ->
- prerr_endline (CicPp.ppterm t1);
- prerr_endline (CicPp.ppterm (whd ~subst context t1));
- prerr_endline (CicPp.ppterm t2);
- prerr_endline (CicPp.ppterm (whd ~subst context t2))
+ Cic.Meta _ ->
+ debug_print (lazy (CicPp.ppterm t1));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
+ debug_print (lazy (CicPp.ppterm t2));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
let t1' = whd ~subst context t1 in
let t2' = whd ~subst context t2 in
aux false (*c t1 t2 ugraph *)
;;
+
+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
+ let decl name t = Some (name, C.Decl t) in
+ let def name t = Some (name, C.Def (t,None)) in
+ match t with
+ | C.Rel n -> t
+ | C.Var (uri,exp_named_subst) ->
+ C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.Meta (i,l) ->
+ C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
+ | C.Sort _ -> t
+ | C.Implicit _ -> t
+ | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
+ | C.Prod (n,s,t) ->
+ let s' = aux ctx s in
+ C.Prod (n, s', aux ((decl n s')::ctx) t)
+ | 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) ->
+ (* the term is already in weak head normal form *)
+ assert false
+ | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
+ | C.Appl [] -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.MutInd (uri,typeno,exp_named_subst) ->
+ C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+ C.MutConstruct (uri, typeno, consno,
+ List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+(*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 *)
+let rec head_beta_reduce =
+ function
+ (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ let he''' =
+ match he'' with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | _ -> Cic.Appl (he''::tl')
+ in
+ head_beta_reduce he'''
+ | Cic.Cast (te,_) -> head_beta_reduce te
+ | t -> t
projects / helm.git / blobdiff