matita/components/binaries/matex/anticipate.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module L = List
  13 module P = Printf
  14
  15 module C = NCic
  16 module T = NCicTypeChecker
  17
  18 module X = Ground
  19 module G = Options
  20 module K = Kernel
  21
  22 (* internal functions *******************************************************)
  23
  24 let fresh = ref 0
  25
  26 let malformed s =
  27    X.error ("anticipate: malformed term: " ^ s)
  28
  29 let ok s =
  30    X.log ("anticipate: ok " ^ s)
  31
  32 let anticipate c v =
  33    incr fresh;
  34    let w = K.typeof c v in
  35    P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
  36
  37 let initial = None, []
  38
  39 let proc_arg c i (d, rtts) t = match d with
  40    | Some _ -> d, (t :: rtts)
  41    | None   ->
  42       if K.is_atomic t || K.not_prop2 c t then d, (t :: rtts) else
  43       let s, w, v, tt = anticipate c t in
  44       Some (i, s, w, v), (tt :: rtts)
  45
  46 let lift_arg ri i tts t =
  47    if ri = i then t :: tts
  48    else K.lift K.fst_var 1 t :: tts
  49
  50 let rec proc_term c t = match t with
  51    | C.Appl []
  52    | C.Meta _
  53    | C.Implicit _             -> malformed "2"
  54    | C.Sort _
  55    | C.Rel _
  56    | C.Const _
  57    | C.Prod _                 -> [], t
  58    | C.Lambda (s, w, t)       ->
  59       let tt = shift_term (K.add_dec s w c) t in
  60       [], K.lambda s w tt
  61    | C.LetIn (s, w, v, t)     ->
  62       if K.not_prop1 c w then
  63          let dt, tt = proc_term (K.add_def s w v c) t in
  64          dt @ K.add_def s w v [], tt
  65       else
  66          let dv, vv = proc_term c v in
  67          let l = L.length dv in
  68          let c = dv @ c in
  69          let w = K.lift K.fst_var l w in
  70          let t = K.lift K.snd_var l t in
  71          let dt, tt = proc_term (K.add_def s w vv c) t in
  72          dt @ (K.add_def s w vv dv), tt
  73    | C.Appl [t]               -> proc_term c t
  74    | C.Appl (C.Appl ts :: vs) -> proc_term c (K.appl (ts @ vs))
  75    | C.Appl ts                -> proc_appl c t ts
  76    | C.Match (w, u, v, ts)    -> proc_case c t w u v ts
  77
  78 and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
  79    | None             , _    -> [], t
  80    | Some (i, s, w, v), rtts ->
  81       let ri = L.length rtts - i in
  82       let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
  83       proc_term c (K.letin s w v (K.appl tts))
  84
  85 and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with
  86    | None               , _    ->
  87       if K.is_atomic v || K.not_prop1 c (C.Const w) then [], t else
  88       let s, w0, v0, vv = anticipate c v in
  89       let u = K.lift K.fst_var 1 u in
  90       let ts = K.lifts K.fst_var 1 ts in
  91       proc_term c (K.letin s w0 v0 (K.case w u vv ts))
  92    | Some (i, s, w0, v0), rtts ->
  93       let ri = L.length rtts - i in
  94       let u = K.lift K.fst_var 1 u in
  95       let v = K.lift K.fst_var 1 v in
  96       let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
  97       proc_term c (K.letin s w0 v0 (K.case w u v tts))
  98
  99 and shift_term c t =
 100    let d, tt = proc_term c t in
 101    K.shift tt d
 102
 103 let shift_named_term s c t =
 104 try
 105    fresh := 0;
 106    let tt = shift_term c t in
 107    if !G.check then begin
 108       let _ = K.typeof c tt in
 109       ok s
 110    end;
 111    tt
 112 with
 113    | T.TypeCheckerFailure s
 114    | T.AssertFailure s           -> malformed (Lazy.force s)
 115
 116 let proc_fun c =
 117    let r, s, i, u, t = c in
 118    if K.not_prop1 [] u then c else
 119    r, s, i, u, shift_named_term s [] t
 120
 121 let proc_obj obj = match obj with
 122    | C.Inductive _
 123    | C.Constant (_, _, None, _, _)   -> obj
 124    | C.Constant (r, s, Some t, u, a) ->
 125       if K.not_prop1 [] u then obj else
 126       let tt = shift_named_term s [] t in
 127       C.Constant (r, s, Some tt, u, a)
 128    | C.Fixpoint (b, cs, a)           ->
 129       C.Fixpoint (b, L.map proc_fun cs, a)
 130
 131 (* interface functions ******************************************************)
 132
 133 let process_top_term s t = shift_named_term s [] t
 134
 135 let process_obj obj = proc_obj obj