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
|
(* $Id$ *)
open Pp
open Util
open Names
open Term
open Sign
open Declarations
open Inductive
open Type_errors
open Safe_typing
open G_minicoq
let (env : safe_environment ref) = ref empty_environment
let lookup_named id =
let rec look n = function
| [] -> mkVar id
| (Name id')::_ when id = id' -> Rel n
| _::r -> look (succ n) r
in
look 1
let args sign = Array.of_list (List.map mkVar (ids_of_named_context sign))
let rec globalize bv c = match kind_of_term c with
| IsVar id -> lookup_named id bv
| IsConst (sp, _) ->
let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
| IsMutInd (sp,_ as spi, _) ->
let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps)
| IsMutConstruct ((sp,_),_ as spc, _) ->
let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
| _ -> map_constr_with_named_binders (fun na l -> na::l) globalize bv c
let check c =
let c = globalize [] c in
let (j,u) = safe_infer !env c in
let ty = j_type j in
let pty = pr_term CCI (env_of_safe_env !env) ty in
mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 pty; 'fNL >])
let definition id ty c =
let c = globalize [] c in
let ty = option_app (globalize []) ty in
let ce = { const_entry_body = Cooked c; const_entry_type = ty } in
let sp = make_path [] id CCI in
env := add_constant sp ce !env;
mSGNL (hOV 0 [< pr_id id; 'sPC; 'sTR"is defined"; 'fNL >])
let parameter id t =
let t = globalize [] t in
let sp = make_path [] id CCI in
env := add_parameter sp t !env;
mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; pr_id id;
'sPC; 'sTR"is declared"; 'fNL >])
let variable id t =
let t = globalize [] t in
env := push_named_assum (id,t) !env;
mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; pr_id id;
'sPC; 'sTR"is declared"; 'fNL >])
let put_DLAMSV lna lc =
match lna with
| [] -> anomaly "put_DLAM"
| na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest
let inductive par inds =
let nparams = List.length par in
let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in
let name_inds = List.map (fun (id,_,_) -> Name id) inds in
let bv = bvpar @ List.rev name_inds in
let par = List.map (fun (id,c) -> (Name id, globalize [] c)) par in
let one_inductive (id,ar,cl) =
let cv = Array.of_list (List.map snd cl) in
let cv = Array.map (fun c -> prod_it (globalize bv c) par) cv in
let c = put_DLAMSV name_inds cv in
(id, prod_it (globalize bvpar ar) par, List.map fst cl, [c])
in
let inds = List.map one_inductive inds in
let mie = {
mind_entry_nparams = nparams;
mind_entry_finite = true;
mind_entry_inds = inds }
in
let sp = let (id,_,_,_) = List.hd inds in make_path [] id CCI in
env := add_mind sp mie !env;
mSGNL (hOV 0 [< 'sTR"inductive type(s) are declared"; 'fNL >])
let execute = function
| Check c -> check c
| Definition (id, ty, c) -> definition id ty c
| Parameter (id, t) -> parameter id t
| Variable (id, t) -> variable id t
| Inductive (par,inds) -> inductive par inds
let parse_file f =
let c = open_in f in
let cs = Stream.of_channel c in
try
while true do
let c = Grammar.Entry.parse command cs in execute c
done
with
| End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0
| exn -> close_in c; raise exn
module Explain = Fhimsg.Make(struct let pr_term = pr_term end)
let rec explain_exn = function
| TypeError (k,ctx,te) ->
mSGNL (hOV 0 [< 'sTR "type error:"; 'sPC;
Explain.explain_type_error k ctx te; 'fNL >])
| Stdpp.Exc_located (_,exn) ->
explain_exn exn
| exn ->
mSGNL (hOV 0 [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >])
let top () =
let cs = Stream.of_channel stdin in
while true do
try
let c = Grammar.Entry.parse command cs in execute c
with
| End_of_file | Stdpp.Exc_located (_, End_of_file) -> exit 0
| exn -> explain_exn exn
done
let main () =
if Array.length Sys.argv = 1 then
parse_file "test"
else
if Sys.argv.(1) = "-top" then top () else parse_file (Sys.argv.(1))
let _ = Printexc.print main ()
|
