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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
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 locals () =
List.map (fun (id,b,t) -> (id, make_path [] id CCI))
(named_context !env)
let lookup_named id =
let rec look n = function
| [] -> mkVar id
| (Name id')::_ when id = id' -> mkRel n
| _::r -> look (succ n) r
in
look 1
let args sign = Array.of_list (instance_from_section_context sign)
let rec globalize bv c = match kind_of_term c with
| Var id -> lookup_named id bv
| Const (sp, _) ->
let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
| Ind (sp,_ as spi, _) ->
let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps)
| Construct ((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 = c; const_entry_type = ty } in
let sp = make_path [] id CCI in
env := add_constant sp ce (locals()) !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 (locals()) !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 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 npar = List.map (fun (id,c) -> (Name id, globalize [] c)) par in
let one_inductive (id,ar,cl) =
let cv = List.map (fun (_,c) -> prod_it (globalize bv c) npar) cl in
{ mind_entry_nparams = nparams;
mind_entry_params = List.map (fun (id,c) -> (id, LocalAssum c)) par;
mind_entry_typename = id;
mind_entry_arity = prod_it (globalize bvpar ar) npar;
mind_entry_consnames = List.map fst cl;
mind_entry_lc = cv }
in
let inds = List.map one_inductive inds in
let mie = {
mind_entry_finite = true;
mind_entry_inds = inds }
in
let sp =
let mi1 = List.hd inds in
make_path [] mi1.mind_entry_typename CCI in
env := add_mind sp mie (locals()) !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 ()
|
