aux s ;
aux t
>]
+ | C.ALetIn (id,ann,_,s,t) ->
+ [< (match !ann with
+ None -> [<>]
+ | Some ann ->
+ (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
+ ) ;
+ aux s ;
+ aux t
+ >]
| C.AAppl (id,ann,li) ->
[< (match !ann with
None -> [<>]
) ;
print_term ty
>]
- | C.AVariable (xid, ann, _, ty) ->
+ | C.AVariable (xid, ann, _, bo, ty) ->
[< (match !ann with
None -> [<>]
| Some ann ->
X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
) ;
+ (match bo with
+ None -> [<>]
+ | Some bo -> print_term bo
+ ) ;
print_term ty
>]
| C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
match obj with
C.ADefinition (_, rann, _, _, _, _) -> rann
| C.AAxiom (_, rann, _, _, _) -> rann
- | C.AVariable (_, rann, _, _) -> rann
+ | C.AVariable (_, rann, _, _, _) -> rann
| C.ACurrentProof (_, rann, _, _, _, _) -> rann
| C.AInductiveDefinition (_, rann, _, _, _) -> rann
in
| C.ACast (_, rann, _, _) -> rann
| C.AProd (_, rann, _, _, _) -> rann
| C.ALambda (_, rann, _, _, _) -> rann
+ | C.ALetIn (_, rann, _, _, _) -> rann
| C.AAppl (_, rann, _) -> rann
| C.AConst (_, rann, _, _) -> rann
| C.AAbst (_, rann, _) -> rann
| Cast of term * term (* value, type *)
| Prod of name * term * term (* binder, source, target *)
| Lambda of name * term * term (* binder, source, target *)
+ | LetIn of name * term * term (* binder, term, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * int (* uri, number of cookings*)
| Abst of UriManager.uri (* uri *)
(int * UriManager.uri list) list (* parameters *)
| Axiom of string * term *
(int * UriManager.uri list) list (* id, type, parameters *)
- | Variable of string * term (* name, type *)
+ | Variable of string * term option * term (* name, body, type *)
| CurrentProof of string * (int * term) list * (* name, conjectures, *)
term * term (* value, type *)
| InductiveDefinition of inductiveType list * (* inductive types, *)
name * annterm * annterm (* binder, source, target *)
| ALambda of id * annotation option ref *
name * annterm * annterm (* binder, source, target *)
+ | ALetIn of id * annotation option ref *
+ name * annterm * annterm (* binder, term, target *)
| AAppl of id * annotation option ref *
annterm list (* arguments *)
| AConst of id * annotation option ref *
string * annterm * (* id, type *)
(int * UriManager.uri list) list (* parameters *)
| AVariable of id * annotation option ref *
- string * annterm (* name, type *)
+ string * annterm option * annterm (* name, body, type *)
| ACurrentProof of id * annotation option ref *
string * (int * annterm) list * (* name, conjectures, *)
annterm * annterm (* value, type *)
[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" ["binder",id] (aux t)
>]
+ | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+ assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+ | C.ALetIn (xid,_,C.Name id,s,t) ->
+ X.xml_nempty "LETIN" ["id",xid]
+ [< X.xml_nempty "term" [] (aux s) ;
+ X.xml_nempty "letintarget" ["binder",id] (aux t)
+ >]
| C.AAppl (id,_,li) ->
X.xml_nempty "APPLY" ["id",id]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
["name",id ; "params",(encode (List.rev params)) ; "id",xid]
[< X.xml_nempty "type" [] (print_term curi ty) >]
>]
- | C.AVariable (xid, _, name, ty) ->
+ | C.AVariable (xid, _, name, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Variable" ["name",name ; "id",xid]
- [< X.xml_nempty "type" [] (print_term curi ty) >]
+ [< (match bo with
+ None -> [<>]
+ | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
+ ) ;
+ X.xml_nempty "type" [] (print_term curi ty)
+ >]
>]
| C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
| C.ACast (id,_,_,_) -> id
| C.AProd (id,_,_,_,_) -> id
| C.ALambda (id,_,_,_,_) -> id
+ | C.ALetIn (id,_,_,_,_) -> id
| C.AAppl (id,_,_) -> id
| C.AConst (id,_,_,_) -> id
| C.AAbst (id,_,_) -> id
"Body", "<node id = '" ^ boid ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
+ | C.ALetIn (id,_,_,ty,bo) ->
+ let boid = get_id bo
+ and tyid = get_id ty in
+ link_hints annotation_window
+ [| "Binder",
+ "<attribute child = '2' name = 'binder' id = '" ^ id ^ "'/>" ;
+ "Term", "<node id = '" ^ boid ^ "'/>" ;
+ "Target", "<node id = '" ^ tyid ^ "'/>"
+ |]
| C.AAppl (id,_,args) ->
let argsid =
Array.mapi
"Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
"Type", "<node id = '" ^ tyid ^ "'/>"
|]
- | C.AVariable (id,_,_,ty) ->
+ | C.AVariable (id,_,_,bo,ty) ->
let tyid = get_id ty in
link_hints annotation_window
- [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
- "Type", "<node id = '" ^ tyid ^ "'/>"
- |]
+ (match bo with
+ None ->
+ [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ | Some bo ->
+ let boid = get_id bo in
+ [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
+ "Body", "<node id = '" ^ boid ^ "'/>" ;
+ "Type", "<node id = '" ^ tyid ^ "'/>"
+ |]
+ )
| C.ACurrentProof (id,_,_,conjs,bo,ty) ->
let boid = get_id bo
and tyid = get_id ty
let newobj =
match newobj with
Some newobj' -> Unchecked newobj'
- | None -> Frozen (Cic.Variable ("frozen-dummy", Cic.Implicit))
+ | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit))
in
HashTable.remove hashtable (uri,0) ;
HashTable.add hashtable (uri,0) newobj
| C.Cast (te, ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
| C.Appl (he::tl) ->
(* Get rid of C.Appl (C.Appl l1) l2 *)
let newtl = List.map (aux k) tl in
let rec cookrec ty =
function
var::tl ->
- let (varname, vartype) =
+ let (varname, varbody, vartype) =
match CicCache.get_obj var with
- C.Variable (varname, vartype) -> (varname, vartype)
+ C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype)
| _ -> raise (WrongUriToVariable (U.string_of_uri var))
in
- cookrec (add_binder (C.Name varname) vartype (cook curi cookingsno var ty)) tl
+ cookrec (add_binder (C.Name varname) varbody vartype
+ (cook curi cookingsno var ty)) tl
| _ -> ty
in
cookrec ty vars
;;
let cook_prod =
- cook_gen (fun n s t -> Cic.Prod (n,s,t))
+ cook_gen (fun n b s t ->
+ match b with
+ None -> Cic.Prod (n,s,t)
+ | Some b -> Cic.LetIn (n,b,t)
+ )
and cook_lambda =
- cook_gen (fun n s t -> Cic.Lambda (n,s,t))
+ cook_gen (fun n b s t ->
+ match b with
+ None -> Cic.Lambda (n,s,t)
+ | Some b -> Cic.LetIn (n,b,t)
+ )
;;
(*CSC: sbagliato da rifare e completare *)
res
with
e ->
+ print_endline ("Filename: " ^ filename ^ "\nException: ") ;
print_endline (Pxp_types.string_of_exn e) ;
raise e
;;
res
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
- and xid = string_of_attr (n#attribute "id") in
- let typ = (get_content (get_content n))#extension#to_cic_term in
- let res = C.AVariable (xid,ref None,name,typ) in
- register_id xid res ;
- res
+ and xid = string_of_attr (n#attribute "id")
+ and (body, typ) =
+ let sons = n#sub_nodes in
+ match sons with
+ [b ; t] when
+ b#node_type = D.T_element "body" &&
+ t#node_type = D.T_element "type" ->
+ let b' = get_content b
+ and t' = get_content t in
+ (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
+ | [t] when t#node_type = D.T_element "type" ->
+ let t' = get_content t in
+ (None, t'#extension#to_cic_term)
+ | _ -> raise (IllFormedXml 6)
+ in
+ let res = C.AVariable (xid,ref None,name,body,typ) in
+ register_id xid res ;
+ res
| D.T_element _
- | D.T_data ->
+ | D.T_data
+ | _ ->
raise (IllFormedXml 7)
;;
end
;;
+class eltype_letin =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let sons = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ match sons with
+ [s ; t] when
+ s#node_type = Pxp_document.T_element "term" &&
+ t#node_type = Pxp_document.T_element "letintarget" ->
+ let name = cic_attr_of_xml_attr (t#attribute "binder")
+ and source = s#extension#to_cic_term
+ and target = t#extension#to_cic_term in
+ let res = Cic.ALetIn (id,ref None,name,source,target) in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 12)
+ end
+;;
+
(* The definition of domspec, an hashtable that maps each node type to the *)
(* object that must be linked to it. Used by markup. *)
"CAST", (new D.element_impl (new eltype_cast)) ;
"PROD", (new D.element_impl (new eltype_prod)) ;
"LAMBDA", (new D.element_impl (new eltype_lambda)) ;
+ "LETIN", (new D.element_impl (new eltype_letin)) ;
"APPLY", (new D.element_impl (new eltype_apply)) ;
"CONST", (new D.element_impl (new eltype_const)) ;
"ABST", (new D.element_impl (new eltype_abst)) ;
| C.Cast (v,t) -> pp v l
| C.Lambda (b,s,t) ->
"[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t (b::l)
+ | C.LetIn (b,s,t) ->
+ "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l)
| C.Appl li ->
"(" ^
(List.fold_right
) x "" ^ match i with "" -> "" | i' -> " " ^ i'
) params "" ^
"):\n" ^ pp ty []
- | C.Variable (name, ty) ->
- "Variable " ^ name ^ ":\n" ^ pp ty []
+ | C.Variable (name, bo, ty) ->
+ "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^
+ (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
| C.CurrentProof (name, conjectures, value, ty) ->
"Current Proof:\n" ^
List.fold_right
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG",
+ CicPp.ppobj (C.Variable ("DEBUG", None,
C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG",
+ CicPp.ppobj (C.Variable ("DEBUG", None,
C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
and type_of_variable uri =
let module C = Cic in
let module R = CicReduction in
+ let module U = UriManager in
(* 0 because a variable is never cooked => no partial cooking at one level *)
match CicCache.is_type_checked uri 0 with
- CicCache.CheckedObj (C.Variable (_,ty)) -> ty
- | CicCache.UncheckedObj (C.Variable (_,ty)) ->
+ CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty
+ | CicCache.UncheckedObj (C.Variable (_,bo,ty)) ->
(* only to check that ty is well-typed *)
let _ = type_of ty in
+ (match bo with
+ None -> ()
+ | Some bo ->
+ if not (R.are_convertible (type_of bo) ty) then
+ raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
+ ) ;
CicCache.set_type_checking_info uri ;
ty
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
| C.Lambda (_,so,dest) ->
does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+ | C.LetIn (_,so,dest) ->
+ does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n nn x) l true
| C.Const _
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
| C.Lambda _ -> raise Impossible (* due to type-checking *)
+ | C.LetIn _ -> raise NotImplemented
| C.Appl _ -> []
| C.Const _
| C.Abst _ -> raise Impossible
check_is_really_smaller_arg n nn kl x safes so &&
check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
(List.map (fun x -> x + 1) safes) ta
+ | C.LetIn (_,so,ta) ->
+ check_is_really_smaller_arg n nn kl x safes so &&
+ check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+ (List.map (fun x -> x + 1) safes) ta
| C.Appl (he::_) ->
(*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
(*CSC: solo perche' non abbiamo trovato controesempi *)
guarded_by_destructors n nn kl x safes so &&
guarded_by_destructors (n+1) (nn+1) kl (x+1)
(List.map (fun x -> x + 1) safes) ta
+ | C.LetIn (_,so,ta) ->
+ guarded_by_destructors n nn kl x safes so &&
+ guarded_by_destructors (n+1) (nn+1) kl (x+1)
+ (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
if not (List.length tl > k) then false
| C.Lambda (_,so,de) ->
does_not_occur n nn so &&
guarded_by_constructors (n + 1) (nn + 1) h de
+ | C.LetIn (_,so,de) ->
+ does_not_occur n nn so &&
+ guarded_by_constructors (n + 1) (nn + 1) h de
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h = 1 &&
List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
(* only to check if the product is well-typed *)
let _ = sort_of_prod (sort1,sort2) in
C.Prod (n,s,type2)
+ | C.LetIn (n,s,t) ->
+ let type1 = type_of_aux env s in
+ let type2 = type_of_aux (type1::env) t in
+ type2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype = type_of_aux env he
and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
debug (type_of te) [] ;
if not (R.are_convertible (type_of te) ty) then
raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
- | C.Variable (_,ty) ->
+ | C.Variable (_,bo,ty) ->
(* only to check that ty is well-typed *)
- (*CSC [] wrong *)
- let _ = type_of ty in ()
+ let _ = type_of ty in
+ (match bo with
+ None -> ()
+ | Some bo ->
+ if not (R.are_convertible (type_of bo) ty) then
+ raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
+ )
| C.InductiveDefinition _ ->
cooked_mutual_inductive_defs uri uobj
) ;
| C.ACast (_,ann,_,_) -> ann
| C.AProd (_,ann,_,_,_) -> ann
| C.ALambda (_,ann,_,_,_) -> ann
+ | C.ALetIn (_,ann,_,_,_) -> ann
| C.AAppl (_,ann,_) -> ann
| C.AConst (_,ann,_,_) -> ann
| C.AAbst (_,ann,_) -> ann
match annobj with
C.ADefinition (_,ann,_,_,_,_) -> ann
| C.AAxiom (_,ann,_,_,_) -> ann
- | C.AVariable (_,ann,_,_) -> ann
+ | C.AVariable (_,ann,_,_,_) -> ann
| C.ACurrentProof (_,ann,_,_,_,_) -> ann
| C.AInductiveDefinition (_,ann,_,_,_) -> ann
;;
C.Prod (name, deannotate_term so, deannotate_term ta)
| C.ALambda (_,_,name,so,ta) ->
C.Lambda (name, deannotate_term so, deannotate_term ta)
+ | C.ALetIn (_,_,name,so,ta) ->
+ C.LetIn (name, deannotate_term so, deannotate_term ta)
| C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l)
| C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno)
| C.AAbst (_,_,uri) -> C.Abst uri
)
| C.AAxiom (_, _, id, ty, params) ->
C.Axiom (id, deannotate_term ty, params)
- | C.AVariable (_, _, name, ty) ->
- C.Variable (name, deannotate_term ty)
+ | C.AVariable (_, _, name, bo, ty) ->
+ C.Variable (name,
+ (match bo with None -> None | Some bo -> Some (deannotate_term bo)),
+ deannotate_term ty)
| C.ACurrentProof (_, _, name, conjs, bo, ty) ->
C.CurrentProof (
name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
projects / helm.git / commitdiff