aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_trees.ml
blob: 8bdecdf8fc2b46ea9231817f5219047d43416618 (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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450

(* $Id$ *)

open Util
open Names
open Term
open Sign
open Evd
open Stamps
open Environ
open Typing

type bindOcc = 
  | Dep of identifier
  | NoDep of int
  | Com

type 'a substitution = (bindOcc * 'a) list

type tactic_arg =
  | Command       of Coqast.t
  | Constr        of constr
  | Identifier    of identifier
  | Integer       of int
  | Clause        of identifier list
  | Bindings      of Coqast.t substitution
  | Cbindings     of constr   substitution 
  | Quoted_string of string
  | Tacexp        of Coqast.t
  | Redexp        of string * Coqast.t list
  | Fixexp        of identifier * int * Coqast.t
  | Cofixexp      of identifier * Coqast.t
  | Letpatterns   of int list option * (identifier * int list) list
  | Intropattern  of intro_pattern

and intro_pattern =
  | IdPat   of identifier
  | DisjPat of intro_pattern list
  | ConjPat of intro_pattern list
  | ListPat of intro_pattern list  

and tactic_expression = string * tactic_arg list


type pf_status = Complete_proof | Incomplete_proof

type prim_rule_name = 
  | Intro
  | Intro_after
  | Intro_replacing
  | Fix
  | Cofix
  | Refine 
  | Convert_concl
  | Convert_hyp
  | Thin
  | Move of bool

type prim_rule = {
  name : prim_rule_name;
  hypspecs : identifier list;
  newids : identifier list;
  params : Coqast.t list;
  terms : constr list }

type local_constraints = Intset.t

type proof_tree = {
  status : pf_status;
  goal : goal;
  ref : (rule * proof_tree list) option; 
  subproof : proof_tree option }

and goal = ctxtty evar_info

and rule =
  | Prim of prim_rule
  | Tactic of tactic_expression
  | Context of ctxtty
  | Local_constraints of local_constraints

and ctxtty = {
  pgm    : constr option;
  mimick : proof_tree option;
  lc     : local_constraints } 

type evar_declarations = ctxtty evar_map


let is_bind = function
  | Bindings _ -> true
  | _ -> false

let lc_toList lc = Intset.elements lc

(* Functions on goals *)

let mk_goal ctxt env cl = 
  { evar_env = env; evar_concl = cl; 
    evar_body = Evar_empty; evar_info = Some ctxt }

(* Functions on the information associated with existential variables  *)

let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }

let get_ctxt gl = out_some gl.evar_info

let get_pgm gl = (out_some gl.evar_info).pgm

let set_pgm pgm ctxt = { ctxt with pgm = pgm }

let get_mimick gl = (out_some gl.evar_info).mimick

let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc }

let get_lc gl = (out_some gl.evar_info).lc

(* Functions on proof trees *)

let ref_of_proof pf =
  match pf.ref with
    | None -> failwith "rule_of_proof"
    | Some r -> r

let rule_of_proof pf =
  let (r,_) = ref_of_proof pf in r

let children_of_proof pf = 
  let (_,cl) = ref_of_proof pf in cl
				    
let goal_of_proof pf = pf.goal

let subproof_of_proof pf =
  match pf.subproof with
    | None -> failwith "subproof_of_proof"
    | Some pf -> pf

let status_of_proof pf = pf.status

let is_complete_proof pf = pf.status = Complete_proof

let is_leaf_proof pf = (pf.ref = None)

let is_tactic_proof pf = (pf.subproof <> None)


(*******************************************************************)
(*            Constraints for existential variables                *)
(*******************************************************************)

(* A local constraint is just a set of section_paths *)

(* recall : type local_constraints = Intset.t *)

(* A global constraint is a mappings of existential variables
   with some extra information for the program and mimick
   tactics. *)

type global_constraints  = evar_declarations timestamped

(* A readable constraint is a global constraint plus a focus set
   of existential variables and a signature. *)

type evar_recordty = {
  focus : local_constraints;
  env   : env;
  decls : evar_declarations }

and readable_constraints = evar_recordty timestamped

(* Functions on readable constraints *)
			     
let mt_evcty lc gc = 
  ts_mk { focus = lc; env = empty_env; decls = gc }

let evc_of_evds evds gl = 
  ts_mk { focus = (get_lc gl); env = gl.evar_env; decls = evds }

let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
		       
let rc_add evc (k,v) = 
  ts_mod
    (fun evc -> { focus = (Intset.add k evc.focus);
                  env   = evc.env;
                  decls = Evd.add evc.decls k v })
    evc

let get_env   evc = (ts_it evc).env
let get_focus evc = (ts_it evc).focus
let get_decls evc = (ts_it evc).decls
let get_gc    evc = (ts_mk (ts_it evc).decls)

