helm/gTopLevel/proofEngine.ml

   1 type binder_type =
   2    Declaration
   3  | Definition
   4 ;;
   5
   6 type metas_context = (int * Cic.term) list;;
   7
   8 type context = (binder_type * Cic.name * Cic.term) list;;
   9
  10 type sequent = context * Cic.term;;
  11
  12 let proof = ref (None : (metas_context * Cic.term * Cic.term) option);;
  13 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
  14 (* Note: the sequent is redundant: it can be computed from the type of the   *)
  15 (* metavariable and its context in the proof. We keep it just for efficiency *)
  16 (* because computing the context of a term may be quite expensive.           *)
  17 let goal = ref (None : (int * sequent) option);;
  18
  19 exception NotImplemented
  20
  21 (*CSC: Funzione che deve sparire!!! *)
  22 let cic_context_of_context =
  23  List.map
  24   (function
  25       Declaration,_,t -> t
  26     | Definition,_,_ -> raise NotImplemented
  27   )
  28 ;;
  29
  30 let refine_meta meta term newmetasenv =
  31  let (metasenv,bo,ty) =
  32   match !proof with
  33      None -> assert false
  34    | Some (metasenv,bo,ty) -> metasenv,bo,ty
  35  in
  36   let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
  37   let bo' =
  38    let rec aux =
  39     let module C = Cic in
  40      function
  41         C.Rel _ as t -> t
  42       | C.Var _ as t  -> t
  43       | C.Meta meta' when meta=meta' -> term
  44       | C.Meta _ as t -> t
  45       | C.Sort _ as t -> t
  46       | C.Implicit as t -> t
  47       | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
  48       | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
  49       | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
  50       | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
  51       | C.Appl l -> C.Appl (List.map aux l)
  52       | C.Const _ as t -> t
  53       | C.Abst _ as t -> t
  54       | C.MutInd _ as t -> t
  55       | C.MutConstruct _ as t -> t
  56       | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  57          C.MutCase (sp,cookingsno,i,aux outt, aux t,
  58           List.map aux pl)
  59       | C.Fix (i,fl) ->
  60          let substitutedfl =
  61           List.map
  62            (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
  63             fl
  64          in
  65           C.Fix (i, substitutedfl)
  66       | C.CoFix (i,fl) ->
  67          let substitutedfl =
  68           List.map
  69            (fun (name,ty,bo) -> (name, aux ty, aux bo))
  70             fl
  71          in
  72           C.CoFix (i, substitutedfl)
  73    in
  74     aux bo
  75   in
  76    proof := Some (metasenv',bo',ty)
  77 ;;
  78
  79 let new_meta () =
  80  let metasenv =
  81   match !proof with
  82      None -> assert false
  83    | Some (metasenv,_,_) -> metasenv
  84  in
  85   let rec aux =
  86    function
  87       None,[] -> 1
  88     | Some n,[] -> n
  89     | None,(n,_)::tl -> aux (Some n,tl)
  90     | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  91   in
  92    1 + aux (None,metasenv)
  93 ;;
  94
  95 (* metas_in_term term                                                *)
  96 (* Returns the ordered list of the metas that occur in [term].       *)
  97 (* Duplicates are removed. The implementation is not very efficient. *)
  98 let metas_in_term term =
  99  let module C = Cic in
 100   let rec aux =
 101    function
 102       C.Rel _
 103     | C.Var _ -> []
 104     | C.Meta n -> [n]
 105     | C.Sort _
 106     | C.Implicit -> []
 107     | C.Cast (te,ty) -> (aux te) @ (aux ty)
 108     | C.Prod (_,s,t) -> (aux s) @ (aux t)
 109     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
 110     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
 111     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
 112     | C.Const _
 113     | C.Abst _
 114     | C.MutInd _
 115     | C.MutConstruct _ -> []
 116     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 117        (aux outt) @ (aux t) @
 118         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
 119     | C.Fix (i,fl) ->
 120         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 121     | C.CoFix (i,fl) ->
 122         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 123   in
 124    let metas = aux term in
 125     let rec elim_duplicates =
 126      function
 127         [] -> []
 128       | he::tl ->
 129          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
 130     in
 131      elim_duplicates metas
 132 ;;
 133
 134 (* perforate context term ty                                                 *)
 135 (* replaces the term [term] in the proof with a new metavariable whose type  *)
 136 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
 137 (* could be easily computed; so the only reasons to have it as an argument   *)
 138 (* are efficiency reasons.                                                   *)
 139 let perforate context term ty =
 140  let module C = Cic in
 141   let newmeta = new_meta () in
 142    match !proof with
 143       None -> assert false
 144     | Some (metasenv,bo,gty) ->
 145        (* We push the new meta at the end of the list for pretty-printing *)
 146        (* purposes: in this way metas are ordered.                        *)
 147        let metasenv' = metasenv@[newmeta,ty] in
 148        let rec aux =
 149         function
 150            (* Is == strong enough? *)
 151            t when t == term -> C.Meta newmeta
 152          | C.Rel _ as t -> t
 153          | C.Var _ as t  -> t
 154          | C.Meta _ as t -> t
 155          | C.Sort _ as t -> t
 156          | C.Implicit as t -> t
 157          | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 158          | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
 159          | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
 160          | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
 161          | C.Appl l -> C.Appl (List.map aux l)
 162          | C.Const _ as t -> t
 163          | C.Abst _ as t -> t
 164          | C.MutInd _ as t -> t
 165          | C.MutConstruct _ as t -> t
 166          | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 167             C.MutCase (sp,cookingsno,i,aux outt, aux t,
 168              List.map aux pl)
 169          | C.Fix (i,fl) ->
 170             let substitutedfl =
 171              List.map
 172               (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
 173                fl
 174             in
 175              C.Fix (i, substitutedfl)
 176          | C.CoFix (i,fl) ->
 177             let substitutedfl =
 178              List.map
 179               (fun (name,ty,bo) -> (name, aux ty, aux bo))
 180                fl
 181             in
 182              C.CoFix (i, substitutedfl)
 183        in
 184         let bo' = aux bo in
 185         (* It may be possible that some metavariables occurred only in *)
 186         (* the term we are perforating and they now occurs no more. We *)
 187         (* get rid of them, collecting the really useful metavariables *)
 188         (* in metasenv''.                                              *)
 189          let newmetas = metas_in_term bo' in
 190           let metasenv'' =
 191            List.filter (function (n,_) -> List.mem n newmetas) metasenv'
 192           in
 193            proof := Some (metasenv'',bo',gty) ;
 194            goal := Some (newmeta,(context,ty)) ;
 195            newmeta
 196 ;;
 197
 198 (************************************************************)
 199 (*                  Some easy tactics.                      *)
 200 (************************************************************)
 201
 202 exception Fail of string;;
 203
 204 let intros () =
 205  let module C = Cic in
 206  let module R = CicReduction in
 207   let metasenv =
 208    match !proof with
 209       None -> assert false
 210     | Some (metasenv,_,_) -> metasenv
 211   in
 212   let (metano,context,ty) =
 213    match !goal with
 214       None -> assert false
 215     | Some (metano,(context,ty)) -> metano,context,ty
 216   in
 217    let newmeta = new_meta () in
 218     let rec collect_context =
 219      function
 220         C.Cast (te,_)   -> collect_context te
 221       | C.Prod (n,s,t)  ->
 222          let (ctx,ty,bo) = collect_context t in
 223           ((Declaration,n,s)::ctx,ty,C.Lambda(n,s,bo))
 224       | C.LetIn (n,s,t) ->
 225          let (ctx,ty,bo) = collect_context t in
 226           ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
 227       | _ as t -> [], t, (C.Meta newmeta)
 228     in
 229      let revcontext',ty',bo' = collect_context ty in
 230       let context'' = (List.rev revcontext') @ context in
 231        refine_meta metano bo' [newmeta,ty'] ;
 232        goal := Some (newmeta,(context'',ty'))
 233 ;;
 234
 235 (* The term bo must be closed in the current context *)
 236 let exact bo =
 237  let module T = CicTypeChecker in
 238  let module R = CicReduction in
 239   let metasenv =
 240    match !proof with
 241       None -> assert false
 242     | Some (metasenv,_,_) -> metasenv
 243   in
 244   let (metano,context,ty) =
 245    match !goal with
 246       None -> assert false
 247     | Some (metano,(context,ty)) ->
 248        assert (ty = List.assoc metano metasenv) ;
 249        (* Invariant: context is the actual context of the meta in the proof *)
 250        metano,context,ty
 251   in
 252    (*CSC: deve sparire! *)
 253    let context = cic_context_of_context context in
 254     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
 255      refine_meta metano bo []
 256     else
 257      raise (Fail "The type of the provided term is not the one expected.")
 258 ;;