aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/subtac_pretyping.ml
blob: 5b42c8ba5f77d91624f9736d3cd02ecb7e7dbf67 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern

open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm

module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)

open Pretyping

let _ = Pretyping.allow_anonymous_refs := true

type recursion_info = {
  arg_name: name;
  arg_type: types; (* A *)
  args_after : rel_context;
  wf_relation: constr; (* R : A -> A -> Prop *)
  wf_proof: constr; (* : well_founded R *)
  f_type: types; (* f: A -> Set *)
  f_fulltype: types; (* Type with argument and wf proof product first *)
}

let my_print_rec_info env t =
  str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
  str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
  str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
  str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
  str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
  str "Full type: " ++ my_print_constr env t.f_fulltype
(*   trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
(* 	   str " and tycon "++ my_print_tycon env tycon ++ *)
(* 	   str " in environment: " ++ my_print_env env); *)

let merge_evms x y =
  Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y

let interp env isevars c tycon =
  let j = pretype tycon env isevars ([],[]) c in
  let _ = isevars := Evarutil.nf_evar_map !isevars in
  let evd = consider_remaining_unif_problems env !isevars in
(*   let unevd = undefined_evars evd in *)
  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
  let evm =  unevd' in
    isevars := unevd';
    nf_evar evm j.uj_val, nf_evar evm j.uj_type

let find_with_index x l =
  let rec aux i = function
      (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
    | [] -> raise Not_found
  in aux 0 l

open Vernacexpr

let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
  Constrintern.intern_constr evd env
let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 
  Constrintern.intern_type evd env

let env_with_binders env isevars l =
  let rec aux ((env, rels) as acc) = function
      Topconstr.LocalRawDef ((loc, name), def) :: tl ->
	let rawdef = coqintern_constr !isevars env def in
	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
	let reldecl = (name, Some coqdef, deftyp) in
	  aux  (push_rel reldecl env, reldecl :: rels) tl
    | Topconstr.LocalRawAssum (bl, k, typ) :: tl ->
	let rawtyp = coqintern_type !isevars env typ in
	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
	let acc =
	  List.fold_left (fun (env, rels) (loc, name) ->
			    let reldecl = (name, None, coqtyp) in
			      (push_rel reldecl env,
			       reldecl :: rels))
	    (env, rels) bl
	in aux acc tl
    | [] -> acc
  in aux (env, []) l

let subtac_process env isevars id bl c tycon =
  let c = Topconstr.abstract_constr_expr c bl in
  let tycon, imps =
    match tycon with
	None -> empty_tycon, None
      | Some t ->
	  let t = Topconstr.prod_constr_expr t bl in
	  let t = coqintern_type !isevars env t in
	  let imps = Implicit_quantifiers.implicits_of_rawterm t in
	  let coqt, ttyp = interp env isevars t empty_tycon in
	    mk_tycon coqt, Some imps
  in
  let c = coqintern_constr !isevars env c in
  let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in
  let coqc, ctyp = interp env isevars c tycon in
  let evm = non_instanciated_map env isevars !isevars in
  let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
    evm, coqc, ty, imps

open Subtac_obligations

let subtac_proof kind hook env isevars id bl c tycon =
  let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
  let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
  let evm' = Subtac_utils.evars_of_term evm evm' coqt in
  let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
    add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars