aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/minicoq.ml
blob: e22b33e24c8d0e88e65e944d8b3039e6e28f1ba5 (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
(************************************************************************)
(*  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$ *)

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.map (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 ()