Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

add the type checked term into cxt

  • Loading branch information...
commit 1419b5f576aa8e79d63928f87e0ae6019cbb8935 1 parent 09ec412
Hongbo Zhang bobzhang authored
Showing with 10 additions and 1 deletion.
  1. +9 −1 fc_p.mly
  2. +1 −0  test/1.ml
10 fc_p.mly
View
@@ -314,6 +314,14 @@ term: LIDENT {FCVar $1}
let ty = $4 in
let term = $6 in
Hashtbl.add term_tbl name (term,Some ty);
+
+ (match Check_term.type_check !Cxt.cxt term with
+ Some ty' when ty' = ty
+ -> cxt := (name,BTermVar ty) :: !cxt
+ | None ->
+ prerr_endline
+ ( name ^ "does not type check during parsing") )
+ ;
term
}
;
@@ -341,7 +349,7 @@ proof: LIDENT {
let tylist = List.map (fun (x,_) -> TyVar x) tys in
CPAssump (proof, tylist)
with Not_found
- -> (prerr_endline ("proof" ^ proof ^ "not found");
+ -> (prerr_endline ("proof " ^ proof ^ " not found");
raise Not_found
)
}
1  test/1.ml
View
@@ -74,3 +74,4 @@ LET is_empty = \ x: (List Nat) -> CASE (Bool,x) {
LET coer_age_nat = \x : (Age) -> (x -> MkAge);
+LET coer_nat_age = \x : (Nat) -> (x -> (SYM MkAge));
Please sign in to comment.
Something went wrong with that request. Please try again.