module D = Deannotate
module PER = ProofEngineReduction
module Ut = CicUtil
-
-(* time stamping ************************************************************)
-
-let print_times =
- let old = ref 0.0 in
- fun msg ->
- let times = Unix.times () in
- let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in
- let lap = stamp -. !old in
- Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout;
- old := stamp
-
-(* raw cic prettyprinter ****************************************************)
-
-let xiter out so ss sc map l =
- let rec aux = function
- | hd :: tl when tl <> [] -> map hd; out ss; aux tl
- | hd :: tl -> map hd; aux tl
- | [] -> ()
- in
- out so; aux l; out sc
-
-let abst s w = Some (s, C.Decl w)
-
-let abbr s v w = Some (s, C.Def (v, w))
-
-let pp_sort out = function
- | C.Type _ -> out "\Type"
- | C.Prop -> out "\Prop"
- | C.CProp _ -> out "\CProp"
- | C.Set -> out "\Set"
-
-let pp_name out = function
- | C.Name s -> out s
- | C.Anonymous -> out "_"
-
-let pp_rel out c i =
- try match List.nth c (pred i) with
- | None -> out (Printf.sprintf "%u[?]" i)
- | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
- with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
-
-let pp_implict out = function
- | None -> out "?"
- | Some `Closed -> out "?[Closed]"
- | Some `Type -> out "?[Type]"
- | Some `Hole -> out "?[Hole]"
-
-let pp_uri out a =
- out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
-
-let rec pp_term out e c = function
- | C.Sort h -> pp_sort out h
- | C.Rel i -> pp_rel out c i
- | C.Implicit x -> pp_implict out x
- | C.Meta (i, iss) ->
- let map = function None -> out "_" | Some v -> pp_term out e c v in
- out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
- | C.Var (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.Const (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.MutInd (a, m, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u" m);
- pp_xss out e c xss
- | C.MutConstruct (a, m, n, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
- pp_xss out e c xss
- | C.Cast (v, w) ->
- out "type "; pp_term out e c w; out " contains "; pp_term out e c v
- | C.Appl vs ->
- xiter out "(" " @ " ")" (pp_term out e c) vs
- | C.MutCase (a, m, w, v, vs) ->
- out "match "; pp_term out e c v;
- out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
- out " to "; pp_term out e c w;
- xiter out " cases " " | " "" (pp_term out e c) vs
- | C.Prod (s, w, t) ->
- out "forall "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.Lambda (s, w, t) ->
- out "fun "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.LetIn (s, v, w, t) ->
- out "let "; pp_name out s;
- out " def "; pp_term out e c v; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abbr s v w :: c) t
- | C.Fix (i, fs) ->
- let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, i, w, v) =
- out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
- | C.CoFix (i, fs) ->
- let map c (s, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, w, v) =
- out s; pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
-
-and pp_xss out e c xss =
- let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
- xiter out "[" "; " "]" map xss
+module DTI = DoubleTypeInference
(* fresh name generator *****************************************************)
in
join (aux k context)
-let mk_fresh_name context = function
- | C.Anonymous -> C.Anonymous
+let mk_fresh_name does_not_occur context = function
| C.Name s -> mk_fresh_name context (split s)
+ | C.Anonymous ->
+ if does_not_occur then C.Anonymous
+ else mk_fresh_name context (split "LOCAL")
(* helper functions *********************************************************)
+let rec list_fold_right_cps g map l a =
+ match l with
+ | [] -> g a
+ | hd :: tl ->
+ let h a = map g hd a in
+ list_fold_right_cps h map tl a
+
+let rec list_fold_left_cps g map a = function
+ | [] -> g a
+ | hd :: tl ->
+ let h a = list_fold_left_cps g map a tl in
+ map h a hd
+
let rec list_map_cps g map = function
| [] -> g []
| hd :: tl ->
let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
- with e ->
- Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+ let error e =
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
raise e
+ in
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with
+ | Rf.RefineFailure s as e ->
+ Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
+ error e
+ | e ->
+ Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
+ error e
let get_type msg c t =
let log s =
prerr_endline ("TC: " ^ s);
prerr_endline ("TC: context: " ^ Pp.ppcontext c);
- prerr_string "TC: term : "; pp_term prerr_string [] c t;
+ prerr_string "TC: term : "; Ut.pp_term prerr_string [] c t;
prerr_newline (); prerr_endline ("TC: location: " ^ msg)
in
try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
| (_, hd) :: _, _ -> hd
| _ -> assert false
-let is_proof c t =
- match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
+let is_prop c t =
+ match get_tail c (get_type "is_prop" c t) with
| C.Sort C.Prop -> true
| C.Sort _ -> false
| _ -> assert false
+let is_proof c t =
+ is_prop c (get_type "is_prop" c t)
+
let is_sort = function
| C.Sort _ -> true
| _ -> false
let cic = D.deannotate_term
+let flatten_appls =
+ let rec flatten_xns (uri, t) = uri, flatten_term t
+ and flatten_ms = function
+ | None -> None
+ | Some t -> Some (flatten_term t)
+ and flatten_fix (name, i, ty, bo) =
+ name, i, flatten_term ty, flatten_term bo
+ and flatten_cofix (name, ty, bo) =
+ name, flatten_term ty, flatten_term bo
+ and flatten_term = function
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Rel _ as t -> t
+ | C.Const (uri, xnss) -> C.Const (uri, List.map flatten_xns xnss)
+ | C.Var (uri, xnss) -> C.Var (uri, List.map flatten_xns xnss)
+ | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, List.map flatten_xns xnss)
+ | C.MutConstruct (uri, tyno, consno, xnss) -> C.MutConstruct (uri, tyno, consno, List.map flatten_xns xnss)
+ | C.Meta (i, mss) -> C.Meta(i, List.map flatten_ms mss)
+(* begin flattening *)
+ | C.Appl [t] -> flatten_term t
+ | C.Appl (C.Appl ts1 :: ts2) -> flatten_term (C.Appl (ts1 @ ts2))
+ | C.Appl [] -> assert false
+(* end flattening *)
+ | C.Appl ts -> C.Appl (List.map flatten_term ts)
+ | C.Cast (te, ty) -> C.Cast (flatten_term te, flatten_term ty)
+ | C.MutCase (sp, i, outty, t, pl) -> C.MutCase (sp, i, flatten_term outty, flatten_term t, List.map flatten_term pl)
+ | C.Prod (n, s, t) -> C.Prod (n, flatten_term s, flatten_term t)
+ | C.Lambda (n, s, t) -> C.Lambda (n, flatten_term s, flatten_term t)
+ | C.LetIn (n, ty, s, t) -> C.LetIn (n, flatten_term ty, flatten_term s, flatten_term t)
+ | C.Fix (i, fl) -> C.Fix (i, List.map flatten_fix fl)
+ | C.CoFix (i, fl) -> C.CoFix (i, List.map flatten_cofix fl)
+ in
+ flatten_term
+
+let sober ?(flatten=false) c t =
+ if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
+
+let alpha_equivalence ?flatten c t1 t2 =
+ let t1 = sober ?flatten c t1 in
+ let t2 = sober ?flatten c t2 in
+ Ut.alpha_equivalence t1 t2
+
let occurs c ~what ~where =
let result = ref false in
let equality c t1 t2 =
- let r = Ut.alpha_equivalence t1 t2 in
+ let r = alpha_equivalence ~flatten:true c t1 t2 in
result := !result || r; r
in
let context, what, with_what = c, [what], [C.Rel 0] in
| [] -> c
| hd :: tl ->
let sname, w = map hd in
- let entry = Some (Cic.Name sname, C.Decl w) in
+ let entry = Some (C.Name sname, C.Decl w) in
add_entries map (entry :: c) tl
let get_sname c i =
try match List.nth c (pred i) with
- | Some (Cic.Name sname, _) -> sname
+ | Some (C.Name sname, _) -> sname
| _ -> assert false
with
| Failure _ -> assert false
let get_cofix_decl (sname, w, v) = sname, w in
let rec bc c = function
| C.LetIn (name, v, ty, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Def (v, ty)) in
let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
C.LetIn (name, v, ty, t)
| C.Lambda (name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl w) in
let w, t = bc c w, bc (entry :: c) t in
C.Lambda (name, w, t)
| C.Prod (name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 t in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl w) in
let w, t = bc c w, bc (entry :: c) t in
C.Prod (name, w, t)
let get_cofix_decl (id, sname, w, v) = sname, cic w in
let rec bc c = function
| C.ALetIn (id, name, v, ty, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Def (cic v, cic ty)) in
let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
C.ALetIn (id, name, v, ty, t)
| C.ALambda (id, name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl (cic w)) in
let w, t = bc c w, bc (entry :: c) t in
C.ALambda (id, name, w, t)
| C.AProd (id, name, w, t) ->
- let name = mk_fresh_name c name in
+ let dno = DTI.does_not_occur 1 (cic t) in
+ let name = mk_fresh_name dno c name in
let entry = Some (name, C.Decl (cic w)) in
let w, t = bc c w, bc (entry :: c) t in
C.AProd (id, name, w, t)
| t -> t
in
bc c t
+
+let is_acic_proof sorts context v =
+ let id = Ut.id_of_annterm v in
+ try match Hashtbl.find sorts id with
+ | `Prop -> true
+ | _ -> false
+ with Not_found -> is_proof context (cic v)
+