diff options
author | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-14 13:59:33 +0000 |
---|---|---|
committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-14 13:59:33 +0000 |
commit | 921f0ef22fcd79e69486e0aec75e57f68dce661e (patch) | |
tree | a8a62246fdbb6363e1f3e1a39d5b8d5ca1c27fcd | |
parent | bb3560885d943baef87b7f99a5d646942f0fb288 (diff) |
Added default canonical structures (see example in test-suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | parsing/prettyp.ml | 4 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 26 | ||||
-rw-r--r-- | pretyping/recordops.ml | 26 | ||||
-rwxr-xr-x | pretyping/recordops.mli | 5 | ||||
-rw-r--r-- | test-suite/success/DefaultCanonicalStructure.v | 49 |
5 files changed, 91 insertions, 19 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6712af8b9..2eb22b177 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -744,7 +744,9 @@ let print_path_between cls clt = let print_canonical_projections () = prlist_with_sep pr_fnl (fun ((r1,r2),o) -> - pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + (match r2 with Some sr2 -> pr_global sr2 | None -> str " _") ++ + str " <- " ++ + pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 93e1c1157..55625232b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -115,15 +115,22 @@ let apprec_nohdbeta env evd c = let check_conv_record (t1,l1) (t2,l2) = try let proji = global_of_constr t1 in - let cstr = global_of_constr t2 in - let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = - lookup_canonical_conversion (proji, cstr) in + let canon_s = + begin + try + let cstr = global_of_constr t2 in + lookup_canonical_conversion (proji, Some cstr) + with _ -> lookup_canonical_conversion (proji,None) + end in + let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = + canon_s in let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 | _ -> assert false in let us2,extra_args2 = list_chop (List.length us) l2 in - c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1 + c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1, + (n,applist(t2,l2)) with _ -> raise Not_found @@ -466,14 +473,15 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | (Rel _ | Var _ | Const _ | Evar _), _ -> assert false | _, (Rel _ | Var _ | Const _ | Evar _) -> assert false -and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = - let (evd',ks) = +and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = + let (evd',ks,_) = List.fold_left - (fun (i,ks) b -> + (fun (i,ks,m) b -> + if m=0 then (i,t2::ks, n-1) else let dloc = (dummy_loc,InternalHole) in let (i',ev) = new_evar i env ~src:dloc (substl ks b) in - (i', ev :: ks)) - (evd,[]) bs + (i', ev :: ks, n - 1)) + (evd,[],n) bs in ise_and evd' [(fun i -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4b93388d6..73ff31180 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -115,12 +115,13 @@ that maps the pair (Li,ci) to the following data type obj_typ = { o_DEF : constr; + o_INJ : int; (* position of trivial argument (negative= none) *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) o_TCOMPS : constr list } (* ordered *) let object_table = - (ref [] : ((global_reference * global_reference) * obj_typ) list ref) + (ref [] : ((global_reference * global_reference option) * obj_typ) list ref) let canonical_projections () = !object_table @@ -128,14 +129,15 @@ let keep_true_projections projs kinds = map_succeed (function (p,true) -> p | _ -> failwith "") (List.combine projs kinds) -(* Intended to always success *) +(* Intended to always succeed *) let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in let lt = List.rev (List.map snd lt) in let args = snd (decompose_app t) in - let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in + let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = + lookup_structure ind in let params, projs = list_chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in @@ -145,12 +147,22 @@ let compute_canonical_projections (con,ind) = match spopt with | Some proji_sp -> let c, args = decompose_app t in - (try (ConstRef proji_sp, global_of_constr c, args) :: l - with Not_found -> l) + begin + try + let ogc,oinj = + try Some (global_of_constr c) , -1 + with _ -> + try + None,pred (destRel c) + with _ -> raise Not_found + in + ((ConstRef proji_sp, ogc,oinj , args) :: l) + with Not_found -> l + end | _ -> l) [] lps in - List.map (fun (refi,c,argj) -> - (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) + List.map (fun (refi,c,inj,argj) -> + (refi,c),{o_DEF=v; o_INJ=inj; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp let open_canonical_structure i (_,o) = diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index c8942b5d4..321584b5b 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -38,11 +38,12 @@ val find_projection_nparams : global_reference -> int type obj_typ = { o_DEF : constr; + o_INJ : int; (* position of trivial argument *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) o_TCOMPS : constr list } (* ordered *) -val lookup_canonical_conversion : (global_reference * global_reference) -> obj_typ +val lookup_canonical_conversion : (global_reference * global_reference option) -> obj_typ val declare_canonical_structure : global_reference -> unit val canonical_projections : unit -> - ((global_reference * global_reference) * obj_typ) list + ((global_reference * global_reference option) * obj_typ) list diff --git a/test-suite/success/DefaultCanonicalStructure.v b/test-suite/success/DefaultCanonicalStructure.v new file mode 100644 index 000000000..f21ea7c8a --- /dev/null +++ b/test-suite/success/DefaultCanonicalStructure.v @@ -0,0 +1,49 @@ + +(* An example with default canonical structures *) + +Variable A B : Type. +Variable plusA : A -> A -> A. +Variable plusB : B -> B -> B. +Variable zeroA : A. +Variable zeroB : B. +Variable eqA : A -> A -> Prop. +Variable eqB : B -> B -> Prop. +Variable phi : A -> B. + +Set Implicit Arguments. + +Record img := { + ia : A; + ib :> B; + prf : phi ia = ib +}. + +Parameter eq_img : forall (i1:img) (i2:img), + eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2). + +Lemma phi_img (a:A) : img. + intro a. + exists a (phi a). + refine ( refl_equal _). +Defined. +Canonical Structure phi_img. + +Lemma zero_img : img. + exists zeroA zeroB. + admit. +Defined. +Canonical Structure zero_img. + +Lemma plus_img : img -> img -> img. +intros i1 i2. +exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)). +admit. +Defined. +Canonical Structure plus_img. + +Print Canonical Projections. + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _); simpl. +Admitted. |