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