let remap evc (k,v) = 
  ts_mod
    (fun evc -> { focus = evc.focus;
                  env   = evc.env;
                  decls = Evd.add evc.decls k v })
    evc

let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false

(* [mentions sigma sp loc] is true exactly when [loc] is defined, and [sp] is
 * on [loc]'s access list, or an evar on [loc]'s access list mentions [sp]. *)

let rec mentions sigma sp loc =
  let loc_evd = Evd.map (ts_it sigma).decls loc in 
  match loc_evd.evar_body with 
    | Evar_defined _ -> (Intset.mem sp (get_lc loc_evd) 
			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
    | _ -> false

(* ACCESSIBLE SIGMA SP LOC is true exactly when SP is on LOC's access list,
 * or there exists a LOC' on LOC's access list such that
 * MENTIONS SIGMA SP LOC' is true. *)

let rec accessible sigma sp loc =
  let loc_evd = Evd.map (ts_it sigma).decls loc in 
  lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)


(* [ctxt_access sigma sp] is true when SIGMA is accessing a current
 * accessibility list ACCL, and SP is either on ACCL, or is mentioned
 * in the body of one of the ACCL. *)

let ctxt_access sigma sp =
  lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus


let pf_lookup_name_as_renamed hyps ccl s =
  Termast.lookup_name_as_renamed (gLOB hyps) ccl s

let pf_lookup_index_as_renamed ccl n =
  Termast.lookup_index_as_renamed ccl n

(*********************************************************************)
(*                  Pretty printing functions                        *)
(*********************************************************************)

open Pp
open Printer

(* Il faudrait parametrer toutes les pr_term, term0, etc. par la
  strategie de renommage choisie pour Termast (en particulier, il
  faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par
  Intros Until fonctionne exactement comme on affiche le but avec
  term0 *)

let pf_lookup_name_as_renamed hyps ccl s =
  Termast.lookup_name_as_renamed (gLOB hyps) ccl s

let pf_lookup_index_as_renamed ccl n =
  Termast.lookup_index_as_renamed ccl n

let pr_idl idl = prlist_with_sep pr_spc print_id idl

let pr_goal g =
  let sign = context g.evar_env in
  let penv = pr_env_opt sign in
  let pc = term0_at_top sign g.evar_concl in
  [< 'sTR"  "; hV 0 [< penv; 'fNL;
		       'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
                       'sTR "============================"; 'fNL ;
                       'sTR" " ; pc>]; 'fNL>]

let pr_concl n g =
  let pc = term0_at_top (context g.evar_env) g.evar_concl in
  [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
     'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]

(* print the subgoals but write Subtree proved! even in case some existential 
   variables remain unsolved, pr_subgoals_existential is a safer version 
   of pr_subgoals *)

let pr_subgoals = function
  | [] -> [< 'sTR"Subtree proved!" ; 'fNL >]
  | [g] ->
      let pg = pr_goal g in v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >]
  | g1::rest ->
      let rec pr_rec n = function
        | [] -> [< >]
        | g::rest ->
            let pg = pr_concl n g in
            let prest = pr_rec (n+1) rest in
            [< 'cUT; pg; prest >] 
      in
      let pg1 = pr_goal g1 in
      let pgr = pr_rec 2 rest in
      v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; pgr >]

let pr_subgoal n =
  let rec prrec p = function
    | [] -> error "No such goal"
    | g::rest ->
       	if p = 1 then
          let pg = pr_goal g in
          v 0 [< 'sTR "subgoal ";'iNT n;'sTR " is:"; 'cUT; pg >]
       	else 
	  prrec (p-1) rest
  in 
  prrec n

let pr_pgm ctxt = match ctxt.pgm with
  | None -> [< >]
  | Some pgm -> let ppgm = fprterm pgm in [< 'sTR"Realizer " ; ppgm >]
					    
let pr_ctxt ctxt =
  let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >]

let pr_seq evd = 
  let env = evd.evar_env
  and cl = evd.evar_concl
  and info = match evd.evar_info with 
    | Some i -> i 
    | None -> anomaly "pr_seq : info = None"
  in
  let (x,y) as hyps = var_context env in
  let sign = List.rev(List.combine x y) in
  let pc = pr_ctxt info in
  let pdcl =
    prlist_with_sep pr_spc
      (fun (id,ty) -> hOV 0 [< print_id id; 'sTR" : ";prterm ty.body >])
      sign 
  in
  let pcl = term0_at_top (gLOB hyps) cl in
  hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]

let prgl gl =
  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
  let pgl = pr_seq gl in
  [< 'sTR"[[" ; plc; 'sTR"]" ; pgl ; 'sTR"]" ; 'sPC >]

let pr_evgl gl =
  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
  let phyps = pr_idl (ids_of_sign (var_context gl.evar_env)) in
  let pc = prterm gl.evar_concl in
  hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]

let pr_evgl_sign gl = 
  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
  let ps = pr_sign (var_context gl.evar_env) in
  let pc = prterm gl.evar_concl in
  hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]

(*  evd.evgoal.lc seems to be printed twice *)
let pr_decl evd =
  let pevgl = pr_evgl evd in
  let pb =
    match evd.evar_body with
      | Evar_empty -> [< 'fNL >]
      | Evar_defined c -> let pc = prterm c in [< 'sTR" => " ; pc;  'fNL  >]
  in
  h 0 [< pevgl; pb >]

let pr_evd evd = 
  prlist_with_sep pr_fnl
    (fun (ev,evd) ->
       let pe = pr_decl evd in 
       h 0 [< print_id (id_of_existential ev) ; 'sTR"==" ; pe >])
    (Evd.to_list evd)
    
let pr_decls decls = pr_evd (ts_it decls)
		       
let pr_focus accl = pr_idl (List.map id_of_existential (lc_toList accl))

let pr_evc evc =
  let stamp = ts_stamp evc in
  let evc   = ts_it evc in
  let pe = pr_evd evc.decls in
  [< 'sTR"#" ; 'iNT stamp ; 'sTR"[" ; pr_focus evc.focus ; 'sTR"]=" ; pe >]

let pr_evars = 
  prlist_with_sep pr_fnl
    (fun (ev,evd) ->
       let pegl = pr_evgl_sign evd in 
       [< print_id (id_of_existential ev); 'sTR " : "; pegl >])

(* Print an enumerated list of existential variables *)
let rec pr_evars_int i = function
  | [] -> [< >]
  | (ev,evd)::rest ->
      let pegl = pr_evgl_sign evd in 
      let pei = pr_evars_int (i+1) rest in
      [< (hOV 0 [< 'sTR "Existential "; 'iNT i; 'sTR " ="; 'sPC;
                   print_id (id_of_existential ev) ; 'sTR " : "; pegl >]); 
	 'fNL ; pei >]

let pr_subgoals_existential sigma = function 
  | [] -> 
      let exl = Evd.non_instantiated sigma in 
      if exl = [] then 
	[< 'sTR"Subtree proved!" ; 'fNL >]
      else
        let pei = pr_evars_int 1 exl in
        [< 'sTR "No more subgoals but non-instantiated existential ";
           'sTR "variables :" ;'fNL; (hOV 0 pei) >]
  | [g] ->
      let pg = pr_goal g in
      v 0 [< 'sTR ("1 "^"subgoal");'cUT; pg >]
  | g1::rest ->
      let rec pr_rec n = function
        | [] -> [< >]
        | g::rest ->
            let pc = pr_concl n g in
            let prest = pr_rec (n+1) rest in
            [< 'cUT; pc; prest >] 
      in
      let pg1 = pr_goal g1 in
      let prest = pr_rec 2 rest in
      v 0 [< 'iNT(List.length rest+1) ; 'sTR" subgoals" ;'cUT; pg1; prest;
             'fNL >]

open Ast
open Termast
open Pretty

let ast_of_cvt_bind f = function
  | (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])])
  | (Dep  id,c) -> ope ("BINDING", [nvar (string_of_id id);
                                      ope  ("COMMAND",[(f c)])]) 
  | (Com,c)     -> ope ("BINDING", [ope ("COMMAND",[(f c)])])

let rec ast_of_cvt_intro_pattern = function
  | IdPat id  -> nvar (string_of_id id) 
  | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
  | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
  | ListPat l -> ope ("LISTPATTERN",  (List.map ast_of_cvt_intro_pattern l))

let ast_of_cvt_arg = function
  | Identifier id   -> nvar (string_of_id id) 
  | Quoted_string s -> str s
  | Integer n       -> num n 
  | Command c       -> ope ("COMMAND",[c])
  | Constr  c       -> 
      ope ("COMMAND",[bdize false (assumptions_for_print []) c])
  | Clause idl      -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
  | Bindings bl     -> ope ("BINDINGS", 
			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
  | Cbindings bl    -> 
      ope ("BINDINGS", 
	   List.map 
	     (ast_of_cvt_bind (bdize false (assumptions_for_print []))) bl)
  | Tacexp ast      -> ope ("TACTIC",[ast]) 
  | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)])
  | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
                                      (num n); 
                                      ope ("COMMAND",[c])]) 
  | Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id)); 
                                          (ope ("COMMAND",[c]))])
  | Intropattern p ->  ast_of_cvt_intro_pattern p
  | Letpatterns _ -> failwith "TODO: ast_of_cvt_arg: Letpatterns"