diff options
Diffstat (limited to 'contrib/correctness/pcic.ml')
| -rw-r--r-- | contrib/correctness/pcic.ml | 231 |
1 files changed, 0 insertions, 231 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml deleted file mode 100644 index 041cd81f..00000000 --- a/contrib/correctness/pcic.ml +++ /dev/null @@ -1,231 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -(* Certification of Imperative Programs / Jean-Christophe Filliātre *) - -(* $Id: pcic.ml 5920 2004-07-16 20:01:26Z herbelin $ *) - -open Util -open Names -open Nameops -open Libnames -open Term -open Termops -open Nametab -open Declarations -open Indtypes -open Sign -open Rawterm -open Typeops -open Entries -open Topconstr - -open Pmisc -open Past - - -(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *) - -let make_hole c = mkCast (isevar, c) - -(* Tuples are defined in file Tuples.v - * and their constructors are called Build_tuple_n or exists_n, - * wether they are dependant (last element only) or not. - * If necessary, tuples are generated ``on the fly''. *) - -let tuple_exists id = - try let _ = Nametab.locate (make_short_qualid id) in true - with Not_found -> false - -let ast_set = CSort (dummy_loc,RProp Pos) - -let tuple_n n = - let id = make_ident "tuple_" (Some n) in - let l1n = Util.interval 1 n in - let params = - List.map (fun i -> - (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set))) - l1n in - let fields = - List.map - (fun i -> - let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in - let id' = make_ident "T" (Some i) in - (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id'))) - l1n - in - let cons = make_ident "Build_tuple_" (Some n) in - Record.definition_structure - ((false, (dummy_loc,id)), params, fields, cons, mk_Set) - -(*s [(sig_n n)] generates the inductive - \begin{verbatim} - Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set := - exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P). - \end{verbatim} *) - -let sig_n n = - let id = make_ident "sig_" (Some n) in - let l1n = Util.interval 1 n in - let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in - let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in - let idp = make_ident "P" None in - let params = - let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in - (idp, LocalAssum typ) :: - (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT) - in - let lc = - let app_sig = mkApp(mkRel (2*n+3), - Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in - let app_p = mkApp(mkRel (n+1), - Array.init n (fun i -> mkRel (n-i))) in - let c = mkArrow app_p app_sig in - List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c - in - let cname = make_ident "exist_" (Some n) in - Declare.declare_mind - { mind_entry_finite = true; - mind_entry_inds = - [ { mind_entry_params = params; - mind_entry_typename = id; - mind_entry_arity = mkSet; - mind_entry_consnames = [ cname ]; - mind_entry_lc = [ lc ] } ] } - -(*s On the fly generation of needed (possibly dependent) tuples. *) - -let check_product_n n = - if n > 2 then - let s = Printf.sprintf "tuple_%d" n in - if not (tuple_exists (id_of_string s)) then tuple_n n - -let check_dep_product_n n = - if n > 1 then - let s = Printf.sprintf "sig_%d" n in - if not (tuple_exists (id_of_string s)) then ignore (sig_n n) - -(*s Constructors for the tuples. *) - -let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1) -let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1) - -let tuple_ref dep n = - if n = 2 & not dep then - pair - else - let n = n - (if dep then 1 else 0) in - if dep then - if n = 1 then - exist - else begin - let id = make_ident "exist_" (Some n) in - if not (tuple_exists id) then ignore (sig_n n); - Nametab.locate (make_short_qualid id) - end - else begin - let id = make_ident "Build_tuple_" (Some n) in - if not (tuple_exists id) then tuple_n n; - Nametab.locate (make_short_qualid id) - end - -(* Binders. *) - -let trad_binder avoid nenv id = function - | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id)) - | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty - -let rec push_vars avoid nenv = function - | [] -> ([],avoid,nenv) - | (id,b) :: bl -> - let b' = trad_binder avoid nenv id b in - let bl',avoid',nenv' = - push_vars (id :: avoid) (add_name (Name id) nenv) bl - in - ((id,b') :: bl', avoid', nenv') - -let rec raw_lambda bl v = match bl with - | [] -> - v - | (id,ty) :: bl' -> - RLambda (dummy_loc, Name id, ty, raw_lambda bl' v) - -(* The translation itself is quite easy. - letin are translated into Cases constructions *) - -let rawconstr_of_prog p = - let rec trad avoid nenv = function - | CC_var id -> - RVar (dummy_loc, id) - - (*i optimisation : let x = <constr> in e2 => e2[x<-constr] - | CC_letin (_,_,[id,_],CC_expr c,e2) -> - real_subst_in_constr [id,c] (trad e2) - | CC_letin (_,_,([_] as b),CC_expr e1,e2) -> - let (b',avoid',nenv') = push_vars avoid nenv b in - let c1 = Detyping.detype avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - let id = Name (fst (List.hd b')) in - RLetIn (dummy_loc, id, c1, c2) - i*) - - | CC_letin (_,_,([_] as b),e1,e2) -> - let (b',avoid',nenv') = push_vars avoid nenv b in - let c1 = trad avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - RApp (dummy_loc, raw_lambda b' c2, [c1]) - - | CC_letin (dep,ty,bl,e1,e2) -> - let (bl',avoid',nenv') = push_vars avoid nenv bl in - let c1 = trad avoid nenv e1 - and c2 = trad avoid' nenv' e2 in - ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None) - - | CC_lam (bl,e) -> - let bl',avoid',nenv' = push_vars avoid nenv bl in - let c = trad avoid' nenv' e in - raw_lambda bl' c - - | CC_app (f,args) -> - let c = trad avoid nenv f - and cargs = List.map (trad avoid nenv) args in - RApp (dummy_loc, c, cargs) - - | CC_tuple (_,_,[e]) -> - trad avoid nenv e - - | CC_tuple (false,_,[e1;e2]) -> - let c1 = trad avoid nenv e1 - and c2 = trad avoid nenv e2 in - RApp (dummy_loc, RRef (dummy_loc,pair), - [RHole (dummy_loc,ImplicitArg (pair,1)); - RHole (dummy_loc,ImplicitArg (pair,2));c1;c2]) - - | CC_tuple (dep,tyl,l) -> - let n = List.length l in - let cl = List.map (trad avoid nenv) l in - let tuple = tuple_ref dep n in - let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in - let args = tyl @ cl in - RApp (dummy_loc, RRef (dummy_loc, tuple), args) - - | CC_case (ty,b,el) -> - let c = trad avoid nenv b in - let cl = List.map (trad avoid nenv) el in - let ty = Detyping.detype (false,Global.env()) avoid nenv ty in - ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None) - - | CC_expr c -> - Detyping.detype (false,Global.env()) avoid nenv c - - | CC_hole c -> - RCast (dummy_loc, RHole (dummy_loc, QuestionMark), - Detyping.detype (false,Global.env()) avoid nenv c) - - in - trad [] empty_names_context p |