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 typeof c t = K.whd c (K.typeof c t)
  33
  34 let not_prop1 c u = match typeof c u with
  35    | C.Sort (C.Prop) -> false
  36    | C.Sort _        -> true
  37    | _               -> malformed "1"
  38
  39 let not_prop2 c t = not_prop1 c (K.typeof c t)
  40
  41 let anticipate c v =
  42    incr fresh;
  43    let w = K.typeof c v in
  44    P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
  45
  46 let initial = None, []
  47
  48 let proc_arg c i (d, rtts) t = match d with
  49    | Some _ -> d, (t :: rtts)
  50    | None   ->
  51       if K.is_atomic t || not_prop2 c t then d, (t :: rtts) else
  52       let s, w, v, tt = anticipate c t in
  53       Some (i, s, w, v), (tt :: rtts)
  54
  55 let lift_arg ri i tts t =
  56    if ri = i then t :: tts
  57    else K.lift K.fst_var 1 t :: tts
  58
  59 let rec proc_term c t = match t with
  60    | C.Appl []
  61    | C.Meta _
  62    | C.Implicit _             -> malformed "2"
  63    | C.Sort _
  64    | C.Rel _
  65    | C.Const _
  66    | C.Prod _                 -> [], t
  67    | C.Lambda (s, w, t)       ->
  68       let tt = shift_term (K.add_dec s w c) t in
  69       [], K.lambda s w tt
  70    | C.LetIn (s, w, v, t)     ->
  71       if not_prop1 c w then
  72          let dt, tt = proc_term (K.add_def s w v c) t in
  73          dt @ K.add_def s w v [], tt
  74       else
  75          let dv, vv = proc_term c v in
  76          let l = L.length dv in
  77          let c = dv @ c in
  78          let w = K.lift K.fst_var l w in
  79          let t = K.lift K.snd_var l t in
  80          let dt, tt = proc_term (K.add_def s w vv c) t in
  81          dt @ (K.add_def s w vv dv), tt
  82    | C.Appl [t]               -> proc_term c t
  83    | C.Appl (C.Appl ts :: vs) -> proc_term c (C.Appl (ts @ vs))
  84    | C.Appl ts                -> proc_appl c t ts
  85    | C.Match (w, u, v, ts)    -> proc_case c t w u v ts
  86
  87 and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
  88    | None             , _    -> [], t
  89    | Some (i, s, w, v), rtts ->
  90       let ri = L.length rtts - i in
  91       let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
  92       proc_term c (K.letin s w v (C.Appl tts))
  93
  94 and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with
  95    | None               , _    ->
  96       if K.is_atomic v || not_prop1 c (C.Const w) then [], t else
  97       let s, w0, v0, vv = anticipate c v in
  98       let u = K.lift K.fst_var 1 u in
  99       let ts = K.lifts K.fst_var 1 ts in
 100       proc_term c (K.letin s w0 v0 (K.case w u vv ts))
 101    | Some (i, s, w0, v0), rtts ->
 102       let ri = L.length rtts - i in
 103       let u = K.lift K.fst_var 1 u in
 104       let v = K.lift K.fst_var 1 v in
 105       let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
 106       proc_term c (K.letin s w0 v0 (K.case w u v tts))
 107
 108 and shift_term c t =
 109    let d, tt = proc_term c t in
 110    K.shift tt d
 111
 112 let shift_named s c t =
 113 try
 114    fresh := 0;
 115    let tt = shift_term c t in
 116    if !G.test then begin
 117       let _ = K.typeof c tt in
 118       ok s
 119    end;
 120    tt
 121 with
 122    | T.TypeCheckerFailure s
 123    | T.AssertFailure s           -> malformed (Lazy.force s)
 124
 125 let proc_fun c =
 126    let r, s, i, u, t = c in
 127    if not_prop1 [] u then c else
 128    r, s, i, u, shift_named s [] t
 129
 130 let proc_obj obj = match obj with
 131    | C.Inductive _
 132    | C.Constant (_, _, None, _, _)   -> obj
 133    | C.Constant (r, s, Some t, u, a) ->
 134       if not_prop1 [] u then obj else
 135       let tt = shift_named s [] t in
 136       C.Constant (r, s, Some tt, u, a)
 137    | C.Fixpoint (b, cs, a)           ->
 138       C.Fixpoint (b, L.map proc_fun cs, a)
 139
 140 (* interface functions ******************************************************)
 141
 142 (* not_prop1 *)
 143
 144 (* not_prop2 *)
 145
 146 let process_top_term s t = shift_named s [] t
 147
 148 let process_obj obj = proc_obj obj