diff options
Diffstat (limited to 'plugins/syntax/r_syntax.ml')
-rw-r--r-- | plugins/syntax/r_syntax.ml | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 545f205db..dac70c673 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -42,24 +42,24 @@ let four = mult_2 two (* Unary representation of strictly positive numbers *) let rec small_r dloc n = - if equal one n then GRef (dloc, glob_R1) - else GApp(dloc,GRef (dloc,glob_Rplus), - [GRef (dloc, glob_R1);small_r dloc (sub_1 n)]) + if equal one n then GRef (dloc, glob_R1, None) + else GApp(dloc,GRef (dloc,glob_Rplus, None), + [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)]) let r_of_posint dloc n = - let r1 = GRef (dloc, glob_R1) in + let r1 = GRef (dloc, glob_R1, None) in let r2 = small_r dloc two in let rec r_of_pos n = if less_than n four then small_r dloc n else let (q,r) = div2_with_rest n in - let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in - if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in - if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0) + let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in + if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in + if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None) let r_of_int dloc z = if is_strictly_neg z then - GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) + GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)]) else r_of_posint dloc z @@ -71,33 +71,33 @@ let bignat_of_r = (* for numbers > 1 *) let rec bignat_of_pos = function (* 1+1 *) - | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) + | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)]) when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two (* 1+(1+1) *) - | GApp (_,GRef (_,p1), [GRef (_,o1); - GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o1,_); + GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three (* (1+1)*b *) - | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult -> + | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult -> if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) - | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number in let bignat_of_r = function - | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero - | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one + | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero + | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp -> + | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp -> let n = bignat_of_r a in if Bigint.equal n zero then raise Non_closed_number; neg n @@ -109,11 +109,12 @@ let uninterp_r p = with Non_closed_number -> None +let mkGRef gr = GRef (Loc.ghost,gr,None) + let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0); - GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult); - GRef(Loc.ghost,glob_R1)], + (List.map mkGRef + [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], uninterp_r, false) |