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))
+ with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
let pp_implict out = function
| None -> out "?"
let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
xiter out "[" "; " "]" map xss
-and pp_attrs out attrs =
+let pp_int out i =
+ out (Printf.sprintf "%u" i)
+
+let pp_attrs out attrs =
let map = function
| _ -> ()
in
let pp_pars out pars =
xiter out " (" ", " ")\n" (pp_uri out) pars
+let pp_point out point =
+ if point then out "ind " else out "coind "
+
+let pp_constructor out (s, w) =
+ out s; out " of "; pp_term out [] [] w
+
+let pp_definition out (s, point, w, ts) =
+ out "let "; pp_point out point; out s; out " of "; pp_term out [] [] w;
+ xiter out "\ndef " "\nor " "" (pp_constructor out) ts
+
let pp_obj out = function
- | C.Constant (s, None, u, pars, attrs) ->
+ | C.Constant (s, None, u, pars, attrs) ->
out "fun "; pp_attrs out attrs; out s; pp_pars out pars;
out " of "; pp_term out [] [] u
- | C.Constant (s, Some t, u, pars, attrs) ->
+ | C.Constant (s, Some t, u, pars, attrs) ->
out "let "; pp_attrs out attrs; out s; pp_pars out pars;
out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
- | C.Variable (s, None, u, pars, attrs) ->
- out "Local declaration"
- | C.Variable (s, Some t, u, pars, attrs) ->
- out "Local definition"
- | C.CurrentProof (s, e, t, u, pars, attrs) ->
+ | C.Variable (s, None, u, pars, attrs) ->
+ out "local fun "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " of "; pp_term out [] [] u
+ | C.Variable (s, Some t, u, pars, attrs) ->
+ out "local let "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
+ | C.InductiveDefinition (us, pars, lpsno, attrs) ->
+ out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars;
+ xiter out "" "\n" "" (pp_definition out) us
+ | C.CurrentProof (s, e, t, u, pars, attrs) ->
out "Current Proof"
- | C.InductiveDefinition (us, pars, lpno, attrs) ->
- out "Inductive Definition"
-
+
module E = CicEnvironment
module Ut = CicUtil
module TC = CicTypeChecker
+module S = CicSubstitution
+module X = HExtlib
let hashtbl_size = 11
(* helper functions *********************************************************)
-let typecheck t =
+let rec count_prods n = function
+ | C.Prod (_, _, t) -> count_prods (succ n) t
+ | _ -> n
+
+let get_ind_type_psnos uri tyno =
+ match E.get_obj Un.default_ugraph uri with
+ | C.InductiveDefinition (tys, _, lpsno, _), _ ->
+ let _, _, ty, _ = List.nth tys tyno in
+ lpsno, count_prods 0 ty
+ | _ -> assert false
+
+let typecheck b t =
if !debug then begin
+ out (Printf.sprintf "Pre Check ; %s\n" b);
+ Ut.pp_term out [] [] t; out "\n";
let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
- out "Typecheck : OK\n"
+ out (Printf.sprintf "Typecheck : %s OK\n" b)
end
let list_pos found l =
type status = {
dn: string -> string; (* name discharge map *)
du: UM.uri -> UM.uri; (* uri discharge map *)
- c : C.context; (* var context of this object *)
ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
rl: UM.uri list; (* reverse var list of this object *)
- h : int (* relocation index *)
+ h : int; (* relocation index *)
+ c : C.context (* local context of this object *)
}
-let add st k = {st with h = st.h + k}
+let add st k es = {st with h = st.h + k; c = List.rev_append es st.c}
let discharge st u = st.h + list_pos (UM.eq u) st.rl
let args = vars_of_uri u in
Hashtbl.add st.ls u args; args
+let proj_fix (s, _, w, _) = s, w
+
+let proj_cofix (s, w, _) = s, w
+
+let mk_context proj discharge_term s =
+ let map e =
+ let s, w = proj e in
+ let w' = discharge_term w in
+ Some (C.Name s, C.Decl w')
+ in
+ List.length s, List.rev_map map s
+
+let rec split_absts named no c = function
+ | C.Lambda (s, w, t) ->
+ let e = Some (s, C.Decl w) in
+ let named = named && s <> C.Anonymous in
+ split_absts named (succ no) (e :: c) t
+ | t ->
+ named, no, c, t
+
+let close is_type c t =
+ let map t = function
+ | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
+ | Some (b, C.Decl w) ->
+ if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
+ | None -> assert false
+ in
+ List.fold_left map t c
+
+let relocate to_what from_what k m =
+ try
+ let u = List.nth from_what (m - k) in
+ let map v m = if UM.eq u v then Some m else None in
+ match X.list_findopt map to_what with
+ | Some m -> m + k
+ | None -> raise (Failure "nth")
+ with
+ | Failure "nth" -> assert false
+
let rec discharge_term st t = match t with
| C.Implicit _
| C.Sort _
discharge_term st w, discharge_term st v,
list_map_sh (discharge_term st) vs
in
+(* BEGIN FIX OUT TYPE *)
+ let lpsno, psno = get_ind_type_psnos u m in
+ let rpsno = psno - lpsno in
+ let named, frpsno, wc, wb = split_absts true 0 [] w' in
+ let w' =
+(* No fixing needed *)
+ if frpsno = succ rpsno then w' else
+(* Fixing needed, no right parametes *)
+ if frpsno = rpsno && rpsno = 0 then
+ let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+ if !debug then begin
+ out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
+ end;
+ C.Lambda (C.Anonymous, vty, S.lift 1 wb)
+ else
+(* Fixing needed, some right parametes *)
+ if frpsno = rpsno then
+ let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in
+ if !debug then begin
+ out "VTY: "; Ut.pp_term out [] st.c vty; out "\n"
+ end;
+ let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in
+ close false wc (C.Lambda (C.Anonymous, vty, wb))
+(* This case should not happen *)
+ else assert false
+ in
+(* END FIX OUT TYPE *)
if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
C.MutCase (u', m, sh w w', sh v v', sh vs vs')
| C.Prod (b, w, v) ->
- let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ let w' = discharge_term st w in
+ let es = [Some (b, C.Decl w')] in
+ let v' = discharge_term (add st 1 es) v in
if w' == w && v' == v then t else
C.Prod (b, sh w w', sh v v')
| C.Lambda (b, w, v) ->
- let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ let w' = discharge_term st w in
+ let es = [Some (b, C.Decl w')] in
+ let v' = discharge_term (add st 1 es) v in
if w' == w && v' == v then t else
C.Lambda (b, sh w w', sh v v')
| C.LetIn (b, y, w, v) ->
- let y', w', v' =
- discharge_term st y, discharge_term st w, discharge_term (add st 1) v
- in
+ let y', w' = discharge_term st y, discharge_term st w in
+ let es = [Some (b, C.Def (y, w'))] in
+ let v' = discharge_term (add st 1 es) v in
if y' == y && w' == w && v' == v then t else
C.LetIn (b, sh y y', sh w w', sh v v')
| C.CoFix (i, s) ->
- let no = List.length s in
- let s' = list_map_sh (discharge_cofun st no) s in
+ let no, es = mk_context proj_cofix (discharge_term st) s in
+ let s' = list_map_sh (discharge_cofun st no es) s in
if s' == s then t else C.CoFix (i, s')
| C.Fix (i, s) ->
- let no = List.length s in
- let s' = list_map_sh (discharge_fun st no) s in
+ let no, es = mk_context proj_fix (discharge_term st) s in
+ let s' = list_map_sh (discharge_fun st no es) s in
if s' == s then t else C.Fix (i, s')
and discharge_nsubst st s =
let t' = discharge_term st t in
if t' == t then s else Some t'
-and discharge_cofun st no f =
+and discharge_cofun st no es f =
let b, w, v = f in
- let w', v' = discharge_term st w, discharge_term (add st no) v in
+ let w', v' = discharge_term st w, discharge_term (add st no es) v in
if w' == w && v' == v then f else
b, sh w w', sh v v'
-and discharge_fun st no f =
+and discharge_fun st no es f =
let b, i, w, v = f in
- let w', v' = discharge_term st w, discharge_term (add st no) v in
+ let w', v' = discharge_term st w, discharge_term (add st no es) v in
if w' == w && v' == v then f else
b, i, sh w w', sh v v'
-let close is_type st t =
- let map t = function
- | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
- | Some (b, C.Decl w) ->
- if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
- | None -> assert false
- in
- List.fold_left map t st.c
+let close is_type st = close is_type st.c
let discharge_con st con =
let b, v = con in
let w' = discharge_term st w in
if w' == w && vars = [] then obj else
let w'' = sh w w' in
- let _ = typecheck w'' in
+(* We do not typecheck because variables are not closed *)
C.Variable (dn b, None, w'', [], attrs)
| C.Variable (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
if w' == w && v' == v && vars = [] then obj else
let w'', v'' = sh w w', sh v v' in
- let _ = typecheck (C.Cast (v'', w'')) in
+(* We do not typecheck because variables are not closed *)
C.Variable (dn b, Some v'', w'', [], attrs)
| C.Constant (b, None, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w' = discharge_term st w in
if w' == w && vars = [] then obj else
let w'' = close true st (sh w w') in
- let _ = typecheck w'' in
+ let _ = typecheck (dn b) w'' in
C.Constant (dn b, None, w'', [], attrs)
| C.Constant (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
if w' == w && v' == v && vars = [] then obj else
let w'', v'' = close true st (sh w w'), close false st (sh v v') in
- let _ = typecheck (C.Cast (v'', w'')) in
+ let _ = typecheck (dn b) (C.Cast (v'', w'')) in
C.Constant (dn b, Some v'', w'', [], attrs)
| C.InductiveDefinition (types, vars, lpsno, attrs) ->
let st = init_status dn du ls vars in
and init_status dn du ls vars =
let c, rl = discharge_vars dn du vars, List.rev vars in
- {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1}
+ {dn = dn; du = du; ls = ls; rl = rl; h = 1; c = c}
projects / helm.git / commitdiff